论文标题
带有递归定义的复发提取和典型语义
Recurrence extraction and denotational semantics with recursive definitions
论文作者
论文摘要
除了一个例外，我们先前关于复发提取和语义语义的工作集中在支持归纳类型和结构递归的源语言上。该异常通过初始翻译为呼叫值处理一般递归。在本说明中，我们从具有一般递归函数定义的语言中提供了一种提取功能，并将递归类型直接传达给类似PCF的复发语言。我们证明了不使用逻辑关系的主要声音结果（实际上是构成了操作成本的句法复发），因此与我们先前的工作相比，大大简化了证据（以对复发语言的模型提出更多要求）。然后，我们定义了复发语言的两个模型，一种用于分析合并排序，另一个用于分析快速排序，作为案例研究，以理解用于证明提取的复发合理性的模型定义。
With one exception, our previous work on recurrence extraction and denotational semantics has focused on a source language that supports inductive types and structural recursion. The exception handles general recursion via an initial translation into call-by-push-value. In this note we give an extraction function from a language with general recursive function definitions and recursive types directly to a PCF-like recurrence language. We prove the main soundness result (that the syntactic recurrences in fact bound the operational cost) without the use of a logical relation, thereby significantly simplifying the proof compared to our previous work (at the cost of placing more demands on the models of the recurrence language). We then define two models of the recurrence language, one for analyzing merge sort, and another for analyzing quick sort, as case studies to understand model definitions for justifying the extracted recurrences.
