みなさま ラムダ計算 をご存知でしょうか。
ラムダ計算はある種の関数型プログラミング言語の体系で、変数と関数, そして関数適用というミニマルな構成要素だけでチューリング完全な表現力を持っています。
この記事では、ラムダ計算の中でも特に単純な 型無しラムダ計算 に着想を得てラムダ計算のステップ評価器を作っている話について書きます。
既存のモデルへの不満
型無しラムダ計算の処理系は昔からいくつも実装されていて、有名なところで Unlambda や Lazy_K などがあります。
どちらも SKI コンビネーター理論 に基づいていて、 s, k, i という たった3つの組み込み関数でプログラムを記述することが可能 1 です。
かく言う私も Unlambda から型無しラムダ計算に入門したクチです。しかし、従来の処理系には長らく不満がありました。それは関数の計算過程が印字不可で、計算の過程が非常に見えづらいことです。
早い話 Unlambda や Lazy_K は print デバッグできないのがツラい という事なのですが。私の見立てではこの print デバッグで試行錯誤できない感が ラムダ計算の世界から入門者を遠ざけている要因になっている ように思います。
ラムダ計算の計算過程を可視化する
そこで、『無いものは作ればいい精神』です。型無しラムダ計算学習用ステップ評価器 skiMogul を作りました。
実際の動作を見てもらう方がイメージしやすいと思うので GIF を、
ラムダ式をステップ評価する様が見て取れると思います。
今のところ
- 論理演算 (
NOT,AND,OR,XOR) - 整数(チャーチ数)の操作 (後者関数
SUCC, 前者関数PRED) - 整数(チャーチ数)の演算 (和
ADD, 差SUB, 積MUL, 商と剰余DIV) - 整数(チャーチ数)の同士の比較 (ゼロ比較
IS_ZERO, 等値比較EQ, 不等比較GT,LT) - 連結リスト操作 (
CONS,CAR,CDR) - 無名再帰 (Y コンビネータ)
- 自作関数の定義
などが出来ます。
シンタックス
skiMogul の記法について簡単に解説してみます。
関数適用 (関数実行)
まず、 i という組み込みの関数があります。 Identity の略で、引数をそのまま返す関数です。
> i i
このように、i 単体を評価しても何も起きません。
では、関数 i に引数 x を与えて実行してみましょう。JavaScript 風にパーレン () で関数呼び出しを書きます。
> i(x) i(x) ⇒ x
はい、実行結果は x です。
このように関数に引数を与えて実行することを 関数適用 と云います。この場合 i に x を適用しました。
他にも組み込み関数を使ってみましょう。定数関数 k は2つの引数を取り、2つめの引数を捨てて1つめの引数をそのまま返します。
k は Constant (Konstant) の略ですね、たぶん。
k(x, y) ⇒ x
「2つの引数を取る」と書きましたが、これは正確な表現ではありません。厳密には Mogul の世界には多変数関数が存在せず、1引数関数しか扱えないからです。
k(x, y) は k(x)(y) と同じ意味に解釈されます。これは k に x を適用した結果に y を適用していると読めます。このように1変数関数を用いて多変数の関数適用を表現する方法を「関数のカリー化」と言います 🍛
もう一つ欠かせない関数 s を使ってみましょう。
s は Substitution の略で、3引数 x, y, z を与えると x(z, y(z)) を返します。
> s(x, y, z) s(x, y, z) ⇒ x(z, y(z))
関数合成 や 引数の入れ替え を実現するために重要な関数です。
関数抽象と関数定義
ラムダ計算に欠かせないのが 関数抽象 です。
モダンなプログラミング言語に親しんだ方であれば 無名関数 または クロージャー (closure) の事だと云えば伝わりやすいでしょうか。
例として、引数 x に対して x(x) を返す関数抽象を以下のように書きます。
x => x(x)
関数抽象に引数を与えて評価することができます。 a を適用してみましょう。
> (x => x(x))(a) (x => x(x))(a) ⇒ a(a)
いいですね。
関数定義
関数抽象は 別の変数に代入する こともできます。
> FOO = x => x(x) > FOO(a) FOO(a) ⇒ (x => x(x))(a) ⇒ a(a)
このようにして自作関数 FOO を定義することができました。これが 関数定義 です。
多変数関数
多変数関数は関数抽象をネストさせることで実現します。
> x => y => y(x) x => y => y(x) > (x => y => y(x))(a)(b) (x => y => y(x))(a)(b) ⇒ (y => y(a))(b) ⇒ b(a)
上手く動いていますね。
このように1引数の関数抽象をネストさせて多変数関数を表現する方法を カリー化 と云います。
ちなみに、skiMogul では多変数風の関数抽象の糖衣構文を用意しているので下記のように書くこともできます。
> (x, y) => y(x) (x, y) => y(x) > ((x, y) => y(x))(a, b) ((x, y) => y(x))(a, b) ⇒ (y => y(a))(b) ⇒ b(a)
関数の定義を参照する
ここまでに見てきたように、 Mogul では関数適用を変数に代入することで自作の関数を定義することが出来ます。
逆に定義済みの関数の定義を参照するには ? コマンド を使います。
> ? s s(x, y, z) = x(z, y(z))
Mogul には他にも多くの組み込み関数が定義されています。 Context パネルで定義済みの関数を一覧できます。
また ? コマンドを単体で実行することでも同じように見ることができます。
> ? i(x) = x k(x, y) = x s(x, y, z) = x(z, y(z)) Y(f) = (x => f(x(x)))(x => f(x(x))) ... XOR(x, y) = x(NOT(y), y) ι(f) = f((x, y, z) => x(z, y(z)), (x, y) => x)
skiMogul で計算っぽいことをやってみる
遊んでみましょう。
論理演算
論理演算のために必要な一通りの関数が用意されています。
TRUE, FALSE, NOT, AND, OR, XOR などです。
> AND(TRUE, FALSE) AND(TRUE, FALSE) ⇒ TRUE(FALSE, FALSE) ⇒ ((x, y) => x)(FALSE)(FALSE) ⇒ (y => FALSE)(FALSE) ⇒ FALSE > AND(TRUE, NOT(FALSE)) AND(TRUE, NOT(FALSE)) ⇒ TRUE(NOT(FALSE), FALSE) ⇒ ((x, y) => x)(NOT(FALSE))(FALSE) ⇒ (y => NOT(FALSE))(FALSE) ⇒ NOT(FALSE) ⇒ FALSE(FALSE, TRUE) ⇒ ((x, y) => y)(FALSE)(TRUE) ⇒ (y => y)(TRUE) ⇒ TRUE > AND(OR(FALSE, TRUE), NOT(FALSE)) AND(OR(FALSE, TRUE), NOT(FALSE)) ⇒ OR(FALSE, TRUE)(NOT(FALSE), FALSE) ⇒ FALSE(TRUE, TRUE)(NOT(FALSE), FALSE) ⇒ ((x, y) => y)(TRUE)(TRUE, NOT(FALSE), FALSE) ⇒ (y => y)(TRUE)(NOT(FALSE), FALSE) ⇒ TRUE(NOT(FALSE), FALSE) ⇒ ((x, y) => x)(NOT(FALSE))(FALSE) ⇒ (y => NOT(FALSE))(FALSE) ⇒ NOT(FALSE) ⇒ FALSE(FALSE, TRUE) ⇒ ((x, y) => y)(FALSE)(TRUE) ⇒ (y => y)(TRUE) ⇒ TRUE
IF を使うと if式 っぽいものを書くこともできます。
> IF(FALSE)(x, y) IF(FALSE, x, y) ⇒ FALSE(x, y) ⇒ ((x, y) => y)(x)(y) ⇒ (y => y)(y) ⇒ y
整数演算
0 ～ 20 までの整数 2 は定義済みです。
和 ADD, 差 SUB, 積 MUL, 商と剰余 DIV を計算することもできます。
> ADD(2, 3) ADD(2, 3) ⇒ (f, x) => 2(f, 3(f, x))
この評価結果はラムダ計算的に正しいのですが、最終結果を見ても釈然としないかも知れませんね。
等価比較 EQ を使って ADD(2, 3) が 5 に等しいことを確かめてみましょう。
> EQ(ADD(2, 3), 5) EQ(ADD(2, 3), 5) ⇒ AND(GTE(ADD(2, 3), 5), LTE(ADD(2, 3), 5)) ⇒ GTE(ADD(2, 3), 5)(LTE(ADD(2, 3), 5), FALSE) ⇒ IS_ZERO(SUB(5, ADD(2, 3)))(LTE(ADD(2, 3), 5), FALSE) ... ⇒ (u => TRUE)(_ => FALSE) ⇒ TRUE
結果は TRUE、つまり 2+3 は 5 に等しいということですね。
実装
skiMogul は Rust で実装されています。
Rust コードを wasm にコンパイルして GitHub Pages にデプロイしています。計算のためにサーバーと通信することはありません。すべての計算はフロントエンドで行われます。つまり全てがブラウザ上で実行されているということです。
全てのソースコード は GitHub に置いています。
今後の展望
最初にも書いたように、私が skiMogul を書き始めた動機は ラムダ計算の入門者のハードルを下げること です。だいたい6～10歳くらいの小学生がシンプルに自然にラムダ計算を学び始められる世界を夢見ています。
skiMogul の機能について要望・意見があれば教えてもらえると嬉しいです。
私からは以上です。
