mazeppa
v0.4.3
SuperCompilation 1は、特定のプログラムを象徴的に評価するプログラム変換手法であり、実行時の値は不明です。そうすることで、元のプログラムの実行パターンを発見し、それらをスタンドアロン関数に合成します。スーパーコンピレーションの結果は、より効率的な残留プログラムです。変換力の観点から、スーパーコンピレーションは森林破壊2と部分評価3の両方を包含し、定理の特定の能力を示します。
Mazeppaは、価値のある機能言語のコンピレーションターゲットになることを目的としたモダンなスーパーコンピラーです。以前のスーパーコンパイラーが熱心に比較され、修正されたMazeppaを持っています
まず、マシン上のOCAMLシステムを準備してください。
$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup
次に、Mazeppaをopamパッケージとしてインストールします。
$ opam install mazeppa
mazeppa --helpインストールを確認します。
または、リポジトリをクローンして、Mazeppaを手動でインストールすることもできます。
$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh
Flambdaは、OCAMLの強力なプログラムインレーナーおよびスペシャイザーです。 Flambda対応のOCAMLコンパイラを使用してMazeppaを構築すると、パフォーマンスがはるかに優れている場合があります。セットアップするには：
$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)
（必要に応じて5.2.0の代わりに別のバージョンを使用できます。）
Flambdaが正常に有効になっているかどうかを確認するには、実行してください。
$ ocamlopt -config | grep flambda
Mazeppaを実際にインストールせずにプレイできます。 OCAMLがインストールされ、リポジトリがクローン化されました（上記のように）、ルートディレクトリから次のコマンドを実行します。
$ ./scripts/play.sh
（Graphvizが必要： sudo apt install graphviz 。）
これによりplayground/main.mzで--inspectを使用してMazeppaを起動し、 target/graph.svgのプロセスグラフを視覚化します。後者は、SVGプレビュー拡張機能によってVSコードで表示できます。
./scripts/play.sh変更された場合、OCAMLのソースを自動的に再コンパイルします。
スーパーコンピレーションがどのように機能するかを理解する最良の方法は、例とともにです。リストを取得し、その2乗要素の合計を計算する次の関数を考えてみましょう。
[ examples/sum-squares/main.mz ]
main(xs) := sum(mapSq(xs));
sum(xs) := match xs {
Nil() -> 0i32,
Cons(x, xs) -> +(x, sum(xs))
};
mapSq(xs) := match xs {
Nil() -> Nil(),
Cons(x, xs) -> Cons(*(x, x), mapSq(xs))
};
このプログラムは、慣用的でリストフルな機能スタイルで書かれています。すべての関数は1つのことだけを行い、それをうまく行います。ただし、ここには深刻な問題があります。MapsQ mapSq 、基本的にsumによってすぐに分解されるリストを作成します。つまり、1）中間リストに追加のメモリを割り当てる必要があり、2）1つではなく2パスの計算が必要です。この問題の解決策は、森林破壊2と呼ばれます。これは、超競合の特別なケースです。
このプログラムでMazeppaが何をしているのか見てみましょう。
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
--inspectフラグは、Mazeppaに、変換プロセスに関する詳細なレポートを提供するように指示します。 sum-squares/target/ Directoryには、次のファイルが含まれます。
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dotには、プログラムの完全なプロセスグラフが含まれています。 dot -Tsvg target/graph.dot > target/graph.svgを実行して、グラフの画像を取得できます。nodes.jsonは、グラフ内のすべてのノードのコンテンツが含まれています。このファイルがなければ、グラフだけから多くを理解することはできません。program.jsonには、 Mazeppa IR ：当社のスーパーコンピラーでの初期プログラムが含まれています。元のプログラムの代わりに、この特定の表現と連携しています。output.mzには、最終的な残差プログラムが含まれています。 output.mzは次のコードが含まれます。
[ examples/sum-squares/target/output.mz ]
main(xs) := f0(xs);
f0(xs) := match xs {
Cons(x, xs') -> +(*(x, x), f0(xs')),
Nil() -> 0i32
};
SuperCompilerは、 sumとmapSq単一の関数f0に統合しました！元のプログラムとは異なり、 f0追加のメモリを割り当てることなく、単一のパスで動作します。
スーパーコンピラーはどのようにしてこの点に到達しましたか？生成されたプロセスグラフを見てみましょう。
参照のために、 nodes.jsonにはJSONに次のデータが含まれています。
[
[ " n0 " , " main(xs) " ],
[ " n1 " , " sum(mapSq(xs)) " ],
[ " n2 " , " sum(.g1(xs)) " ],
[ " n3 " , " xs " ],
[ " n4 " , " sum(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n5 " , " .g0(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n6 " , " +(*(.v0, .v0), sum(mapSq(.v1))) " ],
[ " n7 " , " +(*(.v0, .v0), sum(.g1(.v1))) " ],
[ " n8 " , " *(.v0, .v0) " ],
[ " n9 " , " .v0 " ],
[ " n10 " , " .v0 " ],
[ " n11 " , " sum(.g1(.v1)) " ],
[ " n12 " , " .v1 " ],
[ " n13 " , " +(.v3, .v4) " ],
[ " n14 " , " .v3 " ],
[ " n15 " , " .v4 " ],
[ " n16 " , " sum(Nil()) " ],
[ " n17 " , " .g0(Nil()) " ],
[ " n18 " , " 0i32 " ]
] （この小さな例については、 program.jsonを検査する必要はありませんが、それを見てください。それはあまり複雑ではありません。）
スーパーコンピラーはmain(xs)を含むノードn0から始まります。 2段階の関数が展開した後、 sum(.g1(xs))を含むノードn2に到達します。ここで、 .g1 mapSqに対応するIR関数です。この時点で、 xs実行時に取る可能性のある値を推測することにより、コール.g1(xs)を分析する以外に選択肢はありません。 mapSqはコンストラクターのNilとConsのみを受け入れるため、ケースxs=Cons(.v0, .v1)およびxs=Nil()のみを考慮するだけで十分です。
ノードn4 、 xsにCons(.v0, .v1)を置き換えた後に起こることです。ここで、 .v0と.v1は新鮮な変数です。さらに3つの機能が展開した後、 n7に到着します。これは、コール+(*(.v0, .v0), sum(.g1(.v1)))を.v3=*(.v0, .v0) （ n8 ）および.v4 = sum +(.v3, .v4) .g1（ n11 .v4=sum(.g1(.v1)) （ n13 ）に分割する必要があるのは初めてです。そうする理由は、以前のノード（ n2 ）がn7に構造的に埋め込まれているため、それ以外の場合はスーパーコンピレーションが永遠に続く可能性があるためです。さて、 sum(.g1(.v1)) （ n11 ）はどうなりますか？以前に見たことがあります！ n2にはsum(.g1(xs)) sum(.g1(.v1))含まれていることを思い出してください。したがって、 n11をn2に折り畳むことにしました。なぜなら、同じことを2回スーパーコンパイルすることは意味がないからです。 n7の他の分岐、つまりn13とn8は分解されます。つまり、単に彼らの引数を変換し続けることを意味します。
n2の他の分岐については、 sum(Nil()) （ n16 ）については、この呼び出しを0i32 （ n18 ）に単に展開するだけで十分です。
プロセスグラフが完了した後、残差はそれを最終プログラムに変換します。この段階では、動的実行パターンは関数になります-Node n2 、他のノード（ n11 ）が指しているように、機能f0になりました。あらゆる残留プログラムでは、破線の破線とmainを備えたノードと同じくらい多くの関数があります。
要約すると、スーパーコンピレーションは1）展開関数定義、2）パターンの不明な変数を一致させる呼び出しの分析、3）計算をより小さな部分に分解し、4）折りたたみ繰り返し計算、および5） +(.v3, .v4) （ n13 ）などの分解コールの分解コールで構成されています。一部の計算が危険なほど大きくなり、より大きくなっている場合、それを分解して単独で解決するため、スーパーコンピレーションプロセス全体が終了することが保証されています。
ツリーのようなデータ構造を含む、 examples/フォルダーには、森林伐採の他の興味深い例がたくさんあります。実際、Peter A. JonssonとJohan Nordlander 4 5による、高次の価値のスーパーコンピレーションに関する以前の研究のすべてのサンプルを再実装しました。すべての場合において、Mazeppaは同様にパフォーマンスを発揮しています。
次に、別の例を考えてみましょう。今回は部分的な評価を含みます。
[ examples/power-sq/main.mz ]
main(a) := powerSq(a, 7u8);
powerSq(a, x) := match =(x, 0u8) {
T() -> 1i32,
F() -> match =(%(x, 2u8), 0u8) {
T() -> square(powerSq(a, /(x, 2u8))),
F() -> *(a, powerSq(a, -(x, 1u8)))
}
};
square(a) := *(a, a);
powerSq 、有名な指数ごとのアルゴリズムを実装します。元のプログラムは非効率的です。PowerSQ powerSq xパラメーターを再帰的に調べますが、コンパイル時間では完全に知られています。 Mazeppaをmain(a)で実行すると、次の残留プログラムが得られます。
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
powerSq関数全体が排除されているため、部分的な評価の効果が達成されます。 （ powerSqプログラムxおよび入力データaのインタープリターであると考える場合、それは最初のファタムラの投影です。効率的なターゲットプログラムを取得するインタープリターを専門とすることです。）また、スーパーコンピラーがどのように議論を共有しているかに注目してください*(a, *(a, a)) 2回、それは毎回再構成されないようにします。残留プログラムは、実際には、二乗による指数を反映しています。
森林破壊と部分的な評価を超えてみましょう。 sがpとF()を含む場合、 T()を返す2つの文字列の関数matches(p, s)考えてみましょう。 Mazeppaでの素朴な実装は次のとおりです。P p "aab"に特化しています。
[ examples/kmp-test/main.mz ]
main(s) := matches(Cons('a', Cons('a', Cons('b', Nil()))), s);
matches(p, s) := go(p, s, p, s);
go(pp, ss, op, os) := match pp {
Nil() -> T(),
Cons(p, pp) -> goFirst(p, pp, ss, op, os)
};
goFirst(p, pp, ss, op, os) := match ss {
Nil() -> F(),
Cons(s, ss) -> match =(p, s) {
T() -> go(pp, ss, op, os),
F() -> failover(op, os)
}
};
failover(op, os) := match os {
Nil() -> F(),
Cons(_s, ss) -> matches(op, ss)
};
（ここでは、単純さのための文字のリストとして文字列を表していますが、心配しないでください、Mazeppaは組み込みの文字列も提供します。）
アルゴリズムは正しいが非効率的です。 "aa" 'b'正常に一致したときに何が起こるかを考えてください。アルゴリズムは、 sの2番目の文字から再び"aab"と一致し始めますが、 sの2番目の文字は'a'であるとすでに言えます。 Knuth-Morris-Prattアルゴリズム（KMP） 6によって構築された決定論的な有限オートマトンは、この問題を解決する代替方法です。
上記のサンプルでMazeppaを実行することにより、動作中のKMPを反映するp="aab"の効率的な文字列マッチングアルゴリズムを取得できます。
[ examples/kmp-test/target/output.mz ]
main(s) := f0(s);
f0(s) := match s {
Cons(s', ss) -> match =(97u8, s') {
F() -> f1(ss),
T() -> f2(ss)
},
Nil() -> F()
};
f1(ss) := f0(ss);
f2(ss) := match ss {
Cons(s, ss') -> match =(97u8, s) {
F() -> f1(ss'),
T() -> f4(ss')
},
Nil() -> F()
};
f3(ss) := f2(ss);
f4(ss) := match ss {
Cons(s, ss') -> match =(98u8, s) {
F() -> match =(97u8, s) {
F() -> f1(ss'),
T() -> f4(ss')
},
T() -> T()
},
Nil() -> F()
};
私たちが書いた素朴なアルゴリズムは、よく知られている効率的なバージョンに自動的に変換されました！ナイーブアルゴリズムには複雑さo（| p | * | s |）がありますが、特殊なものはo（| s |）です。
KMPの合成は、他の技術に関する超競合の力を示す標準的な例です（例えば、 7および8を参照）。 matches 9 10の元の定義を変更せずに、部分評価によってKMPを取得することは不可能です。
スーパーコンピレーションの発明者であるバレンティンターチンは、次の方法でメタシステム遷移の概念を説明しています11 12 13 ：
あらゆる種類のシステムを検討してください。おそらくバリエーションで、そこからいくつかのコピーを作成する方法があると仮定します。これらのシステムは、 Sタイプのシステムをサブシステムとして持つ新しいシステムs 'に統合されており、 Sサブシステムの動作と生成を制御する追加のメカニズムも含まれていると仮定します。次に、Sに関するメタシステムと、 S 'A' A Metasystem遷移の作成と呼びます。連続したメタシステム遷移の結果として、制御のマルチレベル構造が発生し、複雑な形式の動作が可能になります。
したがって、スーパーコンピレーションはメタシステムの遷移として容易に見ることができます。Mazeppaにはオブジェクトプログラムがあり、オブジェクトプログラムの実行を制御および監督するMazeppa Supercompilerがあります。ただし、次の例に示すように、さらに進んで、オブジェクトプログラム自体の領域内で任意の数のメタシステム遷移を実行できます。
examples/lambda-calculus/のコードを使用します。以下は、標準の正規化による標準的な正規化手順です。
normalize(lvl, env, t) := quote(lvl, eval(env, t));
normalizeAt(lvl, env, t) := normalize(+(lvl, 1u64), Cons(vvar(lvl), env), t);
vvar(lvl) := Neutral(NVar(lvl));
eval(env, t) := match t {
Var(idx) -> indexEnv(env, idx),
Lam(body) -> Closure(env, body),
Appl(m, n) ->
let mVal := eval(env, m);
let nVal := eval(env, n);
match mVal {
Closure(env, body) -> eval(Cons(nVal, env), body),
Neutral(nt) -> Neutral(NAppl(nt, nVal))
}
};
quote(lvl, v) := match v {
Closure(env, body) -> Lam(normalizeAt(lvl, env, body)),
Neutral(nt) -> quoteNeutral(lvl, nt)
};
quoteNeutral(lvl, nt) := match nt {
NVar(var) -> Var(-(-(lvl, var), 1u64)),
NAppl(nt, nVal) -> Appl(quoteNeutral(lvl, nt), quote(lvl, nVal))
};
indexEnv(env, idx) := match env {
Nil() -> Panic(++("the variable is unbound: ", string(idx))),
Cons(value, xs) -> match =(idx, 0u64) {
T() -> value,
F() -> indexEnv(xs, -(idx, 1u64))
}
};
（ eval / quote 、 reflect / reifyと呼ばれることもあります。）
これは、基本的に、効率的なキャプチャ承認代替のための大きなステップマシンです。各ベータ削減の用語を再構築する代わりに、値の環境を維持します。 eval 「セマンティックドメイン」に用語をプロジェクトしますが、 quoteは反対のものを行います。 normalize 、単にquoteとevalの構成です。新鮮な名前の生成に悩まされることを避けるために、de bruijnインデックスをVarコンストラクターに、 NVarにde bruijnレベルに配置します。後者は、 quoteNeutralで前者に変換されます。
次に、このマシンで何かを計算しましょう。
main() := normalize(0u64, Nil(), example());
example() := Appl(Appl(mul(), two()), three());
two() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))));
three() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64),
Var(0u64))))));
mul() := Lam(Lam(Lam(Lam(Appl(
Appl(Var(3u64), Appl(Var(2u64), Var(1u64))),
Var(0u64))))));
mainの本体は、教会の数字two() three()を掛けるラムダ語のexample()の通常の形式を計算します。
Supercompiling main()により、6の教会数字が得られます。
[ examples/lambda-calculus/target/output.mz ]
main() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64)
, Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))))))));
Lambda Calculus通訳は完全に消滅しました！
この例では、2レベルのメタシステム階段（ターキンの用語14 ）を見たばかりです。レベル0には、オブジェクトプログラムを変換するMazeppaのスーパーコンピラーがあり、レベル1には、Lambda Calculus用語を正常化するオブジェクトプログラムがあります。任意の数の解釈レベルがあり、Mazeppaを使用してそれらすべてを崩壊させることができます。スーパーコンピレーションのこの一般的な行動は、 1 （セクション7）でターキン自身によって調査され、2つの解釈可能なプログラムをスーパーコンピールすることができました。1つはFortranのように、もう1つはLISPで、両方のケースで40のスピードアップ係数を取得しました。
Lambda Normalizerは、高次関数を1次言語に転生する方法も示しています。 Mazeppaでは、機能を値として扱うことはできませんが、シミュレートできないという意味ではありません。メタシステム遷移を実行することにより、1次言語で高次関数を効率的に実装できます。整理解除と閉鎖変換に加えて、この手法は、高次の言語を効率的な1次コードに編集するために使用できます。
関連例：命令的な仮想マシン、セルフインタープレーター。
振り返ってみると、超競合の広範な採用を妨げた主な問題は、その予測不可能性、つまりその力の暗い側面です。それが何を意味するのかを理解するために、「その場で」のSATの問題をどのように解決できるかを考えてください。
[ examples/sat-solver/main.mz ]
main(a, b, c, d, e, f, g) := solve(formula(a, b, c, d, e, f, g));
formula(a, b, c, d, e, f, g) :=
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Var(e), or(Not(g), F()))),
and(or(Var(e), or(Not(g), or(Var(f), F()))),
and(or(Not(g), or(Var(c), or(Var(d), F()))),
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Not(e), or(Var(g), F()))),
and(or(Var(a), or(Var(a), or(Var(c), F()))),
and(or(Not(g), or(Not(d), or(Not(b), F()))),
T()))))))));
or(x, rest) := match x {
Var(x) -> If(x, T(), rest),
Not(x) -> If(x, rest, T())
};
and(clause, rest) := match clause {
If(x, m, n) -> If(x, and(m, rest), and(n, rest)),
T() -> rest,
F() -> F()
};
solve(formula) := match formula {
If(x, m, n) -> analyze(x, m, n),
T() -> T(),
F() -> F()
};
analyze(x, m, n) := match x {
T() -> solve(m),
F() -> solve(n)
};
この完全に正しいコードには2つの間違いがあります。1）スーパーコンピラーは指数空間で式を拡張し、2）スーパーコンピラーは指数関数的な時間で拡張式を解決しようとします。時には、コンパイル時にすべてを評価したくない場合があります。
しかし、絶望しない：私たちはこの問題の解決策を提供します。まず、実行時までフォーミュラの解決を延期する方法を考えてみましょう。私たちがする必要がある唯一のことは、次のように関数formulaに@extractに注釈を付けることであることがわかります。
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
Mazeppaがsolve(formula(a, b, c, d, e, f, g))見ると、 formulaへの呼び出しを抽出して、新鮮な変数.v0に抽出し、抽出された呼び出しとsolve(.v0)単独で解きます。後者の呼び出しは、元のSATソルバーを再現するだけです。
しかし、 formulaへの呼び出しをスーパーコンピールすると、指数関数的な爆発が生じます。なぜこれが起こるのかを調べてみましょう。私たちのオリジナルの式は、 or andの呼び出しで構成されています。一方or明らかに危険ではなくand restパラメーターをIf （最初のmatchケース）の両方のブランチに伝播します。これは、爆発が発生する正確な場所です。それでは、 @extractをマークandてみましょう。
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
それです！変換されるand 、Mazeppaは周囲のコンテキストから呼び出しを抽出し、それを単独で超競争させます。適切な場所に2つの注釈を追加することにより、コード爆発の問題とスーパーコンピレーションの指数関数的な実行時間の両方を解決しました。一般に、Mazeppaがctx[f(t1, ..., tN)]を見るときはいつでも、 fは@extractとctx[.]は、空の周囲のコンテキストではありません. Redexの位置では、新鮮な変数vをctxに接続し、次のノードを個別に変換します： f(t1, ..., tN)およびctx[v] 。
最後に、 @extract低レベルのメカニズムにすぎないことに注意してください。コンパイラのフロントエンドは、追加の機械を抽出する機能をMazeppaに伝える必要があります。これは2つの方法で実行できます。
formula and抽出可能な式の両方をマークし、他のすべての機能を触れられないままにします。両方の方法を組み合わせて、望ましい効果を達成できます。
Mazeppaは、熱心な機能と怠zyなコンストラクターを持つために、興味深いデザインの選択肢を採用しています。次の例では、 magic(1u32, 1u32)がフィボナッチ数を生成する場所は、Haskellから採用されました。
[ examples/lazy-fibonacci/main.mz ]
main() := getIt(magic(1u32, 1u32), 3u64);
magic(m, n) := match =(m, 0u32) {
T() -> Nil(),
F() -> Cons(m, magic(n, +(m, n)))
};
getIt(xs, n) := match xs {
Nil() -> Panic("undefined"),
Cons(x, xs) -> match =(n, 1u64) {
T() -> x,
F() -> getIt(xs, -(n, 1u64))
}
};
コンストラクターが熱心であれば、 magic(1u32, 1u32)決して終了しません。ただし、 Consその議論を評価しません！ getIt無限のリストの有限部分のみを消費しているため、プログラムは2u32終了および印刷します。
$ mazeppa eval
2u32
怠zyなコンストラクターは、以下で説明するように、楽な森林伐採を可能にします。
opamまたは./scripts/install.shを介してMazeppaをインストールした後、OCAMLライブラリとして利用できます！
次のように新しい砂丘プロジェクトを設定します。
$ dune init project my_compiler
mazeppaサードパーティライブラリとしてbin/duneに追加します。
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
次のコードをbin/main.mlに貼り付けます（これは、ocamlでエンコードされたexamples/sum-squares/main.mzです）：
open Mazeppa
let input : Raw_program.t =
let sym = Symbol. of_string in
let open Raw_term in
let open Checked_oint in
[ [], sym " main " , [ sym " xs " ], call ( " sum " , [ call ( " mapSq " , [ var " xs " ]) ])
; ( []
, sym " sum "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), int ( I32 ( I32. of_int_exn 0 ))
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call ( " + " , [ var " x " ; call ( " sum " , [ var " xs " ]) ]) )
] ) )
; ( []
, sym " mapSq "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), call ( " Nil " , [] )
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call
( " Cons "
, [ call ( " * " , [ var " x " ; var " x " ]); call ( " mapSq " , [ var " xs " ]) ] ) )
] ) )
]
;;
let () =
try
let output = Mazeppa. supercompile input in
Printf. printf " %s n " ( Raw_program. show output)
with
| Mazeppa. Panic msg ->
Printf. eprintf " Something went wrong: %s n " msg;
exit 1
;; dune exec my_compilerを実行して、目的の残差プログラムを確認します。
[([], "main", ["xs"], (Raw_term.Call ("f0", [(Raw_term.Var "xs")])));
([], "f0", ["xs"],
(Raw_term.Match ((Raw_term.Var "xs"),
[(("Cons", ["x"; "xs'"]),
(Raw_term.Call ("+",
[(Raw_term.Call ("*", [(Raw_term.Var "x"); (Raw_term.Var "x")]));
(Raw_term.Call ("f0", [(Raw_term.Var "xs'")]))]
)));
(("Nil", []), (Raw_term.Const (Const.Int (Checked_oint.I32 0))))]
)))
]
並列を含めて、あなたが望むだけ何度もMazeppaを呼び出すことができます。限られたインターフェイスをスーパーコンパイラーに公開することに注意してください。特に、プロセスで何をするかを検査する方法はありません（つまり、 --inspect ）。
スーパーコンピレーションに加えて、組み込みの評価者も提供します。
val eval : Raw_program .t -> Raw_term .t main関数がパラメーターを受け入れないプログラムでのみ呼び出すことができます。 supercompileとは異なり、 Raw_term.t型の評価された用語を生成し、おそらく分岐する可能性があります。
lib/mazeppa.mliの他のAPI関数とそのドキュメントを参照してください。
main.mzに、怠zyなフィボナッチのわずかに変更されたバージョンが含まれていると仮定します。
main(n) := getIt(magic(1u32, 1u32), n);
magic(m, n) := match =(m, 0u32) {
T() -> Nil(),
F() -> Cons(m, magic(n, +(m, n)))
};
getIt(xs, n) := match xs {
Nil() -> Panic("undefined"),
Cons(x, xs) -> match =(n, 1u64) {
T() -> x,
F() -> getIt(xs, -(n, 1u64))
}
};
次のコマンドは、GNU拡張機能（つまり、 -std=gnu11 ）を使用してC11に翻訳します。
$ cat main.mz | mazeppa translate --language C --entry fib
#include "mazeppa.h"
MZ_ENUM_USER_TAGS ( op_Cons , op_Nil );
static mz_Value op_main ( mz_ArgsPtr args );
static mz_Value op_magic ( mz_ArgsPtr args );
static mz_Value op_getIt ( mz_ArgsPtr args );
static mz_Value thunk_0 ( mz_EnvPtr env ) {
mz_Value var_m = ( env )[ 0 ];
mz_Value var_n = ( env )[ 1 ];
return ({
struct mz_value args [ 2 ];
( args )[ 0 ] = var_n ;
( args )[ 1 ] = MZ_OP2 ( var_m , add , var_n );
op_magic ( args );
});
}
static mz_Value op_main ( mz_ArgsPtr args ) {
mz_Value var_n = ( args )[ 0 ];
return ({
struct mz_value args [ 2 ];
( args )[ 0 ] = ({
struct mz_value args [ 2 ];
( args )[ 0 ] = MZ_INT ( U , 32 , UINT32_C ( 1 ));
( args )[ 1 ] = MZ_INT ( U , 32 , UINT32_C ( 1 ));
op_magic ( args );
});
( args )[ 1 ] = var_n ;
op_getIt ( args );
});
}
static mz_Value op_magic ( mz_ArgsPtr args ) {
mz_Value var_m = ( args )[ 0 ];
mz_Value var_n = ( args )[ 1 ];
return ({
struct mz_value tmp = MZ_OP2 ( var_m , equal , MZ_INT ( U , 32 , UINT32_C ( 0 )));
switch (( tmp ). tag ) {
case op_T : {
tmp = MZ_EMPTY_DATA ( op_Nil );
break ;
}
case op_F : {
tmp = MZ_DATA ( op_Cons , 2 , MZ_SIMPLE_THUNK ( var_m ), MZ_THUNK ( thunk_0 , 2 , var_m , var_n ));
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
}
static mz_Value op_getIt ( mz_ArgsPtr args ) {
mz_Value var_xs = ( args )[ 0 ];
mz_Value var_n = ( args )[ 1 ];
return ({
struct mz_value tmp = var_xs ;
switch (( tmp ). tag ) {
case op_Nil : {
tmp = mz_panic ( MZ_STRING ( "undefined" ));
break ;
}
case op_Cons : {
mz_Value var_x = (( tmp ). payload )[ 0 ];
mz_Value var_xs$ = (( tmp ). payload )[ 1 ];
tmp = ({
struct mz_value tmp = MZ_OP2 ( var_n , equal , MZ_INT ( U , 64 , UINT64_C ( 1 )));
switch (( tmp ). tag ) {
case op_T : {
tmp = mz_force ( var_x );
break ;
}
case op_F : {
tmp = ({
struct mz_value args [ 2 ];
( args )[ 0 ] = mz_force ( var_xs$ );
( args )[ 1 ] = MZ_OP2 ( var_n , sub , MZ_INT ( U , 64 , UINT64_C ( 1 )));
op_getIt ( args );
});
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
}
extern mz_Value fib ( mz_Value var_n ) {
return MZ_CALL_MAIN ( var_n );
} translateコマンドには、翻訳--entryターゲット言語である--languageと、 main関数に対応する外部シンボルの名前である両方の両方が必要です。入力Mazeppaプログラムは、 stdin （私たちの例ではcat main.mz ）からのものです。出力GNU11プログラムはstdoutに書き込まれます。
さらに進んで、出力プログラムをオブジェクトファイルにコンパイルしましょう。まず、 c/deps/sds.c 、 c/deps/sds.h 、およびc/deps/sdsalloc.hを現在のディレクトリにコピーします。次に、コンピューターにBoehm GCをインストールします。
$ sudo apt install libgc-dev -y
次に、次のコマンドを実行します。
$ cat main.mz
| mazeppa translate --language C --entry fib --dump-header-to .
| gcc -c -o program.o -std=gnu11 -xc -
--dump-header-toオプションは、 mazeppa.hのコンテンツを指定された場所に書き込みます。これは、出力プログラムがコンパイルするために必要です。 gccコマンドは、 stdinから出力プログラムを受け入れ、 program.oを作成します。
残っているのは、実際に生成されたfib関数を呼び出すことです。次のコンテンツでmain.cを作成します。
#include "mazeppa.h"
mz_Value fib ( mz_Value n );
int main ( void ) {
// Always initialize Boehm GC before invoking Mazeppa code.
GC_INIT ();
mz_Value v = fib ( MZ_INT ( U , 64 , 10 ));
printf ( "fib(10) = %" PRIu32 "n" , MZ_GET ( U32 , v ));
}この「ドライバー」プログラムは、Mazeppa Integer（ MZ_INT ）でfibを呼び出し、結果を印刷します。 mz_priv_またはMZ_PRIV_が付いていない場合、 mazeppa.hの機能を使用できます。
すべてのピースをまとめるには：
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out Prints fib(10) = 55および予想通り出口。
--inspect実際の環境に注目してください：デバッグ目的でのみ使用してください。@extract （上記のように）を使用して、スーパーコンピレーションを継続するか、redexを抽出するかを制御します。"otus"は"octopus"よりも小さいが、 "octopusx"そうではない。 Mazeppaは、いくつかの興味深いデザインの選択肢を採用しています（重要性によってランク付けされています）：
一次コード。 Max BolingbrokeとSimon Peyton Jones 15は、1つの特定の例で、Haskellのサブセットの高次スーパーコンピラーは、実行時間の42％を名前の管理と名前変更に費やしたと報告しています。ラムダの用語の正規化などの単純な評価モデルにより、キャプチャ回避の大幅なオーバーヘッドを回避できるようにすることは事実ですが、超強化はより複雑です。たとえば、シンボリック計算を行うことに加えて、スーパーコンピレーションは、以前に計算された結果を分析して、さらなる変換について情報に基づいた決定を下す必要があります。タームインスタンステスト、ホメオモーフィック埋め込みテスト、最も具体的な一般化などを検討します。 Mazeppaでは、漸進的な改善の哲学に固執します。多くの派手な機能を同時に処理しようとする代わりに、1）マシンによる便利な操作のためにコア言語を修正し、2）人間のコア言語をより良くするために必要な数のメタシステム遷移を実行します。
怠zyなコンストラクター。それは、価値のある言語が適切な森林破壊のために困難であるというよく知られている観察です。それらを森林破壊することはまだ可能ですが、追加の分析がないわけではありません4 5 。ただし、コンストラクターが怠zyである場合（つまり、彼らは彼らの議論を評価しません）、森林破壊はただ機能します。 Turchinは、価値のある言語の通常の注文変換によって機能しましたが、その結果、残差コードがより頻繁に終了する可能性があります。 Mazeppaでは、コールバイの価値関数とコールバイネーム（コールバイ）コンストラクターがあります。
タームフリープロセスグラフ。 Mazeppaでは、プロセスグラフには用語への参照が含まれていません。残差はそれらなしでは機能します。その結果、ゴミコレクターは、サブグラフの構築中に使用された用語を扱うことができます。さらに、このポリシーには他のいくつかの重要な利点があります。1）グラフは、検査のためにまだ存在しています--inspect 、2）描画された場合、スーパーコンピラーが行った決定に関する情報のみを明らかにします。いくつかの既存のスーパーコンピラーは、適切なプロセスグラフ（たとえば、ニールミッチェルのスーパー17および前述の15 ）を控えていますが、その結果、1）ユーザーによる検査が少ない、2）アルゴリズムはコード生成の詳細で乱雑になります。
二次元構成分析。通常、スーパーコンピラーは、ノードを変換しながら、すべての先祖のサブセットの「歴史」を保持します。このノードが祖先の1人に「十分に近い」場合、終了を保証するために用語をより小さな部分に分割する時が来ます。 Mazeppaでは、代わりに2つの別々のデータ構造を保持します。ノードの祖先のサブセットを含むものと、完全に変換されたノードのサブセットを含むものです。前者のデータ構造は（通常のように）終了を保証するために使用されますが、後者は残差コードの関数の共有を強化するために使用されます。具体的には、（特別な種類の）現在のノードが、以前に変換されたいくつかのノードの名前を変更している場合、現在のノードをこの前のノードに折ります。このようにして、Mazeppaは構成の垂直分析と水平分析の両方を実行し、残差コードをよりコンパクトでスーパーコンピレーションにより効率的にします。
機能生産性分析。内部関数コールパターンが未知の値を一致させると、2つの潜在的に危険なことが起こります。1）スーパーコンピレーションはパターンマッチング関数の構造を再現します。さらなる制御がなければ、この状況はコードサイズの大幅な爆発につながる可能性があり、時にはスーパーコンピラーが合理的な時間で終了しないようにすることさえあります。改善するために、Mazeppaはコンテキストを複製し、この内部呼び出しが少なくとも1つの出口ポイントから明確なトップレベルの値を生成します。もしそうなら、この値が後続のパターンマッチングによって解体される可能性が高いからです。それ以外の場合、Mazeppaは内部呼び出しを抽出し、それを単独で変換します（まるで@extractでマークされているかのように）。さらに、コンテキストが実際に複製されている場合、次のルールがすべてのブランチに適用されます。ブランチがすべての出口ポイントから明確なトップレベルの値を生成する場合、通常のコンテキストで変換されます。それ以外の場合、ブランチはコンテキストから抽出され、単独で変換されます。実際には、この分析は膨大な量の不必要な専門分野を防ぎ、それにより残留プログラムのサイズを圧縮し、スーパーコンピレーションをはるかに扱いやすくします。
スマートヒストリー。現在のノードをすべての祖先と盲目的に比較する代わりに、よりきめ細かいコントロール、つまり、1）グローバルノード（未知の変数を分析するもの）は、グローバルノードのみと比較されます。コンポーネント）は他のものと比較されません。終了チェックに対するより経済的なアプローチに加えて、このスキームにより、Mazeppaはより多くの最適化の機会を発見することができます。 18 、セクション4.6および4.7を参照してください。スーパーコンピレーションの終了は、ホモモルフィック埋め込みが、グローバルおよびローカル用語のすべての潜在的に無限のサブシーケンスで依然としてテストされているという事実によって保証されます（些細な用語のみの無限のシーケンスは存在できません）。
redex署名。ホイッスルは、同等のredex署名を持つ条件でのみテストされます。 redexの署名は、1）関数のシンボルと2）引数値カテゴリのリストのペアです。値カテゴリとは、引数に関する一種のメテン形成であり、 42i32または"hello world"などの値の1） VConst 、 xまたは+(x, x) 、または3） VCCall(c)のVNeutral Foo(...) 。ホイッスルは、すべての潜在的に無限の項シーケンスでテストされています。これは、無限のシーケンスには、同じredex署名を持つ項の少なくとも1つの無限のサブシーケンスが含まれている必要があるためです。この戦略により、次の2つの例が示しているように、特定の場合にはMazeppaが過剰な世紀化を回避できます。
f(A()) f(g(B(A())))に同質的に埋め込まれています。ただし、Redex演算子は異なるため（ fとg ）、Mazeppaは削減を続け、理想的な結果に達します。f(A(Good()))はf(f(f(B(A(Good())))))に埋め込まれていますが、どちらの場合もredex演算子はfになりますがA(...) fは過剰にB(...)にしません。前の例と同様に、Mazeppaは、削減だけで超強化の理想的な結果に達します。最適化された同質埋め込み。数十年にわたり、同質の埋め込みは、オンライン解雇チェック19の優れた方法であるという評判を得ています。残念ながら、主に非線形制御フロー（ダイビングとカップリングの両方が適用される場合）が原因で、計算するのに許されない可能性があります。さらに悪いことに、新しい用語が歴史に追加されるたびに、すべての資格のある親ノードが再実行されます。これは、歴史が成長するにつれて徐々にスーパーコンピレーションを遅くします。それに対処するために、2つの別々のキャッシュを維持します。
ハッシュコンスト。上記のホモモルフィック埋め込みキャッシュは、共有される用語の数に依存します。したがって、機能体の展開中にハッシュ分析を使用します。いくつかの新しい用語tが既存の用語Sに構造的に等しい場合、後者は再利用されます。メモリリークを避けるために、私たちは弱いポインターを用語に保持しているグローバルなエフェメロンを採用しています。 （メモ化による）スーパーコンピレーション時間の改善に加えて、ハッシュセンシングはメモリ消費も減少させます - ＃4（コメント）を参照してください。
展開中の正規化。関数呼び出しが展開されると、パラメーターを代用し、できるだけ体を正規化します（つまり、さらに展開することなく、終了を保証します）。理由を確認するには、因子関数f(n)を考慮してください。単純な展開を使用すると、 f(1u32)が*(1u32, f(-(1u32, 1u32)))に埋め込まれ、過剰なジェネラル化を引き起こす不快な状況に閉じ込められます。実際には、Mazeppaはf(1u32)を*(1u32, f(0u32))に展開し、後者をさらに展開する候補にします。このアプローチは、 20 、セクション4.5で提案されました。その他のメリットは次のとおりです。1）将来の運転手順の少ない作業、2）プロセスグラフでの「平凡な」計算、3）高価な同性愛埋め込みテストの量の減少。
*(1u32, f(-(1u32, 1u32)))異なるRedex演算子のためにf(1u32)に対してチェックされなくなります。ただし、正規化の他の利点はまだ当てはまります。OCAMLでの実装。 Mazeppaは、OCAMLで行うのは非常に自然な機能的および命令的なプログラミングスタイルの組み合わせを使用して実装されています。例外は、「例外的な」状況だけでなく、関数内の可変性が一般的です。比較のためにHaskellやRustなどの同様のスーパーコンピラーはありませんが、言語と口論して作業を終わらせることなく、私たちに実用的な実装を与えたのはOCAMLであると信じています。
上記のほとんどは特に斬新ではありませんが、これらの機能の組み合わせにより、Mazeppaは前任者よりも実用的な代替品になると考えています。
A symbol <SYMBOL> is a sequence of letters ( a , ... , z and A , ... , Z ) and digits ( 0 , ... , 9 ), followed by an optional question mark ( ? ), followed by an optional sequence of ' characters. The underscore character ( _ ) may be the first character of a symbol, which may informally indicate that the value or function being defined is not used; otherwise, the first character must be a letter. The following sequences of characters are also permitted as symbols: ~ , # , + , - , * , / , % , | , & , ^ , << , >> , = , != , > , >= , < , <= , ++ . The following are reserved words that may not be used as symbols: match , let .
There are four classes of unsigned integer constants :
0b ( 0B ) followed by a non-empty sequence of binary digits 0 and 1 .0o ( 0O ) followed by a non-empty sequence of octal digits 0 , ... , 7 .0 , ... , 9 .0x ( 0X ) followed by a non-empty sequence of decimal digits 0 , ... , 9 and letters a , ... , f ( A , ... , F ).注：
_ ) except for the first position in the sequence of digits.- ) placed right before the sequence of digits and underscore characters.<INT> produced by appending an integer type <INT-TY> ( u8 , u16 , u32 , u64 , u128 , i8 , i16 , i32 , i64 , i128 ) right after the original integer constant. For example, the constants 123i8 , 123u16 , and 123i32 all belong to the set <INT> . A string constant <STRING> is a sequence, between double quotes ( " ), of zero or more printable characters (we refer to printable characters as those numbered 33-126 in the ASCII character set), spaces, or string escape sequences :
| Escape sequence | 意味 |
|---|---|
f | Form feed (ASCII 12) |
n | Line feed (ASCII 10) |
r | Carriage return (ASCII 13) |
t | Horizontal tab (ASCII 9) |
v | Vertical tab (ASCII 11) |
xhh | ASCII code in hexadecimal |
" | " |
\ | |
where h is either 0 , ... , 9 or a , ... , f or A , ... , F .
A character constant <CHAR> is either a sole character enclosed in single quotes ( ' ) or a character escape sequence enclosed in single quotes. The character escape sequence is the same as for strings, except that " is replaced by ' .
There are no other constants in Mazeppa.
A comment <COMMENT> is any sequence of characters after // , which is terminated by a newline character. (We only allow single-line comments for simplicity.)
The entry point <program> is defined by the following rules:
<def-attr-list> <SYMBOL> ( <SYMBOL> , ... , <SYMBOL> ) := <term> ; <program><COMMENT> <program> where <def-attr-list> is a whitespace-separated sequence of function attributes (the same attribute can occur multiple times). Right now, the only allowed function attribute is @extract .
<term> is defined as follows:
<SYMBOL> (a variable)<const> (a constant)<SYMBOL> ( <term> , ... , <term> ) (a function call)match <term> { <match-case> , ... , <match-case> } (pattern matching)let <SYMBOL> := <term> ; <term> (a let-binding)let <pattern> := <term> ; <term> (a pattern let-binding)<COMMENT> <term> (a comment)The rest of the auxiliary rules are:
<const> :
<INT> or <STRING> or <CHAR> . <match-case> :
<pattern> -> <term> <pattern> :
<SYMBOL> ( <SYMBOL> , ... , <SYMBOL> ) . In Mazeppa, primitive operations employ the same syntax as that of ordinary function calls. To distinguish between the two, we define <op1> and <op2> to be the following sets of symbols:
<op1> is one of ~ , # , length , string , <INT-TY> .<op2> is one of + , - , * , / , % , | , & , ^ , << , >> , = , != , > , >= , < , <= , ++ , get . Furthermore, <op2> has the following subclasses:
<arith-op2> is one of + , - , * , / , % , | , & , ^ , << , >> .<cmp-op2> is one of = , != , > , >= , < , <= .<op1> or <op2> . 2) A function must define a symbol starting with a lowercase letter. 3) No duplicate symbols can occur among function parameters. 4) Every free variable inside a function body must be bound by a corresponding parameter in the function definition.match { ... } must not be empty. 2) No duplicate constructors can occur among case patterns in match { ... } . 3) No duplicate symbols can occur among pattern parameters C(x1, ..., xN) . 4) No let-binding can bind <op1> or <op2> . 5) Panic must be called with only one argument; T and F with zero arguments.If a program, function, or term conforms to these restrictions, we call it well-formed .
| 原形 | Desugared form | メモ |
|---|---|---|
// ... rest | rest | rest is in <program> or <term> |
let p := t; u | match t { p -> u } | p is in <pattern> |
c | ASCII(c) | c is in <CHAR> |
where ASCII(c) is an appropriate u8 integer constant, according to the ASCII table; for example, ASCII( 'a' ) is 97u8 .
Suppose that t is a well-formed term closed under environment env (defined below) and program is a well-formed program. Then the evaluation of t is governed by the following big-step environment machine:
eval(env, x) = eval({ }, env(x))eval(env, const) = const , where const is in <const> .eval(env, f(t1, ..., tN)) =t1Val ^= eval(env, t1)tNVal ^= eval(env, tN)eval({ x1 -> t1Val, ..., xN -> tNVal }, body) , where f(x1, ..., xN) := body; is in program .eval(env, C(t1, ..., tN)) = C(t1[env], ..., tN[env]) , where C starts with an uppercase letter.eval(env, op(t)) =tVal ^= eval(env, t)evalOp1(op, tVal) , where op is in <op1> .eval(env, op(t1, t2)) =t1Val ^= eval(env, t1)t2Val ^= eval(env, t2)evalOp2(t1Val, op, t2Val) , where op is in <op2> .eval(env, match t { p1 -> t1, ..., pN -> tN }) =Ci(s1, ..., sN) ^= eval(env, t)eval(env', tI) , whereCi(x1, ..., xN) -> tI is among the rules in match t { ... } , andenv' is env[x1 -> s1, ..., xN -> sN] .eval(env, let x := t; u) =tVal ^= eval(env, t)eval(env[x -> tVal], u)Notation:
env is a total environment over t , whose general form is { x1 -> t1, ..., xN -> tN } . Each tI term must be closed and well-formed; this property is preserved by eval .env(x) is tI , where x -> tI is in env .env[x1 -> t1, ..., xN -> tN] is the environment env extended with new bindings x1 -> t1 , ... , xN -> tN . If some xI is already bound in env , it is rebound.t[env] denotes a simultaneous substitution of all free variables in t by their bound values in env .tVal ^= eval(env, t) evaluates t under env ;それから：Panic(t') , the result of the whole evaluation rule is Panic(t') .tVal is available for the next clauses. (Note that eval is a partial function, so evaluation of t can "get stuck" without a superimposed type system.)
In what follows, 1) signed integers are represented in two's complement notation, 2) panic denotes Panic(s) , where s is some (possibly varying) implementation-defined string constant.
evalOp1 takes care of the unary operators for primitive types ( x is in <INT> , s is in <STRING> ):
evalOp1(~, x) is the bitwise negation of x of the same type.evalOp1(string, x) is the string representation of x (in decimal).evalOp1(ty, x) , where ty is in <INT-TY> , is x converted to an integer of type ty .x is not in the range of ty , the result is panic .evalOp1(#, x) , where x is a u8 integer, is a string containing only the ASCII character of x .x is not printable, the result takes the form "xhh" .evalOp1(length, s) is a u64 integer denoting the length of s .evalOp1(string, s) is s . Likewise, evalOp2 takes care of the binary operators for primitive types:
evalOp2(x, op, y) , where x and y have the same integer type and op is in <arith-op2> , performs a corresponding arithmetic operation on x and y , yielding a value of the same type as that of x and y .evalOp2(x, op, y) , where x and y have the same integer type and op is in <cmp-op2> , performs a corresponding comparison operation on x and y , yielding either T() or F() .evalOp2(s1, op, s2) , where s1 and s2 are strings and op is in <cmp-op2> , performs a corresponding lexicographical comparison on s1 and s2 , yielding either T() or F() .evalOp2(s1, ++, s2) is the concatenation of s1 and s2 .evalOp2(s, get, idx) , where idx is a u64 integer, is the idx -th character (of type u8 ) of s .idx is out of bounds, the result is panic . The definition of eval is now complete.
version field in dune-project and bin/main.ml .dune build to generate mazeppa.opam .CHANGELOG.md .Not yet, we need to battle-test Mazeppa on some actual programming language. Our long-term goal is to find suitable heuristics to profitably supercompile any source file under 10'000 LoC (in Mazeppa).
For debugging and other purposes, we provide a built-in definitional interpreter that can execute Mazeppa programs. You can launch it by typing mazeppa eval (make sure that your main function does not accept parameters). For the purpose of real execution, we recommend translating Mazeppa to C and then compiling C to machine code, as shown above.
Since Mazeppa is a purely functional language, the only way to implement I/O is as in Haskell 23 : having a pure program that performs computation and a dirty runtime that performs side effects issued by the program. There are no plans to introduce direct I/O into Mazeppa: it will only make everything more complicated.
No, we do not think that a type system is necessary at this point. It is the responsibility of a front-end compiler to ensure that programs do not "go wrong".
The more we make supercompilation predictable, the less it is capable of theorem proving. For those interested in program analysis rather than optimization, we suggest looking into distillation 24 .
For the English audience, the following paper presents a decent introduction into supercompilation:
However, the following papers in Russian describe a supercompilation model that is closer the majority of existing supercompilers, including Mazeppa:
Mazeppa itself is inspired by this excellent paper (in English):
Finally, the international META workshops are great collections of articles about supercompilation and adjacent fields:
Several approaches can lead to superlinear speedup of non-esoteric programs by supercompilation:
None of the above is planned to be implemented in Mazeppa, because 1) we think that writing asymptotically good programs is the responsibility of the programmer, not the optimizer, and 2) predictability of supercompilation is of greater importance to us. However, for those who are interested in this topic, the references may be helpful.
Just fork the repository, work in your own branch, and submit a pull request. Prefer rebasing when introducing changes to keep the commit history as clean as possible.
Valentin F. Turchin. 1986. The concept of a supercompiler. ACM Trans.プログラム。 Lang. Syst. 8, 3 (July 1986), 292–325. https://doi.org/10.1145/5956.5957 ↩ ↩ 2
Philip Wadler. 1988. Deforestation: transforming programs to eliminate trees. Theor. Comput. SCI。 73, 2 (June 22, 1990), 231–248. https://doi.org/10.1016/0304-3975(90)90147-A ↩ ↩ 2
Futamura, Y. (1983). Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds) RIMS Symposia on Software Science and Engineering. Lecture Notes in Computer Science, vol 147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11980-9_13 ↩
Peter A. Jonsson and Johan Nordlander. 2009. Positive supercompilation for a higher order call-by-value language. SIGPLAN Not. 44, 1 (January 2009), 277–288. https://doi.org/10.1145/1594834.1480916 ↩ ↩ 2
Jonsson, Peter & Nordlander, Johan. （2010）。 Strengthening supercompilation for call-by-value languages. ↩ ↩ 2
DE Knuth, JH Morris, and VR Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6:page 323 (1977). ↩
Glück, R., Klimov, AV (1993). Occam's razor in metacomputation: the notion of a perfect process tree. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_34 ↩
Sørensen MH, Glück R, Jones ND. A positive supercompiler. Journal of Functional Programming. 1996;6(6):811-838. doi:10.1017/S0956796800002008 ↩
Consel, Charles, and Olivier Danvy. "Partial evaluation of pattern matching in strings." Information Processing Letters 30.2 (1989): 79-86. ↩
Jones, Neil & Gomard, Carsten & Sestoft, Peter. （1993）。 Partial Evaluation and Automatic Program Generation. ↩
Turchin, VF (1996). Metacomputation: Metasystem transitions plus supercompilation. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_24 ↩
Turchin, Valentin F. "Program transformation with metasystem transitions." Journal of Functional Programming 3.3 (1993): 283-313. ↩
Turchin, Valentin F.. “A dialogue on Metasystem transition.” World Futures 45 (1995): 5-57. ↩
Turchin, V., and A. Nemytykh. Metavariables: Their implementation and use in Program Transformation. CCNY Technical Report CSc TR-95-012, 1995. ↩
Maximilian Bolingbroke and Simon Peyton Jones. 2010. Supercompilation by evaluation. In Proceedings of the third ACM Haskell symposium on Haskell (Haskell '10). Association for Computing Machinery, New York, NY, USA, 135–146. https://doi.org/10.1145/1863523.1863540 ↩ ↩ 2
Friedman, Daniel P. and David S. Wise. “CONS Should Not Evaluate its Arguments.” International Colloquium on Automata, Languages and Programming (1976). ↩
Mitchell, Neil. “Rethinking supercompilation.” ACM SIGPLAN International Conference on Functional Programming (2010). ↩
Sørensen, MHB (1998). Convergence of program transformers in the metric space of trees. In: Jeuring, J. (eds) Mathematics of Program Construction. MPC 1998. Lecture Notes in Computer Science, vol 1422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054297 ↩
Leuschel, Michael. "Homeomorphic embedding for online termination of symbolic methods." The essence of computation: complexity, analysis, transformation (2002): 379-403. ↩
Jonsson, Peter & Nordlander, Johan. （2011）。 Taming code explosion in supercompilation. PERM'11 - Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. 33-42. 10.1145/1929501.1929507. ↩ ↩ 2
Tejiščák, Matúš. Erasure in dependently typed programming. Diss. University of St Andrews, 2020. ↩
Glück, Robert, Andrei Klimov, and Antonina Nepeivoda. "Nonlinear Configurations for Superlinear Speedup by Supercompilation." Fifth International Valentin Turchin Workshop on Metacomputation. 2016. ↩
Peyton Jones, Simon. （2002）。 Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. ↩
GW Hamilton. 2006. Poitín: Distilling Theorems From Conjectures.電子。 Notes Theor. Comput. SCI。 151, 1 (March, 2006), 143–160. https://doi.org/10.1016/j.entcs.2005.11.028 ↩
Klyuchnikov, Ilya, and Dimitur Krustev. "Supercompilation: Ideas and methods." The Monad. Reader Issue 23 (2014): 17. ↩
Klimov, Andrei & Romanenko, Sergei. （2018）。 Supercompilation: main principles and basic concepts. Keldysh Institute Preprints. 1-36. 10.20948/prepr-2018-111. ↩
Romanenko, Sergei. （2018）。 Supercompilation: homeomorphic embedding, call-by-name, partial evaluation. Keldysh Institute Preprints. 1-32. 10.20948/prepr-2018-209. ↩
Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. https://dl.acm.org/doi/10.5555/647372.724040 ↩
Secher, JP (2001). Driving in the Jungle. In: Danvy, O., Filinski, A. (eds) Programs as Data Objects. PADO 2001. Lecture Notes in Computer Science, vol 2053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44978-7_12 ↩
Hoffmann, B., Plump, D. (1988). Jungle evaluation for efficient term rewriting. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_71 ↩
Hamilton, Geoff. （2007）。 Distillation: Extracting the essence of programs. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. 61-70. 10.1145/1244381.1244391. ↩
Hamilton, GW (2010). Extracting the Essence of Distillation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_13 ↩
Hamilton, Geoff & Mendel-Gleason, Gavin. （2010）。 A Graph-Based Definition of Distillation. ↩
Hamilton, Geoff & Jones, Neil. （2012）。 Distillation with labelled transition systems. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 15-24. 10.1145/2103746.2103753. ↩
Hamilton, Geoff. "The Next 700 Program Transformers." International Symposium on Logic-Based Program Synthesis and Transformation. Cham: Springer International Publishing, 2021. ↩
Klyuchnikov, Ilya, and Sergei Romanenko. "Towards higher-level supercompilation." Second International Workshop on Metacomputation in Russia. Vol。 2. No. 4.2. 2010. ↩
