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をひっくり返したものだということに後になって気がついてなるほどってなった

AviUtlスクリプト 「自由落下と衝突」 v1.0

この前MAD動画を作るのに作ったAviUtl用のアニメーション効果を公開

概要

上からオブジェクトが落ちてきて, 地面に衝突して跳ね返る動きを実現します.
オブジェクトの位置(Y座標)が地面の高さに対応.

パラメータについて

• 加速度: 重力加速度. 落下にかかる時間に影響.
• Y移動量: 始めのオブジェクトの高さ
• 弾性係数: 地面に反射にした時に, 反射後と反射前の速度比です. 弾性係数がeのとき, 跳ねる高さは1回ごとにe²倍になります. また, e>1のときは跳ねる高さが段々高くなります.
• 閾値: オブジェクトがこの値よりも小さく跳ねることはありません. 跳ねる高さの最小値です.
• 設定>バウンド回数: バウンド回数を指定します. これを超えるとオブジェクトは停止します.
• チェックボックス>高さ0地点からスタート: 高さが0地点からスタートします. (初めて地面に到達した時刻からスタートします. これにチェックを入れた場合, 次に跳ねる高さは Y移動量*弾性係数² になります)

インストール

以下のスクリプトを「自由落下と衝突.anm」として保存し, aviutlフォルダの script/ 以下に配置してください.

宣伝

このスクリプトを使って作った動画:

【ニコニコ動画】ゆゆ式リレーション(修正版)

Theorem Prover Leanの紹介

Microsoftが開発したTheorem Prover Leanを紹介します.

特徴

他の言語と軽く比較する.
あくまで個人的な感想です.

	Lean	Coq*1	Agda	Isabelle
証明の書き方	structured proof, tactic, 函数定義	tactic	函数定義	structured proof, tactic
開発環境	emacs	emacs, CoqIDE	emacs	jEdit
ドキュメント	×	◎	○	△
implicit parameter	○	○	△	(型を使わないので不要)
Equational Reasoning	○(builtinなものはOK. 独自演算子は条件付き)	？(知らない)	◎	○(基本的にbuiltinなもののみサポート)
自動証明	×(なし？)	○(auto, omegaなど)	△(emacsのautoコマンド)	◎(auto, force, sledgehammerなど)
ライブラリ	◎	○？	△	○
パフォーマンス	○？	？(知らない)	×	○

証明の書き方

なんとstructured proof(上から下向きに書ける), tactic, 函数定義の全ての書き方をサポートしている.
他の言語から入ってきた人にも優しい仕様.

開発環境

インストールはバイナリがあるのでそれを入れるだけ.
インストールするとleanemacsというアプリケーションが使えるようになる.
leanemacsではリアルタイムチェッカーが走るし, エラーメッセージも見やすいので(emacsが嫌いじゃなければ)そんなに悪くないと思う.

ドキュメント

公式サイトにTutorialとかがある.
HTML版はブラウザ上でLeanを動かすこともできてすごい.

しかしドキュメントらしきものはこのtutorial.pdfくらいしかなく, より詳細な情報でまとまった文章はおそらく存在しない.
Leanを本格的に使うならここが一番問題.

implicit parameter

カリーハワード対応を使って証明を書くような言語では, implicit parameterが使えるのは結構重要.
Coqは割と優秀と聞く一方で, Agdaは少し省略するとしょっちゅう警告ばかり出す.

ここに関してはLeanもそれなりに優秀で, たくさん省略してもエラーになったり警告が出たりはしない.

Equational Reasoning

独自演算子に対してのReasoningは, それがグローバルに定義された演算子なら, refl attributeなどを対応する命題に付与することで使えるようになる.
ただしstructure(データ型を定義するときに使う)内の演算子に対しては使えないなどの制約があるらしい.
同値関係を含む構造を定義して, それに対するreasoningを書くことが出来ないので微妙に不便.

ちなみに, reasoningはsubst(a == b & ==> P a == P bなど)を自動でやってくれるようで, 実はこれのおかげでLeanでreasoningをすると非常に証明が楽になる.
a == bを指定すると, aの部分を現在のGoalの左辺から探して代入する操作をやってくれるのでこちらでsubstを指定する必要がない.
Leanの目玉機能の一つ.

自動証明

ドキュメントにも書いてないから多分ないです.

追記:
どうもblastがそれに当たるらしい.
blast派生のコマンドがいくつかあって, 代表的なものとしてsimp(simp attributeがついた定理を適用する), rec_simp(帰納法が使える？)などがある.

ライブラリ

(駆け出しの言語にしては)標準で結構色々なものが揃っている.
HoTTライブラリが用意されているあたりもポイント.
拡張子 .hleanがそれ.

ところで, 現在LeanファイルをHTMLやpdfファイルに変換するツールなどはない.
ので.leanファイルを直接見る以外に証明を読む方法がないので(ファイルの依存関係がややこしい場合は特に)結構不便.

パフォーマンス

ちょっと書いた限り重くなったりする気配はあんまりない.
リアルタイムチェッカーが走っている割には軽くて快適. (ここでAgdaの方をチラ見する)

所感

色んな書き方ができるのは, 参入コストが下がると考えれば悪いことではないと思う.
Equational Reasoningでsubstを指定しなくていいのは予想以上に楽だったので, 普段苦労している人はこれだけでも触ってみる価値はあるかもしれない.
あとはリファレンスさえしっかり作ってくれれば2016年以降流行る可能性があるかもしれない.
むしろ流行ってくれ.

証明の例

• rev.lean Listのreverseに関する証明
• yoneda.lean 米田の補題の証明

参照

• Lean 公式サイト
• Tutorial: Theorem Proving in Lean ブラウザでLeanが遊べるハイテクチュートリアル(長い)
• lean/library at master · leanprover/lean · GitHub 標準ライブラリ, 読むと勉強になる
• The Lean Theorem Prover Leanの紹介スライド, 最高にクールで分かりやすいので オススメ

*1:Coq使ってないので適当言ってるかも.