boolean - SKIコンビネータを使用してXORを表現できますか?

Question

SKIコンビネーターについて質問です。

XOR (exclusive or) はS andKコンビネータのみを使用して表現できますか?

私は持っている

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。

の観点からの XORIF _ THEN _ ELSE _

では、このフレームワークが与えられた場合、XOR をどのように実装するのでしょうか? XOR をIF式として定式化できます。

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

イータ還元できる

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)

あとは、 と の 2 つの項を取りx、それを適用する関数を作成する方法を考え出す必要があります。そこにたどり着くには、まず、NOTID

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