Associatività in lambda calcolo

Question

Sto lavorando sulle domande di esercizio di libro Il Lambda calcolo . Una delle domande che mi sono bloccato sta dimostrando quanto segue: Mostrare che l'applicazione non è associativa; infatti, x (yz) non è uguale a (xy) z

Ecco quello che ho lavorato su finora:

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)

È corretto? Ti prego, aiutami a capire.

Answer 1

Le derivazioni sembrano bene, a colpo d'occhio.

Concettualmente, basti pensare che x, yez possono rappresentare qualsiasi funzioni calcolabili, e chiaramente, alcune di queste funzioni non sono associativo. Per esempio, X è 'sottrattivo 2', y è 'divisione per 2', e z 'doppio'. Per questo esempio, x (yz) = 'sottrarre 2' e (xy) z = 'sottrarre 1'.

Answer 2

Credo anche che la vostra contro-esempio è corretto.
Probabilmente si potranno ottenere un contro-esempio più semplice in questo modo:

  

lasciò x = λa.n e y , z variabili allora:

     

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

Answer 3

Sembra ok, ma per semplicità, che ne dici di provare per assurdo?

Si supponga (xy) z = x (yz), e lasciare che

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

e mostra che ((xy) z) 0 ≠ (x (yz)) 0.

Answer 4

Il libro si parla da Barendregt è estremamente formale e preciso (un grande libro), quindi sarebbe bello avere la precisa indicazione del esercizio.

Credo che il vero obiettivo era quello di trovare istanze per x, y, z tali che x (y z) riduce al boolean true = \ xy.x e (x y) z riduce al falso booleano = \ xy.y

Quindi, si può prendere ad esempio x = \ z.true ez = I = \ z.z (y arbitraria).

Ma come possiamo dimostrare che vale non è convertibile con falso? Non hai modo di dimostrarlo all'interno del calcolo, dal momento che non si ha la negazione: si può dimostrare solo uguaglianze e disuguaglianze non. Tuttavia, osserviamo che, se veri = false allora tutti i termini sono uguali.

Infatti, per ogni M e N, se vero = falso allora

                         true M N = false M N

ma vero M N riduce a M, mentre falsa M N riduce a N, quindi

                              M = N

Quindi, se veri = false tutti i termini sarebbero uguali, e il calcolo sarebbe banale. Dal momento che siamo in grado di trovare modelli non banali della lambda calcolo, tale modello può equiparare vero e falso (più in generale possono equiparare i conti con diverse forme normali, che ci richiederebbe di parlare del Bohm-out tecnica).