Just $ A sandbox

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

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

AviUtl

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

概要

f:id:myuon_myon:20160405020022g:plain

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

パラメータについて

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

インストール

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

宣伝

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

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

Theorem Prover Leanの紹介

Agda Isabelle 定理証明

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年以降流行る可能性があるかもしれない.
むしろ流行ってくれ.

証明の例

参照

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

オートマトンで遊ぶやつを作った

Haskell

この記事はHaskell Advent Calendar 2015 18日目の記事です.

Automatoy(オートマトン)で遊ぶやつを作ったので紹介します.

github.com

ブラウザで遊べる.
以下それっぽい解説.

Automatoyについて

http://myuon.github.io/automatoy/

"Def"タブでオートマトンを定義.
"Check"タブで与えられた文字列のacceptance checkができる.
"Conversion"タブでいくつかのサンプルオートマトンを読み込んだり, NFAをDFAに変換(いわゆるpowerset construction)できる.

また, 右上のImport/Exportでjsonに変換したり, jsonを読み込んだりできる.

もう少し扱えるオートマトンのバリエーションを増やしたり, acceptance checkにアニメーションを取り入れたり, アルゴリズムを増やしたり(complementとかそういうやつ)したら面白そう.
ものすごく気が向いたら頑張って開発する. (たぶんしない)

オートマトンの絵を書くのには, Cytoscapeを使った.
Haskellでコードを書いて, HasteでJavascriptにコンパイルしている.

HasteとTemplateHaskell(以下TH)

Hasteでは現在THがサポートされていないのでlensを含む, THが使われているライブラリをインストールして使うことができない.
lensの場合は, THを含まないより簡単なパッケージとしてlens-familyがあるのでこれを使った.

さて, lensには便利なmakeLensesという機能(TH)があるのでこれを使いたいのだが, lens-familyでこれをやるためには以下のコードを書く必要がある.

data Hoge = Hoge { _f1 :: k1, _f2 :: k2, .. , _fn :: kn }

f1 :: Lens' Hoge k1; f1 = lens _f1 (\p x -> p { _f1 = x })
.. -- フィールドの個数だけ繰り返す
fn :: Lens' Hoge kn; fn = lens _fn (\p x -> p { _fn = x })

これが最高に面倒くさい(特に, 各fiの型をそれぞれ宣言しなければならないことと, _fiとfiのいずれもexportしないといけないところ)のでどうにかしたかった.

これを解決する1つの方法として, Extensible Recordsを提供するextensibleというパッケージを使うというのがある.

extensibleはTHを使っているのでこれをそのままHaste環境にインストールはできないけれど, 少しアイデアを借りてそれらしいもの(もっと簡単なやつでよい)を実装することにした*1.

Union Type

結局以下のようなことができれば良い:

  • k1 .. kn型をまとめて管理するコンテナ(リストのようなもの)を用意する
  • コンテナへのアクセサとしてlensを提供する. getter "fi"のようにして値にアクセスできるようにする
  • アクセサはコンパイル時にvalidかどうかをチェックする. 存在しない名前などはコンパイルエラーにする. (コンパイル時にやる必要があるかどうかは趣味の問題だけれど, タイプミスなどはコンパイルエラーにしてくれた方が明らかに便利なので今回はコンパイル時にやる)

1番目はヘテロリスト(1-kind list)でよい.
2番目は型クラスを使って上手くやろう.
3番目は文字列の代わりにSymbolを使えば良い.

実装

data HList (xs :: [*]) where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

data Union (xs :: [*]) = Union (HList xs)

data (:<) (s :: Symbol) a = Tag a
data Name (s :: Symbol) = Name

実際にUnionを使うときは, Union <("intValue", 20), ("charValue", 'a')> のように, Symbolと値をペアにして使う.
これを(s :: Symbol) :< (a :: *)でペアを表すことにしている.
Nameは単にSymbolのみを型としてつかえるようにするもの.

class MakeLense (xs :: [*]) (s :: Symbol) out | xs s -> out where
  getter' :: Name (s :: Symbol) -> HList xs -> out
  setter' :: Name (s :: Symbol) -> (out -> out) -> HList xs -> HList xs

instance MakeLense ((k :< v) ': xs) k v where
  getter' _ (HCons (Tag v) _) = v
  setter' _ f (HCons (Tag v) xs) = HCons (Tag $ f v) xs

instance {-# OVERLAPPABLE #-} MakeLense xs syb out => MakeLense ((k :< v) ': xs) syb out where
  getter' k (HCons _ xs) = getter' k xs
  setter' k f (HCons x xs) = HCons x $ setter' k f xs

getter :: (MakeLense xs s out) => Name (s :: Symbol) -> Getter' (Union xs) out
getter syb = to $ \(Union hl) -> getter' syb hl

setter :: (MakeLense xs s out) => Name (s :: Symbol) -> Setter' (Union xs) out
setter syb = setting $ \f (Union hl) -> Union $ setter' syb f hl

lenses :: (MakeLense xs s out) => Name (s :: Symbol) -> Lens' (Union xs) out
lenses syb = lens (^. getter syb) (\u x -> set (setter syb) x u)

以下のような感じで使う.

data Flag = A | B | C deriving (Show)
data Gender = F | M deriving (Show)
type Ext = Union ["flag" :< Flag, "money" :< Int, "gender" :< Gender]

runExt :: StateT Ext IO ()
runExt = do
  lenses (Name :: Name "flag") .= B
  lenses (Name :: Name "money") += 30
  g <- use (getter (Name :: Name "gender"))
  case g of
    F -> lenses (Name :: Name "gender") .= M
    M -> lenses (Name :: Name "gender") .= F

main = do
  print "hoge"

  let iniExt = Union $ HCons (Tag A) (HCons (Tag 0) (HCons (Tag F) HNil)) :: Ext
  print $ iniExt ^. getter (Name :: Name "flag")
  print $ iniExt ^. getter (Name :: Name "money")

  ext' <- execStateT runExt iniExt
  print $ ext' ^. getter (Name :: Name "flag")
  print $ ext' ^. getter (Name :: Name "money")

Name :: Name "hoge"などと書かなければいけないのは面倒だけれど, 最初に書いたような面倒は多少軽減されたはず.

課題とか

このままだとUnion型の値を定義するのが面倒とか, 存在しないキーがあるときのエラーメッセージがあまりユーザーフレンドリーでないなどの問題がある.
ので, そのへんはextensibleの中では結構上手く解決されているので興味がある人はData.Extensible.Fieldなどを読むとよいでしょう.
自分は下のコードで大体満足しているけれど.

全体

MakeLense.hs(ちょっとだけ改良版)のコードは以下.

MakeLense.hs · GitHub

*1:正確に言えばここからアイデアを借りたわけではなくて, 以下のような実装を考えていたら「これは全く同じことがすでにextensibleで実装されているな」と気がついたわけです. 余談.