Une quine dans le calcul lambda pur

13

Je voudrais un exemple de quine en calcul lambda pur . J'ai été assez surpris de ne pas en trouver un en cherchant sur Google. La page quine répertorie les quines pour de nombreuses langues "réelles", mais pas pour le calcul lambda.

Bien sûr, cela signifie définir ce que je veux dire par une quine dans le calcul lambda, ce que je fais ci-dessous. (Je demande quelque chose de très précis.)

À quelques endroits, par exemple Larkin et Stocks (2004), je vois ce qui suit cité comme une expression "auto-réplicative": (λx.xx)(λx.xx) . Cela se réduit à lui-même après une seule étape de réduction bêta, ce qui lui donne une sensation de quine. Cependant, c'est un peu quine en ce sens qu'il ne se termine pas: de nouvelles réductions bêta continueront à produire la même expression, donc elles ne se réduiront jamais à la forme normale. Pour moi, un quine est un programme qui se termine et se produit lui-même, et je voudrais donc une expression lambda avec cette propriété.

Bien sûr, toute expression qui ne contient pas de redex est déjà sous sa forme normale, et se terminera donc et sortira elle-même. Mais c'est trop trivial. Je propose donc la définition suivante dans l'espoir qu'elle admettra une solution non triviale:

définition (provisoire): une quine dans le calcul lambda est une expression de la forme (où représente une expression spécifique du calcul lambda) telle que devient (\ lambda x. A) , ou quelque chose d'équivalent sous les changements de noms de variables, lorsqu'il est réduit à la forme normale, pour toute entrée y .A ( ( λ x . A )

(λx.A)
A( λ x . A )((λx.A)y)(λx.A)y

Étant donné que le calcul lambda est aussi équivalent à Turing que n'importe quelle autre langue, il semble que cela devrait être possible, mais mon calcul lambda est rouillé, donc je ne peux pas penser à un exemple.

Référence

James Larkin et Phil Stocks. (2004) «Expressions auto-réplicatives dans le Lambda Calculus» Conferences in Research and Practice in Information Technology, 26 (1), 167-173. http://epublications.bond.edu.au/infotech_pubs/158

Nathaniel
la source
Pas une réponse à ma question, mais pour ma future référence (et pour les futurs visiteurs), il sera utile d'avoir un lien vers wiki.haskell.org/Combinatory_logic , dans lequel quelqu'un a des pensées beaucoup plus profondes sur les quines que moi.
Nathaniel
Notez qu'un quine doit produire son propre code source . Produire la fonction qu'il représente n'est pas suffisant.
PyRulez
@PyRulez quel est le code source d'une expression lambda? S'il s'agit d'une séquence de caractères, il est impossible pour une expression lambda de la produire, et par conséquent, nous pouvons définir le mot "quine" pour signifier quelque chose de légèrement différent pour les expressions lambda sans crainte d'ambiguïté. D'un autre côté, si vous pensez que le code source est lui-même l'expression lambda, «le code source» et «la fonction qu'il représente» sont la même chose. Je pense donc que je vais bien ici.
Nathaniel
il y a une église codant pour les chaînes. Un quine de calcul lambda devrait produire le codage d'église de la chaîne de caractères qui le représente.
PyRulez
Bien sûr, ce n'est pas difficile à faire, si vous le définissez de cette façon. Cette question portait sur autre chose.
Nathaniel

Réponses:

8

Vous voulez un terme Q tel que MΛ :

QMβQ

Je ne préciserai aucune autre restriction sur (par exemple en ce qui concerne sa forme et s'il se normalise) et je vous montrerai qu'il doit définitivement être non normalisant.Q

  1. Supposons que est sous une forme normale. Choisissez (nous pouvons le faire parce que le théorème doit tenir pour tout ). Ensuite, il y a trois cas.QMMxM

    • Q est un atome . Alors . Ce n'est pas réductible à .Q M a x aaQMaxa
    • Q est une application . Alors . est une forme normale par hypothèse, donc est également sous forme normale et non réductible à .Q M ( R S ) x ( R S ) ( R S ) x ( R S )(RS)QM(RS)x(RS)(RS)x(RS)
    • Q est une abstraction (si est supposé être libre dansx A , pour simplifier, nous pouvons simplement choisir M équivalent à n'importe quelle variable λ abstraite). Ensuite , Q M ( λ x . A ) x ⊳ la ß A [ x / x ] A . Puisque ( λ x . A ) est sous forme normale, A l' est également. Par conséquent, nous ne pouvons pas réduire A à ( λ x . A(λx.A)xAMλQM(λX.UNE)XβUNE[X/X]UNE(λX.UNE)UNEUNE .(λX.UNE)

    Donc, si un tel existe, il ne peut pas être sous une forme normale.Q

  2. Pour être complet, supposons que a une forme normale, mais n'est pas sous une forme normale (peut-être qu'il se normalise faiblement), c'est-à-dire N β -nf avec N Q tel que M Λ : Q M β Q β NQ Nβ-nfNQMΛ

    QMβQβN

    Alors avec il doit aussi exister une séquence de réduction Q x β N x β N , car:MxQxβNxβN

    • est possible par le fait que Q ⊳ la ß N .QxβNxQβN
    • doit se normaliser puisque N est un β -nf et x est juste un atome.NxNβx
    • Si devait se normaliser à autre chose que N , alors Q x a deux β -nfs, ce qui n'est pas possible par un corollaire au théorème de Church-Rosser. (Le théorème de Church-Rosser déclare essentiellement que les réductions sont confluentes, comme vous le savez probablement déjà.)NxNQxβ

    Mais notons que n'est pas possible par l'argument (1) ci-dessus, donc notre supposition que Q a une forme normale n'est pas tenable.NxβNQ

  3. Si nous permettons un tel , alors, nous sommes certains qu'il doit être non normalisant. Dans ce cas, nous pouvons simplement utiliser un combinateur qui élimine tout argument qu'il reçoit. La suggestion de Denis fonctionne très bien: Q ( λ z . ( Λ x . Λ z . ( X x ) ) ( λ x . Λ z . ( X x ) ) ) Puis en seulement deux β- réductions: Q MQ

    Q(λz.(λx.λz.(xx))(λx.λz.(xx)))
    β
    QM(λz.(λx.λz.(xx))(λx.λz.(xx)))M1β(λx.λz.(xx))(λx.λz.(xx))1β(λz.((λx.λz.(xx))(λx.λz.(xx)))Q

Ce résultat est pas très étonnant, puisque vous êtes essentiellement demandez un terme qui élimine tout argument qu'il reçoit, ce qui est quelque chose que je vois souvent mentionné comme une application directe du théorème du point fixe.

Roy O.
la source
Si je pouvais aussi accepter la réponse de Denis, je le ferais, mais (après avoir appris un peu plus et avoir pu la comprendre pleinement), c'est cette réponse qui m'a vraiment convaincu que ce "combinateur de quine" ne peut pas être mis en œuvre par un expression lambda sous forme normale.
Nathaniel
9

D'une part, cela est impossible, car une quine est censée produire son propre code, et le calcul lambda pur n'a aucun moyen d'effectuer une sortie.

D'un autre côté, si vous supposez que le terme résultant est la sortie, alors chaque forme normale est une quine.

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

Dave Clarke
la source
2
Voilà un point intéressant. Dans la question, j'ai essayé de donner une définition de ce qui pourrait être considéré comme un quine non trivial dans le calcul lambda: une fonction qui, lorsqu'elle est appliquée à n'importe quelle entrée, se réduit en bêta (jusqu'à des substitutions de nom de variable). Il se peut que ce soit impossible, mais ce n'est pas évident, du moins pour moi.
Nathaniel
8

Voici une proposition:

Af=λt.(λz.t)

Y=λg.((λx.g (x x)) (λx.g (x x)))A=Yf=(λx.λz.(x x)) (λx.λz.(x x))

AAλz.Ay(λz.A)yβAβ(λz.A)

Denis
la source
(λz.UNE)y(λz.UNE)UNE
1
yyyUNE(λz.UNE)yUNEUNEλz.UNEUNE
1
λ-cunelculus
Ahh, vous avez bien sûr raison. J'aurais dû voir ça. Je ne sais pas s'il faut accepter votre réponse ou modifier la question pour demander une meilleure définition. Je vais y réfléchir un peu. (Il me semble toujours qu'il devrait être possible de donner une définition non triviale où vous demandez quelque chose qui se terminera, mais je ne sais pas comment.)
Nathaniel
zzUNEUNEif z==p then return q, otherwise return q