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

Just $ A sandbox

プログラミングと計算機科学とかわいさ

Coinductiveのintro rule

定理証明

Type Theory & Functional Programmingに出てきたCoinductive typeのintro ruleに少し悩んだので.

Coinductiveは最大不動点の形でかけるような型.
例えばStream(無限リスト)はP X = N × Xの時のPの最大不動点である.

テキストにはCoinductiveのintro規則と計算規則が以下のように書かれている*1.

CoinI : (d:D) -> ([y:D,z:D->T] => b:P T) -> xif{y,z} b d : Xif P

xif{y,z} b d ~> b[d/y, λw. xif{y,z} b w/z]

ここでd:Dは初期値, y:Dは現在の引数 z:D->Tは現在計算している函数のようにみることができる.
HaskellにはCoListを作るunfoldr :: (b -> Maybe (a, b)) -> b -> [a]という, リストの畳込みの丁度逆の操作を行う函数があって, 引数の順番は違うがあれと同じ感じ.
例を見よう.

fromN : N -> Xif P
fromN := xif{y,z} (y, z (y+1))

fromN 0
~> xif{y,z} (y, z (y+1)) 0
~> (y, z (y+1))[0/y, λw. fromN w/z]
~> (0, fromN (0+1))
~> (0, (1, fromN 2))
... ~> <0, 1, 2, ..>


mapi : (N -> N) -> Xif P -> Xif P
mapi f xs := xif{y,z} (f (head y), z (tail y)) xs

mapi f <x0,x1..>
~> xif{y,z} (f (head y), z (tail y)) <x0,x1..>
~> (f (head y), z (tail y))[<x0,x1..>/y, λw. mapi f w/z]
~> (f x0, mapi f <x1,x2..>)
... ~> <f x0, f x1, f x2 ..>


iterate : (N -> N) -> N -> Xif P
iterate f st := xif{y,z} (y, z (f y)) st

iterate f st
~> (y, z (f y))[st/y, λw. iterate f w/z]
~> (st, iterate f (f st))
... ~> <st, f st, f (f st), f (f (f st)) ..>

慣れてくれば簡単.

なおAgdaやIsabelleではcoinductiveな型に対するパターンマッチによる定義が普通に使えるので,

mapi : (N -> N) -> Colist N -> Colist N
mapi f (x::xs) = f x :: mapi f xs

のようにかけるため, 上のようなことを考えなくてもいい.

参考

*1:XifがFixをひっくり返したものだということに後になって気がついてなるほどってなった