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的强大程序Inliner和专业化程序。如果您使用启用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上启动Mazeppa，并在target/graph.svg中--inspect化过程图。可以通过SVG预览扩展名在VS代码中查看后者。
./scripts/play.sh如果有任何更改，将自动重新编译OCAML中的源。
以身作则，最好了解超级专业的工作方式。考虑以下功能，该功能列出列表并计算其平方元素的总和：
[ 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))
};
该程序以惯用的，列出的功能样式编写。每个功能都只能做一件事，并且做得很好。但是，这里有一个严重的问题： mapSq实质上构建了一个将立即按sum进行解构的列表，这意味着我们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/目录将包含以下文件：
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中的初始程序：我们的SuperCompiler可与此特定表示形式合作，而不是原始程序。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这个小例子，但可以随意查看：它不太复杂。）
SuperCompiler从包含main(xs)的节点n0开始。在函数展开两个步骤后，我们到达包含sum(.g1(xs))的节点n2 ，其中.g1是与我们的mapSq相对应的IR函数。在这一点上，我们别无选择，只能通过猜测xs在运行时可能需要的值来分析呼叫.g1(xs) 。由于我们的mapSq仅接受构造函数Nil和Cons ，因此仅考虑xs=Cons(.v0, .v1)和xs=Nil()的情况就足够了。
节点n4是在我们替换Cons(.v0, .v1)将xs的cons .v0和.v1是新变量的）之后发生的。又有三个功能展开后，我们到达n7 。这是我们第一次必须将呼叫+(*(.v0, .v0), sum(.g1(.v1)))分为.v3=*(.v0, .v0) （ n8 ）和.v4=sum(.g1(.v1)) （ n11 ）（n11）和执行超级付费+(.v3, .v4) （n13）（ n13 ）;这样做的原因是，以前的节点（ n2 ）在结构上嵌入了n7中，因此否则可以永远继续进行超级填充。现在， sum(.g1(.v1)) （ n11 ）会发生什么？我们已经看到了！回想一下n2包含sum(.g1(xs)) ，这只是sum(.g1(.v1)) ;因此，我们决定将n11折叠到n2中，因为两次超级竞争是没有意义的。 n7的其他分支（即n13和n8 ）被分解，这意味着我们只是继续改变他们的论点。
至于n2的另一个分支，sum（nil（ n16 sum(Nil()) ），仅将此呼叫展开至0i32 （ n18 ）就足够了。
过程图完成后，残差将其转换为最终程序。在此阶段，动态执行模式成为函数-Node n2现在成为函数f0 ，因为其他一些节点（ n11 ）指向它。在任何剩余程序中，都有与带有传入虚线的节点和main一样多的功能。
总而言之，超级缩写由1）组成1）展开函数定义，2）分析模式匹配的呼叫未知变量，3）将计算分为较小的部分，4）折叠重复计算，5）在我们的示例中，分解呼叫，例如+(.v3, .v4) （n13）（ n13 ）。整个超级填充过程可以保证终止，因为当某些计算变得越来越大时，我们将其分解为子问题并孤立地解决它们。
在examples/文件夹中，包括树状数据结构，还有许多其他有趣的森林砍伐示例。实际上，我们已经从先前的彼得· A ·琼森（Peter A.在所有情况下，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的x参数，尽管它在编译时是广为人知的。在main(a)上运行Mazeppa将产生以下残差程序：
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
已经消除了整个powerSq函数，从而实现了部分评估的效果。 （如果我们认为powerSq是程序x和输入数据a的解释器，那么它是第一个Futamura投影：专门为解释器获得有效的目标程序。）另外，请注意，SuperCompiler如何设法共享参数*(a, *(a, a))两次，以免每次恢复每次。剩余程序确实通过平方反映了指示。
让我们超越森林砍伐和部分评估。考虑两个字符串的函数matches(p, s) ，如果s包含p和F()则返回T() 。在Mazeppa中的幼稚实施将是以下内容，其中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的第二个字符开始再次与"aab"匹配，尽管可以说s的第二个字符是'a' 。由Knuth-Morris-Pratt算法（KMP） 6构建的确定性有限自动机是解决此问题的另一种方法。
通过在上面的样本上运行Mazeppa，我们可以获得一个有效的字符串匹配p="aab"的算法，该算法反映了行动中的KMP：
[ 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。
超级专业的发明者Valentin Turchin用以下方式描述了Metasystem Transition的概念11 12 13 ：
考虑任何一种系统。假设有一种方法可以从中制作一些副本，可能会有变化。假设这些系统融合为一个新系统S'，该系统将S类型的系统作为其子系统，并且还包括一个控制S-缩写系统的行为和生产的附加机制。然后，我们将S'称为S的Metasystem，以及S'Metasystem Transition的创建。由于连续的Metasystem Transition导致了控制的多级结构，从而允许复杂的行为形式。
因此，可以很容易地将SuperCompilation视为Metasystem Transition：Mazeppa中有一个对象程序，并且有Mazeppa SuperCompiler控制和监督对象程序的执行。但是，如下一个示例所示，我们可以进一步执行对象程序本身领域内的任何数量的Metasystemtrions。
我们将使用examples/lambda-calculus/的代码。以下是一种标准划分的标准化方法，用于获得未型lambda conculus术语的beta正常形式：
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 。）
从本质上讲，这是用于有效避免捕获替代的大步骤：我们维护一个价值环境，而不是重建每个beta的术语。 eval项目的“语义域”术语，而quote则相反； normalize只是quote和eval的组成。为了避免打扰新的名字，我们将de bruijn索引放在NVar的Var构造器和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计算lambda术语example()的正常形式，该术语示例（）乘以教堂数字two()和three() 。
通过SuperCompliting 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微积分解释器已经完全消灭了！
在此示例中，我们刚刚看到了一个两级的元社楼梯（在Turchin的术语14中）：在0级别，我们有Mazeppa SuperCompiler转换对象程序，而在1级上，我们的对象程序正常于lambda calculus项。可以有任意数量的解释水平，可以使用Mazeppa将它们全部崩溃。 Turchin本人在1 （第7节）中探索了超级缩减的这种一般行为，在那里他能够超越两个可解释的程序，一个类似于Tran的程序，一个在LISP中，以在两种情况下获得40个加速因素。
Lambda归一化器还向我们展示了如何将高阶功能化为一阶语言。在Mazeppa中，我们不能将功能视为值，但这并不意味着我们无法模拟它们！通过执行Metasystem Transition，我们可以用一阶语言有效地实现高阶功能。除了已解决和封闭转换外，该技术还可以用于将高阶语言汇编为有效的一阶代码。
相关示例：命令虚拟机，自我拦截。
回想起来，阻止广泛采用超级填充的主要问题是其不可预测性 - 其力量的黑暗面。要了解它的含义，请考虑如何“飞行”解决任何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)
};
这个完全正确的代码有两件事：1）超级委员会将在指数空间中扩展公式，而2）超级委员会将尝试在指数时间内求解扩展的公式。有时，我们只是不想在编译时评估所有内容。
但是，绝望不是：我们为这个问题提供了解决方案。让我们首先考虑如何推迟解决公式直到运行时。事实证明，我们唯一需要做的就是用@extract注释函数formula如下：
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
当Mazeppa看到solve(formula(a, b, c, d, e, f, g)) .v0 ，它会将呼叫提取到formula中，以隔离地进行超级调整的呼叫和solve(.v0) 。后一个电话只会复制原始的SAT求解器。
但是，超级调用formula的呼叫仍会导致指数爆炸。让我们检查为什么会发生这种情况。我们的原始公式由致电or和and ;组成；虽然or显然不危险， and rest参数传播到If的两个分支（第一个match案例） - 这是爆炸发生的确切位置。因此，让我们标记and使用@extract ：
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
就是这样！当and要转换时，Mazeppa将从周围的环境中提取呼叫，并隔离它。通过在适当的位置添加两个注释，我们既解决了代码爆炸问题，又解决了超级缩减的指数运行时间。通常，每当Mazeppa看到ctx[f(t1, ..., tN)]时， f被标记为@extract ，并且ctx[.]是一个非空的环境.在Redex位置，它将将新的变量v插入ctx中，然后分别转换以下节点： f(t1, ..., tN)和ctx[v] 。
最后，请注意， @extract只是一种低级机制。编译器前端必须执行其他机器，以告诉Mazeppa哪些功能要提取。这可以通过两种方式完成：
formula and可提取，使所有其他功能都没有受到影响。两种方法都可以合并以达到预期的效果。
Mazeppa采用有趣的设计选择来具有渴望的功能和懒惰的构造函数。以下示例，其中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
如下所述，懒惰的构造仪可实现轻松的森林砍伐。
通过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称为多次，包括并行。请注意，我们将有限的界面暴露于SuperCompiler；特别是，没有办法检查其在此过程中的作用（即--inspect ）。
除了超级填充外，我们还提供了一个内置的评估器：
val eval : Raw_program .t -> Raw_term .t它只能在main功能不接受参数的程序上调用。与supercompile不同，它产生了Raw_term.t类型的评估术语，并且可能会分歧。
在lib/mazeppa.mli中，请参见其他API函数及其文档。
假设main.mz包含懒惰斐波那契的稍微修改版本示例：
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命令都需要--language ，即翻译的目标语言，也需要--entry ，这是将与您的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并打印结果。您可以使用mazeppa.h的任何功能，前提是它不带有mz_priv_或MZ_PRIV_前缀。
将所有碎片融合在一起：
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out按预期打印fib(10) = 55并退出。
--inspect ：仅将其用于调试目的。@extract （如上所示）来控制是否继续超级填充或提取redex。"otus"比"octopus"小，但"octopusx"不是。 Mazeppa采用了几种有趣的设计选择（按重要性排名）：
一阶代码。 Max Bolingbroke和Simon Peyton Jones 15报告说，在一个特定示例中，他们的高阶SuperCompiler用于Haskell的子集，将执行时间的42％用于管理名称和重命名。虽然确实是，诸如Lambda术语的标准化之类的简单评估模型允许我们避免避免捕获的大量开销，但超级局限器更加复杂。例如，除了进行象征性计算外，超级锻炼还需要分析先前计算的结果，以做出有关进一步转换的明智决定：术语实例测试，同构嵌入测试，最具体的概括等。引入高阶功能不可避免地会使所有这些分析不可避免地复杂化，从而使超级效果变得更慢，使记忆力较低，记忆力更高，更加难理地以及更难的理由，并且是不可避免的。在Mazeppa中，我们坚持逐步改进的理念：我们没有尝试同时处理许多精美的功能，而是修复核心语言，以通过机器来方便地操纵核心语言，2）尽可能多地执行必要的MetasySySten过渡，以使核心语言更好地对人类。
懒惰的构造函数。众所周知的观察结果是，逐个价值语言很难进行适当的森林砍伐。仍然有可能砍伐它们，但没有其他分析4 5 。但是，如果构造函数很懒惰（即，他们没有评估他们的论点），则森林砍伐只是有效的。 Turchin通过正常订单转换的逐个呼叫语言使其起作用，但结果是剩余代码可能更频繁地终止。在Mazeppa中，我们具有逐个呼叫功能和按名称呼叫（按需要呼叫）构造函数，其中1）使森林砍伐成为可能，并且2）保留代码的原始语义。
无项的过程图。在Mazeppa中，过程图不包含对术语的任何参考：在没有它们的情况下，残差可以起作用。结果，垃圾收集器可以处理在构造子图期间使用的术语。此外，此策略还有其他几个重要优势：1）图表仍在那里进行检查， --inspect ，2）当它绘制时，它只揭示有关超级专业人士所做的决定的信息，这使得它更容易查看。几位现有的超级核算器避免了适当的过程图（例如，尼尔·米切尔（Neil Mitchell）的超级17和上述15 ），但结果，1）它们不太能够由用户检查，2）算法对代码生成细节变得混乱。
二维配置分析。通常，超级委员会在转换节点时会保留所有祖先的一个子集的“历史”。如果该节点与其祖先之一“足够接近”，则该将术语分为较小的部分以确保终止。在Mazeppa中，我们保留了两个单独的数据结构：一个包含节点祖先子集的一个和一个包含完全转化的节点子集的数据结构。以前的数据结构用于保证终止（像往常一样），而后者则用于增强剩余代码中功能的共享。具体而言，如果当前节点（特殊类型）是某些先前转换节点的重命名，则将当前节点折叠到以前的节点中。这样，Mazeppa对配置进行了垂直和水平分析，这使剩余代码更加紧凑，超填充更有效。
功能生产力分析。当内部函数呼叫模式匹配未知值时，会发生两个潜在的危险事件：1）超级缩写再现模式匹配函数的结构，2）超缩写将整个周围环境推向此功能的所有分支。没有进一步的控制，这种情况可能会导致代码尺寸的重大爆炸，有时甚至会导致超级专业人士不在合理的时间内终止。为了改善，Mazeppa复制上下文，如果此内部呼叫至少从一个出口点产生明确的顶级值，因为如果这样做，则很大的机会可以通过随后的模式匹配来解构该值。否则，Mazeppa将提取内部呼叫并孤立地转换它（就像用@extract标记一样）。此外，如果上下文实际上是重复的，则以下规则适用于所有分支：如果分支从所有出口点产生确定的顶级值，则在上下文中会在上下文中转换；否则，将分支从上下文中提取并隔离。实际上，该分析阻止了大量不需要的专业，从而压实了剩余程序规模并使超填充更加易于处理。
聪明的历史。 Instead of blindly comparing a current node with all its ancestors, we employ a more fine-grained control, that is: 1) global nodes (the ones that analyze an unknown variable) are compared with global nodes only, 2) local nodes (the ones that reduce linearly in a single step) are compared with local nodes only up to the latest global node, but not including it, and 3) trivial nodes (the ones that break down terms into smaller components)没有与其他任何东西进行比较。除了采取更经济的终止检查方法外，该计划还使Mazeppa发现了更多优化机会。参见第18节4.6和4.7节。通过在全球和局部术语的所有潜在无限的子序列上测试同构嵌入的事实，可以保证超级缩减的终止（不能仅存在无限的琐事术语）。
REDEX签名。哨子仅在具有相等的Redex签名的术语上进行测试。 Redex签名是1）函数符号和2）参数值类别列表。值类别是关于参数的一种元信息，它可以是1） VConst ，对于42i32或"hello world" ，2）诸如x或+(x, x)或3）诸如constructor call（例如Foo(...)之类的构造函数的VNeutral VCCall(c) 。仍在所有潜在的无限术语序列上测试哨子，因为任何无限序列都必须至少包含一个具有相同redex签名的术语的无限子序列。这种策略使Mazeppa在某些情况下避免过度概括，如以下两个例子所示：
f(A())同型嵌入f(g(B(A()))) ;但是，由于Redex运算符不同（ f和g ），因此Mazeppa继续减少并达到理想的结果。f(A(Good()))嵌入f(f(f(B(A(Good()))))) ，并且在这两种情况下，redex运算符都是f ，但mazeppa并没有过度启动，因为这两个术语在其红色签名中具有不同的价值类别：first cane f fript A(...) ，在a（...）中，b in B(...)就像在上一个示例中一样，Mazeppa仅通过还原而达到超级缩减的理想结果。优化的同构嵌入。在过去的几十年中，同构嵌入因成为在线终止检查的绝佳方法而赢得了声誉19 。不幸的是，主要是由于非线性对照流（当应用潜水和耦合）时，计算可能是不可原谅的。更糟糕的是，每当将新术语添加到历史上时，它将重新执行所有合格的家长节点，随着历史的增长，这会逐渐减慢超级缩短的速度：到达大部分超级效果时间！为了应对这一点，我们维持了两个单独的缓存：
哈希求婚。上述同构嵌入库的同构嵌入取决于共享多少个术语。因此，我们在展开函数体时采用哈希构成：如果某些新术语在结构上等于某些现有术语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中很自然。异常不仅用于“特殊”情况，而且功能内部的可突变性很常见。尽管我们没有用EG 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)符号：
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。程序。朗。系统。 8, 3 (July 1986), 292–325. https://doi.org/10.1145/5956.5957 ↩ ↩ 2
Philip Wadler. 1988. Deforestation: transforming programs to eliminate trees.理论。计算。科学。 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.指责。 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.计算。科学。 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.卷。 2. No. 4.2. 2010. ↩
