论文标题
部分可观测时空混沌系统的无模型预测
let (rec) insertion without Effects, Lights or Magic
论文作者
论文摘要
在程序生成中插入的是生产具有定义的代码（Let-Statements）。尽管在生成的代码中使用的定义在使用之前，但是在代码生成期间，“用法”首先出现：我们甚至可能不知道需要定义，直到我们遇到重复出现的表达式。因此，定义是在“事后观看”中生成的，这解释了为什么难以理解和实施此过程的原因 - 甚至是参数化，递归和相互递归的定义。 我们较早提出了一个让（REC）插入的接口 - 即生成（相互递归）的定义。我们证明了其表现力和应用，而不是其实施，这取决于效果和编译器魔法。 现在，我们展示了如何理解让插入的，因此可以在Plain Ocaml中实现它。我们给出了LET（REC）插入的第一个词语语义，该语义根本不依赖任何效果。正式化指导了在当前版本的荟萃分析中插入LET（REC）的实施。
Let insertion in program generation is producing code with definitions (let-statements). Although definitions precede uses in generated code, during code generation `uses' come first: we might not even know a definition is needed until we encounter a reoccurring expression. Definitions are thus generated `in hindsight', which explains why this process is difficult to understand and implement -- even more so for parameterized, recursive and mutually recursive definitions. We have earlier presented an interface for let(rec) insertion -- i.e. for generating (mutually recursive) definitions. We demonstrated its expressiveness and applications, but not its implementation, which relied on effects and compiler magic. We now show how one can understand let insertion, and hence implement it in plain OCaml. We give the first denotational semantics of let(rec)-insertion, which does not rely on any effects at all. The formalization has guided the implementation of let(rec) insertion in the current version of MetaOCaml.
