boolean - 可以使用 SKI 组合子表示 XOR 吗？

Question

我对滑雪组合器有疑问。

XOR（异或）只能使用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。

异或IF _ THEN _ ELSE _

那么给定这个框架，我们如何实现异或呢？我们可以将 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它本身非常投入，但可行

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

最后一步是使最后一行在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

把它们放在一起

总而言之，我们得到了

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)))