将lambda转换为SKI术语 [英] convert flip lambda into SKI terms

问题描述

我在将lambda转换为SKI组合器时遇到了麻烦(我希望这是有道理的).这是我的转换:

I'm having trouble converting the lambda for flip into the SKI combinators (I hope that makes sense). Here is my conversion:

/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组合器不一样...这是我用于转换的规则:

If I understand properly in the B, C, K, W system, C is flip and it's definition in SKI terms is S (S (K (S (K S) K)) S) (K K). obviously my answer isn't the same as the C combinator... Here are the rules I used for the conversions:

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.

我想念什么?

推荐答案

一旦答案被接受，我便对其进行了修改，但我发现它实际上是错误的.

Once the answer being accepted I revised it and I figured out it is actually wrong.

您的最终结果是正确的，尽管这不是教科书中的正式"答案，但是不同的SKI术语实际上可能等效于相同的lambda表达式.

Your final result is correct, although it is not the "official" answer in the text book, but it is possible that different SKI terms are actually equivalent to the same lambda expression.

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组合器.

The above derive, based on left most reduction order, proves that your final term is equivalent to the C combinator.

这篇关于将lambda转换为SKI术语的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！