可以使用SKI組合子表達XOR嗎？

Question

我對SKI-Combinators有疑問。

僅可使用S和K組合子表達異或（不包括）還是僅使用S和K？

我

True = Cancel 
False = (Swap Cancel) 

其中

Cancel x y = K x y = x 
Swap: ff x y = S ff x y = ff y x 

Answer 1

布爾

你的問題是在細節上有點不清楚，但似乎你的意思是，你有以下代表布爾值：

T := K 
F := S K 

這工作，因爲這意味着按下述公式成立：

T t e => t 
F t e => e 

換句話說，b t e可以解釋爲IF b THEN t ELSE e。

XOR在IF _ THEN _ ELSE _

條款，以便給出這個框架，我們如何實現XOR？我們可以制定XOR作爲IF表達：

xor x y := IF x THEN (not y) ELSE y = (IF x THEN not ELSE id) y 

可以是ETA-減少到

XOR x := IF x THEN not ELSE id = x not id 

一些功能組合子

我們有id = SKK作爲標準配置，並且not可以表達作爲flip，因爲flip b t e = b e t = IF b THEN e ELSE t = IF (not b) THEN t ELSE e。 flip it self is quite involved但可行的

flip := S (S (K (S (KS) K)) S) (KK) 

現在我們只需要找出一種方式來寫一個函數，x並將其應用於在兩個方面NOT和ID。爲了達到這個目標，我們首先注意到的是，如果我們設置

app := id 

然後

app f x = (id f) x = f x 

等，

(flip app) x f = f x 

我們幾乎沒有，因爲到目前爲止的所有顯示

((flip app) id) ((flip app) not x) = ((flip app) not x) id = (x not) id = x not id 

最後一步是讓tha t在x上的最後一行免費。我們可以做到這一點的函數合成運算：

((flip app) id) ((flip app) not x) = compose ((flip app) id) ((flip app) not) x 

凡compose要求是

compose f g x = f (g x) 

，我們可以通過設置

compose f g := S (K f) g 

全部放在一起得到

T Ø總結，我們得到了

xor := compose ((flip app) id) ((flip app) not) 

，或者完全展開：

xor = S (K ((flip app) id)) ((flip app) not) 
    = S (K ((flip app) (SKK))) ((flip app) flip) 
    = S (K ((flip SKK) (SKK))) ((flip SKK) flip) 
    = S (K (((S (S (K (S (KS) K)) S) (KK)) SKK) (SKK))) (((S (S (K (S (KS) K)) S) (KK)) SKK) (S (S (K (S (KS) K)) S) (KK)))