OCaml: ラムダ計算と型プログラミング？

友人が楽しそうにうちの研究室の先生に教えてもらった型プログラミングで遊んでいたので、ちょっとそれをまとめています。

考察はこれから。

追記：

@camloeba さんに最初のラムダ計算の簡約が間違っていると指摘をいただき、修正いたしました。ご指摘ありがとうございます。

○ラムダ計算について

まず、簡単に型なしラムダ計算について書いてみます。間違っているところがあったらツッコミを入れてくださいませm(_ _;)m

まず型なしラムダ計算というのは、ものすごく大雑把に言うとOCamlでいうと匿名関数みたいなものです。関数しか無い計算体系なのですが、チューリング完全です。

λx. λy. x y y みたいに書いて、これはx, yの２引数関数を表します。

関数に出来る事は関数適用のみで、例えば

(λx. x x) (λy. z)

=> (λy. z) (λy. z)

=> z

みたいに簡約します。基本的には対応している文字を置き換える事を繰り返します。

どこまで簡約するか、どういう順番に計算するのか、その辺りの戦略は面倒なので省略しますがTypes and programming languages の５章に書いてあります。

今回は自然数の加算を扱いたいです、なのでそこまで紹介します。

ラムダ計算で数はチャーチ数という形で表します。

具体的には０、１，２、３に対応する数は、

C0 = λs. λz. z

C1 = λs. λz. s z

C2 = λs. λz. s (s z)

C3 = λs. λz. s (s (s z))

と定義してみます。ｓの個数がそのチャーチ数に対応する自然数と一致するわけですね。

次に足し算をするために、１足す関数succを定義してみます。

succ = λn. λs. λz. s (n s z)

実際に計算してみましょう。

succ C0 = (λn. λs. λz. s (n s z) ) (λs. λz. z)

=> λs. λz. s ( (λs. λz. z) s z)

=> λs. λz. s ( (λz. z) z)

=> λs. λz. s z //チャーチ数のC1と一緒！

succ C1 = (λn. λs. λz. s (n s z)) (λs. λz. s z)

=> λs. λz. s ( (λs. λz. s z) s z)

=> λs. λz. s ( (λz. s z) z)

=> λs. λz. s (s z) // チャーチ数のC2と一緒！

また、足し算をする関数plusは、

plus = λm. λn. λs. λz. m s (n s z)

ですです。

これで正しい簡約が出来るかどうかは、手を動かして試してみて下さい。

plus C1 C2 = (λm. λn. λs. λz. m s (n s z) ) (λs. λz. s z) (λs. λz. s (s z) )

=>* λs. λz. (λs. λz. s z) s ( (λs. λz. s (s z) ) s z)

=>* λs. λz. (λs. λz. s z) s (s (s z) )

(* 一番左の関数の中のｓをｓで置き換えて、ｚをs zで置き換える。

=>* λs. λz. s (s (s z) ) //チャーチ数C3と一緒！

これと同じような書き方で、ペアも書けるし条件分岐も書けるし無限ループも書けます。チューリング完全ですから。

型プログラミング

まずは試したソースコード。全てOCaml 4.0.1のインタラクティブモードで試しています。詳細は分かってないので話半分に読んで下さい。。。

一応TAPLの型なしラムダ計算を参考に名前をつけているので、それっぽく読めば大体何をするものなのかわかると思います。

実際はOCamlでは型なしのプログラミングが通常はできない（型なしにするオプションってあるんですか？）ので、厳密に上の例と一致するわけではないです。

また型付きラムダ計算はチューリング完全ではありません。チューリング完全にするためには単純型付きラムダ計算には、fixが必要です。

ではまずは型の定義から。

module type ZERO = sig type t end

module type SUCC = functor (X:ZERO) -> ZERO
module type NAT = functor (S:SUCC) -> functor (Z:ZERO) -> ZERO

ZEROは型なしラムダ計算でいうと、チャーチ数のところで扱った引数のzの部分に対応します。SUCCはsに対応しますね。NATはチャーチ数の型です。

module N0 = functor (S:SUCC) -> functor (Z:ZERO) -> Z
module Succ =
functor (N:NAT) ->
functor (S:SUCC) -> functor (Z:ZERO) -> S (N (S) (Z) )

チャーチ数でいうとN0はC0に対応してます（C０は通常の数で言うと０です）

Succは文字通り型レベルで１をたすためのものです。functor周りの機能が分かってないので正確に理解しているわけじゃないのですが…。

おもいっきりSuccの定義がラムダ計算で学習した定義と対応しますね。楽しい。

module N1 = Succ (N0)　(* チャーチ数をいっぱい定義する *)

module N2 = Succ (N1)
module N3 = Succ (N2)

ではこれでチャーチ数が定義できているのか、確かめてみましょう。

# module X = N0 (functor (X:ZERO) -> struct type t = X.t list end) (struct type t = int end);;

module X : sig type t = int end

# module X = N1 (functor (X:ZERO) -> struct type t = X.t list end) (struct type t = int end);;

module X : sig type t = int list end

# module X = N2 (functor (X:ZERO) -> struct type t = X.t list end) (struct type t = int end);;

module X : sig type t = int list list end

# module X = N3 (functor (X:ZERO) -> struct type t = X.t list end) (struct type t = int end);;

module X : sig type t = int list list list end

list の数がチャーチ数と対応していることがわかると思います。あ、太文字は入力で、アンダーラインのある文字はインタラクティブモードでの出力です。

また条件分岐もできます。０かどうか確かめるのは、下のようにできます。

０であればboolが帰ってきて、そうでなければstringが帰ってきますね。

(* isZero を展開したもの *)

# module X = N0 (functor (X:ZERO) -> struct type t = string end) (struct type t = bool end);;

module X : sig type t = bool end

# module X = N1 (functor (X:ZERO) -> struct type t = string end) (struct type t = bool end);;

module X : sig type t = string end

こんなところで…。

なぜかisZeroを定義して使ってみようともしたのですが型が省略されちゃって上手く出力されませんでした。ちょっと考えます。

まぁこういう役に立たなそうなプログラミングって楽しいですね。友人に負けぬよう、色々勉強しなくては。

論文を読みながら次のネタを探さねばなりませんね。最近読んでいるパーフェクトJavaについてか、Haskellを勉強してそれっぽい記事を書いてみるか。

CodeIQの問題を解いてみるのもいいかな。