Syntactically and semantically regular languages of lambda-terms coincide through logical relations

TL;DR

The paper addresses whether recognizability of languages of simply typed $λ$-terms depends on the chosen semantic model or is intrinsic to the calculus. It establishes (i) a syntactic characterization that extends the classical Hillebrand–Kanellakis link between regular languages and $λ$-definability, and (ii) a model-independence result showing that any finitary extensional model of the simply typed $λ$-calculus recognizes exactly the same language class as the category of finite sets ($FinSet$). Both results are derived via logical relations and a gluing construction, situating recognizability within a broader categorical framework. The findings support the canonical nature of recognizable $λ$-term languages and connect to the profinite space of $λ$-terms, suggesting robustness across semantic incarnations. Overall, the work strengthens the understanding of higher-order regularity and its foundational role in higher-order grammars and related logic.

Abstract

A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $λ$-terms, defined using denotational semantics in finite sets. We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic $λ$-definability. Second, we show that any finitary extensional model of the simply typed $λ$-calculus, when used in Salvati's definition, recognizes exactly the same class of languages of $λ$-terms as the category of finite sets does. The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.