Associativité dans le calcul Lambda

Question

Je travaille sur les questions d'exercice du livre Le calcul Lambda . L'une des questions que je suis coincé se révèle ce qui suit: Montrer que l'application n'est pas associative; en fait, x (yz) pas égal à (xy) z

Voici ce que j'ai travaillé à ce jour:

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 très bien, un coup d'oeil.

Conceptuellement, il suffit de penser que x, y et z peuvent représenter toutes les fonctions calculables, et clairement, certaines de ces fonctions ne sont pas associatives. Par exemple, x est 'soustraction 2', y est égal à 'diviser par 2', et z est 'double'. Pour cet exemple, x (yz) = 'soustraire 2' et (xy) = z 'soustraire 1'.

Answer 2

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

  

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

     

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

Answer 3

Il semble ok, mais pour simplifier, comment prouver au sujet de contradiction?

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

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

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

Answer 4

Le livre que vous mentionnez par Barendregt est extrêmement formel et précis (un grand livre), il serait agréable d'avoir l'énoncé précis de l'exercice.

Je suppose que l'objectif réel était de trouver instanciations pour x, y et z tels que x (y z) se réduit à la valeur booléenne true = \ xy.x et (x y) z se réduit à la valeur booléenne false = \ xy.y

Ensuite, vous pouvez par exemple x = \ z.true et z = I = \ z.z (y arbitraire).

Mais comment peut-on prouver que le vrai ne peut être converti en faux? Vous avez aucun moyen de le prouver dans le calcul, puisque vous avez pas de négation: vous ne pouvez prouver égalités et pas les inégalités. Cependant, nous observons que si true = false, tous les termes sont égaux.

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

                         true M N = false M N

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

                              M = N

Par conséquent, si vrai = false tous les termes seraient égaux, et le calcul serait trivial. Étant donné que nous pouvons trouver des modèles non triviaux du calcul lambda, aucune modèle peut assimiler vrai et faux (plus généralement peut assimiler termes avec différentes formes normales, qui nous obligerait à parler de la Bohm-out technique).