自然数

Tuber には 0, 1, 2, …, 20 があらかじめ定義されています。
とはいえラムダ計算にはいわゆる 数 というものは存在しません。ラムダ計算の構成要素は 変数, 関数適用, ラムダ抽象 のみです。Tuber における自然数もとあるラムダ式に名前をつけたものにすぎません。

0

関数 0 の定義は下記のようになっています。

0 = (f, x) => x

引数 f, x に対して x を返すラムダ抽象に 0 という名前を付けて参照可能にしたものです。
「x に対して f を 0 回適用した式」をもって自然数の 0 を表現しています。

1

関数 1 の定義は下記のようになっています。

1 = (f, x) => f(x)

「x に対して f を 1 回適用した式」をもって自然数の 1 を表現しています。

2

関数 2 の定義は下記のようになっています。

1 = (f, x) => f(f(x))

「x に対して f を 2 回適用した式」をもって自然数の 2 を表現しています。

3 ~ 20

関数 3, 関数 4, …, 関数 20 も同様に定義されています。

自然数の演算

繰り返しになりますが 0, 1, 2, …, 20 はただの関数にすぎません。
これらの関数を自然数たらしめているのは、それぞれの関数同士の演算です。

Tuber には下記の自然数演算が組み込みで用意されています。

• 次の数: SUCC
• 前の数: PRED
• 加算: ADD
• 減算: SUB
• 積算: MUL
• 乗算: POW
• 商算: DIV

その他、 比較演算 も用意されています。

次の数 SUCC

SUCC は引数 n の次の数を返します。

EQ(SUCC(3), 4)  # => TRUE

前の数 PRED

PRED は引数 n の前の数を返します。

EQ(PRED(3), 2)  # => TRUE

ただし PRED(0) を評価すると 0 が返ります。

IS_ZERO(PRED(0))  # => TRUE

加算 ADD

ADD は引数 m, n の和を返します。

EQ(ADD(3, 2), 5)  # => TRUE

減算 SUB

SUB は引数 m, n の差を返します。

EQ(SUB(3, 2), 1)  # => TRUE

n が m よりも大きい場合 SUB(m, n) を評価すると 0 が返ります。

IS_ZERO(SUB(2, 3))  # => TRUE

積算 MUL

MUL は引数 m, n の積を返します。

EQ(MUL(3, 2), 6)  # => TRUE

乗算 POW

POW は引数 m, n に対して m を n 乗した値を返します。

EQ(POW(3, 2), 9)  # => TRUE

商算: DIV

DIV は引数 m, n に対して m を n で割ったときの商と余りを返します。
商と余りは CONS で組になっています。逆に、結果の値から CAR, CDR を使って商と余りをそれぞれ取り出すことができます。

DIV(11, 4)  # CONS(2, 3) と同等の値が返る

CAR(DIV(11, 4))  # 商を計算し、2 と同等の値が返る
CDR(DIV(11, 4))  # 余りを計算し、3 と同等の値が返る