ラムダ計算をdartで実装してみた

## 概要

[ラムダ計算][1]をdart言語で実装してみました。
ラムダ計算自体の説明は、上記リンクのWikipedia記事や、こちらの[先駆者][2]の方の解説が詳しいので、そちらを参照してください。

## 自然数（チャーチ数）

まず、自然数（チャーチ数）は以下のように定義します。

```dart
// 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引数の関数になるので、以下のような関数を定義して、通常の自然数に変換します。

```dart
final lambda_to_int = (x) => x((x) => x + 1, 0);
```

以下のように記述すれば、チャーチ数から自然数の変換を確認できます。

```dart
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に記載されているラムダ式の表記で出力することもできます。

```dart
final h = (x) => x.length <= 1 ? 'f${x}' : 'f(${x})';
final lambda_to_str = (x) => "λfx.${x(h, 'x')}";
```

```dart
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))
```

## 後者関数

```dart
// SUCC := λn f x. f (n f x)
final SUCC = (n) => (f, x) => f(n(f, x));
```

```dart
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
```

## 足し算

```dart
// 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を利用した定義もあるので、こちらも実装しておきます。

```dart
// PLUS v2 : PLUS := λm n. m SUCC n
final PLUS = (m, n) => (f, x) => m(SUCC, n)(f, x);
```

```dart
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
```

## 掛け算

```dart
// 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を利用しないバージョンも定義されているので、こちらも実装しておきます。

```dart
// MULT v2 : MULT := λm n f. m (n f)
// (*) (n f)の部分はcurry化で対応
MULT(m, n) => (f, x) => m((v) => n(f, v), x);
```

```dart
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
 ```

## 前者関数

```dart
// 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を利用したバージョンも定義されているので、こちらも実装しておきます。

```dart
// 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);
```

```dart
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
```

## 論理値

```dart
// TRUE := λx y. x
final TRUE = (x, y) => x;
// FALSE := λx y. y
final FALSE = (x, y) => y;
```

自然数の場合と同様に、こちらもdart上の論理値に変換する以下の関数を定義しておきます。

```dart
final lambda_to_boolean = (x) => x(true, false);
```

```dart
print("[論理値]");
print("\tTRUE\t: ${lambda_to_boolean(TRUE)}");
print("\tFALSE\t: ${lambda_to_boolean(FALSE)}");
```

```
[論理値]
	TRUE	: true
	FALSE	: false
```

## 論理積(AND)

```dart
// AND := λp q. p q FALSE
final AND = (p, q) => p(q, FALSE);
```

```dart
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)

```dart
// OR := λp q. p TRUE q
final OR = (p, q) => p(TRUE, q);
```

```dart
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)

```dart
// NOT := λp. p FALSE TRUE
final NOT = (p) => p(FALSE, TRUE);
```

```dart
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)

```dart
// IFTHENELSE := λp x y. p x y
final IF_THEN_ELSE = (p) => (x, y) => p(x, y);
```

```dart
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)

```dart
// ISZERO := λn. n (λx. FALSE) TRUE
final IS_ZERO = (n) => n((x) => FALSE, TRUE);
```

```dart
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);
```

自然数（チャーチ数）のペアを自然数のペアに変換する関数を定義しておきます。

```dart
final lambda_pair_to_int_pair = (lambda_pair) =>
    lambda_pair((x, y) => (lambda_to_int(x), lambda_to_int(y)));
```

```dart
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][1]で、英語の[記事][3]が紹介されていたので、そちらを参考に定義しました。
ちなみに、以下の定義をせずとも、上記で定義したペアを入れ子的に利用することにより `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のリストとして表示するために、以下の関数を定義しておきます。

```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)}]";
```



```dart
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]には、下記の1行目の定義が書かれているのですが、dartでそのまま書くと無限自己参照になりプログラムが終了してしまいます。
そのため、最終的な定義には、無限自己参照を回避するための修正が入っています。

```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][1]に書かれている階乗の定義は以下になります。

```dart
// 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));
```

```dart
print("[階乗]");
print("\tFACT(3)\t : ${lambda_to_int(FACT(THREE))}");
```

```
[階乗]
	FACT(3)	 : 6
```

## まとめ

[Wikipedia][1]に書かれているラムダ式を一通り実装しました。
基本的にはラムダ式の表現(`λxy.xx`など)が読み取れれば、そこまで難しくなかったのですが、再帰で無限自己参照になってしまう件は、先駆者の[記事][2]を参照したり、ChatGPTへの質問してようやく解決しました。
他の数式（冪乗、剰余など）も実装できると思いますが、満足したので、これで終了とします。


[1]: https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
[2]: https://zenn.dev/openlogi/articles/introduction-to-lambda-calculus
[3]: https://en.wikipedia.org/wiki/Church_encoding#List_encodings