A universality theorem for PCF with recursive types, parallel-or and ∃
A universality theorem for PCF with recursive types, parallel-or and ∃
复制标题
具有递归类型、并行或和 ∃ 的 PCF 普适性定理
DOI：
10.1017/s0960129500000384
复制
发表时间：
1994
影响因子：
0.5
通讯作者：
T. Streicher
中科院分区：
文献类型：
--
作者：
T. Streicher
在一个具有最小不动点操作符“λ”、普洛特金的“连续存在量词”∃和递归类型以及构造函数和析构函数的类PCF型按名称调用的计算演算中，所有可计算的对象都可以用编程语言的术语来表示。根据A.Meyer的术语(参见Meyer(1988))，这种编程语言之所以称为通用语言，是因为它的任何扩展都必须是保守的，因为所有可计算的对象都可以用程序术语来表示。作为副产品，我们得到原则上可以完全避免递归类型，因为它们表现为非递归类型→在语法上可表达的缩回，其中和分别是自然数和布尔值的平面域。
In a PCF-like call-by-name typed λ-calculus with a minimal fixpoint operator, ‘parallelor’, Plotkin's ‘continuous existential quantifier’ ∃ and recursive types together with constructors and destructors, all computable objects can be denoted by terms of the programming language. According to A. Meyer's terminology (cf. Meyer (1988)), such a programming language is called universal in the sense that any extension of it must be conservative, as all computable objects can already be expressed by program terms. As a byproduct, we get that, in principle, recursive types could be totally avoided, as they appear as syntactically expressible retracts of the non-recursive type → , where and are the flat domains of natural numbers and boolean values, respectively.