3

私は本The Lambda calculusの演習問題に取り組んでいます。私が立ち往生している質問の 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)

これは正しいです？理解を助けてください。

4

4 に答える 4

4

あなたの反例も正しいと思います。
おそらく、次のようなより単純な反例を得ることができます。

let x = λa.nおよびy , z変数の場合:

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

于 2010-06-20T20:18:51.267 に答える
1

大丈夫そうに見えますが、簡単にするために、矛盾によって証明してみませんか?

(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 であることを示します。

于 2010-06-20T20:17:42.813 に答える
1

一見すると、派生は問題ないように見えます。

概念的には、x、y、および z は計算可能な任意の関数を表すことができると考えてください。明らかに、それらの関数の一部は結合的ではありません。たとえば、x は「2 を引く」、y は「2 で割る」、z は「2 倍」です。この例では、x(yz) = '減算 2' および (xy)z = '減算 1' です。

于 2010-06-20T20:14:48.140 に答える
1

あなたがBarendregtによって言及した本は非常に形式的で正確です（素晴らしい本です）ので、演習の正確な声明があるといいでしょう.

実際の目標は、x (yz) がブール true = \xy.x に還元され、(xy) z がブール false = \xy.y に還元されるような x、y、z のインスタンス化を見つけることだったと思います。

次に、たとえば x = \z.true および z = I = \zz (y は任意) を取ることができます。

しかし、true が false と変換できないことをどのように証明できますか? 否定がないため、微積分の中で証明する方法はありません。証明できるのは等号のみで、不等号は証明できません。ただし、true=false の場合、すべての項が等しいことに注意してください。

実際、任意の M と N について、true = false の場合、

                         true M N = false M N

しかし、真の MN は M に還元され、偽の MN は N に還元されるので、

                              M = N

したがって、true = false の場合、すべての項が等しくなり、計算は自明になります。ラムダ計算の自明ではないモデルを見つけることができるため、そのようなモデルは真と偽を同一視することはできません (より一般的には、項を異なる正規形と同一視する可能性があります。これには、ボームアウト手法について話す必要があります)。

于 2017-01-22T17:11:28.950 に答える