• ビジネス
  • IT
  • テクノロジー
  • 医療
  • 建設・不動産
  • TRENDY
  • WOMAN
  • ショッピング
  • 転職
  • ナショジオ
  • 日経電子版
  • 日経BP
  • PR

  • PR

  • PR

  • PR

  • PR

数理科学的バグ撲滅方法論のすすめ

第14回 型=命題,プログラム=証明

2007/09/12 ITpro

MLの型と型推論

 この連載でも何回か触れたが,MLやHaskellなど多くの静的型付き関数型言語には,「型推論」という機能がある。これは,プログラム中の変数や関数の型を省略しても,「もっとも一般的」な型を言語処理系が勝手に推論してくれる,という機能だ。

 例えば,次のように,二つの引数xとyを受け取って,(x, y)という組を返す関数pairを定義してみよう。

> ocaml
        Objective Caml version 3.10.0

# let pair = fun x y -> (x, y) ;;
val pair : 'a -> 'b -> 'a * 'b = <fun>
# 

 このように,pairは「何らかの型'aを持つ値と,何らかの型'bを持つ値を受け取り,'a型の値と'b型の値の組を返す」と推論される。一般に,t1 -> t2は,型t1の値を受け取って,型t2の値を返す関数の型である。t1 * t2 は,第一要素の型がt1,第二要素の型がt2であるような組の型だ。

 'aや'bは「型変数」といい,任意の型を当てはめることが可能だ。例えば,xとして整数3を,yとして文字列"hello"を与えると,'aには整数の型intが,'bには文字列の型stringが当てはまり,結果は(3, "hello")というint * string型の値になる。他の型の場合も同様だ。

# pair 3 "hello" ;;
- : int * string = (3, "hello")
# pair 1.23 'a' ;;
- : float * char = (1.23, 'a')

 MLなど多くの関数型言語では,関数そのものも値として扱うことができる。したがって,'aや'bには関数型を当てはめることもできる。

# succ (* 整数に1を足す標準ライブラリ関数 *) ;;
- : int -> int = <fun>
# pred (* 整数から1を引く標準ライブラリ関数 *) ;;
- : int -> int = <fun>
# pair succ pred ;;
- : (int -> int) * (int -> int) = (<fun>, <fun>)

 ただし,正確に言うと,MLには「複数の引数を受け取る関数」は存在しない。例えば,上の関数pairは,正確には「'a型の値を受け取り,'b -> 'a * 'b型の関数を返す」という一引数関数だ。返り値も関数なので,再び「'b型の引数を受け取って,'a * 'b型の値を返す」ことができ,見かけは二引数関数のように使えるわけだ。

 だから,もし下のようにpairを定義しても,意味は全く変わらない。いずれにせよ,xを受け取ると「yを受け取って(x, y)を返す関数」を返す,という関数になるからだ。

# let pair = fun x -> fun y -> (x, y) ;;
val pair : 'a -> 'b -> 'a * 'b = <fun>

 ちなみに,'a -> 'b -> 'a * 'bという型は,'a -> ('b -> 'a * 'b)と同じである(->は右結合的)。これは,例えばC言語で,x = y = z;と書いたらx = (y = z);になるのと同じような,一種の文法的慣習だ。また,pair 3 "hello" という式は,(pair 3) "hello" と同じとみなされる(関数適用は左結合的)。これも,普通の数学で,x - y - zと書いたら(x - y) - zになるのと同じことである。

型推論の「逆問題」

 型推論は「式を与えられたら,その型を求める」という問題だった。逆に,「型を与えられたら,その型を持つ式を求める」ことを考えてみよう。ただし,さしあたり再帰や無限ループ,ライブラリ関数,例外や参照セルへの破壊的代入などの副作用は用いないこととする。これらを用いると,例えば下のように「引数も返り値も全く任意の型」という関数が定義できてしまい,問題の意味がなくなってしまうからだ(そのような関数は絶対に値を返さないので,実際の動作と型推論の結果が矛盾するわけではない)。

# let rec f = fun x -> f x ;;
val f : 'a -> 'b = <fun>
# let f = fun x -> failwith "exception" ;;
val f : 'a -> 'b = <fun>

 例えば,'a -> 'aという型を考えよう。これは「'a型の値を受け取り,'a型の値を返す関数」の型だ。したがって,受け取った引数をそのまま結果として返す関数fun x -> xが考えられる。

# fun x -> x ;;
- : 'a -> 'a = <fun>

 'a * 'b -> 'b * 'aという型ならばどうだろうか。これは「'a型の値と'b型の値の組を受け取り,'b型の値と'a型の値の組を返す」という関数の型だ。だから,受け取った組の第一要素と第二要素を取り出し,要素の順番を入れ替えた組を作って返せば良さそうである。

# fun (x, y) -> (y, x) ;;
- : 'a * 'b -> 'b * 'a = <fun>

 もう少しややこしい例として,('a -> 'b) * ('b -> 'c) -> ('a -> 'c)という型を考えてみよう。->は右結合的だから,これは('a -> 'b) * ('b -> 'c) -> 'a -> 'cと同じだ。つまり,'a -> 'b型の関数(fとする)と,'b -> 'c型の関数(gとする)の組,および'a型の値(xとする)を受け取り,'c型の値を返せば良いはずだ。そのためには,まずfをxに適用し,その結果にgを適用すればOKだ。これは関数fとgの合成にあたる。

# fun (f, g) x -> g (f x) ;;
- : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c = <fun>

関数は「ならば」の証明,組は「かつ」の証明

 このような一見すると何の役にも立たない問題に,何の意味があるのだろうか?

 実は,「'a -> 'a」「'a * 'b -> 'b * 'a」「('a -> 'b) * ('b -> 'c) -> ('a -> 'c)」といった型は,ある種の論理式とみなすことができる。'aや'bのような型変数はAやBなどの命題変数に,->は論理記号の⇒(ならば)に,*は∧(かつ)に対応する。例えば,'a -> 'aはA ⇒ A(AならばA)という論理式に,'a * 'b -> 'b * 'aはA ∧ B ⇒ B ∧ A(AかつBならばBかつA)という論理式にあたる。また,('a -> 'b) * ('b -> 'c) -> ('a -> 'c)は(A ⇒ B) ∧ (B ⇒ C) ⇒ (A ⇒ C),つまり,「AならばB」かつ「BならばC」ならば「AならばC」という論理式にあたる。

 型が論理式(命題)にあたるとすれば,その型を持つ式(プログラム)は何にあたるのだろうか? 実は,「式」は「型」が表す命題の証明とみなすことができる。例えば,fun (x, y) -> (y, x)という式は,命題A ∧ Bの証明である(x, y)を受け取り,命題B ∧ Aの証明である(y, x)を返す,とみなせる。そのような式が存在することから,A ∧ Bが成り立てば,B ∧ Aが成り立つことが確認できるわけだ。

 あるいは,('a -> 'b) * ('b -> 'c) -> ('a -> 'c)の例を考えてみよう。fun (f, g) x -> g (f x)という式は,fun (f, g) -> fun x -> g (f x) と同じだ。

# fun (f, g) -> fun x -> g (f x) ;;
- : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c = <fun>

 この関数は,A ⇒ Bの証明にあたる関数fと,B ⇒ Cの証明にあたる関数gの組を受け取り,A ⇒ Cの証明にあたる関数fun x -> g (f x)を返す。つまり,「A ⇒ BとB ⇒ Cが成り立てば,A ⇒ Cが成り立つ」という証明になるわけだ。

 このような「型=命題,プログラム=証明」という対応のことを,カリー・ハワードの対応(Curry-Howard correspondence)という。この名前は,ハスケル・カリーとウイリアム・ハワードという二人の論理学者に由来する(ちなみに,関数型言語Haskellの名前もハスケル・カリーに由来する)。

「または」を表す型

 関数の型が「ならば」を,組の型が「かつ」を表すならば,「または」を表す型は何だろうか?

 それが第7回にも出てきたバリアント型だ。バリアント型は,「type t = A of 型1 | B of 型2 | ...」のように定義され,「型1または型2」のような型を表すのだった。そこで,論理記号の∨(または)を,以下のように定義される型or_tで表すことにしよう(ちなみにOCamlでは,「or」は「true or false」のようにbool値の論理和を表す予約語なので,型名として使用することはできない)。

# type ('a, 'b) or_t = Left of 'a | Right of 'b ;;
type ('a, 'b) or_t = Left of 'a | Right of 'b

 or_tは,'aと'bという二つの型変数をとり,「'aまたは'b」という型を表す。例えば「intまたはstring」だったら,(int, string) or_tという型になる。

# let f = fun x -> if x then Left 123 else Right "abc" ;;
val f : bool -> (int, string) or_t = <fun>
# f true ;;
- : (int, string) or_t = Left 123
# f false ;;
- : (int, string) or_t = Right "abc"

 or_tを用いれば,∨(または)を含む論理式を型として表すことができる。例えばA ∨ B ⇒ B ∨ Aだったら,('a, 'b) or_t -> ('b, 'a) or_tとなるわけだ。これは実際に成り立つはずなので,('a, 'b) or_t型の値を受け取って,('b, 'a) or_t型の値を返す関数を考えてみると,以下のようになる。

# fun x ->
    match x with
      Left y -> Right y
    | Right z -> Left z ;;
- : ('a, 'b) or_t -> ('b, 'a) or_t = <fun>

 この関数はまず,('a, 'b) or_t型の引数xが,Left yの形だった場合とRight zの形だった場合に場合分けをする。これは仮定である「AまたはB」のうち,Aが成り立つ場合と,Bが成り立つ場合にあたる。前者の場合,yは'a型だから,Right yを返せば,結論である「BまたはA」のAのほうを証明したことになる。後者の場合,zは'b型だから,Left zを返せば,やはり結論である「BまたはA」のBのほうを証明したことになる。したがって,仮定「AまたはB」から結論「BまたはA」を導くことができた。つまり,「AまたはBならばBまたはA」が示せたことになる。

ここから先はITpro会員(無料)の登録が必要です。

次ページ 真,偽,および否定を表す型
  • 1
  • 2

あなたにお薦め

連載新着

連載目次を見る

今のおすすめ記事

ITpro SPECIALPR

What’s New!

経営

アプリケーション/DB/ミドルウエア

クラウド

運用管理

設計/開発

サーバー/ストレージ

クライアント/OA機器

ネットワーク/通信サービス

セキュリティ

もっと見る