ラムダ計算の関連性

Question

私は本の演習の質問に取り組んでいます ラムダ計算. 。私が立ち往生している質問の1つは、次のことを証明することです。アプリケーションが連想的ではないことを示します。実際、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

派生は、一見してうまくいくようです。

概念的には、x、y、zは計算可能な関数を表すことができると考えてください。明らかに、それらの関数の一部は連想的ではないと考えています。たとえば、xは「2」、yは「2で除算」、zは「二重」です。この例では、x（yz）= 'suppract 2'および（xy）z = 'subtract 1'。

Answer 2

また、あなたの反例は正しいと思います。
おそらく、このようなよりシンプルなカウンターエクサムを得ることができます：

させて x =λa.n と y, z 変数：

（xy）z =>（（λa.n）y）z => nz
x（yz）=>（λa.n）（yz）=> n

Answer 3

大丈夫のようですが、簡単にするために、矛盾によって証明するのはどうですか？

（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 4

Barendregtが言及した本は非常にフォーマルで正確なものです（素晴らしい本）ので、演習の正確な声明を持っているといいでしょう。

実際の目標は、x、y、zのインスタンス化を見つけることで、x（yz）がboolean true = xy.xに減少し、（xy）zがboolean false = xy.yに減少することだったと思います。

次に、eg x = z.trueおよびz = i = zz（y任意）を取得できます。

しかし、どうすれば真が偽で変換されないことを証明できますか？否定がないので、微積分の内部でそれを証明する方法はありません。あなたは不平等ではなく、均等を証明することしかできません。ただし、true = falseの場合、すべての用語が等しいことを観察しましょう。

確かに、任意のmとnの場合、true = falseの場合、

                         true M N = false M N

しかし、真Mnはmに減少し、偽のMnはnに減少するため、

                              M = N

したがって、true = falseの場合、すべての用語は等しく、計算は些細なものになります。 Lambda計算の些細なモデルを見つけることができないため、そのようなモデルは真と偽を等しく等しくすることはできません（より一般的には、条件を異なる通常の形と同一視する可能性があります。