2011/10/31 by Murdoch J. Gabbay, Dominic P. Mulligan
Computer Science · #Advanced Algebra and Logic #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.71.5
published as EPTCS 71, 2011, pp. 58-75 · In Proceedings LFMTP 2011, arXiv:1110.6685
openalex publication_date 2011/10/31 · arxiv created 2011/11/01 · arxiv updated 2011/11/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
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.