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 exhibit a class of categorical models of the simply typed $\lambda$-calculus, which we call finitely pointable, and we show that, when used in Salvati's definition, they all recognize 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.

翻译：自动机理论中的一个基本主题是单词和树的正则语言及其众多等价定义。Salvati提出了一种对单类型λ-项正则语言的推广，该推广通过有限集合中的指称语义进行定义。本文为该框架的鲁棒性提供了若干证据。首先，我们给出了一种等价的句法刻画，自然地扩展了Hillebrand和Kanellakis关于单词正则语言与句法λ-可定义性之间联系的开创性工作。其次，我们展示了一类单类型λ-演算的范畴模型，称为有限可点化模型，并证明当将其应用于Salvati的定义时，它们与有限集合范畴所识别的λ-项语言类完全一致。这两个结果的证明均依赖于逻辑关系，并可视为一种更通用的范畴构造的实例，该构造受到先前使用粘合构造对逻辑关系进行范畴化描述的启发。