Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

TL;DR

This paper introduces nominal algebraic Henkin-style models for simply typed lambda-calculus, where variables map to names and lambda-abstraction is modeled as name-abstraction, leading to smaller, more manageable denotations and a theory of incomplete functions.

Contribution

It develops a novel class of nominal models for lambda-calculus and extends the syntax with existential meta-variables to represent incomplete functions.

Findings

Denotations are smaller and better-behaved than traditional models.

Models support a theory of incomplete functions with holes and partial objects.

Enables new approaches to lambda-calculus semantics and incomplete term reasoning.

Abstract

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 \lambda-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.