Two-Level積木
変数や式を static（コンパイル時既知）と dynamic（実行時）に色分けし、部分評価で残余プログラムを生成。
部分評価(Partial Evaluation)は、プログラム p と一部の入力 sを受け取り、特殊化された残余プログラム p_s を生成する手法。Jonesらは2レベル言語で binding-time（束縛時刻）を表現し、各部分式を S/D に分類する BTA (Binding-Time Analysis) を行う。
左の式の各トークンを S または D に塗り、右の specializer を実行して、正しく特殊化された残余コードを得よう。
左の式の各トークンを S または D に塗り、右の specializer を実行して、正しく特殊化された残余コードを得よう。
static (コンパイル時に既知 → 評価)
dynamic (実行時にしか分からない → 残余)
BT 矛盾 (D に依存する S は不可)
2-Level プログラム
未注釈のトークンがあります
残余プログラム
— specialize ボタンを押す —
正解! static な部分はコンパイル時に消え、dynamic だけが残った。
これが 第一フタムラ射影:
これが 第一フタムラ射影:
spec(p, s) = p_s。pow(2, x) のような累乗に n=5 を static で食わせると x*x*x*x*x という展開済みコードが残る — 横山研のrev_PE 研究はこの理論基盤(Two-level languages)で可逆性を保つ部分評価器を作っている。
操作
左のコードのトークンをクリックして S/D を塗る。トップのブラシで色を切替。auto BTA ボタンは束縛時刻解析を自動実行（一貫性をチェック）。specialize で残余プログラムを生成。
BTA: τ ::= S | D e^S ⇒ 即時評価 e^D ⇒ 残余コードに残す 制約: D の値に依存する式は S にできないOffline PE は (1) BTA で型注釈 → (2) Specializer が S を消費しコードを生成、の2段階。可逆計算では 残余コードも可逆でなければならず、ヤコビアン保存に対応する制約が加わる。