Séquençage ou passage de continuation en lambda-calcul pur
J'essaye de résoudre l'exercice suivant donné ici .
Considérez la représentation numérique suivante. Comment définir l'addition?
|0| = λx.x
|1| = λx.λx.x
...
|n + 1| = λx.|n|
Les opérateurs successeurs et prédécesseurs sont faciles à définir:
Succ n = λx.n
Pred n = n (λx.x)
Une solution "évidente" pour définir l'addition est d'utiliser l'opération successeur plus le test pour zéro avec le combinateur à virgule fixe, quelque chose comme (YF) pour F donné ci-dessous (l'opérateur si et les booléens sont définis comme d'habitude):
F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))
Mais définir Is0 semble non trivial. Le problème est qu'un nombre | N | consomme N + 1 arguments, et N arguments en sont simplement effacés. Par conséquent, si j'applique une telle fonction, il semble raisonnable d'arrêter son application lorsqu'il devient clair que le chiffre, par exemple, n'est pas une identité. Je suppose que c'est une sorte de continuation, mais je ne peux pas imaginer comment la modéliser dans le pur lambda-calcul. Peut-être que quelqu'un connaît des conseils qui pourraient vous aider?
Un opérateur de séquençage peut également aider à définir l'addition. Si une application d'un nombre | m | est retardé jusqu'à ce qu'un nombre | n | est appliqué à tous ses arguments, le résultat sera exactement un nombre | n + m | . Peut-être existe-t-il une variante d'un tel combinateur de séquençage dans le lambda-calcul pur?
La réponse fournie par l'auteur de l'exercice utilise une opération non pure (à savoir, IsProcedure qui vérifie si son argument est une fonction).
UPD: Il n'est pas difficile de faire un CPS en lambda-calcul (les détails pour CBV peuvent être trouvés ici ). Cela ne semble pas suffisant pour résoudre le problème.
UPD : Si nous avons une version des fonctions quote-eval pour le pur lambda-calcul, alors il doit y avoir une fonction$eq$, qui reconnaît si les expressions lambda citées sont syntaxiquement égales, et nous pouvons construire Is0 en utilisant$eq$. Mais je doute que$eq$est définissable. La raison est le "lemme de la généricité" (livre de Barendregt, lemme 14.3.24). Si nous avons pu tester l'égalité sur les termes lambda cités alors ($eq$( Citation $\Omega$) ( Citation $\lambda x.x$)) retournerais $False$, et la généricité implique que ($eq$( Citation $\lambda x.x$) ( Citation $\lambda x.x$)) retournerait également $False$. Est-ce que cela contredit une possibilité de construire Quote dans le pur lambda-calcul?
Réponses
Je ne pense pas que vous trouverez ce que vous recherchez dans le calcul lambda pur. La clé est cette déclaration que vous avez faite:
Un opérateur de séquençage peut également aider à définir l'addition. Si une application d'un nombre | m | est retardé jusqu'à ce qu'un nombre | n | s'applique à tous ses arguments, ...
Eh bien, les modèles du calcul lambda sont censés être comme:
$$U \cong U^U$$
Et le point de ce que chaque valeur sémantique$u \in U$peut être appliqué à quelque chose. Cela n'a donc aucun sens de parler de quelque chose qui est «appliqué à tous ses arguments». Il n'y a aucune valeur qui ne puisse pas être appliquée à plus d'arguments dans le calcul lambda pur.
Je ne connais pas par hasard un modèle / argument que cette représentation des naturels rend impossible à mettre en œuvre IsZero, bien que certaines réflexions à ce sujet la rendent improbable. Cependant, pour que cela soit possible dans le calcul lambda pur, il devra avoir un sens sémantiquement, et ne pas être basé sur des notions qui ne sont que syntaxiques.
Edit: voici une esquisse d'un argument. Une définition de$\mathsf{IsZero}$ doit éventuellement réduire comme:
$$\mathsf{IsZero}\ n \rightsquigarrow^* n \overrightarrow v$$
La raison en est que l'application à un certain nombre de valeurs est le seul mécanisme du calcul lambda permettant de distinguer réellement les chiffres. Il doit être le cas que:$$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ Cependant, pour chaque $\overrightarrow v$ c'est le cas que: $$||\overrightarrow v| + k|\overrightarrow v = |k|$$ (où $|\overrightarrow v|$ est la longueur de $\overrightarrow v$). Mais, seulement$|1| = \mathsf{false}$(si c'est la convention choisie). En anglais, il n'y a pas de limite sur le nombre de termes requis pour obtenir un booléen en appliquant un chiffre. Donc il ne peut pas y avoir de$\overrightarrow v$ qui satisfait les équations pour tous les nombres, et donc $\mathsf{IsZero}$ ne peut pas être défini.