日々の流転

λ. Coqで“無限オブ無限”

稲葉さんの「無限オブ無限」は余再帰的な関数(corecursive function)の良い例題なのではないかと思い、Coqでも書いてみることにした。 何故いつものAgdaではなくCoqかというと、Agdaはまだcodataに対応しておらず無限リストやストリームを直接扱うことが出来ないため。

まず、Coqでは余再帰的な関数は、全域関数であることを保証するために guarded corecursion の形で書かないといけない。ので、guarded corecursion の形で書こうとしたのだけど、色々試してもどうも書けない。 何故かと思って落ち着いて考えてみたら、そもそも iflatten (repeat []) が実効的(effective)に定義出来ないから、この関数 iflattern は全域的な計算可能関数ではないのだった。

色々細かい条件を色々加えればCoqでも定義できるだろうけど、Coq初心者の私にはそれは面倒なので、とりあえず無限リストの無限リストの場合のみで定義してみた。Coqでマトモに何かを書くのは初めてなので、変な書き方をしてるかも知れないけど、そこは識者のツッコミに期待しておきます(^^;

(* IFlatten.v *)
Section IFlatten.

Require Import List.
Require Import Streams.

(* anamorphisms (co-iteration) *)
CoFixpoint unfold (A X : Set) (phi : X -> A*X) (x : X) : Stream A
:= match phi x with
     | (a, x) => Cons a (unfold A X phi x)
   end.
Implicit Arguments unfold [A X].

Inductive CV (A X : Set) : Set :=
  | CVLast : X -> CV A X
  | CVCons : A * CV A X -> CV A X.
Implicit Arguments CVLast [A X].
Implicit Arguments CVCons [A X].

(* futumorphisms (course-of-values co-iteration) *)
Definition futu (A X : Set) (phi : X -> A * CV A X) (x : X) : Stream A
:= let psi cv :=
         match cv with
           | CVLast x => phi x
           | CVCons p => p
         end
   in unfold psi (CVLast x) .
Implicit Arguments futu [A X].

Definition add_prefix (A : Set) (xs : list A) (X : Set) (cv : CV A X) : CV A X
:= fold_right (fun a cv => CVCons (a, cv)) cv xs.
Implicit Arguments add_prefix [A X].

Definition iflatten (A : Set) (ss : Stream (Stream A)) : Stream A
:= let phi x :=
          match x with
          | (ss, ls) =>
             let s := hd ss in
             let ss2 := tl ss in
             let ls2 := tl s :: List.map (fun x => tl x) ls in
               ( hd s
               , add_prefix
                 (List.map (fun x => hd x) ls)
                 (CVLast (ss2, ls2))
               )
          end
   in futu phi (ss, nil).
Implicit Arguments iflatten [A].

End IFlatten.

(* Haskell のコードを出力する *)
Extraction Language Haskell.
Extraction "IFlatten" iflatten.

これをCoqIDEに読み込ませたら、ちゃんと通った。 Coqで定義が通ったので、少なくともちゃんと全域関数になっていることは分かる。そして、ExtractionでHaskellのソースコードを生成したので、正しく定義できているか簡単に確認してみることに。 このままだと試しにくいのでまずは簡単なラッパを定義する。

import IFlatten

l2s :: [a] -> Stream a
l2s (x:xs) = Cons0 x (l2s xs)

s2l :: Stream a -> [a]
s2l (Cons0 x xs) = x : s2l xs

iflatten' :: [[a]] -> [a]
iflatten' xss = s2l $ iflatten $ l2s [l2s xs | xs <- xss]

で、試す。

Main> take 10 $ iflatten' [[(i,j) | j<- [1..]] | i<-[1..]]
[(1,1),(2,1),(1,2),(3,1),(2,2),(1,3),(4,1),(3,2),(2,3),(1,4)]

うん、ちゃんと定義できてるみたい。 折角Coqで定義したので、題意を満たしていることをちゃんと形式的に証明したいところだけど、それはまだやっていない。

【2007-12-10追記】 にわとり小屋でのプログラミング日記のyoshihiro503さんが、形式的な証明をしてくれたようです。わーい。 ⇒ Coqで”無限オブ無限” - にわとり小屋でのプログラミング日記