Coq 末尾再帰の等価性の証明
レイトレーシングを実装する際、光の反射の計算に再帰を用いる。擬似コードを以下に示す。
let ref f ... argN = let a = ~~~~ in (* 加算:光源など *) let b = ~~~~ in (* 乗算:反射での減衰など *) let finished = ~~~~ in (* 計算を終了するか *) if ( finished ) then a else a + b * (f ...)
しかし、このような実装ではスタックオーバーフローが起こる可能性がある。 (特に不偏レンダリングをする際) これを回避するためには再帰しないような関数に書き直す必要がある。
これはwhile を用いた C++ の例であるが、関数型っぽく実装したい場合は末尾再帰呼び出しに書き換える事が考えられる。
let ref f arg0 arg1 ... argN (s, t) = let a = ~~~~ in let b = ~~~~ in let finished = ~~~~ in if ( finished ) then s + a * t else f ... (s + a * t, t * b)
本当に等価なのか怪しいので Coq で証明する。Coq だと上のように停止するかわからない関数は書けないので適当な変数 n を導入し停止する関数にエンコードする。
(* 再帰 *) Fixpoint f (a b : nat -> nat) (n: nat) := match n with | O => a 0 | S n' => (a (S n')) + (b (S n')) * f a b n' end. (* 末尾再帰 *) Fixpoint f_tr (a b : nat -> nat) (n: nat) (acc : nat * nat) := match n with | O => (fst acc) + (a 0) * (snd acc) | S n' => f_tr a b n' ((fst acc) + (a (S n')) * (snd acc), (snd acc) * (b (S n'))) end.
あとは証明を行う。特に難しくない。*1。 肝は a
b
を一般化したままにしておくぐらいか。
Lemma tail_rec_equiv_st : forall (a b : nat -> nat) (n s t : nat) , t * (f a b n) + s = f_tr a b n (s, t). Proof. intros a b n. induction n. - intros s t. simpl. rewrite plus_comm, mult_comm. reflexivity. - simpl. intros s t. rewrite <- IHn. (* やるだけ *) rewrite Nat.mul_add_distr_l. rewrite mult_assoc, mult_comm. assert(H: forall x y z, x + y + z = y + (z + x)). { intros x y z. omega. } apply H. Qed. Theorem tail_rec_equiv : forall (a b : nat -> nat) (n: nat), f a b n = f_tr a b n (0, 1). Proof. intros a b n. rewrite <- tail_rec_equiv_st. omega. Qed.
この証明を行う上において、もっと簡単な fact
の末尾再帰の例を先に証明しそれを参考にした。
Fixpoint f (n: nat) := match n with | O => 1 | S n' => n' * f n' end. Fixpoint f_tr (n: nat) (acc : nat) := match n with | O => acc | S n' => f_tr n' (acc * n') end. Theorem tail_rec_equiv: forall (n : nat) (p : nat), p * f n = f_tr n p. Proof. intros n. induction n. - intros p. simpl. omega. - simpl. intros p. rewrite <- IHn. rewrite Nat.mul_assoc. auto. Qed.
*1: 僕は詰まりました
まとめ
- [プログラミング言語] Rust to WebAssembly, Made Easy – Lord i/o
- Rust から WebAssembly に変換する方法
- [プログラミング言語] A Taxonomy of Software Smells
- コードスメル (危険度の高いコード) の目録
- [プログラミング言語] Braid
- [プログラミング言語] Fable: JavaScript you can be proud of!
- F# to JS
- [Web] React Mosaic
- React でサイズ可変なウィンドウタイルを作るライブラリ
- [Web] Spirit - The animation tool for the web
- CSS Animation をキーフレームベースで制作するツール。プライベートベータ。
- [Web] Paw – A full-featured visual HTTP client
- [Web] Devhints — TL;DR for developer documentation
- 主に Web 技術に関するチートシート一覧
今週のまとめ
- [プログラミング言語] Ruby の JIT
- mrubyのJITの概要 - Qiita mruby の JIT についてのリンク集
- VMに手を加えずRubyを高速化するJITコンパイラ「YARV-MJIT」の話 - k0kubun's blog
- [プログラミング言語] GitHub - Microsoft/napajs: Napa.js: a multi-threaded JavaScript runtime
- JSのマルチスレッドライブラリ
- Node.js の Cluster に対し、メモリ共有をサポートしているとのこと
- Intro: https://github.com/Microsoft/napajs/wiki/introduction
- [プログラミング言語] Hotswapping Haskell · Simon Marlow
- Haskell プラットフォームでホットスワッピング (Hot code reloading) を行う
- [プログラミング言語] The Zig Programming Language
- AltC 言語
- Rust よりも機能は少なめのように感じた
- [数学] GitHub - hmemcpy/milewski-ctfp-pdf: Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source
- Bartosz Milewski 氏のブログ記事 "Category Theory for Programmers" の PDF 版
- CCなので非公式でこういうことができるの便利
- [セキュリティ] Introducing Miscreant: a multi-language misuse resistant encryption library
- GitHub - miscreant/miscreant: Misuse-resistant symmetric encryption library supporting the AES-SIV (RFC 5297) and CHAIN/STREAM constructions
- AES-CTR のような使い方を間違えて脆弱になるような暗号があるが、そのような誤用に対する耐用性がある暗号 AES-SIV など *1 の実装
- AES-SIV の 日本語の解説記事はここ RFC 5297 AES-SIV モード - Tociyuki::Diary
- [プログラミング言語] 一階の単一化を証明する (PDF)
- [その他] BOOLR | A digital logic simulator
*1: 他のは実装中?
まとめ : Algebraic Effects and Handlers とか
- [プログラミング言語] Recursion Schemes, Part IV: Time is of the Essence
- explains Recursion Schemes, especially futumorphism and histomorphism
- 2年前に書いた dynamorphism の記事も参照 手前味噌 http://45deg.github.io/rogyAdC2015/
- [プログラミング言語] GitHub - Marwes/haskell-compiler: A mostly functional haskell compiler written in rust
[プログラミング言語] Algebraic Effects and Handlers
-
Algebraic effects and handlers provide a modular abstraction for expressing effectful computation, allowing the programmer to separate the expression of an effectful computation from its implementation.
*1- a more modular alternative to monads という人もいたりする。
- Haskeller にとっては Freer モナドでおなじみですね。
- シンプルな例 (擬似コード、Effでの例 → https://gist.github.com/45deg/055cd32e8723ead25a64d8256f292f03)
-
printName = { name <- readLine; print ("hello " . name) }
という副作用のあるプログラム(関数)があったとする。 - ここで
inputJohn = fun e -> match e with readLine () k -> (k "John")
*2 という handler を定義する。これは副作用を制御する関数 (handler)である。- k は継続で元の呼び出し部に帰る。これを discard すれば呼び出し部には戻らない。
- Multicore OCaml 等だと
continue k "John"
という呼び出しをする。
-
handle printName with inputJohn
のように組み合わせるように記述する。この場合 キーボードの入力はされずに "hello john" という文字列が即座に出力される。 - つまり 副作用のあるコードの表現 (the expression of an effectful computation) とその(副作用の)実際の実装 (its implementation)を分離して記述することが出来る抽象化の手法である。
-
- より詳しい例は GitHub - ocamllabs/ocaml-effects-tutorial: Concurrent Programming with Effect Handlers (CUFP'17) が詳しい (OCaml)。演習問題付き。
- 言語: Eff, Koka, Multicore OCaml など
- Multicore OCaml は fiber (coroutine) が concurrency primitive になってるっぽい https://www.cl.cam.ac.uk/~sd601/papers/multicore_slides.pdf
- 参考文献リスト: GitHub - yallop/effects-bibliography: A collaborative bibliography of work related to the theory and practice of computational effects
- 中でも An Introduction to Algebraic Effects and Handlers (MFPS 2015) は入門記事っぽくておすすめ http://www.eff-lang.org/handlers-tutorial.pdf
- 個人的にはテストの時便利そうだなと思った。( IO 等の mock として handler が有効活用できそう )
*1: Effective Concurrency with Algebraic Effects · KC Sivaramakrishnan
*2:e: effect, readLine : unit -> continuation -> unit
まとめ
- [Haskell] Building a CPU with Haskell - Part 1 :: Will Yager
- [Go][モバイル] Matcha - Mobile apps in Go
- [JavaScript] GitHub - cherow/cherow: A fast, Typescript-based ECMAScript parser
- JavaScript 製の ECMAScript パーサ
- パフォーマンスに重点を置いているらしい → Cherow: Speed Comparisons
- [数学] HoTTSQL
- WebSite: Cosette: An Automated SQL Solver
- Paper: https://arxiv.org/abs/1607.04822
- 解説ブログ
- Homotopy Type Theory (ホモトピー型理論)の実用アプリケーション
- アプリは SQL の Equivalence をチェックするツール
- yabai
まとめ
- [ソフトウェア] Uber Open Source - Jaeger
- [アルゴリズム] Pipe Logic
- MOSFET素子を模した実行ファイルとその間のパイプIOで回路っぽいものを作る
- [JavaScript] Jalangi - A Dynamic Analysis Framework for Frontend and Backend JavaScript
- JSのための動的解析ツール
- コードインジェクションしてるっぽい
- [JavaScript] Passport
- Node.js 向けの認証ミドルウェア
- 有名だけど備忘録として
- [OCaml] GitHub - inhabitedtype/angstrom: Parser combinators built for speed and memory efficiency
- OCaml 向けのモナディックパーサ
- 有名だけど(略)
ひとこと:メタプログラミングRuby読んでるけど、この本が優れているのはいかにメタプログラミングをまともなエンジニアリングに組み込むかが主眼になっているということだと思う。単なる Ruby はこんな書き方できるんですよ、変でしょ?で終わってない点がこの本が評価されているゆえんなのかなと思っている。
追記:言語やツールについてのカンファレンスである StrangeLoop というのが最近開かれたらしく、動画がいくつか上がっていた
まとめ (消化)
何週間も更新してないけど特にネタを蓄積したわけでもない。 とりあえずメモに残っていたぶんを放出
- [セキュリティ] Reverse Engineering Malware 102 | Malware Unicorn
- マルウェアの解析(RE)を step-by-step で解説
- How Does a Database Work? | Let’s Build a Simple Database
- http://bittorrent.org/beps/bep_0052.html
- ビットトレントの仕様
- https://aphyr.com/tags/jepsen
- 分散システムのベリフィケーションツールの Jepsen を real-world な例に適用してできた豊富な屍の山。こんなに成果出ると楽しいだろうなぁ
- [プログラミング言語] higher-order-unification/explanation.md at master · jozefg/higher-order-unification · GitHub
- higher-order unification を行う Huet’s algorithm の Haskell 実装での解説