文章基本信息
- 标题：Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
- 本地全文：下载
- 作者：Murdoch J. Gabbay ; Dominic P. Mulligan
- 期刊名称：Electronic Proceedings in Theoretical Computer Science
- 电子版ISSN：2075-2180
- 出版年度：2011
- 卷号：71
- 页码：58-75
- DOI：10.4204/EPTCS.71.5
- 出版社：Open Publishing Association
- 摘要：We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models.
Using these new models, we then develop a generalisation of λ-term syntax enriching them with existential meta-variables, thus yielding a theory of incomplete functions. This incompleteness is orthogonal to the usual notion of incompleteness given by function abstraction and application, and corresponds to holes and incomplete objects.
