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

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

参考

• Type Theory and Functional Programming
• 帰納法と余帰納法の何がどう双対なのか（初等的に） - sumiiの日記

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