Beta réduction calcul Lambda

Question

Je suis en train de réduire les éléments suivants en utilisant la réduction de la bêta:

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

Je reçois coincé après la première substitution car il semble donner (λx. λy.x x)(λx. λy.x x) qui mettrait fin en nature d'une boucle . Qu'est-ce que je fais mal?

Answer 1

Voici une illustration de l'évaluation

beta reduction 1 
(λx.xx) (λx.λy.x x)    →β x [x := (λx.λy.x x)] 
(λx.(λx.λy.x x)(λx.λy.x x)) 

beta reduction 2 
(λx.λy.xx) (λx.λy.x x)   →β x [x := (λx.λy.x x)] 
(λx.λy.(λx.λy.x x)(λx.λy.x x)) 

result 
λy.(λx.λy.x x) (λx.λy.x x)

Maintenant, nous avons atteint faible Tête normale Forme - à savoir, nous avons un lambda λy sans aucun argument à appliquer à.

Pour se rendre à la tête normale forme, nous pouvons essayer de réduire sous lambda ...

reduction 1 
λy.(λx.λy.xx) (λx.λy.x x)  →β x [x := (λx.λy.x x)] 
λy.(λx.λy.(λx.λy.x x)(λx.λy.x x)) 

reduction 2 ... 
λy.λy.(λx.λy.x x) (λx.λy.x x) 

Ok, on voit tout de suite que ce modèle se répète. Chaque fois que nous essayons de réduire sous le lambda, le résultat est enveloppé dans un autre λy. Ainsi, cette expression lambda particulière n'a pas de forme normale de tête - c'est-à-dire que l'évaluation de cette expression (lorsqu'elle est appliquée à un argument) ne se terminera jamais; il n'atteindra jamais la forme normale.

Answer 2

Vous ne faites rien de mal.

L'expression (λx.x x) (λx. λy.x x) bêta-réduit en une seule étape à (λx. λy.x x)(λx. λy.x x), ce qui réduit à la bêta-λy.(λx. λy.x x)(λx. λy.x x) puis à λy.λy.(λx. λy.x x)(λx. λy.x x).
À chaque étape, chaque nouvelle expression est la même qu'avant, mais contenue dans une nouvelle abstraction.

En Lambda Calculus, le processus de réduction peut ne pas se terminer. En d'autres termes, les programmes peuvent ne pas se terminer (comme dans tout langage de programmation complet).

Un autre exemple est le terme Ω = (λx.x x)(λx.x x)