Comment transformer les termes sans terminaison en combinateurs à virgule fixe?

J'ai pensé à ces questions:

Existe-t-il un calcul lambda typé cohérent et complet de Turing?

/cs/65003/if-%CE%BB-xxx-has-a-type-then-is-the-type-system-inconsistent

et il y a déjà quelques questions difficiles à répondre dans le cadre non typé ! Plus précisément, je suis curieux de savoir si nous pouvons récupérer l'intégralité de Turing de la non-résiliation de la manière suivante:

Question: Étant donné une (pure) -terme avec aucune forme normale de tête faible, il ne toujours existe un combinateur point fixe tel que $\lambda$ $t$ $Y_t$
$Y_{t} (λ x . x) = t$ $Y_t\ (\lambda x.x) = t$

Les égalités sont toutes prises modulo . $\beta\eta$

En fait, je soupçonne que cette version de la question est fausse , donc on peut assouplir la question aux combinateurs en boucle , où un combinateur en boucle est défini comme un terme tel que pour chaque où doit à nouveau être un combinateur en boucle. Bien sûr, cela suffit pour définir les fonctions récursives comme d'habitude. $Y$ $f$

Y f = f (Y^{'} f)

$Y\ f=f\ (Y'\ f)$

Y^{'}

$Y'$

Plus généralement, je suis intéressé à trouver des moyens «naturels» de passer d'un sans terminaison à un combinateur en boucle, même si l'équation ci-dessus n'est pas satisfaite. $t$

Je suis également intéressé par les versions plus faibles de la question ci-dessus, par exemple, peut être considéré comme une application avec chaque sous une forme normale (bien que je ne suis pas sûr que cela aide vraiment). $t$ $t\equiv t_1\ t_2\ldots t_n$ $t_i$

Jusqu'à présent: l'approche naturelle consiste à prendre les applications et "poivre" de partout, par exemple $t$ $f$

Ω := (λ x . x x) (λ x . x x)

$\Omega:=(\lambda x.x\ x)(\lambda x.x\ x)$

devient l'habituel

Y_{Ω} := λ f . (λ x . f (x x)) (λ x . f (x x))

$Y_\Omega:= \lambda f.(\lambda x. f\ (x\ x))\ (\lambda x.f\ (x\ x))$

L'idée est de réduire la tête de à une application et remplacez-le par , mais l'étape suivante n'est pas claire (et je suis sceptique que cela puisse conduire à n'importe quoi). $t$ $\lambda x. t'$ $\lambda x.f\ t'$

Je ne suis pas sûr de bien comprendre les arbres Böhm pour voir s'ils ont quelque chose à dire, mais j'en doute fortement, car l' arbre Böhm de est simplement , qui ne ressemble en rien à celui de : an arbre d'abstractions infini. $\Omega$ $\bot$ $Y_\Omega$

Edit : Un de mes amis a fait remarquer que cette approche naïve ne fonctionne pas avec le terme: L'approche naïve donnerait Mais ce n'est pas un combinateur à virgule fixe! Cela peut être corrigé en remplaçant la deuxième application de par , mais alors ne donne pas le terme d'origine. Il n'est pas clair si ce terme est un contre-exemple à la question d'origine (et ce n'est certainement pas un contre-exemple à la plus générale).

(λ x . x x x) (λ x . x x x)

$(\lambda x.x\ x\ x)(\lambda x.x\ x\ x)$

(λ X . F (X X X)) (λ X . F (X X X))

$(\lambda x.f\ (x\ x\ x))(\lambda x.f\ (x\ x\ x))$

f

$f$

λ y z . f y

$\lambda y z.f\ y$

f \mapsto I

$f\mapsto \mathrm{I}$

lambda-calculus combinatory-logic cody
la source

Je crois que l'exigence selon laquelle t n'a pas de forme normale de tête devrait être renforcée pour exclure également les formes normales de tête faible. Si t est capable de produire un lambda, alors, comme en position de tête vous avez toujours un combinateur de point fixe (commençant par f = id), le lambda devrait être produit par lui, ce n'est pas possible.

Andrea Asperti

@AndreaAsperti vous avez raison, bien sûr. Je vais modifier la question.

cody

Cette très belle question comporte plusieurs aspects, je structurerai donc cette réponse en conséquence. $\newcommand{\setof}[1]{\{#1\}}$ $\newcommand{\thra}{\twoheadrightarrow}$ $\newcommand{\codeof}[1]{\lceil #1 \rceil}$

1. La réponse à la question encadrée est non . Le terme suggéré par votre ami est en effet un contre-exemple. $\Omega_3 = (\lambda x.xxx)(\lambda x.xxx)$

Il a été remarqué plus tôt dans les commentaires que l'on a des contre-exemples comme le "ogre" , jusqu'à ce que la question se limite aux termes sans forme normale de tête faible. Ces termes sont appelés termes zéro . Ce sont des termes qui ne se réduisent jamais à un lambda, quelle que soit la substitution. $K^\infty=Y K$

Pour tout combinateur à virgule fixe (fpc) , est un terme dit muet (AKA "root-active"): chaque réduction de celui-ci se réduit davantage à un redex. $Y$ $Y I$

$K^\infty$ n'est pas muet; ni comme cela se manifeste en inspectant son ensemble de réductions, qui est $\Omega_3$ $-$

{Ω_{3} \underset{k}{\underset{⏟}{(λ x . x x x) \dots (λ x . x x x)}} ∣ k \in N}

$\setof{\Omega_3 \underbrace{(\lambda x. xxx) \cdots (\lambda x. xxx)}_k \mid k \in \mathbb{N}}$

Plutôt que de donner un argument précis sur la raison pour laquelle est muet pour tous les fpcs (en effet, pour tout combinateur de boucle) ce qui peut être laborieux mais espérons-le assez clair je traiterai la généralisation évidente de votre question, en me limitant également aux termes muets. $Y I$ $Y$ $-$ $-$

Les termes muets sont une sous-classe de termes nuls qui sont une sous-classe de termes insolubles. Ensemble, ce sont peut-être les choix les plus populaires pour le concept de «vide de sens» ou «non défini» dans le calcul lambda, correspondant respectivement aux arbres triviaux de Berarducci, Levy-Longo et B \ "ohm. Le réseau de notions de termes sans signification a été analysé en détail par Paula Severi et Fer-Jan de Vries. [1] Les termes muets constituent l'élément inférieur de ce réseau, c'est-à-dire la notion la plus restrictive de "non défini".

2. Soit un terme muet, et être une boucle combinateur avec la propriété que . $M$ $Y$ $YI = M$

D' abord , nous pensons que, pour une nouvelle variable , ressemble en fait beaucoup comme le que vous avez décrit, obtenu par « saupoudrage autour de » certains reduct de . $z$ $Yz$ $Y_M$ $z$ $M$

Par Church-Rosser, et ont une réduction commune, . Prenez une réduction standard . Chaque sous-terme de correspond à un sous-terme unique de sous cette réduction. Pour tout sous-terme , les facteurs comme , où la jambe centrale est une faible réduction de la tête (et la jambe finale) est interne). est "gardé" par un si cette deuxième étape contracte une redex , avec un descendant de la substitution . $YI$ $M$ $M'$ $R : YI \thra_s M'$ $M'$ $YI\equiv Yz[z:=I]$ $C[N]=M'$ $R$ $YI \thra C[N_0] \thra_{wh} C[N_1] \thra_i C[N]$ $N$ $z$ $I P$ $I$ $[z:=I]$

Évidemment, doit garder certains sous- termes de , sinon il serait également muet. D'un autre côté, il faut faire attention à ne pas garder les sous-termes nécessaires à la non-terminaison, sinon il ne pourrait pas développer l'arborescence infinie B \ "ohm d'un combinateur en boucle. $Y$ $M$

Il suffit donc de trouver un terme muet dans lequel chaque sous-terme, de chaque réduction, est nécessaire pour la non-normalisation, en ce sens que placer une variable devant ce sous-terme donne un terme normalisant.

Considérez , où . C'est comme , mais à chaque itération, on vérifie que l'occurrence de dans la position d'argument n'est pas "bloquée" par une variable head, en lui donnant une identité. Mettre un devant n'importe quel sous-terme aboutira finalement à une forme normale de forme , où chaque est soit , soit un " saupoudrage" de ceux-ci. Donc est un contre-exemple de la question généralisée. $\Psi = W W$ $W = \lambda w. w I w w$ $\Omega$ $W$ $z$ $zP_1\cdots P_k$ $P_i$ $I$ $W$ $z$ $\Psi$

THÉORÈME. Il n'y a pas de combinateur de bouclage tel que . $Y$ $YI = \Psi$

PREUVE. L'ensemble de toutes les réductions de est . Pour être convertible avec , doit se réduire à l'un d'eux. L'argument est identique dans tous les cas; pour le concret, supposons que . $\Psi$ $\setof{WW,WIWW,IIIIWW,IIIWW,IIWW,IWW}$ $\Psi$ $YI$ $YI \thra IIWW$

Toute réduction standard peut être factorisée comme $YI \thra_s IIWW$

\begin{aligned} Oui je ↠_{w} P N_{4}, P ↠_{w} Q N_{3}, Q ↠_{w} N_{1} N_{2}, Donc Oui je ↠_{w} N_{1} N_{2} N_{3} N_{4} \\ N_{1} ↠ je, N_{2} ↠ je, N_{3} ↠ W, N_{4} ↠ W \end{aligned}

$\begin{align*} YI \thra_w P N_4, P \thra_w Q N_3, Q \thra_w N_1 N_2, \text{thus } YI \thra_w N_1 N_2 N_3 N_4\\ N_1 \thra I, N_2 \thra I, N_3 \thra W, N_4 \thra W \end{align*}$

Faisons référence à la réduction comme , et aux réductions partant de comme . $YI \thra_w N_1 N_2 N_3 N_4$ $R_0$ $N_i$ $R_i$

Ces réductions peuvent être levées sur la substitution pour donner pour que soit la composition . $[z:=I]$

\begin{aligned} R_{0}^{z} : Oui z ↠ z^{k} (M_{1} M_{2} M_{3} M_{4}) \\ N_{je} \equiv M_{je} [z : = je] \end{aligned}

$\begin{align*} R^z_0 : Yz \thra z^k(M_1 M_2 M_3 M_4)\\ N_i \equiv M_i[z:=I] \end{align*}$

R_{0}

$R_0$

Y I \overset{R_{0}^{z} [z := I]}{↠} I^{k} (N_{1} \dots N_{4}) ↠_{w}^{k} N_{1} \dots N_{4}

$YI \stackrel{R^z_0[z:=I]}{\thra} I^k(N_1 \cdots N_4) \thra^k_w N_1 \cdots N_4$

De même, nous pouvons soulever chaque comme $R_i : N_i \thra N \in \setof{I,W}$

\begin{aligned} R_{je}^{z} : M_{je} ↠ N_{je}^{z} \\ R_{je} : N_{je} \overset{R_{je}^{z} [z : = je]}{↠} N_{je}^{z} [z : = je] ↠_{je} N \end{aligned}

$\begin{align*} R^z_i : M_i \thra N^z_i\\ R_i : N_i \stackrel{R^z_i[z:=I]}{\thra} N^z_i[z:=I] \thra_I N \end{align*}$

La seconde étape de cette factorisation de consiste précisément à contracter les -exexes créés par la substitution . (En particulier, puisque est une forme normale, .) $R_i$ $I$ $N^z_i[z:=I]$ $N$ $N^z_i$

$N^z_i$ est ce que nous appelons un « -sprinkling de », obtenue en plaçant un nombre quelconque de s autour un nombre quelconque de sous - terme de . Puisque , la forme de sera l'une des $z$ $N$ $z$ $N$ $N \in \setof{I,W}$ $N^z_i$

\begin{aligned} z^{k_{1}} (λ X . z^{k_{2}} (X)) \\ z^{k_{1}} (λ w . z^{k_{2}} (z^{k_{3}} (z^{k_{5}} (z^{k_{sept}} (w) z^{k_{8}} (λ X . z^{k_{9}} (X))) z^{k_{6}} (w)) z^{k_{4}} (w))) \end{aligned}

$\begin{align*} &z^{k_1}(\lambda x. z^{k_2}(x))\\ &z^{k_1}(\lambda w. z^{k_2}( z^{k_3}( z^{k_5}( z^{k_7}(w) z^{k_8}(\lambda x. z^{k_9}(x)) ) z^{k_6}(w) ) z^{k_4}(w) )) \end{align*}$

Donc , avec un saupoudrage de pour et de pour . $M_1 M_2 M_3 M_4 \thra N^z_1 N^z_2 N^z_3 N^z_4$ $N^z_i$ $z$ $I$ $i =1,2$ $W$ $i=3,4$

Dans le même temps, le terme devrait encore se réduire pour donner l'arbre de Bohm fpc infini . Il doit donc exister un "saupoudrer" dans l'un des qui vient infiniment souvent en tête du terme, sans pour en bloquer de nouvelles réductions. $N^z_1 N^z_2 N^z_3 N^z_4$ $z(z(z(\cdots)))$ $z^{k_j}$ $N^z_i$

Et maintenant, nous avons terminé. En inspectant chaque , pour , et chaque valeur possible de , pour , nous constatons qu'aucune telle aspersion n'existe. $N^z_i$ $i \le 4$ $k_j$ $j \le 2+7\lfloor \frac{i-1}{2} \rfloor$

Par exemple, si nous modifions le dernier de en , alors nous obtenons la réduction de normalisation $W$ $IIWW$ $W^z = \lambda w. z(wIww)$

je je W W^{z} \to je W W^{z} \to W W^{z} \to W^{z} je W^{z} W^{z} \to z (je je je je) W^{z} W^{z} ↠ z je W^{z} W^{z}

$IIWW^z \to I W W^z \to WW^z \to W^z I W^z W^z \to z (I I I I) W^z W^z \thra z I W^z W^z$

(Notez que admet une telle aspersion précisément parce qu'un certain sous-terme peut être "gardé" sans affecter la non-normalisation. La variable vient en position de tête, mais suffisamment de redex restent en dessous.) $\Omega$

3. La "transformation par aspersion" a d'autres utilisations. Par exemple, en plaçant devant chaque redex dans , on obtient un terme qui est une forme normale, encore satisfait à l'équation . Cela a été utilisé par Statman dans [2], par exemple. $z$ $M$ $N = \lambda z. M_z$ $N I = M$

4. Alternativement, si vous relâchez l'exigence que , vous pouvez trouver divers fpcs (faibles) qui simulent la réduction de , tout en émettant une chaîne de s en cours de route. Je ne suis pas sûr que cela répondrait à votre question générale, mais il existe certainement un certain nombre de transformations (calculables) qui produisent des combinateurs en boucle pour chaque muet , de telle sorte que le graphique de réduction de est structurellement similaire à celui de . Par exemple, on peut écrire $Y I = M$ $Y$ $M$ $z$ $M \mapsto Y_M$ $M$ $Y_M$ $M$

Oui ⌈ M ⌉ z = {\begin{cases} z (Oui ⌈ P [X : = Q] ⌉ z) & M \equiv (λ X . P) Q \\ Oui ⌈ N ⌉ z & M n'est pas un redex et M \to_{w h} N \end{cases}

$Y \codeof{M} z = \begin{cases} z (Y \codeof{P[x:=Q]} z) &M\equiv (\lambda x.P)Q\\ Y \codeof{N} z &M \text{ is not a redex and }M \to_{wh} N \end{cases}$

[1] Severi P., de Vries FJ. (2011) Décomposer le réseau d'ensembles sans signification dans le calcul infinitaire de Lambda. Dans: Beklemishev LD, de Queiroz R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Notes de cours en informatique, vol 6642.

[2] Richard Statman. Il n'y a pas de combinateur S, K hyperrécurrent. Rapport de recherche 91-133, Département de mathématiques, Université Carnegie Mellon, Pittsburgh, Pennsylvanie, 1991.

Andrew Polonsky
la source

Cette réponse est excellente et je l'accepterai probablement. Cependant, je ne sais pas quels sont les théorèmes réels que vous décrivez, à part "il n'y a pas de combinateur de boucle tel que ". Je pense qu'énoncer les théorèmes séparément rendra les arguments beaucoup plus faciles à suivre.

Y

$Y$

Y I = Ω_{3}

$Y\ I=\Omega_3$

cody

Bon point. Je viens de mettre à jour la réponse.

Andrew Polonsky

Comment transformer les termes sans terminaison en combinateurs à virgule fixe?

Réponses: