Ассоциативность в лямбда-исчислении

Question

Я работаю над вопросами упражнения из книги Лямбда-исчисление .Один из вопросов, который я застрял, - это доказать следующее: показать, что приложение не является ассоциативным;на самом деле x (yz) не равно (xy) z

Вот то, над чем я работал до сих пор:

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)

Это правильно?Пожалуйста, помогите мне понять.

Answer 1

Я также думаю, что ваш контрпример является правильным.
Возможно, вы можете получить более простой контрпример, например, такой:

let x = λa.n и y , z переменных, затем:

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

Answer 2

Вроде бы нормально, но для простоты, как насчет доказать противоречие?

Предположим (xy) z = x (yz), и пусть

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

и покажем, что ((xy) z) 0 ≠ (x (yz)) 0.

Answer 3

Выводы кажутся хорошими, на первый взгляд.

Концептуально, просто подумайте, что x, y и z могут представлять любые вычислимые функции, и, очевидно, некоторые из этих функций не ассоциативны.Скажем, x - это «вычитание 2», y - «деление на 2», а z - «удвоение».В этом примере x (yz) = «вычесть 2» и (xy) z = «вычесть 1».

Answer 4

Книга, которую вы упомянули в Barendregt, чрезвычайно формальна и точна (отличная книга), поэтому было бы неплохо получить точное изложение упражнения.

Я полагаю, что реальная цель состояла в том, чтобы найти экземпляры для x, y и z, которые бы x (y z) сводится к логическому значению true = \ xy.x, а (x y) z сводится к логическому значению false = \ xy.y

Тогда вы можете взять, например, x = \ z.true и z = I = \ z.z (y произвольно).

Но как мы можем доказать, что истина не преобразуется в ложь? У вас нет возможности доказать это внутри исчисления, поскольку у вас нет отрицания: вы можете доказать только равенства, а не неравенства. Однако заметим, что если true = false, то все члены равны.

Действительно, для любых M и N, если true = false, тогда

                         true M N = false M N

но истинное M N уменьшается до M, в то время как ложное M N уменьшается до N, поэтому

                              M = N

Следовательно, если true = false, все члены будут равны, и исчисление будет тривиальным. Поскольку мы не можем найти нетривиальные модели лямбда-исчисления, нет таких модель может приравнивать истину и ложь (в более широком смысле могут приравнивать термины к различным нормальным формам, что потребовало бы от нас говорить о технике Бум-аута).