將flip lambda轉換爲SKI條款

Question

我無法將flip的lambda轉換爲SKI combinators（我希望有道理）。這裏是我的轉換：

/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是翻蓋，它的滑雪條件定義爲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. 

我缺少什麼？

Answer 1

一旦答案被接受，我修改了它，我發現它實際上是錯誤的。

您的最終結果是正確的，雖然它不是教科書中的「官方」答案，但有可能不同的SKI術語實際上等同於相同的lambda表達式。

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組合子。