はじめに
プログラミング言語 Lazy K とは何か、どのように書くのか、実際に使うときの注意点までを追っていきます。
今回は、Lazy Kの入出力と、それに必要なチャーチ数とリストについて理解を深めたいと思います。
第１回：コンビネータとラムダ計算
第２回：Lazy K の入出力とチャーチ数 ← いまここ
第３回：ラムダ計算のいろいろ
第４回：(Lazy K プログラムを書いてみる)[https://qiita.com/amoyris/items/cc146c54f156a283cb6b]
Lazy K の仕様
Lazy K の仕様をThe Lazy K Programming Languageから読み取ってみましょう。
入出力の章を見てみると、次のように書かれています。
How to handle input and output in a language without side effects? In a certain sense, input and output aren't side effects; they are, so to speak, front- and back-effects. So it is in Lazy K, where a program is simply treated as a function from the space of possible inputs to the space of possible outputs.
（日本語訳）副作用のない言語で入出力はどのように扱うべきでしょうか？ある意味では、入出力とは副作用ではなく、いわば前処理および後処理作用（訳註：つまり引数と評価値）です。Lazy K のプログラムは、入力空間から出力空間への関数として扱われます。
Lazy Kでは、入力を受け取って出力を返す一つの関数がコードになります。
つまり、$f(input) = output$ となるような関数を作ります。
Input and output streams are represented as lists of natural numbers from 0 to 255, each corresponding to one byte. End-of-file is represented by the value 256, not by end of list. (This is because it is often easier to deal with EOF as a character than as a special case. Nevertheless, I wonder if it wouldn't be better to use end-of-list.)
（日本語訳）入力ストリームと出力ストリームは、0から255までの自然数のリストとして表現され、各リストは1バイトに対応します。ファイル終端(EOF)は、リストの終端としてではなく、値256で表されます。（これは、EOFを特殊なケースとして扱うよりも、文字として扱う方が簡単な場合が多いからです。とはいえ、リストの終端を使った方が良いのかもしれません。）
The input list is infinite in length, and all elements after the first occurrence of 256 are also 256.
（日本語訳）入力リストは無限長で、256 が最初に出現した後のすべての要素も 256 です。
The present interpreter actually accepts any value of 256 or greater as the end of the output, and its return code to the operating system is that value minus 256.
（日本語訳）現在のインタプリタは、実際には256以上の任意の値を出力の終了値として受け入れ、オペレーティングシステムへの戻り値はその値から256を引いた値となります。
入力はバイト値（0〜255）のリストとして渡されます。
入力の終端にはEOFとして値256が渡されます。
入力リストには、EOF以降も値256が無限に格納されています。
出力も同様に、終端に256を加えたバイト値のリストを返します。
256以上の数字は同様に出力終了として扱われ、その値が $n$ のとき終了コードは $n - 256$ になります。
256以上の値が見つかった時点でそれ以降のリスト内の値は無視されます。
For the purpose of making these lists, pairs are represented in the usual way (that is, the pair (X . Y) is the function (lambda (f) (f X Y))) and natural numbers are represented as Church numerals (that is, the number n is represented by the operation of n-fold composition).
（日本語訳）これらのリストを作成する目的で、ペアは通常の方法で表現され（つまり、ペア（X,Y）は関数（λf. f X Y）で表されます）、自然数はチャーチ数で表現されます（つまり、数nは（訳註：関数の）n重合成の演算で表されます）。
入出力のリストは、チャーチ数というものを使って作成します。
純粋ラムダ計算には数値の原始型がないため、そのままでは通常の数字を使った演算はできません。
そのため、別の方式で数字を受け取る必要があります。
それがチャーチ数です。
これについて、次の章から述べていきます。
チャーチ数
チャーチ数とは「関数のみを使って自然数(0を含む)を表現する」方法です。
ラムダ計算の創案者であるアロンゾ・チャーチの名前からとられています。
チャーチ数では数字を以下のように表します。
0 := λf. λx. x
1 := λf. λx. f x
2 := λf. λx. f (f x)
3 := λf. λx. f (f (f x))
...
つまり、xにfを $n$ 回適用したもので数値 $n$ を表します。
fに $\lambda x. x + 1$、xに $0$ を適用することによって、通常の数値が得られます。
(λf. λx. x) (λx. x + 1) 0 = 0
(λf. λx. f x) (λx. x + 1) 0 = (λx. x + 1) 0 = 1
(λf. λx. f (f x)) (λx. x + 1) 0 = (λx. x + 1) 1 = 2
...
別の言い方をすると、そのような $f$ および $0$ を引数としてとると $n$ になるような関数を $n$ として扱います。
ペアとリスト
次にリストについてみていきたいと思います。
ラムダ計算では、一般的にリストを作るときはペアのネストで表します。
ペア(x,y)を表現しているのが以下の式です。
CONS := λx. λy. λf. f x y
CONS x y // (x,y)のペア
また、次のように定めます。
CAR := λp. p (λx. λy. x)
CDR := λp. p (λx. λy. y)
このように定義することによって、一つ目のデータと二つ目のデータを次のように取り出すことができます。
CAR (CONS x y) → x
CDR (CONS x y) → y
以下、簡単のため一つ目のデータをcar、二つ目のデータをcdrと呼称します。
リストを作る際には、ペアのcdrに新たなペアを入れていきます。
つまり、一般には(a_1, (a_2, (a_3, (..., (a_n, NIL)))))というような構造です。（NILは空リストを表す式を用途に合わせて定義します。例えばλx. λy. yとか）
（Lazy K の入出力では、終端記号として NIL ではなく EOF を表す 256 を使います。）
ここから、CARおよびCDRを使って中のデータを取得できるようになっています。
（他にもリストの作り方はいくつかありますが、Lazy Kではこの方法で行っているはずです）
チャーチ数の演算
チャーチ数は数値なので、加減乗除の演算ができないといけません。
演算についてみていきます。
加算
まずは加算から見ていきます。
その前に、数値 $n$ を受け取って $n+1$ を返す関数 SUCC (successor) について考えましょう。
満たすべきは SUCC(n) = n + 1 なので、数値のラムダ抽象の中の式を $f$ に適用すればよさそうです。
次の式は SUCC を表します。
SUCC := λn. λf. λx. f (n f x)
小さい数で試してみると、
SUCC 0 = λf. λx. f (0 f x)
= λf. λx. f x
SUCC 1 = λf. λx. f (1 f x)
= λf. λx. f (f x)
SUCC 2 = λf. λx. f (2 f x)
= λf. λx. f (f (f x))
で確かにできています。
これを用いて一般の加算 PLUS(m, n) を作ってみましょう。
数値 $m$ は $x$ に関数 $f$ を $m$ 回適用する関数でした。
つまり、 $x$ に $n$ 、$f$ に SUCC を適用すればいけそうです。
PLUS := λm. λn. m SUCC n
→α λm. λn. m (λn. λf. λx. f (n f x)) n
→β λm. λn. (λf. λx. f ... (f x)) (λn. λf. λx. f (n f x)) n
→β λm. λn. ((λn. λf. λx. f (n f x)) ... ((λn. λf. λx. f (n f x)) n))
→β λm. λn. ((λn. λf. λx. f (n f x)) ... (λf. λx. f (n f x)))
→→β
→β λm. λn. (λf. λx. (f ... (f (n f x))))
→β λm. λn. (λf. λx. m f (n f x))
= λm. λn. λf. λx. m f (n f x)
これがPLUSの定義になります。
乗算
乗算についてみていきます。
まず、 $m \times n$ を加算を使って表します。
すると、「$0$ に $n$ を $m$ 回足したもの」となります。
つまり、乗算MULTは、先のPLUSと同じように考えると(SUCCはPLUS 1と同じ)、
MULT := λm. λn. m (PLUS n) 0
→α λm. λn. m ((λn. λk. λf. λx. n f (k f x)) n) 0
→β λm. λn. m (λk. λf. λx. n f (k f x)) 0
= λm. λn. (λf. λx. f (f ... (f x))) (λk. λf. λx. n f (k f x)) 0
→β λm. λn. ((λk. λf. λx. n f (k f x)) ((λk. λf. λx. n f (k f x)) ... ((λk. λf. λx. n f (k f x))) 0))
→β λm. λn. ((λk. λf. λx. n f (k f x)) ((λk. λf. λx. n f (k f x)) ... (λk. λf. λx. n f x)))
→→β
→β λm. λn. (λf. λx. n f (n f ... (n f x)))
→β λm. λn. (λf. λx. m (n f) x)
= λm. λn. λf. λx. m (n f) x
となります。
場合によってはη変換（λx. E x →η E、実際に式を適用すれば同じである）を施してλm. λn. λf. m (n f)となっている場合もあります。
（補足）累乗
累乗も同様に定義できます。
POW := λm. λn. n (MULT m) 1
→α λm. λn. n (λk. λf. m (k f)) 1
→β λm. λn. ((λk. λf. m (k f)) ... ((λk. λf. m (k f)) 1))
→β λm. λn. ((λk. λf. m (k f)) ... (λf. m (λx. f x)))
→→β
→β λm. λn. (λf. m ... (m (λx. f x)))
→β λm. λn. (λf. n m (λx. f x))
→η λm. λn. (λf. n m f)
→η λm. λn. n m
減算
次に減算を考えます。
加算・乗算は「関数を何回適用するか」という観点で比較的そのまま定義できました。
一方で減算は、単純に「逆向きに適用する関数」を作ればよいわけではありません。
そこでまず、加算と同様に数値 $m$ を受け取って $m-1$ を返す関数 PRED（predecessor）を作り、それを繰り返すことで減算を定義します。
チャーチ数における PRED は、ペアを使うと作りやすくなります。
「状態」を (a,b) として、初期状態を (0,0) にし、1ステップごとに (a,b) -> (b, b+1) と更新します。
$n$ 回更新した結果は、$n>0$ なら (n-1, n)（$n=0$ なら (0,0)）になるので、先頭を取り出せば前者の場合に n-1 が得られます。
この更新関数をラムダ式で書くと、次のようになります（どうせ綺麗な形にはならないので、β簡約などはしません）。
STEP := λp. CONS (CDR p) (SUCC (CDR p))
よって、PREDは以下のようになります。
PRED := λn. CAR (n STEP (CONS 0 0))
ここで注意しなければならないのは、PRED 0 = 0となることです。
負の数は許されません。
PRED ができたので、$m - n$ は「m に PRED を n 回適用する」と考えられます。
SUB := λm. λn. n PRED m
これもPREDと同じく、$0$ 未満を許さない形になっています。
つまり、$m < n$ のときは $0$ になります。
SUB 5 2 = 3
SUB 3 3 = 0
SUB 2 5 = 0
除算...
次に除算、といきたいところですが、除算の定義はさらに難しくなるため、次回ということにさせてください。
終わりに
今回は、Lazy K の入出力仕様を入口にして、チャーチ数・ペア・リスト、そして基本演算（加算・乗算・減算）までを見てきました。
次回は、ラムダ計算のデータ構造をみていきたいと思います。