読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

OCamlでlet recを使わずにfact関数を定義する

OCaml 再帰関数 不動点演算 ProofCafe CPDT

今日はProofCafeCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。

Inductive t (A: Set) : Set :=
  | T : (t A -> A) -> t A.

一見なんの問題も無さそうな この型定義は失敗し、次のようなコンパイルエラーが出力される。

Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".

もしこの型が定義できたとすると次のような関数が定義できてしまう。

Definition ワォ (T f) := f (T f).

ここで (ワォ (T ワォ)) はいくら評価しても同じ項になり、無限ループしてしまう。無限ループはCoqでは御法度なので以上のようなt型は定義できないということなのだ。

以下からが、本日の本題だ。この現象を逆手に取って OCamlで使えばlet recを使わずにループが表現できるんじゃないかと考えてみた。
OCamlでは上のような再帰型は問題なく定義できる。

type 'a t = T of ('a t -> 'a)
let wow (T f) = f (T f)

let _ = wow (T wow)

このコードはlet recを使っていないが、コンパイルすると無限ループで止まらないプログラムが得られる。もう少し工夫して次のように定義すると、関数fixpが定義出来る。fixpは(fixp f ≡ f (fixp f))を満たす不動点演算子だ。

type ('a,'b) t = F of (('a,'b) t -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b)
let fixp_aux (F fld) = fld (F fld)
let v = F (fun self f x -> f (fixp_aux self f) x)
let fixp f x = fixp_aux v f x

このfixpを使って階上を計算するfact関数は次のように記述できる。

let fact =
  fixp (fun fact x -> if x = 0 then 1 else x * fact (x-1))
let _ = print_int (fact 10)

このコードは型定義とlet定義しか使っていないが、ちゃんと(fact 10)が正しい値3628800を返す。OCamlが今偶然手元にない人もIDEONEの結果をみて確かめる事ができる: http://ideone.com/W2yJB

[追記 2010-07/25]
id:KeisukeNakanoさんのより詳しい記事がありました。多相バリアントを使ったより高度な定義を見る事ができます。#009 賢人鳥をまねる - λx.x K S K @ はてな