1

与えられた

S=\x.\y.\z.x z (y z)

と

K=\x.\y.x

(SKK) 形式または同等の拡張形式から開始した場合、同じ式 (SKK) の 2 つのベータ版の同等の形式が型なしラムダ計算で異なる結果をもたらす方法を理解できません。

(S K K) = ((S K) K) -> ((\y.(\z.((K z) (y z)))) K) -> (\z.((K z) (K z))) ->
(\z.((\y.z) (K z))) -> (\z.z) -> 4 reductions!

(S K K) = \x.\y.\z.x z (y z) \x.\y.x \x.\y.x -> 0 reductions!

圧縮された形式と展開された形式では括弧が異なるようです。実際、最初のものは次のように括弧で囲まれています。

(S K K) = ((S K) K)

2番目は次のようになります。

\x.\y.\z.x z (y z) \x.\y.x \x.\y.x =
(\x.(\y.(\z.(((x z) (y z)) (\x.(\y.(x (\x.(\y.x)))))))))

誰かがこれについて何か洞察を持っていますか??? ありがとうございました

4

2 に答える 2

4

ウィキペディアでラムダ計算の正式な定義を確認してください。抽象化とアプリケーションには、常に括弧で囲まれたセットがあります。これは、SとKのより正確な定義が次のとおりであることを意味します。

S = (\x.\y.\z.x z (y z))

と

K = (\x.\y.x)

これらをに代入すると(S K K)、正しい結果が得られます。

于 2011-12-07T17:48:50.590 に答える
1

では(S K K)、一部の括弧は暗黙的です。((S K) K)関数の適用は常にバイナリであり、左結合と見なされるため、この形式は の省略形です。

于 2011-12-07T17:00:53.460 に答える