自作ラムダ計算インタプリタで階乗を計算する

この記事は、CAMPHOR- Advent Calendar 2021 の 15 日目の記事です。

ラムダ計算とは、関数定義と関数の適用からなるプログラミング言語で、チューリング完全な計算モデルです。以前ラムダ計算のインタプリタを OCaml で実装しました。この記事ではそのインタプリタで n の階乗を求めるまでの道のりを書きます。

実装したインタプリタは以下にあります。

https://github.com/atrn0/lambda

動機

僕が所属している研究室では、B4 の前期にTypes and Programming Languagesの輪読と数学演習、OCaml と Coq の演習をやります。OCaml 演習では基本的に B3 でやるインタプリタ実験の続きをやります。

OCaml 演習は，実験 3SW の続きをやってみてください． ... あとは，OCaml で面白いソフトウェア（できれば言語処理系？）を実装してみるのもよいかもしれません．

プログラミング言語処理系という授業を落として再履修していた僕は、この授業の課題としてインタプリタ実験の続きはどうせやるので、「面白いソフトウェア（できれば言語処理系？）」も実装することにしました。題材の言語は、TaPL の輪講でちょうど読んでいて、性質が面白いかつ処理系の実装が簡単そうな型無しラムダ計算を選びました。

(型無し)ラムダ計算

複雑なプログラミング言語が、その本質的な仕組みを表現できる核となる計算モデルと、その核に変換される派生形式の集まりとして定式化できるという考え方があります。その一つの計算モデルがラムダ計算で、Lisp, Scheme, ML などの言語の核となる計算モデルです。他にも$\pi$計算やオブジェクト計算などの計算モデルがあり、それぞれメッセージベースの並行処理言語、オブジェクト指向言語の核となる機能を持っています。これらの計算モデルはそれ自体で計算が記述できる単純なプログラミング言語であるのと同時に、数学的対象としてもみなせるので、一般的なプログラミング言語の仕様の記述や、設計、実装、研究において広く使われています。

ラムダ計算では全ての計算が関数の定義と適用に帰着されます。実装したインタプリタで扱える型無しラムダ計算の文法と意味論(プログラムがどう評価されるか)を見ていきます。

文法(シンタックス)

プログラムの文法は以下です。

t ::=
  | x     (変数)
  | \x. t (関数定義)
  | t t   (関数適用)

これは BNF 風の記法で書いていて、tはxまたは\x. tまたはt tであるという意味です。右辺のtは左辺のtで、関数定義のxは任意の変数で置き換えることができます。それと、カッコは適当につけることができます。

例えば、以下のようなプログラムが許容されます。

• y: 1 つの変数 y
• \y. y: y を引数として受け取り、y を返す関数(恒等関数)
• f x: 引数 x を関数 f に適用する
• \x. f x: x を引数として受け取り、f に適用して返す関数
• \x. (\x. x) x: x を引数として受け取り、恒等関数に適用して返す関数

このように、基本的に関数の定義と適用のみを使ってプログラムを書きます。

また、関数適用は左結合で、関数適用は関数定義より優先されます。つまり、

• x y zというプログラムは(x y) zと等価 (左結合)
• \x. y zというプログラムは(\x. y) zではなく\x. (y z)と等価 (関数適用を優先)

とします。

意味論(セマンティクス)

次に、プログラムとして入力した文字列がインタプリタにどのように評価(解釈)されるかを決める必要があります。

ラムダ計算では、「(\x. s) t という形が来たら、s の中に出てくる x を t で置き換える」(ベータ簡約) という方針でプログラムを変換します。この変換によってプログラムが評価、計算されます。例えば、プログラムは以下のように変換されます。

(\x.x) ((\x.x) (\z. (\x.x) z))
→ (\x. x) (\z. ((\x. x) z))
→ \z. ((\x. x) z)
→ \z. z

実装したインタプリタでは、(\x. s) t という形がなくなるまでこの操作を繰り返すことにします。

計算の例

ここまででプログラミング言語を定義することができました。この言語を使って早速プログラムを書いて実行したいところですが、この言語には数値、算術演算、条件式、レコード、ループ、列など、一般的な言語に備わっていそうな機能は何もありません 🥺。ないものは仕方ないので、今の言語機能でなんとかすることにします。

とりあえず n の階乗を求めることを目標にします。n の階乗を求める関数は、例えば C だと以下のように書けます。

int f(int n) {
  return n == 0 ? 1 : f(n - 1) * n;
}

n の階乗を求めるために必要そうな要素は、

• 条件分岐
• 数
• 乗算
• 再帰演算

などです。1 つずつ作っていきます。

条件分岐

まず、条件分岐をするためにブール値が欲しいです。trueやfalseというプリミティブな定数はないので、代わりにこれらを関数にエンコードします。

true  = \t. \f. t
false = \t. \f. f

trueは 2 つの引数を受け取って 1 つ目の引数を返す関数、falseは 2 つ目の引数を返す関数です。(複数引数の関数はカリー化によって高階関数に変換します。) このようにエンコードすると、条件分岐は以下のように書けます。

test = \l. \m. \n. l m n

testは 3 つの引数 l, m, n を受け取って、l がtrueのとき m を、falseのとき n を返す関数です。

例えば、test true x yというプログラムは、

= (\l. \m. \n. l m n) (\t. \f. t) x y
→ (\m. \n. (\t. \f. t) m n) x y
→ (\n. (\t. \f. t) x n) y
→ ((\t. \f. t) x) y
→ (\f. x) y
→ x

と評価され、確かに x になります。

数

次に数をエンコードします。

0 = \s. \z. z
1 = \s. \z. s z
2 = \s. \z. s (s z)
3 = \s. \z. s (s (s z))
...

このように、自然数 n は 2 つの引数 s, z を受け取り、s を z に n 回適用する関数として表します。このエンコード方法はチャーチ数と呼ばれます。

この数を使うと、例えば加算、乗算は

plus = \m. \n. \s. \z. m s (n s z)
times = \m. \n. m (plus n) 0

と書けます。

再帰演算

再帰演算は不動点コンビネータと呼ばれる関数を使って行います。不動点コンビネータとは、ラムダ計算の過程でfix g → g (fix g)と変換されるような関数fixのことです。

例えば、f = \n. f nのような再帰関数を使った演算は、引数にfをとる関数 g を使って以下のように行うことができます。

g = \f. \n. f n
(fix g) i
→ g (fix g) i
= (\f. \n. f n) (fix g) i
→ (\n. (fix g) n) i
...

このように、(fix g)が再帰的に関数内に現れるように変換できます。

階乗の計算

以上のように、一般的な言語に備わっている機能をラムダ計算にエンコードすることができます。実装したインタプリタでは、階乗の計算を行うために以下のようなマクロを定義しています。

let initial_env = Environment.from_list [
  ("test", parse "λl. λm. λn. l m n");
  ("tru", parse "λt. λf. t");
  ("fls", parse "λt. λf. f");
  ("iszro", parse "λm. m (λx. fls) tru");
  ("c0", parse "λs. λz. z");
  ("c1", parse "λs. λz. s z");
  ("plus", parse "λm. λn. λs. λz. m s (n s z)");
  ("times", parse "λm. λn. m (plus n) c0");
  ("pair", parse "λf. λs. λb. b f s");
  ("fst", parse "λp. p tru");
  ("snd", parse "λp. p fls");
  ("prd", parse "λm. fst (m (λp. pair (snd p) (plus c1 (snd p))) (pair c0 c0))");
  ("fix", parse "λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))");
  ("factorial", parse "fix (λf. λn. test (iszro n) (λx. c1) (λx. (times n (f (prd n)))) c0)");
]

factorialが階乗を計算する関数です。factorialの中身を見てみると、不動点コンビネータfixを用いてfが関数内で再帰的に使える構造になっていることがわかります。まずtestを用いて n が 0 かどうか(iszro n)で条件分岐しています。n が 0 の場合はλx. c1が、そうでない場合はλx. (times n (f (prd n)))) c0が計算結果になります。後者の場合はtimesを用いてnと、prd n (n - 1) をfに適用した数の積が計算されます。

例えば 4 の階乗を求めるためには次のようなプログラムを実行します。

# factorial (times (scc c1) (scc c1))
→ (λs. (λz. (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))))))))))))))))

s が 24 個並んでいるので、無事 4 の階乗を求めることができました 🎉

因みに、インタプリタには verbose モードがあり、プログラムが変換される様子をみることができます。

さいごに

インタプリタの解説というよりラムダ計算の説明が大部分になってしまいましたが、単純な計算体系で実用的な計算ができるという面白さが伝わっていたら幸いです。