Not Enough Points Is Enough
Not Enough Points Is Enough
复制标题
积分不够就够了
DOI：
10.1007/978-3-540-74915-8_24
复制
发表时间：
2007
影响因子：
0.8
通讯作者：
Giulio Manzonetto
中科院分区：
文献类型：
--
作者：
A. Bucciarelli;T. Ehrhard;Giulio Manzonetto
非类型化λ演算的模型既可以定义为满足一阶公理的应用结构(λ模型)，也可以定义为笛卡尔闭合范畴中的自反对象(范畴模型)。在这篇文章中，我们证明了λ演算的任何范畴模型都可以被表示为λ模型，即使基础范畴没有足够的点。我们给出了一个λ演算在没有足够点的集合和关系范畴中的扩展模型的一个例子。最后，我们给出了它的一些代数性质，这些性质使它适合于处理λ演算的非确定性扩张。
Models of the untyped λ-calculus may be defined either as applicative structures satisfying a bunch of first-order axioms (λ-models), or as reflexive objects in cartesian closed categories (categorical models). In this paper we show that any categorical model of λ-calculus can be presented as a λ-model, even when the underlying category does not have enough points. We provide an example of an extensional model of λ-calculus in a category of sets and relations which has not enough points. Finally, we present some of its algebraic properties which make it suitable for dealing with non-deterministic extensions of λ-calculus.