はじめに
プログラミング言語 Lazy K とは何か、どのように書けるのか、実際に使うときに気をつけないといけないことまでを追っていきたいと思っています。
今回はLazy Kとは何かについて理解を深めていきたいと思います。
第１回：コンビネータとラムダ計算 ← いまここ
第２回：Lazy K の入出力とチャーチ数
第３回：ラムダ計算のいろいろ
第４回：(Lazy K プログラムを書いてみる)[https://qiita.com/amoyris/items/cc146c54f156a283cb6b]
Lazy K とは
Lazy K とは組み込み関数が３つ（！）しかない純粋関数型言語（注釈１）です。
SKIコンビネータ論理（combinatory logic）を用いてこれを実現しています。
これを用いることで、関数s、k、iのみを用いてチューリング完全な言語が構成されます。
似た言語に非純粋関数型言語である Unlambda があります。
こちらもSKIコンビネータが言語の根幹をなしていますが、Lazy Kと異なり非純粋な（副作用がある）言語です。
Lazy Kの"Lazy"は遅延評価(lazy evaluation)を行うことからきています。
遅延評価とは、値が必要になるまでその評価を行わない、と言うものです。
例えば $0\times 7^6$ を計算するときに $7^6$ を計算しないようなものです（ちょっと違うけど）。
これによって実際の計算をしやすいように設計されています。
SKIコンビネータ
ここでは、SKIコンビネータについて導入していきたいと思います。
正直、コンビネータについて理解するのは難しいので、ラムダ計算についてわかっていればいいと思います。
結局Lazy Kコードを書くときもラムダ計算で書いてトランスパイルするほうが楽だと思います。
なので、別にこの章がわからなくても問題はないです。
前置きはここまでにして、コンビネータ論理とは何かから述べていこうと思います。
コンビネータ論理は計算を単純化したモデルとして使われます。
関数と見ても良いと思います。
SKIコンビネータで用いる３つの関数のうち、最も理解しやすいのはIで、変数x（変数といってもコンビネータだったり関数だったりすることもある）を以下のように変換するコンビネータです。
I x = x
これは（日本語に直すと）恒等コンビネータ（Identity combinator）と呼ばれ、適用された変数をそのまま返すものです。
関数的に書くと、$f(x) = x$ と書けるような関数 $f$ です。
次にKですが、以下のようなものです。
(K x) y = K x y = x
一つ目の式変形に関しては、カッコがなく3つ以上の項が並んでいたら左側から適用されると言う表記のルールを示しているだけなので、あまり気にする必要はないです。
数学的に書くと $f(x,y):=(f(x))(y)$ としましょうね、と言うようなものです。
Kは（日本語に直すと）定数コンビネータ（Constant (独：Konstant) combinator）で、一つ目の引数を受け取ると、二つ目の引数を無視してその値を返す定数関数となるコンビネータです。
数学的に書くと $f(x, y) = x$ となる $f$ といえます。
もう一つのSに関しては次のとおりです。
S x y z = x z (y z)
Sは（日本語に直すと）置換コンビネータ（Substitution combinator）で、一つ目の引数に三つ目の引数と、二つ目に三つ目を適用したものを順に適用するものです。
数学的には $f(g, h, z) = (g(z))(h(z))$ となる $f$ とかになるでしょうか。
これらを使うことで、チューリング完全な体系を作ることができます。（証明に関してはここでは述べません）
さらには、SKKx = Kx(Kx) = x = IxとなるのでSとKだけでもチューリング完全になります。
ラムダ計算
正直、コンビネータで式を作っていくのは非直感的なので、ラムダ計算を導入します。
ラムダ計算は以下の式の組み合わせからなるものです。
<expr> ::= <identifier> (変数)
λ<identifier>.<expr> (ラムダ抽象)
<expr><expr> (関数適用)
<identifier>は識別子を表し、任意の変数のことです。
x、y、hogeなど任意の変数名を使用できます。
問題なのは下二つのラムダ抽象、関数適用だと思います。
ラムダ抽象に関しては、数学的な関数を考えると良いかと思います。
（注１）もちろん他のプログラミング言語でわかるならそれでも良いです。例えばPythonのラムダ式など。
（注２）理解のため数学的な関数を使いますが、厳密性はないのであしからず。
ラムダ抽象λx.xを考えます。
これは数学的な表記に直すと $f(x) := x$と言う関数になります。
λの直後にある変数を引数として取ってきて.の後の式を返すと言うものです。
これにyを関数適用すると、式は(λx.x)yとなりますが、これは、先の関数 $f$ に $y$を代入する、つまり、$f(y)=y$ と言うことで、このことから(λx.x)y = yとなります。
つまり簡単には、ラムダ抽象は関数定義、関数適用は代入と見れば良いです。
ここで、ラムダ計算で重要になる2つの操作を紹介します。
α変換（変数名の付け替え）
α変換は、束縛されている変数名を別の名前に変えるだけの操作です。
例えば、
λx.x =α λy.y
は同じ意味です。
関数の中で使っている引数名を変えただけで、やっていることは変わりません。
ただし、自由変数を巻き込まないように注意が必要です。
例えば以下の変換はできません。
//これは正しくない
λx.x y =α λy.y y
この場合、yは自由変数なので、これをうっかり束縛する形に変えてしまうと別の式になります。
β簡約（関数適用の実行）
β簡約は、関数適用を実際に計算する操作です。
基本形は次のとおりです。
(λx.M) N ->β M[x := N]
これは「M の中の x を N で置き換える」という意味です。
例として、
(λx.x) y ->β y
は、先ほど説明した「代入」と同じ話です。
もう少しだけ複雑な例では、
(λx.λy.x) z ->β λy.z
となります。
実用上は、β簡約を安全に行うために必要なら先にα変換する、という順序で考えると混乱しにくいです。
（自由変数の束縛を避けるためです。）
コンビネータとラムダ計算
では、ここまでの話がどうつながるかを見ます。
結論から言うと、ラムダ計算で書いた式は SKI コンビネータに機械的に変換できます。
変換を $T[ \cdot ]$とすると、以下のように定義できます。
1. T[x] => x
2. T[(E₁ E₂)] => (T[E₁] T[E₂])
3. T[λx.E] => (K T[E]) (Eに自由変数としてxが現れない場合)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]]
6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
詳細は省きますが、これらの操作によってすべてのラムダ計算の式をSKIコンビネータで表すことができます。
つまり、実際に Lazy K を書くときの流れはだいたい次のようになります。
- 先にラムダ計算で式を作る
- 上の規則で SKI に落とす
- 最後に Lazy K の記法に直す
この手順にしておくと、いきなり s、k、i で書き始めるよりもはるかに見通しが良くなります。
Lazy K の書き方
Lazy K では上記SKIコンビネータのs、k、iを用いて一つの式を作ります。
気をつけなければいけないのは、入力に対して返すことができるのは出力だけだと言うことです。
途中結果を出力するといったことはできません。
実際の入出力の方法については、次回行う予定です。
実際にトランスパイルを行うのは、Zennの記事が参考になります。
The Lazy K Programming Languageも参考になります。
終わりに
とりあえずここまでで一旦今回は終わりとします。
次回以降、実際にどのように式(関数)を作っていけば良いのか、見ていこうと思います。
ありがとうございました。
（注釈１）関数型言語とは
プログラミング言語にはプログラミングパラダイムというものがあります。
「~~型プログラミング」のようなものです。
言語設計をする人以外はあまり気にする必要がないと思います。
- 例）オブジェクト指向プログラミング、手続型プログラミング、論理型プログラミング、etc.
その中の一つに関数型プログラミングというものがあります。
これを核としているのが関数型（プログラミング）言語です。
ここでいう関数とは、参照透過性を持つもののことで、つまり、同じ引数が渡されたら結果は同じであるようなものを言います。
呼び出しの回数によって答えが違っていたりしてはいけません。
数学で言う関数と似たようなものです。
関数型言語の中でも、純粋関数型言語と非純粋関数型言語に分けることができます。
純粋関数型言語で有名なのはHaskell、Leanあたりでしょうか。
副作用を許さないと言うのが純粋関数型言語の特徴です。
副作用とは、関数の途中で入出力をするなど、返り値以外で外部に影響を与えるようなもののことです。
逆に非純粋関数型言語は副作用を許すものです。
有名なのはErlang、Lisp、MLなどでしょうか。
まあ、プログラミング言語にはいろいろあるんだな、くらいの理解で良いと思います。
（注釈２） Lazy Kの方言
Lazy K には幾つかの書き方があります。
代表的なのは次の2つです。
- 括弧を使って書く書き方（コンビネータ計算様式）
- バッククォート（`）で関数適用を前置する書き方（Unlambda様式）
例えば、同じ式でも次のように見た目が変わります。
((S K) K) = S K K // コンビネータ計算様式
``skk // Unlambda様式（`ab = (a b)）
意味はどれも同じで、書き方だけが違います。
大文字のSKIを使う時はコンビネータ計算様式で書くとき、小文字のskiはUnlambda様式を使って書く時です。
他にIota様式(*とiでかく。ι = λx.xSKを使う。このコンビネータだけでチューリング完全)、Jot様式(0と1でかく。ちょっとよくわからない)がありますが、これらはとりあえずは気にする必要はないでしょう。