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.

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