概要
ラムダ計算をdart言語で実装してみました。
ラムダ計算自体の説明は、上記リンクのWikipedia記事や、こちらの先駆者の方の解説が詳しいので、そちらを参照してください。
自然数（チャーチ数）
まず、自然数（チャーチ数）は以下のように定義します。
// 0 := λf x. x
final ZERO = (f, x) => x;
// 1 := λf x. f x
final ONE = (f, x) => f(x);
// 2 := λf x. f (f x)
final TWO = (f, x) => f(f(x));
// 3 := λf x. f (f (f x))
final THREE = (f, x) => f(f(f(x)));
ラムダ計算の自然数（チャーチ数と言う）は、通常の自然数ではなく、2引数の関数になるので、以下のような関数を定義して、通常の自然数に変換します。
final lambda_to_int = (x) => x((x) => x + 1, 0);
以下のように記述すれば、チャーチ数から自然数の変換を確認できます。
print("[自然数(チャーチ数)] 自然数表示");
print("\tZERO\t: ${lambda_to_int(ZERO)}");
print("\tONE\t: ${lambda_to_int(ONE)}");
print("\tTWO\t: ${lambda_to_int(TWO)}");
print("\tTHREE\t: ${lambda_to_int(THREE)}");
[自然数(チャーチ数)] 自然数表示
ZERO : 0
ONE : 1
TWO : 2
THREE : 3
また、以下のような関数を用意すれば、Wikipediaに記載されているラムダ式の表記で出力することもできます。
final h = (x) => x.length <= 1 ? 'f${x}' : 'f(${x})';
final lambda_to_str = (x) => "λfx.${x(h, 'x')}";
print("[自然数(チャーチ数)] ラムダ式表示");
print("\tZERO\t: ${lambda_to_str(ZERO)}");
print("\tONE\t: ${lambda_to_str(ONE)}");
print("\tTWO\t: ${lambda_to_str(TWO)}");
print("\tTHREE\t: ${lambda_to_str(THREE)}");
実行すると、以下のようになります。
[自然数(チャーチ数)] ラムダ式表示
ZERO : λfx.x
ONE : λfx.fx
TWO : λfx.f(fx)
THREE : λfx.f(f(fx))
後者関数
// SUCC := λn f x. f (n f x)
final SUCC = (n) => (f, x) => f(n(f, x));
print("[後者関数]");
print("\tSUCC ZERO\t: ${lambda_to_int(SUCC(ZERO))}");
print("\tSUCC ONE\t: ${lambda_to_int(SUCC(ONE))}");
print("\tSUCC TWO\t: ${lambda_to_int(SUCC(TWO))}");
print("\tSUCC THREE\t: ${lambda_to_int(SUCC(THREE))}");
[後者関数]
SUCC ZERO : 1
SUCC ONE : 2
SUCC TWO : 3
SUCC THREE : 4
足し算
// PLUS v1 : PLUS := λm n f x. m f (n f x)
final PLUS = (m, n) => (f, x) => m(f, n(f, x));
Wikipedia上には、以下のようにSUCCを利用した定義もあるので、こちらも実装しておきます。
// PLUS v2 : PLUS := λm n. m SUCC n
final PLUS = (m, n) => (f, x) => m(SUCC, n)(f, x);
print("[足し算]");
print("\tPLUS ONE TWO\t: ${lambda_to_int(PLUS(ONE, TWO))}");
print("\tPLUS TWO THREE\t: ${lambda_to_int(PLUS(TWO, THREE))}");
[足し算]
PLUS ONE TWO : 3
PLUS TWO THREE : 5
掛け算
// MULT v1 : MULT := λm n. m (PLUS n) 0
// (*) (PLUS n)の部分はcurry化で対応
final MULT = (m, n) => (f, x) => m((v) => PLUS(n, v), ZERO)(f, x);
Wikipedia上には、PLUSを利用しないバージョンも定義されているので、こちらも実装しておきます。
// MULT v2 : MULT := λm n f. m (n f)
// (*) (n f)の部分はcurry化で対応
MULT(m, n) => (f, x) => m((v) => n(f, v), x);
print("[掛け算]");
print("\tMULT TWO ZERO\t: ${lambda_to_int(MULT(TWO, ZERO))}");
print("\tMULT TWO THREE\t: ${lambda_to_int(MULT(TWO, THREE))}");
[掛け算]
MULT TWO ZERO : 0
MULT TWO THREE : 6
前者関数
// PRED v1 : PRED := λn f x. n (λg h. h (g f)) (λu. x) (λu. u)
final PRED = (n) => (f, x) => n((g) => (h) => h(g(f)), (u) => x)((u) => u);
Wikipedia上には、PLUSを利用したバージョンも定義されているので、こちらも実装しておきます。
// PRED v2 : PRED := λn. n (λg k. (g 1) (λu. PLUS (g k) 1) k) (λv. 0) 0
final PRED = (n) => (f, x) =>
n((g) => (k) => g(ONE)((u) => PLUS(g(k), ONE), k), (v) => ZERO)(ZERO)(f, x);
print("[前者関数]");
print("\tPRED ZERO\t: ${lambda_to_int(PRED(ZERO))}");
print("\tPRED ONE\t: ${lambda_to_int(PRED(ONE))}");
print("\tPRED TWO\t: ${lambda_to_int(PRED(TWO))}");
print("\tPRED THREE\t: ${lambda_to_int(PRED(THREE))}");
[前者関数]
PRED ZERO : 0
PRED ONE : 0
PRED TWO : 1
PRED THREE : 2
論理値
// TRUE := λx y. x
final TRUE = (x, y) => x;
// FALSE := λx y. y
final FALSE = (x, y) => y;
自然数の場合と同様に、こちらもdart上の論理値に変換する以下の関数を定義しておきます。
final lambda_to_boolean = (x) => x(true, false);
print("[論理値]");
print("\tTRUE\t: ${lambda_to_boolean(TRUE)}");
print("\tFALSE\t: ${lambda_to_boolean(FALSE)}");
[論理値]
TRUE : true
FALSE : false
論理積(AND)
// AND := λp q. p q FALSE
final AND = (p, q) => p(q, FALSE);
print("[AND]");
print("\tAND FALSE FALSE\t: ${lambda_to_boolean(AND(FALSE, FALSE))}");
print("\tAND FALSE TRUE\t: ${lambda_to_boolean(AND(FALSE, TRUE))}");
print("\tAND TRUE FALSE\t: ${lambda_to_boolean(AND(TRUE, FALSE))}");
print("\tAND TRUE TRUE\t: ${lambda_to_boolean(AND(TRUE, TRUE))}");
[AND]
AND FALSE FALSE : false
AND FALSE TRUE : false
AND TRUE FALSE : false
AND TRUE TRUE : true
論理和(OR)
// OR := λp q. p TRUE q
final OR = (p, q) => p(TRUE, q);
print("[OR]");
print("\tOR FALSE FALSE\t: ${lambda_to_boolean(OR(FALSE, FALSE))}");
print("\tOR FALSE TRUE\t: ${lambda_to_boolean(OR(FALSE, TRUE))}");
print("\tOR TRUE FALSE\t: ${lambda_to_boolean(OR(TRUE, FALSE))}");
print("\tOR TRUE TRUE\t: ${lambda_to_boolean(OR(TRUE, TRUE))}");
[OR]
OR FALSE FALSE : false
OR FALSE TRUE : true
OR TRUE FALSE : true
OR TRUE TRUE : true
否定(NOT)
// NOT := λp. p FALSE TRUE
final NOT = (p) => p(FALSE, TRUE);
print("[NOT]");
print("\tNOT FALSE\t: ${lambda_to_boolean(NOT(FALSE))}");
print("\tNOT TRUE\t: ${lambda_to_boolean(NOT(TRUE))}");
[NOT]
NOT FALSE : true
NOT TRUE : false
条件式(IF_THEN_ELSE)
// IFTHENELSE := λp x y. p x y
final IF_THEN_ELSE = (p) => (x, y) => p(x, y);
print("[IF_THEN_ELSE]");
print("\tIF TRUE THEN 'then' ELSE 'else' : ${IF_THEN_ELSE(TRUE)("then", "else")}");
print("\tIF FALSE THEN 'then' ELSE 'else' : ${IF_THEN_ELSE(FALSE)("then", "else")}");
[IF_THEN_ELSE]
IF TRUE THEN 'then' ELSE 'else' : then
IF FALSE THEN 'then' ELSE 'else' : else
ゼロ判定(IS_ZERO)
// ISZERO := λn. n (λx. FALSE) TRUE
final IS_ZERO = (n) => n((x) => FALSE, TRUE);
print("[IS_ZERO]");
print("\tIS_ZERO ZERO : ${lambda_to_boolean(IS_ZERO(ZERO))}");
print("\tIS_ZERO ONE : ${lambda_to_boolean(IS_ZERO(ONE))}");
print("\tIS_ZERO TWO : ${lambda_to_boolean(IS_ZERO(TWO))}");
[IS_ZERO]
IS_ZERO ZERO : true
IS_ZERO ONE : false
IS_ZERO TWO : false
ペア
Lispでおなじみのペア(CONS)を実装します。
CARは1番目の要素、CDRは2番目の要素を返す関数になります。
// CONS := λs b f. f s b
final CONS = (s, b) => (f) => f(s, b);
// CAR := λp. p TRUE
final CAR = (p) => p(TRUE);
// CDR := λp. p FALSE
final CDR = (p) => p(FALSE);
自然数（チャーチ数）のペアを自然数のペアに変換する関数を定義しておきます。
final lambda_pair_to_int_pair = (lambda_pair) =>
lambda_pair((x, y) => (lambda_to_int(x), lambda_to_int(y)));
print("[ペア]");
print("\t(ZERO, ONE)\t : ${lambda_pair_to_int_pair(CONS(ZERO, ONE))}");
print("\tCAR (ZERO, ONE)\t : ${lambda_to_int(CAR(CONS(ZERO, ONE)))}");
print("\tCDR (ZERO, ONE)\t : ${lambda_to_int(CDR(CONS(ZERO, ONE)))}");
[ペア]
(ZERO, ONE) : (0, 1)
CAR (ZERO, ONE) : 0
CDR (ZERO, ONE) : 1
リスト
Wikipediaで、英語の記事が紹介されていたので、そちらを参考に定義しました。
ちなみに、以下の定義をせずとも、上記で定義したペアを入れ子的に利用することにより CONS (2 (CONS 1 NIL))のような感じでリストを生成することが可能です。
| ラムダ式 | 説明 |
|---|---|
| NIL | 空リスト |
| IS_NIL | リストが空かどうかを判定 |
| LCONS | ペア |
| HEAD | 先頭要素の取得 |
| TAIL | 先頭以外の要素を取得 |
// NIL := λc n. n
final NIL = (c, n) => n;
// IS_NIL := λl. l (λh t. FALSE) TRUE
final IS_NIL = (l) => l(((h, t) => FALSE), TRUE);
// LCONS := λh t c n. c h t
final LCONS = (h, t) => (c, n) => c(h, t);
// HEAD := λl. l (λh t. h) FALSE
final HEAD = (l) => l((h, t) => h, NIL);
// TAIL := λl. l (λh t. t) NIL
final TAIL = (l) => l((h, t) => t, NIL);
ラムダ式のリストをdartのリストとして表示するために、以下の関数を定義しておきます。
String _lambda_to_list_loop(x) {
if (lambda_to_boolean(IS_NIL(x))) {
return "";
}
final head = HEAD(x);
final tail = TAIL(x);
if (lambda_to_boolean(IS_NIL(tail))) {
return "${lambda_to_int(head)}";
}
return "${lambda_to_int(head)}, " + "${_lambda_to_list_loop(tail)}";
}
final lambda_to_list = (x) => "[${_lambda_to_list_loop(x)}]";
print("[リスト]");
print("\tNIL\t\t\t\t : ${lambda_to_list(NIL)}");
print("\t(ZERO, NIL)\t\t\t : ${lambda_to_list(LCONS(ZERO, NIL))}");
print("\t(ONE, (ZERO, NIL))\t\t : ${lambda_to_list(LCONS(ONE, LCONS(ZERO, NIL)))}");
print("\t(TWO, (ONE, (ZERO, NIL)))\t : ${lambda_to_list(LCONS(TWO, LCONS(ONE, LCONS(ZERO, NIL))))}");
print("\tIS_NIL NIL\t\t\t : ${lambda_to_boolean(IS_NIL(NIL))}");
print("\tIS_NIL (ZERO, NIL)\t\t : ${lambda_to_boolean(IS_NIL(LCONS(ZERO, NIL)))}");
print("\tHEAD (THREE, (ONE, NIL))\t : ${lambda_to_int(HEAD(LCONS(THREE, LCONS(ONE, NIL))))}");
print("\tTAIL (ZERO, (ONE, NIL))\t\t : ${lambda_to_list(TAIL(LCONS(ZERO, LCONS(ONE, NIL))))}");
print("\tHEAD (TAIL (ZERO, (ONE, NIL)))\t : ${lambda_to_int(HEAD(TAIL(LCONS(ZERO, LCONS(ONE, NIL)))))}");
[リスト]
NIL : []
(ZERO, NIL) : [0]
(ONE, (ZERO, NIL)) : [1, 0]
(TWO, (ONE, (ZERO, NIL))) : [2, 1, 0]
IS_NIL NIL : true
IS_NIL (ZERO, NIL) : false
HEAD (THREE, (ONE, NIL)) : 3
TAIL (ZERO, (ONE, NIL)) : [1]
HEAD (TAIL (ZERO, (ONE, NIL))) : 1
再帰
まずYコンビネータの定義を行います。
Wikipediaには、下記の1行目の定義が書かれているのですが、dartでそのまま書くと無限自己参照になりプログラムが終了してしまいます。
そのため、最終的な定義には、無限自己参照を回避するための修正が入っています。
// Y := λg. (λx. g (x x)) (λx. g (x x))
// 愚直に書くと以下のようになるが、無限自己参照になってしまう
// final Y = (g) => ((x) => g(x(x)))((x) => g(x(x)));
// そのため以下のように記述する
final Y = (g) => ((x) => g((y) => x(x)(y)))((x) => g((y) => x(x)(y)));
Wikipediaに書かれている階乗の定義は以下になります。
// final FIX = (f) => ((x) => f((y) => x(x)(y)))((x) => f((y) => x(x)(y)));
// FACT : g := λf n. (1, if n = 0; and n × f(n − 1), if n > 0)
final FACT = Y((f) => (n) =>
IF_THEN_ELSE(IS_ZERO(n))((x) => ONE, (x) => MULT(n, f(PRED(n))))((x) => x));
print("[階乗]");
print("\tFACT(3)\t : ${lambda_to_int(FACT(THREE))}");
[階乗]
FACT(3) : 6
まとめ
Wikipediaに書かれているラムダ式を一通り実装しました。
基本的にはラムダ式の表現(λxy.xxなど)が読み取れれば、そこまで難しくなかったのですが、再帰で無限自己参照になってしまう件は、先駆者の記事を参照したり、ChatGPTへの質問してようやく解決しました。
他の数式（冪乗、剰余など）も実装できると思いますが、満足したので、これで終了とします。