Asociatividad en el cálculo lambda

Question

Estoy trabajando en las preguntas del ejercicio de libro El cálculo lambda . Una de las preguntas que estoy atascado está demostrando ser la siguiente: Demostrar que la aplicación no es asociativa; de hecho, x (yz) no es igual a (xy) z

Esto es lo que he trabajado en lo que va:

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)

¿Es esto correcto? Por favor, me ayudan a entender.

Answer 1

Las derivaciones parecen estar bien, de un vistazo.

Conceptualmente, sólo piensa que x, y, z pueden representar cualquier función computable, y claramente, algunas de esas funciones no son asociativos. Say, X es 'reste 2', y es 'divide por 2', y z es 'doble'. Para este ejemplo, x (yz) = 'restar 2' y (xy) = z 'restar 1'.

Answer 2

También creo que su contraejemplo es correcta.
Es probable que pueda conseguir un contraejemplo simple como esto:

  

dejó x = ?a.n y y , z las variables a continuación:

     

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

Answer 3

Parece bien, pero por simplicidad, ¿qué hay de demostrar por contradicción?

Supongamos (xy) z = x (yz), y dejar

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

y mostrar que ((xy) z) 0 ? (x (yz)) 0.

Answer 4

El libro que mencionas por Barendregt es extremadamente formal y preciso (un gran libro), por lo que sería bueno tener la indicación precisa del ejercicio.

supongo que el objetivo real era encontrar ejemplificaciones para x, y, z tal que x (y z) se reduce a la boolean true = \ xy.x y (x y) z reduce a la falsa boolean = \ xy.y

A continuación, se puede tomar, por ejemplo, x = \ z.true y z = I = \ z.z (y arbitraria).

Pero, ¿cómo podemos probar que la verdadera no es convertible con falsa? Usted no tiene manera de demostrarlo dentro del cálculo, ya que no tienen la negación: sólo se puede probar igualdades y desigualdades no. Sin embargo, observemos que si es cierto = false entonces todos los términos son iguales.

De hecho, para cualquier M y N, de ser cierto = false entonces

                         true M N = false M N

pero cierto M N se reduce a M, mientras que falsa M N se reduce a N, por lo

                              M = N

Por lo tanto, si verdaderos = false todos los términos serían iguales, y el cálculo sería trivial. Ya que podemos encontrar modelos no triviales de la cálculo lambda, tal modelo puede equiparar verdadero y falso (más generalmente puede equiparar con términos diferentes formas normales, eso nos obliga a hablar de la técnica de Bohm de salida).