🧮

ラムダ計算入門

akabe

2023/12/20に公開

この記事は OPENLOGI Advent Calendar 2023 20日目の記事です。

ラムダ計算 (lambda calculus) は関数型プログラミング言語の基礎となる計算モデルです。計算モデルというと難しそうですが、本稿を読む上では「超シンプルなプログラミング言語」くらいに思ってもらえれば十分です。ラムダ計算にはいろいろな拡張や亜種がありますが、ここでは最も純粋なラムダ計算を扱います。このラムダ計算には変数と無名関数と関数の呼び出ししか構成要素がありません。恐るべきことに、数値などのリテラルや四則演算、制御構文などの普通のプログラミング言語が兼ね備えているような機能は直接的には備わっていません。しかし、工夫すると関数だけで全てを表現することができ、その計算能力はチューリングマシン完全であることが知られています。今日はこの面白さを伝えたいと思います。パズルや頭の体操みたいなノリで読んでください。

この記事では以下のような読者に向けてラムダ計算を解説します。

関数型プログラミングの基礎理論に興味がある。
何らかのプログラミング言語を使ってプログラムを書いたことがある。
再帰関数、無名関数やラムダ式を使ったことがある。

一方、ラムダ計算の応用事例や、ラムダ計算がチューリング完全であることの証明などについては触れません。本当にただただラムダ計算を説明するだけの記事です。

型なしラムダ計算

構文

ラムダ計算における式は以下の構文で定義されます。

e  ::=  x         (変数)
     |  λx. e     (ラムダ抽象)
     |  e1 e2     (関数適用)

構成要素は変数とラムダ抽象と関数適用の 3 つだけです。単に「ラムダ計算」といった場合は、本章によって定義されるラムダ計算を指すものと思ってください。

変数

x 以外に y でも foo でも（構文的に曖昧ではない範囲で）任意の文字列を使うことができます。

ラムダ抽象

ラムダ抽象 (lambda abstraction) は「引数を 1 つだけ受け取る無名関数」です。λx. e をいくつかのメジャーな言語で書くと、以下のようになります。

lambda x: e (Python)
(x) => e, function (x) { return e } (JavaScript, TypeScript)

ラムダ抽象の e には任意の式を書くことができ、e（の実行結果）が関数の返り値となります。ラムダ抽象は必ず引数を受け取らなければならず、必ず返り値を返さなければいけません。

複数の引数を受け取る場合は、λx. λy. e のように関数を返す関数として定義します。他の言語で書くと、

lambda x: lambda y: e (Python)
(x) => ((y) => e) (JavaScript, TypeScript)

となります。本稿では便宜上、上記のような関数を「2 つ引数を取る関数」と表現します。「関数を返す関数」だけでなく「関数を引数に取る関数」なども作ることができ、引数・戻り値には任意の関数・式を渡すことができます。

関数適用

関数適用 (application) は「関数の呼び出し」です。e1 e2 は多くのプログラミング言語では e1(e2) のように記述します。Haskell, OCaml などでは e1 e2 とそのまま表記しますね。e1 が呼び出す関数であり、e2 は実引数です。例えば、

(λx. x) y

という式は

(lambda x: x)(y) (Python)
((x) => x)(y) (JavaScript, TypeScript)

となります。

もう少し複雑な例も見てみましょう。

(λa. λb. a b) (λc. c) d

関数適用は左結合なので ((λa. λb. a b) (λc. c)) d と同じです。他の言語で書くと

(lambda a: lambda b: a(b))(lambda c: c)(d) (Python)
((a) => ((b) => b))((c) => c)(d) (JavaScript, TypeScript)

となります。

ベータ簡約

プログラミング言語を構成する重要な要素は二つあります。一つは構文 (syntax) であり、これは先ほど説明しました。もう一つは意味論 (semantics) と呼ばれる「プログラムの動作規則」です。構文だけだとプログラムは単なる記号の羅列ですが、意味論を定めることで処理を表現できるようになります。ラムダ計算の意味論の定め方はいろいろな流儀がありますが、ここでは式を「ステップ実行」するための規則を紹介します ^[1]。

式 e1 をステップ実行した結果、式 e1' になるとき e1 → e1' と表記します。ステップ実行により式が書き変わることで、ラムダ計算の動作を表現します。式の書き換えのことをベータ簡約 (beta reduction) と呼び、これ以降は単に簡約と書きます。

値呼び

本稿では基本的には、多くのプログラミング言語で一般的に採用されている値呼びをベースとした評価戦略を扱います ^[2]。簡約できる箇所は関数適用だけなので、関数適用だけを考えます。まず、一番基本的な簡約規則を見てみます。

(λx. e11) e2  →  [x ↦ e2] e11

この規則は (λx. e11) e2 という形の式が登場した場合、「e11 の中の自由変数 x を e2 で置き換えた式 ([x ↦ e2] e11)」に書き換えることを表しています。例えば、(λx. x x) (λy. y) という式に上記の規則を適用すると

   (λx. x x) (λy. y)
→  [x ↦ (λy. y)] (x x)
=  (λy. y) (λy. y)

と簡約できます。この規則は関数適用 e1 e2 のうち、e1 = λx. e11 かつ e2 がこれ以上簡約できない式である場合にのみ適用できます。部分式 e1, e2 が簡約できる場合は、左から順番に簡約していくことにします。正確に規則を書き下すと以下のようになります。

e1 → e1' という簡約が可能な時、e1 e2 → e1' e2
e1 がこれ以上簡約できず、e2 → e2' という簡約が可能な時、e1 e2 → e1 e2'
e2 がこれ以上簡約できない時、(λx. e11) e2 → [x ↦ e2] e11

上記の規則を踏まえると、

   (λa. a) (λb. b) ((λc. c) d)
   ^^^^^^^^^^^^^^^  まずは左の式を簡約
→  (λb. b) ((λc. c) d)
            ^^^^^^^^^  左の式がこれ以上できないので、右の式を簡約
→  (λb. b) d
   ^^^^^^^^^  右の式も簡約できなくなったので、最後に全体を簡約
→  d

というような簡約ができます。ここで、長い簡約を簡潔に書くため、1 ステップ以上の簡約は →→ と表記することにします。上記の簡約は

   ((λa. a) (λb. b)) ((λc. c) d)
→→ d

と一つにまとめて書けます。

ラムダ抽象内部の簡約

値呼びではラムダ抽象の中を簡約してはいけませんが、説明の都合上、以下のようにラムダ抽象の中身も必要に応じて簡約することにします ^[3]。

   λa. (λb. b) a c
       ^^^^^^^^^  必要であれば、ここを簡約して良い
→  λa. a c

ラムダ計算の特徴

ラムダ計算は純粋な関数型プログラミング言語で、変数に破壊的代入をすることはできません。関数の仮引数に実引数を束縛することはできるものの、既に値が決まった変数を後から変更する手段がありません。

また、他の多くのプログラミング言語とは異なり、式以外の構成要素が存在しません。言語仕様として、条件分岐やループなどの制御構文、数値や文字列などのリテラル、演算子が提供されていないことが、構文の定義からわかります。したがって、1 + 2 や x > y ? x : y のような記述は構文エラーとなります。しかし、工夫すると関数だけで条件分岐や自然数などに相当する機能を実現できます。次章からその具体的な方法を紹介します。

ブール値と条件分岐

ブール値

まずは、true と false に相当するような要素を関数を使って表現していきます。

TRUE  :=  λthn. λels. thn
FALSE :=  λthn. λels. els

TRUE, FALSE は 2 つ引数を受け取りますが、最初の引数は then 節の結果、2 つ目の引数は else 節の結果を受け取るためのものです。これらは単純なブール値に留まらず、条件分岐の機能を持っています。一般的なプログラミング言語にある三項演算子と比較すると以下のようになります。

三項演算子で書いた式	ラムダ計算での表現
`true ? e1 * e2`	`TRUE e1 e2`
`false ? e1 * e2`	`FALSE e1 e2`

条件分岐

このブール値は条件分岐の機能を持っているため、if 文は簡単にかけます。IF は条件文、then, else 節に対応する 3 つの引数を受け取る関数です。

IF  :=  λcond. λthn. λels. cond thn els

IF の引数として then, else を与えてしまうと、then, else 節の実行順序が変わってしまうのでは？と感じた人は鋭いですね。上記の IF は then, else 節を両方とも実行した後に条件分岐の処理が走るのに対して、一般的な条件分岐は条件分岐後に then, else 節を実行します。条件文によって、then, else 節のうちどちらかは実行されないため、例えば以下のようなプログラムもエラーなく実行されます。

if (true) {
  return 42;
} else {
  // 常にエラーになる処理
}

値呼びにおいて上記の振る舞いを実現するためには、IF に渡す then, else 節の式をラムダ抽象でラップすると良いです。こうすると、条件分岐の実行後に then, else 節が実行されるようになります。

(IF e1 (λx. e2) (λy. e3)) (λz. z)

※ x, y は e2, e3 に出現しない変数です。単に実行を遅延させる目的でラムダ抽象を挟んでいるので、引数は受け取った後捨てます。(λz. z) が実際に捨てられる実引数なので、（無限ループしない範囲で）好きな式を渡せます。

論理演算

ちなみに、AND, OR などの演算子も定義できます。

AND  :=  λx. λy. x y FALSE
OR   :=  λx. λy. x TRUE y
NOT  :=  λx. λy. x FALSE TRUE

試しに、AND の機能を確認してみましょう。

   AND FALSE TRUE
=  (λx. λy. x y FALSE) FALSE TRUE
   ^^^^^^^^^^^^^^^^^^^^^^^^^  x ↦ FALSE としてラムダ抽象に適用
→  (λy. FALSE y FALSE) TRUE
   ^^^^^^^^^^^^^^^^^^^^^^^^  y ↦ TRUE として適用
→  FALSE TRUE FALSE
=  (λx. λy. y) TRUE FALSE
   ^^^^^^^^^^^^^^^^  x ↦ TRUE として適用
→  (λy. y) FALSE
   ^^^^^^^^^^^^^  y ↦ FALSE として適用
→  FALSE

データ構造

二つ組

ブール値を応用して、二つの値を組にする関数を定義します。一番シンプルなデータ構造ですね。

PAIR    :=  λfst. λsnd. λbool. bool fst snd
FIRST   :=  λp. p TRUE    # 組 p の 1 つ目の要素を返す
SECOND  :=  λp. p FALSE   # 組 p の 2 つ目の要素を返す

PAIR は 3 つ引数をとり、先頭 2 つが組にする要素、最後の 1 つがブール値です。PAIR e1 e2 で定義した組に対して、TRUE を渡すと 1 つ目の要素が返り、FALSE を渡すと 2 つ目の要素が返ることを利用して、組を分解する関数 FIRST, SECOND を定義しています。

という形にエンコードすることを考えます。c, n は Lisp でお馴染み cons, nil を連想しますね。ただし、c, z は単純にリストを構築するオペレータという機能に留まらず、任意の値（関数）を当てはめられる点が異なります。まず、空リストに対応する NIL を

NIL  :=  λc. λn. n

と定めます。そして、リスト l の先頭に要素 x を追加したリストを返す関数 CONS は

CONS  :=  λx. λl. (λc. λn. c x (l c n))

と定義されます。CONS と NIL を使って、実際にリストが構成できるか試してみます。

   CONS a1 (CONS a2 (CONS a3 NIL))
=  CONS a1 (CONS a2 ((λx. λl. λc. λn. c x (l c n)) a3 NIL))
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  x ↦ a3, l ↦ NIL
→→ CONS a1 (CONS a2 (λc. λn. c a3 (NIL c n)))
                                   ^^^^^^^  NIL c n → n （ラムダ抽象の中を簡約）
→→ CONS a1 (CONS a2 (λc. λn. c a3 n))
=  CONS a1 ((λx. λl. λc. λn. c x (l c n)) a2 (λc'. λn'. c' a3 n'))
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
              x ↦ a2, l ↦ (λc'. λn'. c' a3 n') として適用
→→ CONS a1 (λc. λn. c a2 ((λc'. λn'. c' a3 n') c n))
                          ^^^^^^^^^^^^^^^^^^^^^^^^  c' ↦ c, n' ↦ n （ラムダ抽象の中を簡約）
→→ CONS a1 (λc. λn. c a2 (c a3 n))
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  同様に簡約
→→ λc. λn. c a1 (c a2 (c a3 n))

思った通りの形になりました。

実は c a1 (c a2 (c a3 n)) という形は、リストに対する畳み込み演算 (fold) に対応しています。OCaml では fold_right、Haskell では foldr という名前の関数です。例えば、OCaml を例にとると、

fold_right c [a1; a2; a3] n
= c a1 (c a2 (c a3 n))

というように、畳み込みの結果とリストの構造が対応するように定義しています。この後紹介するチャーチ数と組み合わせると、例えば自然数のリストの合計値を計算する関数は

SUM_OF_LIST  :=  λlst. lst PLUS C0

のように実装できます。リスト自体が畳み込みの機能を持っているため、fold のような専用関数を使わずに実現できます。

自然数

チャーチ数

ラムダ計算で自然数を表現する方法はいくつかあるみたいですが、ここではチャーチ数 (Church numerals) を紹介します。自然数 0, 1, 2, 3, ... に対応するチャーチ数は以下のように定義されます。

C0  :=  λs. λz. z
C1  :=  λs. λz. s z
C2  :=  λs. λz. s (s z)
C3  :=  λs. λz. s (s (s z))
...

チャーチ数は 2 つの引数 s, z を受け取る関数です。z は zero、s は successor（引数に +1 する関数）に対応しています。

C0 はゼロに対応するので、z をそのまま返す。
C1 は s z = 1 + 0 を返す。
C2 は s (s z) = 1 + 1 + 0 を返す。
...

というように、s を適用する回数により自然数が表現されています。

加算

これだけだと自然数っぽく見えないと思いますが、自然数の演算を定義していくことで、だんだんとチャーチ数が自然数に見えてくると思います。

まず、チャーチ数の加算は以下のように定義できます。

PLUS  :=  λm. λn. λs. λz. m s (n s z)

PLUS m n が m と n の和に対応するチャーチ数となります。上記の式にある n s z を簡約すると s が n 回出現するはずで、これに対してさらに s を m 回適用するため、結果として全体の s の個数は m + n 個になります。

試しに使ってみると、PLUS C3 C2 →→ C5 になることがわかります。

   PLUS C3 C2
=  (λm. λn.(λs. λz. m s (n s z)) C3 C2
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  m ↦ C3, n ↦ C2
→→ λs. λz. C3 s (C2 s z)
=  λs. λz. C3 s ((λs'. λz'. s' (s' z')) s z)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^  s' ↦ s, z' ↦ z
→→ λs. λz. C3 s (s (s z))
=  λs. λz. (λs'. λz'. s' (s' (s' z'))) s (s (s z))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   s' ↦ s, z' ↦ s (s z)
→→ λs. λz. λz'. s (s (s (s (s z))))
=  C5

後半に登場する以下の簡約がキモとなります。C3 の z' に s (s z) を束縛しているため、C3 に由来する 3 個の s に加え、C2 に由来する 2 個の s が組み合わさり、最終的に 5 個の s が出現しています。

   (λs'. λz'. s' (s' (s' z')))) s (s (s z))
             |----------------|   |------|
               sが3個 (C3由来)      sが2個 (C2由来)
→→ s (s (s (s (s z))))
  |-------||------|
  C3由来のs  C2由来のs

乗算

先程は、z に与える引数を工夫することで、加算を実現しました。乗算では s に与える引数を工夫し、「引数に n を足す関数を C0 に m 回適用する」ことで実現できます。

MULT  :=  λm. λn. m (PLUS n) C0

動作確認してみると、MULT C2 C3 →→ C6 となり正しく掛け算できていることがわかります。

   MULT C2 C3
=  (λm. λn. m (PLUS n) C0) C2 C3
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  m ↦ C2, n ↦ C3
→→ C2 (PLUS C3) C0
=  (λs. λz. s (s z)) (PLUS C3) C0
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  s ↦ PLUS C, z ↦ C0
→→ PLUS C3 (PLUS C3 C0)
   ^^^^^^^^^^^^^^^^^^^^  あとは PLUS の時と同様に簡約
→→ C6

減算

意外なことに、加算や乗算に比べると減算はとても複雑です。定義の仕方はいくつか流儀がありますが、ここではその一つを紹介します。まずは、自然数から 1 を引く関数を考えます。

\mathrm{PRED}(n) = \begin{cases} 0 & \hbox{if n = 0,} \\\\ n - 1 & \hbox{otherwise.} \end{cases}

この PRED は以下のように定義できます。

PRED  :=  λn. λf. λx. n (λg. λh. h (g f)) (λh. x) (λu. u)

導出過程の解説については、Derivation of predecessor function - Wikipedia をご覧ください。ここでは、簡単な動作確認に留めたいと思います。まず、簡約を見やすくするために、PRED の一部を別な関数として切り出します。

PRED  :=  λn. λf. λx. n INC CONST (λu. u)
INC   :=  λg. λh. h (g f)
CONST :=  λh. x

INC, CONST は PRED が受け取る減算対象のチャーチ数 n の引数 s, z に渡される関数です。例として PRED C3 の簡約を見てみると

   PRED C3
   ^^^^^^^  n ↦ C3
→  λf. λx. C3 INC CONST (λu. u)
=  λf. λx. (λs. λz. s (s (s z))) INC CONST (λu. u)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  s ↦ INC, z ↦ CONST
→→ λf. λx. INC (INC (INC CONST)) (λu. u)
                     ^^^^^^^^^  ここの簡約は以下参照

ここで、INC CONST の部分を簡約してみると、

   INC CONST
=  (λg. λh. h (g f)) (λu. x)
→  λh. h ((λh'. x) f)
→  λh. h x

と「関数を1つ受け取り x を適用して返す関数」になります。この結果を先ほどの PRED C3 の簡約に当てはめると

   PRED C3
→→ λf. λx. INC (INC (λh. h x)) (λu. u)
                ^^^^^^^^^^^^   ここの簡約は以下参照

です。次に INC (λh. h x) の部分を簡約すると、λh. h (f x) になり、「関数を1つ受け取り f x を適用して返す関数」になります。同様に簡約していくと、

   PRED C3
→→ λf. λx. INC (λh. h (f x)) (λu. u)
           ^^^^^^^^^^^^^^^^  ここを簡約すると λh. h (f (f x))
→→ λf. λx. (λh. h (f (f x))) (λu. u)
           ^^^^^^^^^^^^^^^^^^^^^^^^  ここを簡約すると f (f x)
→→ λf. λx. f (f x)
=  C2

というように PRED C3 →→ C2 であることが確認できました。INC (... (INC CONST)) の簡約がキモになっていて、常に INC の回数よりも 1 少ない数の f が簡約後に現れるようになっています。

簡約前	簡約後
`CONST`	`λh. x`
`INC CONST`	`λh. h x`
`INC (INC CONST)`	`λh. h (f x)`
`INC (INC (INC CONST))`	`λh. h (f (f x)`

この PRED を使うと、減算 MINUS は以下のようになります。

MINUS  :=  λm. λn. n PRED m

反復処理（再帰）

ここまでで、基本的なデータやデータ構造を構成し、条件分岐についても紹介しました。これらに加えて「繰り返し」を表現する手段があれば、いろいろな処理を記述できるようになります。

関数型プログラミングに馴染みのある人は再帰 (recursion) による反復処理が思いつくでしょう。再帰関数を使えば、引数 n を受け取り、0 から n までの自然数の和を返す関数は以下のように実装できます。

function mysum(n) {
    if (n == 0) {
        return 0;
    } else {
        return n + mysum(n - 1);
    }
}

愚直にラムダ計算に翻訳すると以下のような関数になります（IF の then, else 節をラムダ抽象でラップしていることに注意）。

MYSUM := λn. (
             IF (IS_ZERO n)                   # if (n == 0)
               (λx. C0)                       # return 0
               (λx. PLUS n (MYSUM (PRED n)))  # return n + mysum(n - 1)
           ) (λx. x)
IS_ZERO := λn. n (λx. FALSE) TRUE

しかし、このような定義はできません。ラムダ抽象は無名関数なので、定義右辺の MYSUM が未定義となります。したがって、自分自身を直接呼び出すような式は書けません。そこで、関数の定義中に登場する MYSUM を引数 f で置き換えます。

- MYSUM := λn. (
+ MYSUM1 := λf. λn. (
               IF (IS_ZERO n)               # if (n == 0)
                 (λx. C0)                   # return 0
-                (λx. PLUS n (MYSUM (PRED n)))  # return n + mysum(n - 1)
+                (λx. PLUS n (f (PRED n)))  # return n + f(n - 1)
             ) (λx. x)

f には「MYSUM のような関数」がどうにかして渡されることを期待しており、外部から自分自身を渡してもらう作戦です。この MYSUM1 に対して適切な f を渡し、最終的に MYSUM のような関数を生成するため、不動点コンビネータを定義します。

FIX  :=  λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

FIX を使うと、MYSUM は次のように定義できます。

MYSUM  :=  FIX MYSUM1

では、動作確認してみましょう。まず、MYSUM 関数だけを簡約してみます。

   MYSUM
=  FIX MYSUM1
→  (λx. MYSUM1 (λy. x x y)) (λx. MYSUM1 (λy. x x y))
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  x ↦ (λx. MYSUM1 (λy. x x y)
→  MYSUM1 (λy. (λx. MYSUM1 (λy'. x x y')) (λx. MYSUM1 (λy'. x x y')) y)
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                   ここは MYSUM の簡約結果と同じなので、MYSUM' とおく
=  MYSUM1 (λy. MYSUM' y)

MYSUM' は MYSUM を一回簡約した形の式であるため、MYSUM とほぼ同じものだと思ってもらって大丈夫です。MYSUM を簡約することで、再び MYSUM と同様の式 MYSUM' が現れるところが興味深いですね。もともと MYSUM1 の引数 f に渡したかった「自分自身」に相当する MYSUM' を渡せていることがわかります。

ここで、実際に値を渡して計算結果が合っているか確認します。MYSUM C3 を簡約すると

   MYSUM C3
→→ MYSUM1 (λy. MYSUM' y) C3
   ^^^^^^^^^^^^^^^^^^^^^^^^
     f ↦ (λy. MYSUM' y), n ↦ C3 として MYSUM1 に適用した後、
     頑張って簡約すると以下の形になります。
→→ PLUS C3 ((λy. MYSUM' y) (PRED C3))
                           ^^^^^^^^^  PRED C3 → C2
→→ PLUS C3 ((λy. MYSUM' y) C2)
            ^^^^^^^^^^^^^^^^^  y ↦ C2
→  PLUS C3 (MYSUM' C2)

となり 3 + mysum(2) に対応する式が出現します。あとはこれを繰り返していけば、PLUS C3 (PLUS C2 (PLUS C1 C0) となり、3 + 2 + 1 + 0 の計算が行われることが確認できます。

おまけ：JavaScript で実験

本稿で紹介した要素を JavaScript で演算を動かしてみましょう ^[4]。ブラウザの開発者コンソールを使って試してください。JavaScript 以外で試しても良いですが、動的型付きプログラミング言語をお勧めします。型システムの表現力次第ですが、静的型付きプログラミング言語だと型検査に引っかかる恐れがあります。

まず、チャーチ数は以下のように実装できます。

C0 = (s) => (z) => z;          // λs. λz. z
C1 = (s) => (z) => s(z);       // λs. λz. s z
C2 = (s) => (z) => s(s(z));    // λs. λz. s (s z)
C3 = (s) => (z) => s(s(s(z))); // λs. λz. s (s (s z))

そして、PLUS は次のように定義できます。

PLUS = (m) => (n) => (s) => (z) => m(s)(n(s)(z)); // λm. λn. (λs. λz. m s (n s z))

PLUS(C2)(C3) の結果は C5 になるはずですが、関数の中身を確認するのは難しいです。そこで、s に (x) => x + 1、z に 0 を与えて JavaScript の整数に変換してみます。

Y = PLUS(C2)(C3);  // C5 になるはず
Y((x) => x + 1)(0);
//>> 5

ちゃんと、想定した結果が返ってきましたね。次に、トリッキーな定義だった PRED を動かしてみましょう。

// PRED := λn. λf. λx. n (λg. λh. h (g f)) (λh. x) (λu. u)
PRED  = (n) => (f) => (x) => n((g) => (h) => h(g(f)))((h) => x)((u) => u);
PRED(C3)((x) => x + 1)(0);  // C2 になるはず
//>> 2

おお、素晴らしい！ちゃんと -1 できています。

では、最後に FIX により反復処理が実装できているか確認してみます。まずは、MYSUM1 を定義します。

TRUE  = (x) => (y) => x; // λx. λy. x
FALSE = (x) => (y) => y; // λx. λy. y
IF    = (cond) => (thn) => (els) => cond(thn)(els); // λcond. λthn. λels. cond thn els
IS_ZERO = (n) => n((x) => FALSE)(TRUE); // λn. n (λx. FALSE) TRUE
MYSUM1 = (f) => (n) => (
              IF(IS_ZERO(n))
                ((x) => C0)
                ((x) => PLUS(n)(f(PRED(n))))
            )((x) => x);

次に FIX を定義して、MYSUM を作ります。

// FIX := λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
FIX = (f) => ((x) => f((y) => x(x)(y)))((x) => f((y) => x(x)(y)));
MYSUM = FIX(MYSUM1);

MYSUM(C3) を実行すると、ちゃんと C6 になっていることが確認できました！すごい！

MYSUM(C3)((x) => x + 1)(0);  // C0 + C1 + C2 + C3 = C6 になるはず
//>> 6

まとめ

ラムダ計算の構文・意味論を定義した後、ブール値や自然数のほか、条件分岐や反復処理を実装する方法を紹介しました。多くのプログラミング言語において、これらの要素はリテラルや制御構文として予め言語仕様に組み込まれた形で提供されます。しかし、ラムダ計算では関数だけでこれらの機能を実現できるため、言語仕様に含める必要がなく「糖衣構文 (syntax sugar)」として実装することができます。関数が最もプリミティブな要素で、関数だけであらゆるものを実装できるという発想はとても興味深いと個人的には思っています。本稿を読んでラムダ計算に興味を持っていただければ幸いです。

なお、この記事は型システム入門 −プログラミング言語と型の理論−を参考に執筆しました。

脚注

専門的にはステップ実行により意味論を定義していくスタイルを small-step 操作的意味論と言います。 ↩︎
値呼びの特徴は実引数を関数に渡す前に実行することです。関数に実行前の実引数を渡して、必要になった時に実行する「名前呼び」や「必要呼び」などの評価戦略もあります。 ↩︎
ラムダ抽象の中身を含む、簡約可能なあらゆる場所を好きな順序で簡約して良い「完全ベータ簡約」という戦略もあります。 ↩︎
この用途で JavaScript を使うことが適切かわかりませんが、誰でも実行環境を持っていて、ユーザーが多そうな言語を選んでいます。 ↩︎

OPENLOGI Tech BlogPublication

私たちは身近な社会課題である物流の未来を変えるべく、「物流版AWS」をコンセプトとしたプラットフォームの開発、データの活用によって、業界全体の最適化を目指す会社です。

Discussion

1e0nhard96

はじめまして。

   (λa. a) (λb. b) ((λc. c) d)
   ^^^^^^^^^^^^^^^  まずは左の式を簡約
→  (λb. b) ((λc. c) d)
            ^^^^^^^^^  左の式がこれ以上できないので、右の式を簡約
→  (λc. c) d
   ^^^^^^^^^  右の式も簡約できなくなったので、最後に全体を簡約
→  d

と記載がありますが

   (λa. a) (λb. b) ((λc. c) d)
   ^^^^^^^^^^^^^^^  まずは左の式を簡約
→  (λb. b) ((λc. c) d)
            ^^^^^^^^^  左の式がこれ以上できないので、右の式を簡約
→  (λb. b) d
   ^^^^^^^^^  右の式も簡約できなくなったので、最後に全体を簡約
→  d

ではないでしょうか？間違っていたらすみません。

akabe

おっしゃる通りですね。ご指摘ありがとうございます。後ほど修正します。