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 的定义中使用任何简单类型λ演算的有限外延模型时，所识别的λ项语言类别与有限集范畴所识别的完全一致。这两个结果的证明依赖于逻辑关系，并可视为一种更一般的范畴结构构造的实例，该构造受先前使用粘合构造对逻辑关系进行范畴化描述的启发。