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をひっくり返したものだということに後になって気がついてなるほどってなった
AviUtlスクリプト 「自由落下と衝突」 v1.0
この前MAD動画を作るのに作ったAviUtl用のアニメーション効果を公開
概要
上からオブジェクトが落ちてきて, 地面に衝突して跳ね返る動きを実現します.
オブジェクトの位置(Y座標)が地面の高さに対応.
パラメータについて
- 加速度: 重力加速度. 落下にかかる時間に影響.
- Y移動量: 始めのオブジェクトの高さ
- 弾性係数: 地面に反射にした時に, 反射後と反射前の速度比です. 弾性係数がeのとき, 跳ねる高さは1回ごとにe2倍になります. また, e>1のときは跳ねる高さが段々高くなります.
- 閾値: オブジェクトがこの値よりも小さく跳ねることはありません. 跳ねる高さの最小値です.
- 設定>バウンド回数: バウンド回数を指定します. これを超えるとオブジェクトは停止します.
- チェックボックス>高さ0地点からスタート: 高さが0地点からスタートします. (初めて地面に到達した時刻からスタートします. これにチェックを入れた場合, 次に跳ねる高さは Y移動量*弾性係数2 になります)
インストール
以下のスクリプトを「自由落下と衝突.anm」として保存し, aviutlフォルダの script/ 以下に配置してください.
宣伝
このスクリプトを使って作った動画:
