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

TL;DR

This paper demonstrates that regular languages of lambda-terms defined via denotational semantics are equivalent to those characterized syntactically, using logical relations and categorical methods, confirming the robustness of Salvati's generalization.

Contribution

It provides a syntactic characterization of regular lambda-term languages and proves their equivalence across different models using logical relations and categorical constructions.

Findings

Syntactic characterization extends Hillebrand and Kanellakis's work.

Regular languages recognized by any finitary extensional model match those recognized by finite sets.

Logical relations and categorical methods underpin the equivalence proofs.

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 $\lambda$-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 $\lambda$-definability. Second, we show that any finitary extensional model of the simply typed $\lambda$-calculus, when used in Salvati's definition, recognizes exactly the same class of languages of $\lambda$-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.