元は" The 90 minute Scheme to C compiler" Marc Feeley (90-min-scc.pdf) 。元の文章との整合性は保証しないよ。CPS が何かわかって、コンパイラを作ることに興味が出たら幸い。
ただし、これだけではコンパイラはできないよ。Scheme で作りたいなら、http://www.eidos.ic.i.u-tokyo.ac.jp/~tau/lecture/scheme_compiler/gen/resume/all.pdf がおすすめ。
将来的に浮動小数点を含むコンパイラを作りたいなら、あらかじめ OCaml をつかったコンパイラを目指した方がよい(らしい)。
https://esumii.github.io/min-caml/jpaper.pdf
https://github.com/esumii/min-caml
A正規形とK正規形というのもある(らしい)。
http://d.hatena.ne.jp/sumii/20071229/p1
論文のThe Essence of Compiling with Continuations には A 正規形の話があり、CPS が否定されているように思った。
A Multiple Pairs Shortest Path Algorithm 解説Osamu Masutani
?
National Cheng Kung UniversityのWang氏の多点間最短経路探索(MPSP)に関する論文の解説。
Wang, I-Lin, Ellis L. Johnson, and Joel S. Sokol. "A multiple pairs shortest path algorithm." Transportation science 39.4 (2005): 465-476.
Towards formal verification of neural networksMasahiro Sakai
?
- Two vehicle trajectories are presented, with the first being non-colliding and the second colliding
- Methods for predicting vehicle trajectories and determining if collisions may occur are discussed
- Features like position, velocity, acceleration, and interaction between vehicles over time are considered in the analysis
Towards formal verification of neural networksMasahiro Sakai
?
- Two vehicle trajectories are presented, with the first being non-colliding and the second colliding
- Methods for predicting vehicle trajectories and determining if collisions may occur are discussed
- Features like position, velocity, acceleration, and interaction between vehicles over time are considered in the analysis
This document summarizes a presentation on SAT/SMT solving in Haskell. It discusses two main Haskell libraries for SMT solving - sbv, which provides a high-level DSL for specifying SMT problems and interfaces with multiple solvers, and toysolver, which contains the toysat SAT solver and toysmt SMT solver implemented natively in Haskell. It then demonstrates solving the "send more money" puzzle using sbv and running a simple problem on toysmt.
Introduction to Max-SAT and Max-SAT EvaluationMasahiro Sakai
?
This document provides an introduction to Max-SAT and Max-SAT evaluation. It discusses SAT and related problems like Max-SAT and pseudo-boolean optimization. The author shares their experience submitting their solver "toysat" to the Max-SAT evaluation in 2013. For Max-SAT 2014, the author plans to submit improved versions of SCIP, FibreSCIP, and toysat. The document concludes by discussing interactions between AI/CP and OR communities in developing solvers.
1. The document demonstrates how a CDCL SAT solver works on a small example problem with 9 variables and 7 clauses.
2. It shows the step-by-step deductions made by the solver as it decides variable assignments, deduces implications, and detects a conflict.
3. When a conflict is found, the solver performs conflict analysis to determine the reason for the inconsistency and learns a new clause, which is added to its clause database.
“Adoption and Focus: Practical Linear Types for Imperative Programming”他の紹介@P...Masahiro Sakai
?
PLDIr#6 (2010-02-11) での Adoption and Focus: Practical Linear Types for Imperative Programming と MaJIC: Compiling MATLAB for Speed and Responsivenes の紹介。
7. Hot Subpath の解析
WPPは色々な解析に便利
ここでは Hot Subpath の発見を取り上げる
Hot Subpath:
Acyclic subpath の短い列で、実行コストが高い
か、実行頻度が高いかによって、コストの大きい
もの。
特に極小の Hot Subpath を知りたい。
極小でないものは極小のものを拡大すれば得られる
ので
8. Hot Subpath の例
S→AAA a, b, c の実行コストを1と
A→BC して、長さ4未満でコスト
が6以上の hot subpath
B→ab は?
C→bc ? ab, bc, bb, ca
この論文のアルゴリズム
は ab, bc を発见。
bb, ca はこの二つを
extendして得られるとある
abbcabbcabbcのWPP が
と実行回数