すべてのものは…である

 SmalltalkやRubyなど,いわゆる生粋のオブジェクト指向言語では,「すべてのものはオブジェクトである」(everything is an object)と言われることがある。JavaやC++などと異なり,整数の「123」や浮動小数の「4.56」といった,基本データ型の値もオブジェクトとして扱うことができるからだ(ちなみに,現在のJavaには自動ボックス化という機能があり,基本データ型からオブジェクト型への変換が自動で行われる場合も多い。しかし,両者の差異が全くなくなったわけではない。例えば123.toString()のようなメソッド呼び出しはできない)。

 では,オブジェクト指向言語のまねをして,関数型言語において「すべてのものは関数である」と言うことはできるだろうか?

 もちろん,オブジェクト指向と違って,関数型プログラミングはあくまで「数学的な(=副作用のない)関数を中心とするプログラミング」に過ぎず,「すべてのものを関数とみなす」ことを目指しているわけではない。したがって,通常,「123」や「4.56」を関数とみなす,といった欲求はない。

 ところが,関数型言語のモデルとなっている基礎理論では,実は「すべてのものを関数で表す」ことができる。より正確にいうと,(計算機自体の一般的なモデルである)「チューリングマシン」で可能な計算は,すべて関数で表せることが知られている。それが今回紹介するλ計算(ラムダ計算)という計算モデルだ。

λ計算の構文と直観的意味

 本連載第11回で紹介した,並行言語のモデルであるπ計算と同様(あるいはそれ以上)に,λ計算にも非常に様々な変種がある。

 今回は,それらすべての基本となる,もっとも純粋なλ計算について紹介しよう(なお,ここでいう「純粋」は,「副作用がない」という意味の「純粋」とは関係がない。整数などを関数で表すのではなく,プリミティブとして追加した「応用λ計算」も存在する。第10回でインタプリタを作成したMyFun言語も,応用λ計算の一種だ)。

 純粋なλ計算は,一言でいうと「関数しかないプログラミング言語」だ。純粋なλ計算のプログラム(λ式)の構文は,以下の3行で表される。

  • λ抽象「λx. e」
  • 関数適用「e1 e2」
  • 変数「x」

 ただし,xは変数一般を表す記号,e,e1,e2などはλ式一般を表す記号とする。

 λ抽象「λx. e」は,OCamlの「fun x -> e」に相当する構文で,xを受け取ると,eを評価して返す関数を表す。関数適用と変数の意味はOCamlと同様だ。

論理値と条件式をλ式で表す

 たったこれだけの構文で,関数型言語の様々な式や値をどうやって表現するのだろうか?

 まず,簡単な例として,変数を定義するlet式「let x = e1 in e2」を考えてみよう。これは(λx. e2) e1というλ式で表すことができる。どちらも,まず変数xがe1(ないしe1を評価して得られる値)に束縛され,それからe2が評価されるからだ。

 では,条件式「if e1 then e2 else e3」はどうだろうか。この式は,e1がtrueになればe2に,e1がfalseになればe3になってほしいはずだ。そのためには,まず,trueやfalseをどう表すかを考えなければならない。

 ここで,ちょっと発想を逆転して,trueやfalse自身にif式の動作を「仕込む」ことにしよう。つまり,「e2とe3を受け取って,e2のほうを返す」関数でtrueを,e3のほうを返す関数でfalseを表すことにする。

true   =   λx. λy. x
false   =   λx. λy. y

 trueやfalse自身に条件分岐の機能を「仕込んだ」ので,if式はe1にe2とe3を与えるだけで良い。

if e1 then e2 else e3   =   e1 e2 e3

 そうすれば,確かにif true then e2 else e3は,(λx. λy. x) e2 e3つまりe2となる。同様にif false then e2 else e3はe3となる。true,falseとif式が表せれば,&&や||といった論理演算も容易に表現できる。

e1 && e2   =   if e1 then e2 else false
e1 || e2   =   if e1 then true else e2
not(e)   =   if e then false else true

 ただし,OCamlのような値呼び(call-by-value)の言語では,関数適用の前に引数が評価されるので,「e1 e2 e3」ではe2やe3が先に評価されてしまう。つまり,if式のthen節とelse節が両方とも評価されてしまう。

 仮に入出力や例外などの副作用はないとしても,e2やe3が無限ループすることはあり得るので,これはまずい。λ計算自身は一般的なモデルなので,値呼び以外の評価順を考えることもできるが,値呼びも考慮したい場合は,以下のようにe2やe3をダミーの引数を受け取る関数とすれば良い。

if e1 then e2 else e3   =   e1 (λd. e2) (λd. e3)
true   =   λx. λy. x e  
false   =   λx. λy. y e

 ただし,dはe2やe3に出現しない変数で,eは適当なダミーのλ式(例えばλx. xなど)とする。

 試しに,true && falseに当たるλ式がどのような値に評価されるか,OCamlで確認してみよう。まず,OCamlのプリミティブ値である「true」や「false」とは別に,上のように関数で表した「my_true」と「my_false」を定義する。また,型をわかりやすく表示するために,'a my_bool型も定義する。'a my_boolの'aは,その論理値に対する条件分岐の結果の型に当たる。一つの論理値をいろいろな型のif式で使うために,'aという型変数にしておくわけだ。また,上のダミー変数dやダミー式eの型として,'a my_unit型も定義する。

# type 'a my_unit = 'a -> 'a ;;
type 'a my_unit = 'a -> 'a
# type 'a my_bool = ('a my_unit -> 'a) -> ('a my_unit -> 'a) -> 'a ;;
type 'a my_bool = ('a my_unit -> 'a) -> ('a my_unit -> 'a) -> 'a
# let e : 'a my_unit = fun x -> x ;;
val e : 'a my_unit = <fun>
# let my_true : 'a my_bool = fun x -> fun y -> x e ;;
val my_true : 'a my_bool = <fun>
# let my_false : 'a my_bool = fun x -> fun y -> y e ;;
val my_false : 'a my_bool = <fun>

 先の考え方に従えば,true && falseはif true then false else falseつまりtrue (λd. false) (λd. false)と表せるはずだ。

# let ans1 : 'a my_bool =
    my_true (fun d -> my_false) (fun d -> my_false) ;;
val ans1 : '_a my_bool = <fun>

 しかし,このままでは,答えであるはずの関数ans1が単に<fun>と表示されてしまい,中身を確かめることができない。そこで,前回のtype-directed部分評価を使って,ans1の無駄な部分を省略した「ソースコード」を復元してみよう。型がややこしいが,ここでは深く考えないことにして,前回と同様,型変数は「z」で,->は^->で機械的に置き換えれば良い(ただし,前回は関数適用の前後の括弧を省略してしまったので,"%s %s"を"(%s %s)" に修正しておく必要がある)。

# val2str (((z ^-> z) ^-> z) ^-> ((z ^-> z) ^-> z) ^-> z) ans1 ;;
- : string = "(fun x1 -> (fun x2 -> (x2 (fun x3 -> x3))))"

 これは確かに上のmy_falseと(引数の名前や括弧など以外は)「同じ」式になっている。