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比其前任更實用。
符號<SYMBOL>是一系列字母（ a ， ... ， z和A ， ... ， Z ）和數字（ 0 ， ... ， 9 ），然後是可選的問號（ ? ），然後是'字符”的可選順序。下劃線字符（ _ ）可能是符號的第一個字符，該字符可能非正式地表明未使用的值或函數不使用；否則，第一個字符必須是字母。以下字符序列也允許作為符號： ~ ， # ， + ， - ， * ， / ， % ， | ， & ^ ， << ， >> ， = ， != ， > ， >= ， < ， <= ， ++ 。以下是保留的單詞，這些單詞可能不被用作符號： match ， let 。
有四類未簽名的整數常數：
0b （ 0B ），然後是非空數數字0和1的非空序列。0o （ 0O ），然後是八分位數0 ， ... ， 7 。0 ， ... ， 9 。0x （ 0X ），然後是十進制數字0 ， ... ， 9和字母a ， ... ， f （ A ， ... ， F ）的非空序列。筆記：
_ ）。- ）形成了一個否定的整數常數。<INT>通過在原始整數常數之後，通過附加整數類型<INT-TY> （ u8 ， u16 ， u32 ， u64 ，u64， u128 ，u128， i8 ， i16 ，i32， i32 ，i32， i64 ， i128 ）。例如，常數123i8和123u16 123i32屬於集合<INT> 。字符串常數<STRING>是零或更可打印字符的雙引號（ " ）之間的序列（我們將可打印字符稱為ASCII字符集中編號為33-126的字符），空格或字符串逃生序列：
| 逃脫序列 | 意義 |
|---|---|
f | 形式飼料（ASCII 12） |
n | 線飼料（ASCII 10） |
r | 馬車返回（ASCII 13） |
t | 水平標籤（ASCII 9） |
v | 垂直選項卡（ASCII 11） |
xhh | 十六進制中的ASCII代碼 |
" | " |
\ | |
其中h是0 ， ... ， 9或a ， ... ， f或A ， ... ， F 。
字符常數<CHAR>是單個引號（ ' ）中包含的唯一字符，或者是單個引號中包含的字符逃脫序列。字符逃逸序列與字符串相同，只是"被'取代。
Mazeppa中沒有其他常數。
評論<COMMENT>是//之後的任何字符序列，它是由newline字符終止的。 （我們僅允許單行註釋才能簡單。）
入口點<program>由以下規則定義：
<def-attr-list> <SYMBOL> ( <SYMBOL> ， ... ， <SYMBOL> ) := <term> ; <program><COMMENT> <program>其中<def-attr-list>是函數屬性的偏差序列（可以多次發生相同的屬性）。現在，唯一允許的函數屬性是@extract 。
<term>定義如下：
<SYMBOL> （變量）<const> （常數）<SYMBOL> ( <term> ， ... ， <term> ) （函數調用）match <term> { <match-case> ， ... ， <match-case> } （模式匹配）let <SYMBOL> := <term> ; <term> （一個釋放）let <pattern> := <term> ; <term> （一種模式放置）<COMMENT> <term> （評論）其餘的輔助規則是：
<const> ：
<INT>或<STRING>或<CHAR> 。 <match-case> ：
<pattern> -> <term> <pattern> ：
<SYMBOL> ( <SYMBOL> ， ... ， <SYMBOL> ) 。在Mazeppa中，原始操作採用與普通函數調用相同的語法。要區分這兩者，我們將<op1>和<op2>定義為以下符號集：
<op1>是~ ， # ， length ， string ， <INT-TY>之一。<op2>是+ ， - ， * ， / ， % ， | ， & ， ^ ， << ， >> ， = ， != ， > =， >= ， < ， <= ， ++ ， get 。此外， <op2>具有以下子類：
<arith-op2>是+ ， - ， * ， / ， % ， | ， & ， ^ ， << ， >> 。<cmp-op2>是= ， != ， > ， >= ， < ， <= 。<op1>或<op2> 。 2）函數必須定義以小寫字母開頭的符號。 3）在函數參數之間不可能發生重複的符號。 4）功能主體內部的每個自由變量都必須在函數定義中受相應參數綁定。match { ... }中的案例順序不得為空。 2）在match { ... }中的情況模式之間，不會發生重複的構造函數。 3）在模式參數C(x1, ..., xN)之間不可重複的符號。 4）沒有let結合可以結合<op1>或<op2> 。 5）必須只用一個論點來調用Panic ； T和F零參數。如果程序，功能或術語符合這些限制，我們稱其為良好的形式。
| 原始形式 | desugared形式 | 筆記 |
|---|---|---|
// ... rest | rest | rest在<program>或<term>中 |
let p := t; u | match t { p -> u } | p在<pattern>中 |
c | ASCII（C） | c在<CHAR>中 |
根據ASCII表，其中ASCII（C）是合適的u8整數常數；例如， ASCII（ 'a' ）為97u8 。
假設T是在環境Env （定義下定義）下封閉的術語良好的術語，並且程序是一個形式良好的程序。然後， T的評估由以下大步驟環境機器約束：
eval(env, x) = eval({ }, env(x))eval(env, const) = const ，其中const在<const>中。eval(env, f(t1, ..., tN)) =t1Val ^= eval(env, t1)tNVal ^= eval(env, tN)eval({ x1 -> t1Val, ..., xN -> tNVal }, body) ，其中f(x1, ..., xN) := body;在程序中。eval(env, C(t1, ..., tN)) = C(t1[env], ..., tN[env]) ，其中C從大寫字母開始。eval(env, op(t)) =tVal ^= eval(env, t)evalOp1(op, tVal) ，其中op在<op1>中。eval(env, op(t1, t2)) =t1Val ^= eval(env, t1)t2Val ^= eval(env, t2)evalOp2(t1Val, op, t2Val) ，其中op在<op2>中。eval(env, match t { p1 -> t1, ..., pN -> tN }) =Ci(s1, ..., sN) ^= eval(env, t)eval(env', tI) ，其中Ci(x1, ..., xN) -> tI是match t { ... }規則之一，並且env'是env[x1 -> s1, ..., xN -> sN] 。eval(env, let x := t; u) =tVal ^= eval(env, t)eval(env[x -> tVal], u)符號：
env是T的總環境，其通用形式為{ x1 -> t1, ..., xN -> tN } 。每個tI術語必須關閉且形成良好；該屬性由eval保留。env(x)是tI ，其中x -> tI在env中。env[x1 -> t1, ..., xN -> tN]是環境env並用新的bindings x1 -> t1 ， ... ， xN -> tN擴展。如果某些xI已經綁定在env中，則它是反彈的。t[env]表示在env中通過其t值同時替換了所有自由變量。tVal ^= eval(env, t)在env下評估t ；然後：Panic(t') ，則整個評估規則的結果是Panic(t') 。tVal將用於下一個條款。 （請注意， eval是部分函數，因此無需疊加類型系統就可以“卡住”評估。）
在接下來的內容中，1）簽名的整數在兩個補充符號中表示，2）恐慌表示Panic(s) ，其中s是某些（可能變化的）實現定義的字符串常數。
evalOp1照顧原始類型的一元操作員（ x在<INT>中， s在<STRING>中）：
evalOp1(~, x)是同一類型的x的x否定。evalOp1(string, x)是x的字符串表示（小數為小數）。ty在<INT-TY>中的evalOp1(ty, x) x轉換為ty型整數。x不在ty的範圍內，則結果是恐慌。evalOp1(#, x) ，其中x是u8整數，是一個僅包含x的ascii字符的字符串。x不可打印，則結果為"xhh" 。evalOp1(length, s)是表示s長度的u64整數。evalOp1(string, s)是s 。同樣， evalOp2照顧原始類型的二進制運營商：
evalOp2(x, op, y) ，其中x和y具有相同的整數類型，而op在<arith-op2>中，在x和y上執行相應的算術操作，產生與x和y的相同類型的值。evalOp2(x, op, y) ，其中x和y具有相同的整數類型，並且op在<cmp-op2>中，在x和y上執行相應的比較操作，產生T()或F() 。evalOp2(s1, op, s2) ，其中s1和s2是字符串， op在<cmp-op2>中，對s1和s2進行相應的詞典比較，得出T()或F() 。evalOp2(s1, ++, s2)是s1和s2的串聯。evalOp2(s, get, idx) ，其中idx是u64整數，是s的idx -th字符（u8 type u8 ）。idx超出了邊界，則結果是恐慌。 eval的定義已完成。
dune-project和bin/main.ml中更新version字段。dune build以生成mazeppa.opam 。CHANGELOG.md 。還沒有，我們需要使用一些實際的編程語言進行測試。我們的長期目標是找到合適的啟發式方法，以超越10'000 LOC（Mazeppa）以下的任何源文件。
為了調試和其他目的，我們提供了一個內置的定義解釋器，可以執行Mazeppa程序。您可以通過鍵入mazeppa eval來啟動它（確保您的main函數不接受參數）。為了實現實際執行的目的，我們建議將Mazeppa轉換為C，然後將C彙編為機器代碼，如上所示。
由於Mazeppa是一種純粹的功能性語言，因此實現I/O的唯一方法就是Haskell 23 ：具有執行計算的純程序和執行該程序發出的副作用的骯髒運行時。沒有計劃將直接I/O引入Mazeppa：它只會使一切變得更加複雜。
不，我們認為此時不需要類型系統。前端編譯器的責任是確保程序不會“出錯”。
我們使超級填充可預測的越多，它的定理能力就越少。對於那些對程序分析而不是優化感興趣的人，我們建議研究蒸餾24 。
對於英國觀眾來說，以下論文介紹了超級詳細介紹：
但是，俄羅斯的以下論文描述了一個超級局限制模型，該模型比現有的超級專家（包括Mazeppa）更接近：
Mazeppa本身的靈感來自此優秀論文（英文）：
最後，國際元元研討會是有關超級專業和鄰近領域的大量文章：
多種方法可以通過超級縮寫導致非運動程序的超線性加速：
以上都沒有計劃在Mazeppa中實施，因為1）我們認為編寫漸近的良好程序是程序員的責任，而不是優化器的責任，而不是2）超級填充的可預測性對我們來說更為重要。但是，對於那些對此主題感興趣的人，參考文獻可能會有所幫助。
只是叉子存儲庫，在您自己的分支機構工作，然後提交拉動請求。在引入更改時，更喜歡重新審議，以使提交歷史記錄盡可能清潔。
Valentin F. Turchin。 1986年。超級委員會的概念。 ACM Trans。程式.朗。系統。 8，3（1986年7月），292–325。 https://doi.org/10.1145/5956.5957↩2
菲利普·沃德勒。 1988年。森林砍伐：改造程序以消除樹木。理論。計算。科學。 73，2（1990年6月22日），231–248。 https://doi.org/10.1016/0304-3975(90)90147-a↩2
Futamura，Y。 （1983）。程序的部分計算。在：Goto，E.，Furukawa，K.，Nakajima，R.，Nakata，I.，Yonezawa，A。 （編輯）RIMS軟件科學與工程學研討會。計算機科學的講義，第147卷。施普林格，柏林，海德堡。 https://doi.org/10.1007/3-540-11980-9_13↩
彼得·瓊森（Peter A. Jonsson）和約翰·諾德蘭（Johan Nordlander）。 2009年。逐個呼叫語言的積極超級縮寫。 Sigplan不。 44，1（2009年1月），277–288。 https://doi.org/10.1145/1594834.1480916↩2
約翰·喬恩（Jonsson），彼得（Peter）和諾德蘭（Nordlander），約翰（Johan）。 （2010）。加強逐個呼叫語言的超級縮寫。 ↩2
De Knuth，JH Morris和VR Pratt。弦樂中的快速圖案匹配。 Siam on Computing雜誌，6：第323頁（1977）。 ↩
Glück，R.，Klimov，AV（1993）。 Occam的剃須刀在Metacompontain中：完美的過程樹的概念。在：Cousot，P.，Falaschi，M.，Filé，G.，Rauzy，A。 （eds）靜態分析。 WSA 1993。計算機科學的講義，第724卷。施普林格，柏林，海德堡。 https://doi.org/10.1007/3-540-57264-3_34↩
SørensenMH，GlückR，Jones ND。積極的超級委員會。功能編程雜誌。 1996; 6（6）：811-838。 doi：10.1017/s0956796800002008↩
Consel，Charles和Olivier Danvy。 “字符串中模式匹配的部分評估”。信息處理信30.2（1989）：79-86。 ↩
瓊斯，尼爾和戈馬德，卡斯滕和塞斯托夫，彼得。 （1993）。部分評估和自動程序生成。 ↩
Turchin，VF（1996）。 Metacompuntion：Metasystem Transitions和SuperCompilation。在：Danvy，O。 ，Glück，R。 ，Thiemann，P。 （eds）部分評估。計算機科學的講義，第1110卷。 Springer，柏林，海德堡。 https://doi.org/10.1007/3-540-61580-6_24↩
Turchin，Valentin F.“具有Metasystem Transitions的程序轉換”。功能編程雜誌3.3（1993）：283-313。 ↩
Turchin，Valentin F ..“關於Metasystem過渡的對話。”世界期貨45（1995）：5-57。 ↩
Turchin，V。和A. Nemytykh。 Metavariables：它們在程序轉換中的實現和使用。 CCNY技術報告CSC TR-95-012，1995。
Maximilian Bolingbroke和Simon Peyton Jones。 2010。通過評估超級縮減。在Haskell（Haskell '10）的第三次ACM Haskell研討會論文集。計算機協會，美國紐約，紐約，135-146。 https://doi.org/10.1145/1863523.1863540↩2
弗里德曼（Friedman），丹尼爾（Daniel P.）和戴維·S·懷斯（David S.Wise）。 “缺點不應評估其論點。”國際自動機，語言和編程座談會（1976）。 ↩
米切爾，尼爾。 “重新思考超級縮減。” ACM Sigplan國際功能編程會議（2010年）。 ↩
Sørensen，MHB（1998）。在樹木的度量空間中，程序變壓器的收斂。在：Jeuring，J。 （eds）程序構建數學。 MPC 1998。計算機科學的講義，第1422卷。 Springer，柏林，海德堡。 https://doi.org/10.1007/bfb0054297↩
Leuschel，邁克爾。 “同構嵌入符號方法的在線終止。”計算的本質：複雜性，分析，轉換（2002）：379-403。 ↩
約翰·喬恩（Jonsson），彼得（Peter）和諾德蘭（Nordlander），約翰（Johan）。 （2011）。馴服代碼爆炸在超級填充中。 Perm'11-第20 ACM Sigplan研討會論文集，內容是部分評估和計劃操縱。 33-42。 10.1145/1929501.1929507。 ↩2
Tejiščák，Matúš。刪除依賴類型的編程。指責。聖安德魯斯大學，2020年。
Glück，Robert，Andrei Klimov和Antonina Nepeivoda。 “通過超級填充的非線性配置，用於超線性加速。”第五屆國際瓦倫丁·塔爾丘文（Valentin Turchin）關於元數據的研討會。 2016.↩
佩頓·瓊斯（Peyton Jones），西蒙（Simon）。 （2002）。解決笨拙的小隊：Haskell中的Monadic輸入/輸出，並發，例外和外語電話。 ↩
GW漢密爾頓。 2006。 Poitín：從猜想中提取定理。電子。注意理論。計算。科學。 151，1（2006年3月），143-160。 https://doi.org/10.1016/j.entcs.2005.11.028↩
Klyuchnikov，Ilya和Dimitur Krustev。 “超級專業：思想和方法。”單子。讀者第23（2014）：17。
Klimov，Andrei＆Romanenko，Sergei。 （2018）。超級專輯：主要原理和基本概念。 Keldysh Institute預印本。 1-36。 10.20948/prepr-2018-111。 ↩
羅曼尼科，謝爾蓋。 （2018）。超級分組：同構嵌入，呼叫名稱，部分評估。 Keldysh Institute預印本。 1-32。 10.20948/prepr-2018-209。 ↩
RobertGlück和Morten HeineSørensen。 1996年。通過超級縮減到元數據的路線圖。在來自國際研討會的部分評估論文中。施普林格·弗拉格（Springer-Verlag），柏林，海德堡（Heidelberg），137-160。 https://dl.acm.org/doi/10.5555/647372.724040↩
Secher，JP（2001）。在叢林中行駛。在：俄勒岡州Danvy，A。 Filinski（eds）程序作為數據對象。 Pado 2001。計算機科學的講義，第2053卷。施普林格，柏林，海德堡。 https://doi.org/10.1007/3-540-44978-7_12↩
Hoffmann，B.，Plump，D。 （1988）。叢林評估有效期重寫。在：Grabowski，J。 ，Lescanne，P.，Wechler，W。 （Eds）代數和邏輯編程。 ALP 1988。計算機科學的講義，第343卷。施普林格，柏林，海德堡。 https://doi.org/10.1007/3-540-50667-5_71↩
漢密爾頓，傑夫。 （2007）。蒸餾：提取程序的本質。 ACM Sigplan研討會論文集，是部分評估和基於語義的程序操作的。 61-70。 10.1145/1244381.1244391。 ↩
漢密爾頓，GW（2010）。提取蒸餾的本質。在：Pnueli，A.，Virbitskaite，I.，Voronkov，A。 （編輯）系統信息學的觀點。 PSI 2009。計算機科學的講義，第5947卷。施普林格，柏林，海德堡。 https://doi.org/10.1007/978-3-642-11486-1_13↩
漢密爾頓，傑夫和門德爾 - 格林，加文。 （2010）。基於圖的蒸餾定義。 ↩
漢密爾頓，傑夫和瓊斯，尼爾。 （2012年）。用標記的過渡系統蒸餾。編程語言原理的年度ACM年度研討會的會議記錄。 15-24。 10.1145/2103746.2103753。 ↩
漢密爾頓，傑夫。 “接下來的700個程序變壓器。”國際基於邏輯的程序綜合和轉型研討會。 CHAM：Springer International Publishing，2021年。
Klyuchnikov，Ilya和Sergei Romanenko。 “邁向更高級別的超級填充。”第二屆國際元庫納在俄羅斯的研討會。卷。 2。第4.2號。 2010年
