Associativité dans le calcul lambda

Question

Je travaille sur les questions de l'exercice du livre The Lambda calculus. Une des questions que je suis bloqué prouve ce qui suit: Montrer que l'application n'est pas associative; en fait, x (yz) pas égaux (xy) z

Voici ce que j'ai travaillé jusqu'à présent:

Let x = λa.λb. ab 
Let y = λb.λc. bc 
Let z = λa.λc. ac 

(xy)z => ((λa.λb. ab) (λb.λc. bc)) (λa.λc. ac)  
=> (λb. (λb.λc. bc) b) (λa.λc. ac)  
=> (λb.λc. bc) (λa.λc. ac)  
=> (λc. (λa.λc. ac) c) 

x(yz) => (λa.λb. ab) ((λb.λc. bc) (λa.λc. ac))  
=> (λb. ((λb.λc. bc) (λa.λc. ac)) b)  
=> (λb. (λc. (λa.λc. ac) c) b) 

Est-ce exact? S'il vous plaît aidez-moi à comprendre.

Answer 1

Les dérivations semblent bien, en un coup d'œil. Conceptuellement, il suffit de penser que x, y et z peuvent représenter n'importe quelle fonction calculable, et clairement, certaines de ces fonctions ne sont pas associatives. Say, x est 'soustraire 2', y est 'diviser par 2', et z est 'double'. Pour cet exemple, x (yz) = 'soustraire 2' et (xy) z = 'soustraction 1'.

Answer 2

Cela semble correct, mais pour plus de simplicité, que diriez-vous prouver par contradiction?

Supposons que (xy) z = x (yz), et laisser

x = λa.λb. a  # x = const 
y = λa. -a  # y = negate 
z = 1   # z = 1 

et montrer que ((xy) z) 0 ≠ (x (yz)) 0.

Answer 3

Je pense aussi que votre contre-exemple est correct.
Vous pouvez probablement obtenir un simple contre-exemple comme ceci:

let x = λa.n et y, variables z puis:

(xy) z => ((λa.n) y) z => nz
x (yz) => (λa.n) (yz) => n

Answer 4

Le livre que vous mentionnez par Barendregt est extrêmement formel d précis (un grand livre), donc ce serait bien d'avoir l'énoncé précis de l'exercice. Je suppose que le but réel était de trouver des instanciations pour x, y et z telles que x (yz) se réduit au booléen vrai = \ xy.x et (xy) z se réduit au booléen false = \ xy. y

Ensuite, vous pouvez prendre par exemple x = \ z.true et z = I = \ z.z (y arbitraire). Mais comment peut-on prouver que le vrai n'est pas convertible avec le faux?

Vous n'avez aucun moyen de le prouver à l'intérieur du calcul, puisque vous n'avez pas de négation: vous ne pouvez prouver que des égalités et non des inégalités. Cependant, observons que si true = false alors tous les termes sont égaux.

En effet, pour tout M et N, si true = false,

      true M N = false M N 

mais vrai MN réduit à M, alors que faux MN réduit à N, si

       M = N 

Par conséquent, si elle est vraie = faux tous les termes seraient égaux, et le calcul serait trivial.Puisque nous pouvons trouver des modèles non triviaux du lambda-calcul, aucun modèle ne peut égaler vrai et faux (plus généralement, nous pouvons assimiler des termes à des formes normales différentes, ce qui nous obligerait à parler de la technique bohm-out).