SKK = I

SKK の名前を考えたときに Combinatory Logic での有名な等式 SKK = I が念頭にあったのは事実です．ずい分昔に Henk Barendregt さんにこの話をしたこともありました．Combinatory Logic は一般にはあまり知られていないので簡単に紹介をしてみます．

Combinatory Logic は，λ計算と同様，すべての項 (term, 計算機の言葉で言えば，プログラムに相当するもの)が関数であるような体系である．Logic という名前がついているのは，その上に論理を展開することを目的としていたからであるが，論理の体系としては成功しなかった．しかし，λ計算と密接な関係があることから，計算の体系としては重要なものである．

Combinatory Logic の項 (combinator) は以下の文法規則で定義される．

    項 ::= 変数 | 定数 | 項(項)

すなわち，項は，変数であるか，定数であるか，(関数としての)項 f に(引数としての)項 a を適用した項 f(a) のいずれかである． 通常よく用いられる定数には S, K, I がある．したがって，たとえば，I, S, S(K), S(K)(K) はすべて上の定義により項になる．

なお，通常，Combinatory Logic では f の a への適用 f(a) のことを適用の演算子 * を用いて f*a のように書いて，* は左に結合すると約束する．したがって，f*x*y と書けば，これは (f*x)*y のことであり，f*(x*y)のことではない．その上で，さらに，通常は，* も省略することを許しているので，今の例は fxy となる．しかし，ここでは，そのような省略はしない．fxy とは書かないで，f(x)(y) と書くことにする．ふつう，Combinatory Logic で SKK と書かれる項は，S(K)(K) のことである．

Combinatory Logic の項は引数をひとつだけとるので，apply を用いて app を定義しておく．これにより，項 f(x) を Emacs Lisp で (app f x) と書くことができるようになる．

    (defun app (f x) (apply f (list x)))

Combinatory Logic の定数 S は等式 S(f)(g)(x) = f(x)(g(x)) を満足する combinator として定義される．

    i.e., (app (app (app S f) g) x) = (app (app f x) (app g x))

λ計算では S を以下のように定義できる (λ計算の解説は省略するが，第 0 近似としては Lisp だと思ってよい:-) もちろん，歴史的にはλ計算が Lisp に影響を与えているのであるが．．．)．

    S = λ(f)[λ(g)[λ(x)[f(x)(g(x))]]]

この S を Emacs Lisp で定義すると次のようになる．

    (defconst S
      (lambda (f) `(lambda (g) (let ((f ,f))
                                 `(lambda (x) (app (app ,f x) (app ,g x)))))))

3 つ目の引数 x がコピーされてふたつになることが S のポイントである．

K combinator は等式 K(x)(y) = x を満足する定数として定義される．

    i.e., (app (app K x) y) = x

λ計算では K を以下のように定義できる．

    K = λ(x)[λ(y)[x]]

この K を Emacs Lisp で定義すると次のようになる．

    (defconst K (lambda (x) `(lambda (y) ,x)))

2 つ目の引数をすてることが K のポイントである．

I combinator は恒等関数を表し，等式 I(x) = x を満足する．

    i.e., (app I x) = x

λ計算では I を以下のように定義できる．

    I = λ(x)[x]

I を Emacs Lisp で定義すると次のようになる．

    (defconst I (lambda (x) x))

Combinatory Logic で S(K)(K) = I という等式が成り立つということの意味は，任意の combinator x に対して，S(K)(K)(x) を計算してみると

    S(K)(K)(x) = K(x)(K(x)) = x

となり，I についても I(x) = x なので，どちらも，任意の入力 x について何も変更を加えないで x をそのまま出力する関数と考えられということである．日本語入力システム SKK という名前には，ユーザの頭の中にある日本語のテキストを，なるべくストレスなしに，そのままディスプレイに出力するプログラムにしたいという気持ちが込められている．

Emacs Lisp でも S(K)(K) を以下のように定義することにより，恒等関数をつくることができる．

    (defconst SKK (app (app S K) K))

examples

    (app SKK 2) ;; -> 2
    (app I 2) ;; -> 2
    (app SKK "SKK") ;; -> "SKK"
    (app I "SKK") ;; -> "SKK"
    (equal SKK (app SKK SKK)) ;; -> t
    (equal I (app I I)) ;; -> t
    (equal SKK I) ;; -> nil となるのは，SKK と I はプログラムとしては同じふるまい
                  ;;    をするが，コードとしては異るからである．

    (defun SKK (x) (app SKK x))
    (SKK 2) ;; -> 2
    (SKK "SKK") ;; -> "SKK"

Combinatory Logic のすごいところは， S と K だけで計算可能な関数をすべて記述できるということです．あまりにすごいのでプログラミング言語として使う人はいないようです．これに対して，λ計算は，同じようにすごい言語ですが，Lisp や型付の関数型言語として姿を変て現在もよく使われています．その理由は自然演繹とよばれる論理の体系との関係が深いからだと私は考えています．

===================================================================================
この小文の草稿について有益な質問，コメントを寄せてくださった中島幹夫氏に感謝します．
===================================================================================

Copyright (C) 2002 佐藤雅彦 (京都大学名誉教授)