SKK Openlab - SKK = I

SKK の名前を考えたときに Combinatory Logic での有名な等式 SKK = I が念頭にあったのは事実です．ずい分昔に Henk Barendregt さんにこの話をしたこともありました．Combinatory Logic は一般にはあまり知られていないので簡単に紹介をしてみます． Combinatory Logic は，λ計算と同様，すべての項 (term, 計算機の言葉で言えば，プログラムに相当するもの)が関数であるような体系である．Logic という名前がついているのは，その上に論理を展開することを目的としていたからであるが，論理の体系としては成功しなかった．しかし，λ計算と密接な関係があることから，計算の体系としては重要なものである． Combinatory Logic の項 (combinator) は以下の文法規則で定義される． 項 ::= 変数 | 定数 |

[faerie]

ocaml だと let s a b c = (a c)(b c);; let k a b = a;; let i a = a;; (i 765) = (s k k 765);;

[gojoe]

SKKの語源とCombinatorの説明