3

フリップのラムダを SKI コンビネータに変換するのに問題があります (意味があることを願っています)。これが私の変換です：

/fxy.fyx
/f./x./y.fyx
/f./x.S (/y.fy) (/y.x)
/f./x.S f (/y.x)
/f./x.S f (K x)
/f.S (/x.S f) (/x.K x)
/f.S (/x.S f) K
/f.S (S (/x.S) (/x.f)) K
/f.S (S (K S) (K f)) K
S (/f.S (S (K S) (K f))) (/f.K)
S (/f.S (S (K S) (K f))) (K K)
S (S (/f.S) (/f.S (K S) (K f))) (K K) 
S (S (K S) (/f.S (K S) (K f))) (K K)
S (S (K S) (S (/f.S (K S)) (/f.K f))) (K K)
S (S (K S) (S (/f.S (K S)) K)) (K K)
S (S (K S) (S (S (/f.S) (/f.K S)) K)) (K K)
S (S (K S) (S (S (K S) (/f.K S)) K)) (K K)
S (S (K S) (S (S (K S) (S (/f.K) (/f.S))) K)) (K K)
S (S (K S) (S (S (K S) (S (K K) (K S))) K)) (K K)

B、C、K、Wシステムで正しく理解すると、Cはフリップであり、SKI用語での定義は ですS (S (K (S (K S) K)) S) (K K)。明らかに、私の答えは C コンビネータと同じではありません...変換に使用したルールは次のとおりです。

K y = /x.y  - K combinator
(SKK) = /x.x  -  I combinator
(S (/x.f) (/x.g)) = (/x.fg)  -  S combinator
y = (/x.yx)  -  eta reduction
/x./y.f = /xy.f  - currying
Note that the S rule can convert longer expressions - for example, λ x.abcdeg can be converted by setting f = abcde.

私は何が欠けていますか？

4

1 に答える 1

4

回答が受け入れられたら、それを修正しましたが、実際には間違っていることがわかりました。

テキストブックの「公式」回答ではありませんが、最終結果は正しいですが、異なるSKI用語が実際には同じラムダ式と同等である可能性があります。

S [S (K S) (S (S (K S) (S (K K) (K S))) K)] [K K] f x y
-> S (K S) (S (S (K S) (S (K K) (K S))) K) f (K K f) x y
-> K S f (S (S (K S) (S (K K) (K S))) K f) (K K f) x y
-> S [S (S (K S) (S (K K) (K S))) K f] (K K f) x y
-> S [S (K S) (S (K K) (K S))] K f x (K K f x) y
-> S [K S] [S (K K) (K S)] f (K f) x (K K f x) y
-> K S f (S (K K) (K S) f) (K f) x (K K f x) y
-> S [S (K K) (K S) f] [K f] x (K K f x) y
-> S [K K] [K S] f x (K f x) (K K f x) y
-> K K f (K S f) x (K f x) (K K f x) y
-> K (K S f) x (K f x) (K K f x) y
-> K S f (K f x) (K K f x) y
-> S [K f x] [K K f x] y
-> K f x y (K K f x y)
-> f y (K K f x y)
-> f y (K x y)
-> f y x

上記の派生は、左端の縮小順序に基づいており、最終項が C コンビネータと同等であることを証明しています。

于 2015-08-20T11:43:43.907 に答える