Les types récursifs MALL + sans restriction sont-ils Turing-complete?

Si vous regardez les combinateurs récursifs dans le lambda-calcul non typé, tels que le combinateur Y ou le combinateur oméga: Il est clair que tous ces combinateurs finissent par dupliquer une variable quelque part dans leur définition.

\begin{array}{lcl} ω & = & (λ X . X X) (λ X . X X) \\ Oui & = & λ F . (λ X . F (X X)) (λ X . F (X X)) \end{array}

$\begin{array}{lcl} \omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\;x)\\ Y & = & \lambda f.\,(\lambda x.\,f\;(x\;x))\; (\lambda x.\,f\;(x\;x)) \\ \end{array}$

De plus, tous ces combinateurs sont typables dans le calcul lambda simplement typé, si vous l'étendez avec des types récursifs , où peut se produire négativement dans le type récursif. $\mu\alpha.\,A(\alpha)$ $\alpha$

Cependant, que se passe-t-il si vous ajoutez des types récursifs complets (à occurrence négative) au fragment sans exponentielle de la logique linéaire (c.-à-d. MALL)?

$!A$

! UNE ≜ μ α . je & UNE & (α \otimes α)

$!A \triangleq \mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$

Est-il vrai que MALL plus les types récursifs non restreints se normalisent toujours?

lo.logic pl.programming-languages linear-logic Neel Krishnaswami
la source

Je pensais à cela juste l'autre jour, et j'ai passé quelques heures à jouer avec certaines idées, mais je n'ai pas pu trouver un moyen d'exprimer une valeur récursive ni me convaincre que ce n'était pas possible. Mon intuition est que ce n'est pas le cas! Je n'ai pas considéré l'autre sens cependant - si vous assumez la règle d'introduction pour! et les types récursifs, cela vous permet-il de définir un combinateur à virgule fixe?

CA McCann

J'ai toujours pensé qu'un terme

dans lequel chaque variable se produit au plus une fois est typable dans le fragment simplement typé. Cela montrerait donc que vous ne pouvez pas définir un combinateur de points fixes dans lequel les variables sont utilisées de manière linéaire.

λ

$\lambda$

Andrej Bauer

Je pense que vous venez de répondre à la question de MLL, mais les additifs

n'autorise les variables à dupliqués (linéarité implique alors des occurrences uniques dans les séquences de réduction, à peu près).

A & B

$A & B$

Neel Krishnaswami

Réponses:

Si des commutations additives sont omises dans MALL, il est facile de montrer que la taille d'une preuve diminue à chaque étape d'élimination de coupure. Si des commutations additives sont autorisées, la preuve n'est pas aussi simple, mais elle a été fournie dans le document original «Linear Logic». C'est ce qu'on appelle le petit théorème de normalisation (Corollaire 4.22, p71), qui dit que tant que la règle de contraction-promotion n'est pas impliquée (ce qui est le cas dans MALL), la normalisation tient. L'argument ne repose pas sur les formules elles-mêmes, elles pourraient être infinies (par exemple définies de manière récursive).

Cela signifie qu'il n'est pas possible de coder une promotion pour le type dans MALL, car cela permettrait des combinateurs de points fixes. Une construction de récursivité supplémentaire serait nécessaire pour cela. $\mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$

Remarque: Je pense qu'il est possible d'utiliser MALL avec un principe de coinduction (introduction du de dual) pour maintenir la normalisation du système et obtenir une promotion pour cet encodage de . Autoriser les types récursifs dans la coinduction MALL + rendrait alors Turing complet. Mais tant que MALL est considéré seul, autoriser les types récursifs n'est pas un gros problème. $\mu$ $!A$

Stéphane Gimenez
la source

Notez également que le type suggéré est brièvement mentionné à la page 101 (dernière page) du document.

Stéphane Gimenez