Qu'est-ce que le logarithme ou l'opération racine dans l'espace de type?

27

Je lisais récemment Les deux dualités du calcul: types négatifs et fractionnaires . Le document développe les types de somme et les types de produits, donnant une sémantique aux types a - bet a/b.

Contrairement à l'addition et à la multiplication, il n'y a pas un mais deux inverses d'exponentiation, de logarithmes et d'enracinement. Si les types de fonction (a → b) sont une exponentiation théorique du type, étant donné le type a → b(ou b^a) que signifie avoir le type logb(c)ou le type a√c?

Est-il judicieux d'étendre les logarithmes et les racines aux types?

Dans l'affirmative, y a-t-il eu des travaux dans ce domaine et quelles sont les bonnes orientations sur la façon de comprendre les répercussions?

J'ai essayé de rechercher des informations à ce sujet via la logique, en espérant que la correspondance Curry-Howard pourrait m'aider, mais en vain.

efrey
la source

Réponses:

40

Un type a un logarithme pour baser de exactement quandX P C P XCXPCPX . Autrement dit, peut être considérée comme un conteneur de X éléments dans des positions données par P . En effet, il est une question de demander à ce que la puissance P , nous devons élever X pour obtenir C .CXPPXC

Il est logique de travailler avec F est un foncteur, chaque fois que le logarithme existe, ce qui signifie l o glogFF . Notez que si FlogX(FX) , alors nous avons certainement FFXlogFX , donc le conteneur ne nous dit rien d'autre d'intéressant que ses éléments: les conteneurs avec un choix de formes n'ont pas de logarithmes.F11

Les lois familières des logarithmes ont un sens lorsque vous pensez en termes d'ensembles de positions

log(K1)=0aucune position dans un conteneur videlogje=1conteneur pour une, une positionlog(F×g)=logF+loggpaire de conteneurs, choix de positionslog(Fg)=logF×loggconteneur de conteneurs, paire de positions

On gagne aussi du Z = l o glogX(νOui.T)=μZ.logXT sous le classeur. C'est-à-dire que lecheminvers chaque élément dans certaines codées est défini de manière inductive en itérant le logarithme. Par exemple,Z=logXOui

logStreunem=logX(νOui.X×Oui)=μZ.1+Z=Nunet

Étant donné que la dérivée nous indique le type dans des contextes à un trou et que le logarithme nous indique les positions, nous devrions nous attendre à une connexion, et en effet

F11logFF1

Lorsqu'il n'y a pas de choix de forme, une position est identique à un contexte à un trou avec les éléments effacés. Plus généralement, représente toujours le choix d'uneforme F avec la position d'un élément dans cette forme.F1F

J'ai peur d'avoir moins à dire sur les racines, mais on pourrait partir d'une définition similaire et suivre son nez. Pour plus d'utilisations des logarithmes de types, consultez "Fonctions mémo, polytypiquement!" De Ralf Hinze. Je dois y aller...

travailleur porcin
la source
3
La réponse de Da Man lui-même. Bienvenue Conor!
Andrej Bauer
Hmm, je suis intéressé de voir quels sont les types de racines, car ils nécessiteraient des types ayant un nombre imaginaire d'habitants. A moins que je ne me trompe. J'accepterai votre réponse, mais si vous avez le temps d'élaborer sur les racines, ce serait très apprécié.
efrey
Cela peut-il être lié à la série Taylor de ln (1 + x) d'une manière ou d'une autre?
yatima2975
2
Avec les logarithmes et les exponentielles, je me demande ... de quoi avons-nous besoin pour construire un objet Napier ? (par exemple l'objet supposé unique etel que ∂e = e)
Rhymoid
1

Je ne connais aucun travail qui poursuive cette ligne, mais quelques instants à ce sujet m'ont conduit à cette hypothèse: la "racine" du type exponentiel ne serait-elle pas simplement le codomaine et le "logarithme" de l'exponentielle juste le domaine?

Marc Hamann
la source
Bon, donc je pense que votre intuition est bonne mais votre conclusion est fausse. L'opération racine et l'opération logarithme sont ce que vous obtenez lorsque vous "inversez" respectivement le codomaine ou le domaine, pas le (co) domaine lui-même. La question est, qu'entendons-nous par inverser et quelle est l'opération de type binaire qu'il produit?
efrey
XyyXXy
Désolé, je n'ai pas été totalement clair dans ma terminologie. Je ne veux pas demander "quelle est la racine, quel est le résultat de l'application de la fonction logarithme". Je me demande ce qu'est l'opération d'enracinement. Quelle est l'opération de recherche du logarithme. Si est expenentiation, ce qui est un deux types sous l'opération racine. Quels sont deux types sous l'opération logarithme. Ce que je veux dire par "inverser l'argument" est quelque chose qu'il n'y a pas de temps à expliquer ici. Je vais clarifier ma question, merci.
efrey
L'article que j'ai lié fournit une sémantique pour le type a - bet le type a / b. Je ne m'intéresse pas au résultat de la réduction du logarithme et de la racine des opérations, mais à la compréhension de leur sémantique en tant qu'opérateurs de type binaire.
efrey