SKIコンビネータにてConsを作るまで

俺が如何なる考え方にてSKIコンビネータにてConsを作ることができたかを記録しておく。
もっと別の経路でやれば短くなるのかもしれないが。

この記事はS(KS)KとかS(K(SI))Kとかが、見た瞬間に何なのかわかるくらいの人向けなので、わからない人は別のところで勉強してからが良いかと。
まあ知らなくても見てればわかる人にはわかるだろうけど。

目的物

今回作るのは、Cons。 (Cons a b) f → f a b となるように作る。
こうすることで Car=True=K , Cdr=False=KI=SK と表記できるのは周知の事実である。
また、これを求める途中で(Cons a b)全体(つまりcar部とcdr部が埋め込まれた状態)の表記も求めることになる。

前提

基本的にS,K,Iは大文字、それ以外の変数には小文字アルファベットをあてる。
また、頻出のコンビネータとして以下のものには特別に大文字のアルファベットをあてる。 Axyz → S(KS)Kxyz → S(Ka)bc → a(bc) Rxy → S(K(SI))Kxy → SI(Kx)y → yx 上記の式の途中経過(Rx=SI(Kx) など)も多用するので忘れないように。

また、Consなど名称を用いてコンビネータを指す場合は、引数は空白で区切って記すことにする。 Cons a b Car → a といった具合である。
また、一文字のコンビネータのみを用いる場合も、括弧によっては空白や改行を使用する。

作ってみる (引数組み込み済)

経路

今回は、 fxy ← Rxfy ← Bxyf を目標として考えてみる。
また、最初に(Cons x y)の表現を求めたのち、Consと引数を分離することにしよう。

Bxyf → Rxfy

ここで注目すべきは、引数の順番。
xyf(123)からxfy(132)となっている。ここで Cxyz → xzy となるようなコンビネータCあるいはCxyの表現(zはConsの第3引数にあたるので組み込んではいけないが、xとyは良い)が求まれば、見出しの式と比べて C(Rx)yf → Rxfy → fxy とできる。
さて、ここでxの出現する順番(最初)が変わらないのはヒントとなる。
以下のような発想ができるかどうかが、成功と失敗の分かれ目なのかもしれない。
とはいっても、A=S(KS)Kを試行錯誤で手作りしたことのある人には経験として染み付いた考えかただと思われるが。 Sxyz → xz(yz) よって Sx(Ky)z → xz(Kyz) → xzy 簡単である。

さて、これによってCxyの表現がわかる。 Sx(Ky)z → xzyより S(Rx)(Ky)z → (Rx)zy → zxy よって Rx=SI(Kx) より (Cons x y) = S(SI(Kx))(Ky) 結果が出た。実際に計算してみると、 (Cons x y) Car = S(SI(Kx))(Ky)K → SI(Kx)K(KyK) → IK(KxK)y → kxy → x (Cons x y) Cdr = S(SI(Kx))(Ky)(KI) → SI(Kx)(KI)(Ky(KI)) → I(KI)(Kx(KI))y → KIxy → y たしかに正しい。あっけないものだ。
しかし問題(というか面倒)なのはここからなのだ。

Cons単体を作ってみる

幸運なことに、上で求めたものではx,yとも1回ずつ、順番を変えずに出現している。 そこで、まずは少々変形して (Cons x y) = S(Rx)(Ky) ← ASRx(Ky) = (ASR)x (Ky) とした上で、 Dxy → ax(by) となるようなDを求めてみる。
もちろんここでは a=(ASR), b=K である。

Dxy → ax(by)

こういうのは、いつものやり方が一番スマートに求まるものなので、無理に工夫せず普通に求める。

D = Scd とすると Dxy = Scdxy → cx(dx)y c = A のとき cx(dx)y = Ax(dx)y → x(dxy)

y側はなんとかなりそう。xの左にも何か付ける。
ex(dxy) ← A(ex)(dx)y ← AAex(dx)y
という感じでどうだろうか。これだと c = AAe である

c = AAe のとき cx(dx)y = AAex(dx)y → A(ex)(dx)y → ex(dxy) この場合 e = a である。 ここで dxy→by 、すなわち dx→b となってほしい。 dx → b より d = Kb このとき c = AAe = S(KA)e = S(K(S(KS)K))a である。 よって D = Scd = S (S(K(S(KS)K))a) (Kb) である。実際、 Dxy = S(S(K(S(KS)K))a)(Kb)xy = S(AAa)(Kb)xy → AAax(Kbx)y → A(ax)by → ax(by) さて、 a=(ASR) 、 b=K であるから a = ASR → S(KS)R = S(KS)(S(K(SI))K) より D = S(S(K(S(KS)K))a)(Kb) = S( S (K(S(KS)K)) (S(KS)(S(K(SI))K)) )(KK) すなわち Cons = S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)

これでConsが求まった。確認してみよう。

Cons x y z = S (S(K(S(KS)K))(S(KS)(S(K(SI))K))) (KK) x yz → S (K(S(KS)K)) (S(KS)(S(K(SI))K)) x (KKx) yz → K(S(KS)K)x (S (KS) (S(K(SI))K) x) Kyz → S(KS)K (KSx (S(K(SI))Kx)) Kyz → S (KS) K (S(S(K(SI))Kx)) Kyz → KS(S(S(K(SI))Kx)) (K(S(S(K(SI))Kx))) Kyz → S (K(S(S(K(SI))Kx))) K y z → K(S(S(K(SI))Kx))y (Ky) z → S (S(K(SI))Kx) (Ky) z → S (K(SI)) K x z (Kyz) → K(SI)x (Kx) z y → SIx(Kx) zy → I(Kx)(x(Kx)) zy → Kx(x(Kx)) zy → xzy 合っている。よかった。

以上によってConsをSKIコンビネータにて表すことができた。

まとめ

(Cons x y) = S(SI(Kx))(Ky) Cons = S(S(K(S(KS)K))(S(KS)(S(K(SI))K)))(KK)

おまけ

最初に書いたとおり True=Car , False=Cdr なので、Consを利用して Not が簡単に書ける。 Not: Not True → False Not False → True Not = (Cons False True) = S(SI(K(KI)))(KK) 棚からぼたもち的かも。

追記

もっと簡単な発想でcar部・cdr部組み込みのconsは作れますね。

C = (Cons x y) とおく。 Cf → fxy C = Sab とすると Cf = Sabf → af(bf) a = Scd とすると af(bf) = Scdf(bf) → cf(df)(bf) ここで cf = f , df = x , bf = yであればよいので c = I , d = Kx , b = Ky よって a = Scd = SI(Kx) よって C = Sab = S(SI(Kx))(Ky)