The Elimination of Nesting in SPCF
The Elimination of Nesting in SPCF
复制标题
SPCF 中嵌套的消除
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Laird
中科院分区：
文献类型：
--
作者：
J. Laird
我们使用一个完全抽象的指称模型表明，嵌套的函数调用和递归定义可以从SPCF（一种类型化的函数语言，具有简单的非局部控制算子）中消除，而不会失去表达能力。我们描述-通过简单的打字规则-仿射片段的SPCF中，函数嵌套和递归（迭代）是不允许的。我们证明，这个仿射片段是完全表达的意义上说，每一项的SPCF是观测等价的仿射项。
我们的证明是基于朗利的观察-已经用来证明的普遍性和充分的抽象结果的模型SPCF -每一种类型的SPCF是一个撤回的一阶类型。我们描述的这种是可定义的仿射片段的撤回。这使得我们可以将任意的SPCF项转换为仿射项，方法是将其映射到一阶项，获得（仿射）范式，然后投影回原始类型。在有限SPCF的情况下，收回是基于一个简单的归纳，这产生的结果项的大小的界限。在无穷大的情况下，它是基于SPCF可定义的功能和策略，依次计算它们之间的关系的分析。
We use a fully abstract denotational model to show that nested function calls and recursive definitions can be eliminated from SPCF (a typed functional language with simple non-local control operators) without losing expressiveness. We describe — via simple typing rules — an affine fragment of SPCF in which function nesting and recursion (other than iteration) are not permitted. We prove that this affine fragment is fully expressive in the sense that every term of SPCF is observationally equivalent to an affine term.
Our proof is based on the observation of Longley — already used to prove universality and full abstraction results for models of SPCF — that every type of SPCF is a retract of a first-order type. We describe retractions of this kind which are definable in the affine fragment. This allows us to transform an arbitrary SPCF term into an affine one by mapping it to a first-order term, obtaining an (affine) normal form, and then projecting back to the original type. In the case of finitary SPCF, the retraction is based on a simple induction, which yields bounds for the size of the resulting term. In the infinitary case, it is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially.