IRIF & Université Paris Cité & Inria Paris, France and
http://www.irif.fr/~moreaumoreau@irif.frhttps://orcid.org/0009-0005-0638-1363
Laboratoire de l’informatique du parallélisme (LIP), École normale supérieure
de Lyon, France and
https://nguyentito.eu/nltd@nguyentito.euhttps://orcid.org/0000-0002-6900-5577Supported
by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the
program Investissements d’Avenir (ANR-11-IDEX-0007) operated by the French
National Research Agency (ANR). Vincent Moreau and Lê Thành Dũng Nguyễn
[500]Theory of computation Denotational semantics [300]Theory of computation
Regular languages Official conference proceedings
versionhttps://dx.doi.org/10.4230/LIPIcs.CSL.2024.40

###### Acknowledgements.

We would like to thank Amina Doumane, Sam van Gool, Paul-André Melliès and
Sylvain Salvati for in-depth discussions that significantly helped us refine
our ideas. We are also grateful to Sam and Paul-André for proof-reading drafts
of this paper, and to the ReFL discussion group https://www.engboris.fr/refl/
for hosting a reading group on logical relations and normalization by
evaluation. The first author would like to thank the Felicissimo family for
their support during the writing process of this article.Aniello Murano and
Alexandra Silva 2 32nd EACSL Annual Conference on Computer Science Logic (CSL
2024) CSL 2024 CSL 2024 February 19–23, 2024 Naples, Italy 288 12

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

Vincent Moreau  Lê Thành Dũng (Tito) Nguyễn

###### 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.

###### keywords:

regular languages, simple types, denotational semantics, logical relations

###### category:

###### keywords:

linktext=doi:10.4230/LIPIcs.CSL.2024.40

##  1 Introduction

Much work has been devoted to the study of regular languages of words and
trees – also called recognizable – and their equivalent characterizations,
typically in terms of automata, algebra, and logic. The remarkable robustness
of this notion of regularity has led to attempts to extend it to several other
structures, such as infinite words/trees or graphs of bounded treewidth – many
examples can be found, for instance, in [DBLP:journals/corr/abs-2008-11635].

This paper focuses on a less studied extension: recognizable languages of
simply typed $\lambda$-terms, introduced by Salvati
[DBLP:conf/wollic/Salvati09]. They are a conservative generalization
[DBLP:conf/wollic/Salvati09, §3]:111Alternatively, see [entics:12280,
Proposition 7.1] for the case of words. using the Church encoding, finite
words and trees can be represented in the simply typed $\lambda$-calculus, and
recognizability for Church encodings coincides with the usual notion of
regularity. Furthermore, as Salvati explains in his habilitation thesis
[DBLP:books/hal/Salvati15], regular languages of $\lambda$-terms can be used
to shed light on several classical topics concerning the simply typed
$\lambda$-calculus, such as higher-order matching [DBLP:conf/wollic/Salvati09,
§6.2] and higher-order grammars [DBLP:journals/iandc/KobeleS15].

However, not many characterizations of the class of recognizable languages of
simply typed $\lambda$-terms are known, and it would be desirable to have more
evidence that it is robust. Moreover, if we know that this class of languages
is a truly canonical object, then so is its Stone dual, namely the recently
introduced space of profinite $\lambda$-terms [entics:12280]. Currently, there
exist two definitions of recognizable languages of $\lambda$-terms, both
provided in [DBLP:conf/wollic/Salvati09]:

  * •

The first one [DBLP:conf/wollic/Salvati09, Definition 1] uses denotational
semantics into the finite standard models of the simply typed
$\lambda$-calculus. This may be understood as generalizing to higher orders
the computational aspects of deterministic finite automata. In the same vein,
the concrete construction of profinite $\lambda$-terms in [entics:12280]
depends on specific properties of the category $\mathbf{FinSet}$ of finite
sets and functions between them.

  * •

The second one, grounded in intersection types [DBLP:conf/wollic/Salvati09,
§4], turns out to admit an equivalent presentation in terms of a denotational
semantics in finite domains [DBLP:books/hal/Salvati15, Theorem 25]. Indeed,
the connection between intersection types and semantics is standard, see e.g.
[ronchidellarocca:LIPIcs:2018:9861].

Both definitions can be seen as an instance of the following pattern: the
interpretation of a simply typed $\lambda$-term in some denotational model
with a finitary flavor should suffice to know whether the term belongs to our
language of interest. This is closely analogous to the algebraic definition of
regular word languages. Indeed, viewing the set $\Sigma^{*}$ of words over a
finite alphabet $\Sigma$ as the free monoid generated by $\Sigma$, a language
$L\subseteq\Sigma^{*}$ is regular if and only if, for some homomorphism
$\varphi\colon\Sigma^{*}\to M$ to a finite monoid $M$, the interpretation
$\varphi(w)$ determines222More formally, $L=\varphi^{-1}(P)$ for some
$P\subseteq M$. whether $w\in L$ for each $w\in\Sigma^{*}$. Asking for
$\varphi$ to be a homomorphism parallels the compositionality property of
denotational semantics.

We may therefore ask:

  * •

What kind of semantics yield the same notion of recognizable language? More
precisely, with a definition of $\mathbf{C}$-recognizable language for any
cartesian closed category (CCC) $\mathbf{C}$, i.e. any categorical model of
the simply typed $\lambda$-calculus with products, the question becomes: when
do recognizability by $\mathbf{C}$ and by $\mathbf{FinSet}$ coincide?

  * •

Alternatively, is there any characterization of regular languages of
$\lambda$-terms that does not involve denotational semantics?

For the latter, we propose a positive answer inspired by the following result
of Hillebrand and Kanellakis [DBLP:conf/lics/HillebrandK96, Theorem 3.4]: a
language of words is regular if and only if it can be decided by a simply
typed $\lambda$-term operating on Church-encoded words. By replacing the type
of Church encodings with any simple type $A$, we get a natural notion of
syntactically regular language of $\lambda$-terms, defined by means purely
internal to the simply typed $\lambda$-calculus.

#### Contributions and proof methods.

The main results of this paper are as follows:

Theorem 3.2

any non-degenerate cartesian closed category can recognize at least every
language which is syntactically regular.

Theorem 5.10

every language recognized by a locally finite and well-pointed CCC – in other
words, a finitary extensional model of the simply typed $\lambda$-calculus –
is recognized by $\mathbf{FinSet}$. This was first stated by Salvati without
proof in [DBLP:books/hal/Salvati15, Lemma 20].

Theorem 6.5

every language recognized by $\mathbf{FinSet}$ is syntactically regular.

These three theorems, taken together, show that all non-degenerate, well-
pointed and locally finite CCCs yield the same notion of regular language of
$\lambda$-terms, which is the same as the syntactic one.

To achieve this goal, we introduce a construction on CCCs, which we call
squeezing, and combine it with the standard categorical account of logical
relations based on sconing. Indeed, Salvati claims in
[DBLP:books/hal/Salvati15] that Theorem 5.10 can be established via logical
relations, and it turns out that this falls out directly from our squeezing
construction; but its versatility also allows us to apply it to prove the more
diffcult Theorem 6.5 on syntactic recognizability.

#### Related work.

Morally, the study of regular languages of $\lambda$-terms amounts to
understanding what information can be extracted by evaluating simply typed
$\lambda$-terms in finitary models. A seminal result in this spirit is
Statman’s finite completeness theorem [DBLP:journals/jsyml/Statman82], which
can be rephrased as the regularity of all singleton languages of
$\lambda$-terms – a perspective that has led to a simplified proof
[DBLP:journals/ipl/SrivathsanW12]. The idea of using another CCC than
$\mathbf{FinSet}$, easier to use to show Statman’s theorem, has been exploited
in [DBLP:journals/iandc/KobeleS15]. This shows the advantage to use an
appropriate CCC to recognize a given language, a possibility which is extended
to a vast class of CCCs in this paper (see Proposition 7.3 for an example of
application).

Finitary semantics are powerful tools, in particular, for understanding the
computational power of the simply typed $\lambda$-calculus. For instance, in
[DBLP:conf/lics/HillebrandK96], Hillebrand and Kanellakis use the finite set
semantics to prove their aforementioned theorem on regular word languages; as
for finite Scott domains presented as intersection types, they have been
applied by Terui [Terui] to study the complexity of normalizing simply typed
$\lambda$-terms.

As can be seen inter alia from rather surprising results of Statman
[DBLP:journals/apal/Statman04] and Plotkin
[DBLP:journals/corr/abs-2206-08413], finitary models are also useful to tame
the infinitary aspects of an extension of the simply typed $\lambda$-calculus
with a fixed-point operator, called the $\lambda Y$-calculus. Furthermore, the
well-studied higher-order model checking problem is about testing regular
properties on infinite trees that can be Church-encoded in the $\lambda
Y$-calculus; it sits at the interface between automata and programming
languages, with applications to the formal verification of functional programs
(see e.g. [DBLP:conf/ppdp/Kobayashi19]). Decidability of higher-order model
checking, first established by Ong through game semantics
[DBLP:conf/lics/Ong06], now admits proofs based on intersection types
[DBLP:journals/jacm/Kobayashi13, DBLP:conf/lics/Ong15] and on finitary
semantics [DBLP:journals/siglog/Walukiewicz16, grellois:tel-01311150]. Drawing
on this line of work, higher-order parity automata [HOParity] generalize to
$\lambda Y$-terms the recognizable languages of simply typed $\lambda$-terms.

The theme of syntactic recognizability à la Hillebrand and Kanellakis, for its
part, has been recently revived in Nguyễn and Pradic’s implicit333The name is
a nod to implicit computational complexity, a field concerned with alternative
definitions of complexity classes that avoid low-level machine models and
explicit resource bounds. As an example, in addition to their result on
regular word languages in the simply typed $\lambda$-calculus, Hillebrand and
Kanellakis’s paper [DBLP:conf/lics/HillebrandK96] also contains
characterizations of the $k$-EXPTIME and $k$-EXPSPACE hierarchies based on
$\lambda$-terms, that are again proved by evaluation in finite sets. automata
theory. They use substructural $\lambda$-calculi and Church encodings to
characterize star-free languages [iatlc1] and classes of string-to-string
functions computed by transducers [titoPhD].

#### Plan of the paper.

We start by recalling in Section 2 the semantics of the simply typed
$\lambda$-calculus, the notion of language recognized by a CCC as defined in
[DBLP:conf/wollic/Salvati09] for finite sets, and by introducing the notion of
syntactically regular language, generalizing recognition as defined in
[DBLP:conf/lics/HillebrandK96]. In Theorem 3.2 of Section 3, we show that
every non-degenerate CCC recognizes all syntactically regular languages. In
Section 4, we recall the definition of logical relations and introduce the
squeezing construction
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(-){}{}$
which will be a crucial tool for the two next sections. In Section 5, we
recall the definition of locally finite and well-pointed CCCs, and show in
Theorem 5.10 that CCCs enjoying both conditions do not recognize more
languages than finite sets do. In Theorem 6.5 of Section 6, we show that
languages recognized by finite sets are syntactically regular. We finish this
paper by giving some consequences of the equivalence established by these
three theorems in Section 7.

##  2 Languages of -terms

### Syntax and semantics

We first specify the syntax we are working with. The grammars of types and
preterms are

$A,B::=\mathbbmss{o}\mid A\Rightarrow B\mid A\times B\mid
1\quad\text{and}\quad t,u::=x\mid\lambda(x:A).\,t\mid t\ u\mid\langle
t,u\rangle\mid t_{i}\text{ for $i=1,2$}$

and we consider the usual typing rules and $\beta\eta$-conversion rules, see
e.g. [DBLP:books/daglib/0093287-amadio-curien, §4.1]. We extend the notation
of $t_{i}$, for the projection to the $i^{\text{th}}$ coordinate, to the case
where $t$ is of type $A_{1}\times\dots\times A_{n}$ and $i$ is between $1$ and
$n$. As the $\lambda$-abstractions are annotated, a closed $\lambda$-term has
at most one type derivation. For any simple type $A$, we write
$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\Lambda}(A){}{}$
for the set of closed simply typed $\lambda$-terms of type $A$, taken modulo
$\beta\eta$-conversion.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

We recall the semantics of the simply typed $\lambda$-calculus into cartesian
closed categories, abbreviated as CCC, see [DBLP:books/daglib/0093287-amadio-
curien, Chapter 4] for more details. For any CCC $\mathbf{C}$, object $c$ of
$\mathbf{C}$ and simple type $A$, we define an object $\llbracket
A\rrbracket_{c}$ of $\mathbf{C}$ by induction on $A$ as follows:

$\llbracket\mathbbmss{o}\rrbracket_{c}\ :=\ c\qquad\llbracket A\Rightarrow
B\rrbracket_{c}\ :=\ \llbracket A\rrbracket_{c}\Rightarrow\llbracket
B\rrbracket_{c}\qquad\llbracket A\times B\rrbracket_{c}\ :=\ \llbracket
A\rrbracket_{c}\times\llbracket B\rrbracket_{c}\qquad\llbracket
1\rrbracket_{c}\ :=\ 1$

Using the CCC structure of $\mathbf{C}$, one can define a family of set-
theoretic functions

$\left\llbracket{-}\right\rrbracket_{c}\quad:\quad{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}\
\longrightarrow\ \mathbf{C}(1,\llbracket A\rrbracket_{c})\qquad\text{for every
simple type\leavevmode\nobreak\ $A$}$

called semantic brackets, sending closed $\lambda$-terms to points of the
objects $\llbracket A\rrbracket_{c}$.

These assignments can be described in another way. Let $\mathbf{Lam}$ be the
category whose objects are simple types and whose set of morphisms from $A$ to
$B$ is
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A\Rightarrow
B){}{}$, with the expected composition. This category is the free CCC on one
object, i.e., for every CCC $\mathbf{C}$ and object $c$ of $\mathbf{C}$, there
exists a unique CCC functor
$\left\llbracket-\right\rrbracket_{c}:\mathbf{Lam}\to\mathbf{C}$ such that
$\left\llbracket\mathbbmss{o}\right\rrbracket_{c}=c$. This can be represented
by the commutativity of the following diagram:

${\mathbf{Lam}}$${1}$${\mathbf{C}}$$\scriptstyle{c}$$\scriptstyle{\mathbbmss{o}}$$\scriptstyle{\left\llbracket-\right\rrbracket_{c}}$
(1)

In this paper, the CCCs come with specified terminal object, cartesian
products, and exponentials, and CCC functors are required to respect these
structures strictly, _on the nose_. In that way, the unicity in the universal
property of $\mathbf{Lam}$ depicted in Equation 1 holds up to equality, and
not merely isomorphism.

We write $\mathbf{FinSet}$ for the cartesian closed category of finite sets.
The semantics of the simply typed $\lambda$-calculus in this CCC corresponds
to its naive set-theoretic interpretation. For ease of notation, we identify
the finite set $Q$ with the set of functions $\mathbf{FinSet}(1,Q)$.

### Recognizable languages of -terms, semantically

We now define the notion of $\mathbf{C}$-recognizable language of
$\lambda$-terms, for any CCC $\mathbf{C}$. The case
$\mathbf{C}=\mathbf{FinSet}$ corresponds to the notion of regular language of
simply typed $\lambda$-terms introduced in [DBLP:conf/wollic/Salvati09,
Definition 1].

######  Definition 2.1.

Let $\mathbf{C}$ be a CCC and $c$ be an object of $\mathbf{C}$. For every
simple type $A$ and subset $F\subseteq\mathbf{C}(1,\llbracket
A\rrbracket_{c})$, the language
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}$
of $\lambda$-terms of type $A$ is defined as

$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}L}_{F}{}{}\quad:=\quad\\{t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}\mid\left\llbracket
t\right\rrbracket_{c}\in F\\}\ .$

We define the set
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{c}(A){}{}$
of languages of $\lambda$-terms of type $A$ recognized by $c$ as

$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\operatorname{Rec}}_{c}(A){}{}\quad:=\quad\\{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}:F\subseteq\mathbf{C}(1,\llbracket
A\rrbracket_{c})\\}\ .$

Finally, a language $L$ of $\lambda$-terms of type $A$ is
$\mathbf{C}$-_recognizable_ if there exists an object $c$ of $\mathbf{C}$ such
that $L$ belongs to the set
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{c}(A){}{}$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Example 2.2.

For any natural number $n$, we define the associated simple type

${\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\textsf{{Church}}}}_{n}{}{}\
:=\
(\mathbbmss{o}\Rightarrow\mathbbmss{o})^{n}\Rightarrow\mathbbmss{o}\Rightarrow\mathbbmss{o}\
.$

There is a bijection between the sets
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{n}{}{}){}{}$
and $\\{1,\dots,n\\}^{*}$, the set of finite words over an alphabet with $n$
letters, called the _Church encoding_. For example, the word $12212$ over the
two letter-alphabet $\\{1,2\\}$ is encoded as the $\lambda$-term

$\lambda(a:(\mathbbmss{o}\Rightarrow\mathbbmss{o})^{2}).\,\lambda(e:\mathbbmss{o}).\
a_{2}\ (a_{1}\ (a_{2}\ (a_{2}\ (a_{1}\
e))))\quad\in\quad{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}){}{}\
.$

Under this bijection, a language of $\lambda$-terms of type
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{n}{}{}$
is $\mathbf{FinSet}$-recognizable, in the sense of Definition 2.1, if and only
if the language of words associated by the Church encoding is a regular
language of finite words, see [entics:12280, Proposition 7.1].

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Example 2.3.

We give a detailed example using the Church encoding. We show that the
language $L$ of $\lambda$-terms of type
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}$
which are encodings of words in $\\{1,2\\}^{*}$ that contain an even number of
1s and an odd number of 2s, is $\mathbf{FinSet}$-recognizable.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

Let $Q$ be the finite set $\\{q_{\top},q_{\bot}\\}$ and $F$ be the subset of
$\llbracket{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}\rrbracket_{Q}$
defined as

$F\ :=\ \\{f\in(Q\Rightarrow Q)\times(Q\Rightarrow Q)\Rightarrow Q\Rightarrow
Q\mid
f(\mathrm{not},\operatorname{Id}_{Q})(q_{\top})=f(\operatorname{Id}_{Q},\mathrm{not})(q_{\bot})=q_{\top}\\}$

where $\mathrm{not}:Q\to Q$ is the function defined as
$\mathrm{not}(q_{\top})=q_{\bot}$ and $\mathrm{not}(q_{\bot})=q_{\top}$. The
language $L$ is equal to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}$
which belongs to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{Q}({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}){}{}$,
so $L$ is $\mathbf{FinSet}$-recognizable.

The idea is that, given the semantic interpretation
$f\in\llbracket{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}\rrbracket_{Q}$
of the encoding of a word $w\in\\{1,2\\}^{*}$, the states
$f(\mathrm{not},\operatorname{Id}_{Q})(q_{\top})$ and
$f(\operatorname{Id}_{Q},\mathrm{not})(q_{\bot})$ are the states reached
respectively, after reading $w$, in the two following deterministic finite
automata:

$\;q_{\top}\;$start$q_{\bot}$1122 $\;q_{\top}\;$$q_{\bot}$start2211

The language $L$ is the intersection of the two languages recognized by these
automata.

######  Example 2.4.

We consider the simple type

$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\textsf{{UntypedTerms}}}{}{}\quad:=\quad((\mathbbmss{o}\Rightarrow\mathbbmss{o})\Rightarrow\mathbbmss{o})\Rightarrow(\mathbbmss{o}\Rightarrow\mathbbmss{o}\Rightarrow\mathbbmss{o})\Rightarrow\mathbbmss{o}\
.$

There is a canonical bijection – which is classical, see e.g.
[DBLP:conf/tlca/Atkey09] for an in-depth treatment – between
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}){}{}$
and the set of closed untyped $\lambda$-terms modulo $\alpha$-renaming, i.e.
syntax trees with binders, without $\beta$-conversion. Here are examples of
encodings of the latter into the former (for the general definition, see
Appendix A):

$\displaystyle\lambda x.\,x\,x\quad\rightsquigarrow\quad$
$\displaystyle{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\lambda(\ell:(\mathbbmss{o}\Rightarrow\mathbbmss{o})\Rightarrow\mathbbmss{o}).\,\lambda(a:\mathbbmss{o}\Rightarrow\mathbbmss{o}\Rightarrow\mathbbmss{o}).}\,$
$\displaystyle\quad{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\ell\
(}\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}x{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a}\
x\
x{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625})}$
$\displaystyle(\lambda x.\,x\,x)\ (\lambda
x.\,x\,x)\quad\rightsquigarrow\quad$
$\displaystyle{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\lambda(\ell:(\mathbbmss{o}\Rightarrow\mathbbmss{o})\Rightarrow\mathbbmss{o}).\,\lambda(a:\mathbbmss{o}\Rightarrow\mathbbmss{o}\Rightarrow\mathbbmss{o}).}\,$
$\displaystyle\quad{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a\
(\ell}\
(\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}x{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a}\
x\
x){\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625})}\
{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(\ell}\
(\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}x{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a}\
x\
x){\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625})}$
$\displaystyle\lambda f.\,(\lambda x.\,x\,x)\,(\lambda
x.\,f\,(x\,x))\quad\rightsquigarrow\quad$
$\displaystyle{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\lambda(\ell:(\mathbbmss{o}\Rightarrow\mathbbmss{o})\Rightarrow\mathbbmss{o}).\,\lambda(a:\mathbbmss{o}\Rightarrow\mathbbmss{o}\Rightarrow\mathbbmss{o}).}\,$
$\displaystyle\quad{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\ell\
(}\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}f{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a\
(\ell}\
(\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}x{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a}\
x\
x){\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625})}$
$\displaystyle\quad\phantom{{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\ell\
(}\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}f{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a\
(\ell}}\
{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(\ell}\
(\lambda{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}(}x{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}\
:\mathbbmss{o})}.\,{\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a}\
f\
({\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}a}\
x\
x)){\color[rgb]{0.6640625,0.44921875,0.16015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6640625,0.44921875,0.16015625}))}$

This can be seen as an extension of Church encodings to higher-order abstract
syntax: indeed, the variable $\ell$ plays the role of a constructor and
introduces a bound variable.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

A closed untyped term is _affine_ if and only if every bound variable occurs
at most once. We now give the outline of the proof, detailed in Appendix A,
that the encodings in
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}){}{}$
of closed untyped affine terms form a $\mathbf{FinSet}$-recognizable language.

Let $Q$ be the finite set $\\{0,1,\infty\\}\times\\{\top,\bot\\}$, where
$\\{0,1,\infty\\}$ is seen as the additive monoid $\mathbb{N}$ truncated to
$2=3=\dots=\infty$. We consider the two set-theoretic functions
$f_{\textup{{app}}}:Q\to(Q\Rightarrow Q)$ and
$f_{\textup{{abs}}}:(Q\Rightarrow Q)\to Q$ defined as

$f_{\textup{{app}}}(k,b)(k^{\prime},b^{\prime})\ :=\ (k+k^{\prime},\;b\wedge
b^{\prime})\quad\text{and}\quad f_{\textup{{abs}}}(g)\ :=\
(g_{1}(0,\top),\;g_{2}(0,\top)\wedge(g_{1}(1,\top)\leq 1))$

where $g_{1}:Q\to\\{0,1,\infty\\}$ and $g_{2}:Q\to\\{\top,\bot\\}$ are the
compositions of $g:Q\to Q$ with the two projections. We verify that, for any
closed untyped term $t$, we have

$\left\llbracket
t\right\rrbracket_{Q}(f_{\textup{{abs}}})(f_{\textup{{app}}})\quad=\quad(0,b)\qquad\text{where
$b$ is $\top$ if and only if $t$ is affine.}$

Therefore, if $F$ is the subset of
$\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}\rrbracket_{Q}$
defined as

$F\ :=\ \\{s\in((Q\Rightarrow Q)\Rightarrow Q)\Rightarrow(Q\Rightarrow
Q\Rightarrow Q)\Rightarrow Q\mid
s(f_{\textup{{abs}}})(f_{\textup{{app}}})=(0,\top)\\}$

then the $\mathbf{FinSet}$-recognizable language
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}$
of terms of type UntypedTerms is the language of affine terms.

To the best of our knowledge, this regularity result is original. It also
strongly suggests that the notion of $\mathbf{FinSet}$-recognizable language,
when applied to the type UntypedTerms of syntax trees with binders, differs
from the recognizability of these syntax trees by the nominal tree automata of
[vanheerdt_et_al:LIPIcs:2019:11434, §3.1]. Indeed, nominal automata cannot
recognize the language of data words whose letters are all different
[DBLP:journals/corr/BojanczykKL14, Proof of Lemma 5.4].

######  Remark 2.5.

Let $\mathbf{C}$ and $\mathbf{D}$ be CCCs and $G:\mathbf{C}\to\mathbf{D}$ be a
CCC functor. By the universal property of $\mathbf{Lam}$, see Equation 1, for
every object $c$ of $\mathbf{C}$, the following diagram commutes:

${\mathbf{Lam}}$${1}$${\mathbf{C}}$${\mathbf{D}}$$\scriptstyle{\mathbbmss{o}}$$\scriptstyle{c}$$\scriptstyle{G}$$\scriptstyle{\left\llbracket-\right\rrbracket_{c}}$$\scriptstyle{\left\llbracket-\right\rrbracket_{G(c)}}$

In particular, this means that for every simple type $A$, the objects
$\llbracket A\rrbracket_{G(c)}$ and $G(\llbracket A\rrbracket_{c})$ are equal,
and that for every simply typed $\lambda$-terms $t$ and $t^{\prime}$ of type
$A$,

$\text{if}\quad\left\llbracket t\right\rrbracket_{c}\ =\ \left\llbracket
t^{\prime}\right\rrbracket_{c}\qquad\text{then}\quad\left\llbracket
t\right\rrbracket_{G(c)}\ =\ \left\llbracket
t^{\prime}\right\rrbracket_{G(c)}\ .$

This means that interpreting the simply typed $\lambda$-calculus at the object
$c$ will always be at least as fine as interpreting it at $G(c)$. In
particular, this entails that
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{G(c)}(A){}{}\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{c}(A){}{}$.
If $G$ is moreover faithful, we then have that
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{G(c)}(A){}{}={\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{c}(A){}{}$
for any object $c$ of $\mathbf{C}$. Therefore, all languages which are
$\mathbf{C}$-recognizable are $\mathbf{D}$-recognizable.

### Recognizable languages of -terms, syntactically

A syntactic approach to recognition is described in
[DBLP:conf/lics/HillebrandK96]. This syntactic approach uses the type
substitution, also called cast, whose definition we now recall.

######  Definition 2.6.

If $A$ and $B$ are simple types, we define a simple type
$A[B]=A\\{\mathbbmss{o}:=B\\}$ by replacing every occurence of $\mathbbmss{o}$
in $A$ by $B$. We extend this to $\lambda$-terms by induction:

$\displaystyle x[B]\ $ $\displaystyle:=\ x$
$\displaystyle(\lambda(x:A).\,t)[B]\ $ $\displaystyle:=\
\lambda(x:A[B]).\,t[B]$ $\displaystyle(t\ u)[B]\ $ $\displaystyle:=\ t[B]\
u[B]$ $\displaystyle\langle t,u\rangle[B]\ $ $\displaystyle:=\ \langle
t[B],u[B]\rangle$ $\displaystyle t_{i}[B]\ $ $\displaystyle:=\ (t[B])_{i}$

######  Claim 1.

For every simple types $A$ and $B$ and
$t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}$,
we have
$t[B]\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A[B]){}{}$.

######  Remark 2.7.

A more categorical way to understand casting is to see it as the unique CCC
functor $(-)[B]:\mathbf{Lam}\to\mathbf{Lam}$ such that the following diagram
commutes:

${\mathbf{Lam}}$${1}$${\mathbf{Lam}}$$\scriptstyle{B}$$\scriptstyle{\mathbbmss{o}}$$\scriptstyle{(-)[B]}$

As such, it is the semantic bracket functor
$\left\llbracket-\right\rrbracket_{B}:\mathbf{Lam}\to\mathbf{Lam}$.

Finally, we recall the encoding of Booleans into the simply typed
$\lambda$-calculus.

######  Definition 2.8.

Let Bool be the simple type $\mathbbmss{o}^{2}\Rightarrow\mathbbmss{o}$. Its
two inhabitants are the $\lambda$-terms

$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\textsf{{true}}}{}{}\
:=\
\lambda(x:\mathbbmss{o}^{2}).\,x_{1}\qquad\text{and}\qquad\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\textsf{{false}}}{}{}\
:=\ \lambda(x:\mathbbmss{o}^{2}).\,x_{2}\ .$

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

The following definition naturally generalizes the one given in
[DBLP:conf/lics/HillebrandK96] for
$A={{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{n}{}{}$.

######  Definition 2.9.

For any simple type $A$, a language
$L\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}$
is _syntactically regular_ if there exists a simple type $B$ and a
$\lambda$-term $r$ of type
$A[B]\Rightarrow{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}$
such that

$L\ =\
\\{t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}\mid
r\
t[B]=_{\beta\eta}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}\\}\
.$

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Theorem 2.10 (Hillebrand & Kanellakis, [DBLP:conf/lics/HillebrandK96,
Theorem 3.4]).

A language of $\lambda$-terms of type
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{n}{}{}$
is syntactically regular if and only if the associated language of finite
words by the Church encoding is regular in the usual sense.

######  Example 2.11.

The Church encodings of words in $\\{1,2\\}^{*}$ with an even number of 1s and
an odd number of 2s is syntactically regular. Indeed, we consider the
following $\lambda$-terms

$\displaystyle\mathsf{and}\ $ $\displaystyle:=\
\lambda(p:{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}\times{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}).\,\lambda(x:\mathbbmss{o}\times\mathbbmss{o}).\,p_{1}\
\langle p_{2}\ x,x_{2}\rangle$ $\displaystyle\mathsf{id}\ $ $\displaystyle:=\
\lambda(b:{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}).\,b$
$\displaystyle\mathsf{not}\ $ $\displaystyle:=\
\lambda(b:{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}).\,\lambda(x:\mathbbmss{o}\times\mathbbmss{o}).\,b\
\langle x_{2},x_{1}\rangle$

and choose, as in Definition 2.9, the type $B$ to be Bool and the simply typed
$\lambda$-term $r$ to be

$\lambda(w:{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}[{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}]).\,\mathsf{and}\
\langle w\ \mathsf{not}\ \mathsf{id}\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{},\
w\ \mathsf{id}\ \mathsf{not}\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{false}}}{}{}\rangle\quad:\quad{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{2}{}{}[{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}]\Rightarrow{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}\
.$

Just as in Example 2.3, this term can be seen as running two DFAs, both having
two states, over the encoding of an input word.

When restricted to types
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{n}{}{}$
for any natural number $n$, the notion of $\mathbf{FinSet}$-recognizable and
syntactically regular languages coincide, as they both boil down to the usual
notion of regular language of finite words, as seen in Example 2.2 and Theorem
2.10 respectively. One of the contributions of the present paper is to show
that these two notions coincide at every simple type.

##  3 Syntactic recognition implies semantic recognition

In this section, we state Theorem 3.2 and prove it by extending the semantic
evaluation argument, described by Hillebrand and Kanellakis in their proof of
Theorem 2.10 for the case of languages of words, to the more general case of
languages of any type.

######  Definition 3.1.

A CCC $\mathbf{C}$ is said to be _non-degenerate_ if there exist two objects
$c^{\prime},c$ of $\mathbf{C}$ such that there exist two distinct morphisms
$f,g\colon c^{\prime}\to c$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Theorem 3.2.

If $\mathbf{C}$ is a non-degenerate CCC, then any language of $\lambda$-terms
which is syntactically regular is $\mathbf{C}$-recognizable.

######  Proof 3.3.

We observe first that the non-degeneracy assumption means that the two
projections $\pi_{1},\pi_{2}\colon c\times c\to c$ are not equal, since they
yield different results when pre-composed with the morphism $c^{\prime}\to
c\times c$ obtained by pairing $f$ and $g$.

Let $A$ be a simple type and $L$ be a language of $\lambda$-terms of type $A$
which is syntactically regular. There exists a simple type $B$ together with a
$\lambda$-term
$r\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A[B]\Rightarrow{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}){}{}$
such that

$L\quad=\quad\\{t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}\mid
r\
t[B]=_{\beta\eta}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}\\}\
.$

In order to show that $L$ belongs to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{\llbracket
B\rrbracket_{c}}(A){}{}$, we work with the interpretation of the simply typed
$\lambda$-calculus at the object $\llbracket B\rrbracket_{c}$ of $\mathbf{C}$.
By the universal property of the CCC $\mathbf{Lam}$, the following diagram
commutes

$\immediate\immediate\immediate\leavevmode\hbox to120.22pt{\vbox
to46.41pt{\pgfpicture\makeatletter\hbox{\hskip 60.11108pt\lower-23.2526pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-60.11108pt}{-23.15276pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
14.09723pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.79169pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbf{Lam}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
14.09723pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
6.80554pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${1}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
6.80554pt\hfil&\hfil\hskip 38.0972pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.79169pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbf{Lam}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
14.09723pt\hfil&\hfil\hskip 31.91663pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.61111pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathbf{C}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.91666pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-39.00832pt}{-20.65276pt}\pgfsys@lineto{-8.51662pt}{-20.65276pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.31664pt}{-20.65276pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.39285pt}{-18.29999pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{B}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{} { {}{}{}}{}{ {}{}{}}{}{
{}{}{}}{}{ {}{}{}}{}{ {}{}{}}{}{{{}}{{}}{{}}{}}{}{{}}{{}}{ {}{}{}}{}{
{}{}{}}{}{ {}{}{}}{}{{{}}{{}}{{}}{}}{}{{}}{ {}{}{}}{}{{}}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}}{}{}{}{}{{}}{}{{}}{}{}{}{}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-31.71663pt}{13.59259pt}\pgfsys@curveto{-6.03981pt}{17.3529pt}{23.4215pt}{7.70744pt}{43.79295pt}{-12.37422pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.71214}{-0.70203}{0.70203}{0.71214}{43.93536pt}{-12.5146pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.41603pt}{14.06755pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\left\llbracket-\right\rrbracket_{\llbracket
B\rrbracket_{c}}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-46.01385pt}{-12.84862pt}\pgfsys@lineto{-46.01385pt}{4.74036pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-46.01385pt}{4.94034pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-51.86662pt}{-5.3611pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathbbmss{o}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-35.69049pt}{5.14032pt}\pgfsys@lineto{-7.45811pt}{-12.24997pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.85144}{-0.52446}{0.52446}{0.85144}{-7.28786pt}{-12.35486pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.05127pt}{0.44307pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{(-)[B]}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{20.4778pt}{-20.65276pt}\pgfsys@lineto{43.67781pt}{-20.65276pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{43.87779pt}{-20.65276pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.99562pt}{-16.9pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\left\llbracket-\right\rrbracket_{c}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\ .$

More concretely, this states that, for every simply typed $\lambda$-term $t$,
the two morphisms $\left\llbracket t[B]\right\rrbracket_{c}$ and
$\left\llbracket t\right\rrbracket_{\llbracket B\rrbracket_{c}}$ are equal. By
viewing $r$ as a morphism from $A[B]$ to Bool in the category $\mathbf{Lam}$,
the compositionality of the semantic interpretation gives us that

$\left\llbracket r\ t[B]\right\rrbracket_{c}\ =\ \left\llbracket
r\right\rrbracket_{c}\circ\left\llbracket t[B]\right\rrbracket_{c}\ =\
\left\llbracket r\right\rrbracket_{c}\circ\left\llbracket
t\right\rrbracket_{\llbracket B\rrbracket_{c}}\ .$

By non-degeneracy, the semantic interpretation
$\left\llbracket-\right\rrbracket_{c}:{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}){}{}\to\mathbf{C}(1,\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Bool}}}{}{}\rrbracket_{c})$
is injective: indeed,
$\left\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}\right\rrbracket_{c}=\pi_{1}\neq\pi_{2}=\left\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{false}}}{}{}\right\rrbracket_{c}$.
Therefore, we get the following equivalences

$t\in L\ \iff\ r\
t[B]=_{\beta\eta}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}\
\iff\ \left\llbracket r\
t[B]\right\rrbracket_{c}=\left\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}\right\rrbracket_{c}\
\iff\ \left\llbracket t\right\rrbracket_{\llbracket B\rrbracket_{c}}\in F$

where $F$ is the subset of $\mathbf{C}(1,\llbracket A\rrbracket_{\llbracket
B\rrbracket_{c}})$ defined as $\\{q\in\mathbf{C}(1,\llbracket
A\rrbracket_{\llbracket B\rrbracket_{c}})\mid\left\llbracket
r\right\rrbracket_{c}\circ
q=\left\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}\right\rrbracket_{c}\\}$.
This shows that $L$ belongs to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{\llbracket
B\rrbracket_{c}}(A){}{}$, hence that it is a $\mathbf{C}$-recognizable
language.

##  4 Logical relations and the squeezing construction

### Sconing in a nutshell

In this paragraph, we recall the construction of a CCC of logical relations
from one CCC to another. We first recall the construction of logical
predicates, also called sconing, which will be general enough to give logical
relations as a special case. This method is well-known, see for instance
[DBLP:conf/csl/MitchellS92] for an introductory account.

######  Definition 4.1.

Let $\mathbf{C}$ be a CCC. The category of logical predicates over
$\mathbf{C}$, that we denote by
$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\mathbf{P}}(\mathbf{C}){}{}$,
is defined as follows:

  * •

its objects are the pairs $(c,S)$ of an object $c$ of $\mathbf{C}$ together
with a subset $S\subseteq\mathbf{C}(1,c)$,

  * •

its morphisms from $(c,S)$ to $(c^{\prime},S^{\prime})$ are the morphisms
$f:c\to c^{\prime}$ of $\mathbf{C}$ such that $f\circ(-)$ restricts to a set-
theoretic function $S\to S^{\prime}$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Claim 2.

This category
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{P}}(\mathbf{C}){}{}$
is a CCC, with exponentiation given by

$(c,S)\Rightarrow(c^{\prime},S^{\prime})\quad=\quad(c\Rightarrow
c^{\prime},\\{f\in\mathbf{C}(1,c\Rightarrow c^{\prime})\mid\forall s\in
S,\operatorname{ev}_{c,c^{\prime}}\circ\langle f,s\rangle\in S^{\prime}\\})$

The forgetful functor $(c,S)\mapsto c$ is a CCC functor.

See [DBLP:conf/csl/MitchellS92, p. 5], where the notation $\tilde{\mathbf{C}}$
is used for the category
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{P}}(\mathbf{C}){}{}$.

######  Definition 4.2.

Let $\mathbf{C}_{1}$ and $\mathbf{C}_{2}$ be two CCCs. The _CCC of logical
relations_ from $\mathbf{C}_{1}$ to $\mathbf{C}_{2}$ is the CCC
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{P}}(\mathbf{C}_{1}\times\mathbf{C}_{2}){}{}$,
which admits a CCC functor
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{P}}(\mathbf{C}_{1}\times\mathbf{C}_{2}){}{}\to\mathbf{C}_{1}\times\mathbf{C}_{2}$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Remark 4.3.

We have defined the CCC of logical relations in terms of the logical predicate
construction
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{P}}(-){}{}$
of Definition 4.1. More concretely, this construction gives a category that
can be described in the following way:

  * •

its objects are triples $(c_{1},c_{2},\Vdash)$ where $c_{i}$ is an object of
$\mathbf{C}_{i}$ for $i=1,2$ and $\Vdash$ is a subset of
$\mathbf{C}_{1}(1,c_{1})\times\mathbf{C}_{2}(1,c_{2})$, and is thus a relation
between the points of $c_{1}$ and of $c_{2}$,

  * •

its morphisms from $(c_{1},c_{2},\Vdash)$ to
$(c_{1}^{\prime},c_{2}^{\prime},\Vdash^{\prime})$ are pairs
$(f_{1},f_{2})\in\mathbf{C}_{1}(c_{1},c_{1}^{\prime})\times\mathbf{C}_{2}(c_{2},c_{2}^{\prime})$
such that for every pair
$(x_{1},x_{2})\in\mathbf{C}_{1}(1,c_{1})\times\mathbf{C}_{2}(1,c_{2})$,

$\text{if}\ x_{1}\Vdash x_{2}\ ,\quad\text{then}\ f_{1}\circ
x_{1}\Vdash^{\prime}f_{2}\circ x_{2}\ .$

For the proof that this category is a CCC, see [DBLP:conf/csl/MitchellS92,
Proposition 4.3].

######  Remark 4.4.

The CCC of logical relations from $\mathbf{C}_{1}$ to $\mathbf{C}_{2}$ comes
with two projections to $\mathbf{C}_{1}$ and to $\mathbf{C}_{2}$ which are CCC
functors. By Remark 2.5, we get that for any relation $(c_{1},c_{2},\Vdash)$,

$\llbracket A\rrbracket_{(c_{1},c_{2},\Vdash)}\quad=\quad(\llbracket
A\rrbracket_{c_{1}},\llbracket A\rrbracket_{c_{2}},\Vdash^{A})\quad\text{for
some $\Vdash^{A}\ \subseteq\ \mathbf{C}_{1}(1,\llbracket
A\rrbracket_{c_{1}})\times\mathbf{C}_{2}(1,\llbracket A\rrbracket_{c_{2}})$.}$

The interpretation of a $\lambda$-term
$t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}$
at an object $(c_{1},c_{2},\Vdash)$ is a morphism of the form

$(\left\llbracket t\right\rrbracket_{c_{1}},\left\llbracket
t\right\rrbracket_{c_{2}})\quad:\quad 1\ \longrightarrow\ \llbracket
A\rrbracket_{(c_{1},c_{2},\Vdash)}\qquad\text{which means
that}\qquad(\left\llbracket t\right\rrbracket_{c_{1}},\left\llbracket
t\right\rrbracket_{c_{2}})\in\Vdash^{A}\ .$

This is the _fundamental lemma of logical relations_ , see e.g.
[DBLP:books/daglib/0093287-amadio-curien, Lemma 4.5.3].

######  Remark 4.5.

At this stage, the categories $\mathbf{C}_{1}$ and $\mathbf{C}_{2}$ play a
symmetric role. However, this will not always be the case in the rest of the
paper, and we therefore say CCC of logical relations from $\mathbf{C}_{1}$ to
$\mathbf{C}_{2}$ to emphasize the order.

### The squeezing construction

We describe here a construction, which we call squeezing, which produces a CCC
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$
from a CCC $\mathbf{C}$ equipped with an additional structure that we call a
squeezing structure. Intuitively, the objects of
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$
are objects of $\mathbf{C}$ coming with bounds induced by the structure,
inspired by the squeeze theorem of calculus. This construction can be seen as
the proof-irrelevant counterpart to the twisted gluing construction described
in [DBLP:conf/ctcs/AltenkirchHS95, Definition 5]. The notion of squeezing
structure that is used is related to the hypotheses of
[DBLP:journals/mscs/Fiore22, Lemma 6]; this pattern also occurs in the older
proof theory tradition, see for instance [girard:hal-01322183, §8.A].

Throughout this paragraph, we fix any CCC $\mathbf{C}$. We recall that a wide
subcategory is a subcategory containing all objects, and can hence be seen as
a predicate on morphisms, closed under finite compositions.

######  Definition 4.6.

A _squeezing structure_ on $\mathbf{C}$ is the data of

  * •

two wide subcategories ${\mathbf{C}}_{\operatorname{left}}$ and
${\mathbf{C}}_{\operatorname{right}}$ of $\mathbf{C}$ with associated
notations $\xrightarrow{\operatorname{l}}$ and
$\xrightarrow{\operatorname{r}}$ for morphisms, which are stable under finite
cartesian products and such that for all
$u:c_{l}\xrightarrow{\operatorname{l}}c_{l}^{\prime}$ and
$v:c_{r}\xrightarrow{\operatorname{r}}c_{r}^{\prime}$,

$v\Rightarrow u\ :\ c_{r}^{\prime}\Rightarrow
c_{l}\overset{\operatorname{l}}{\longrightarrow}c_{r}\Rightarrow
c_{l}^{\prime}\qquad\text{and}\qquad u\Rightarrow v\ :\
c_{l}^{\prime}\Rightarrow
c_{r}\overset{\operatorname{r}}{\longrightarrow}c_{l}\Rightarrow
c_{r}^{\prime}\ .$

  * •

for every object $c$ of $\mathbf{C}$, two objects $L_{c}$ and $R_{c}$ of
$\mathbf{C}$ such that there exists morphisms:

$\immediate\immediate\begin{matrix}L_{1}\overset{\operatorname{l}}{\longrightarrow}1\quad&\quad
L_{c\times c^{\prime}}\overset{\operatorname{l}}{\longrightarrow}L_{c}\times
L_{c^{\prime}}\quad&\quad L_{c\Rightarrow
c^{\prime}}\overset{\operatorname{l}}{\longrightarrow}R_{c}\Rightarrow
L_{c^{\prime}}\\\ 1\overset{\operatorname{r}}{\longrightarrow}R_{1}\quad&\quad
R_{c}\times
R_{c^{\prime}}\overset{\operatorname{r}}{\longrightarrow}R_{c\times
c^{\prime}}\quad&\quad L_{c}\Rightarrow
R_{c^{\prime}}\overset{\operatorname{r}}{\longrightarrow}R_{c\Rightarrow
c^{\prime}}\ .\end{matrix}$ (2)

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Remark 4.7.

As we work in a proof-irrelevant setting, we are merely interested in the
existence of these morphisms. Nonetheless, knowing that they belong to
${\mathbf{C}}_{\operatorname{left}}$ or ${\mathbf{C}}_{\operatorname{right}}$
gets us back some precious information, as we will see in Lemma 4.10 and
Section 6.

######  Definition 4.8.

For a squeezing structure on $\mathbf{C}$, the category
$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\mathbf{Sqz}}(\mathbf{C}){}{}$
is the full subcategory of $\mathbf{C}$ whose objects are the objects $c$ of
$\mathbf{C}$ for which there exist both a left morphism
$L_{c}\xrightarrow{\operatorname{l}}c$ and a right morphism
$c\xrightarrow{\operatorname{r}}R_{c}$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

Notice that we write
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$
even though this construction depends both on the CCC $\mathbf{C}$ and on a
squeezing structure on $\mathbf{C}$.

######  Theorem 4.9.

For a squeezing structure on $\mathbf{C}$, the category
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$
is a sub-CCC of $\mathbf{C}$.

The proof is in Appendix B.

### Partial surjections

Logical relations which are partial surjections, i.e. both functional and
surjective relations, can be a useful tool to obtain partial equivalence
relations and to prove semantic results, see [Bucciarelli96, §3],
[DBLP:journals/tcs/Ehrhard12, §1.4.2] and [entics:12280, Theorem A]. We now
show that the squeezing construction can be applied to get partial surjections
for free.

######  Lemma 4.10.

Let $\mathbf{C}_{1}$ and $\mathbf{C}_{2}$ be two CCCs and $\mathbf{R}$ be the
CCC of logical relations from $\mathbf{C}_{1}$ to $\mathbf{C}_{2}$, whose
objects are triples containing relations. Suppose that we are given a
squeezing structure on $\mathbf{R}$ such that

  * •

the relations in the objects $L_{c}$ are surjective,

  * •

the relations in the objects $R_{c}$ are functional,

  * •

the morphisms $(u_{1},u_{2})$ in ${\mathbf{R}}_{\operatorname{left}}$ are such
that $\mathbf{C}_{2}(1,u_{2})$ is a surjective function,

  * •

the morphisms $(v_{1},v_{2})$ in ${\mathbf{R}}_{\operatorname{right}}$ are
such that $\mathbf{C}_{2}(1,v_{2})$ is an injective function,

where, for $u\in\mathbf{C}(a,b)$, the function
$\mathbf{C}(1,u):\mathbf{C}(1,a)\to\mathbf{C}(1,b)$ is the composition
$u\circ(-)$.

Then, the relation of any object belonging to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{R}){}{}$
is a partial surjection.

The proof is in Appendix C. We end this section by giving a definition which
will appear in squeezing structures in Proposition 6.4 and in the proof of
Proposition 5.9.

######  Definition 4.11.

Let $\mathbf{R}$ be the CCC of logical relations from $\mathbf{C}_{1}$ to
$\mathbf{C}_{2}$. We say that a morphism
$(f_{1},f_{2}):(c_{1},c_{2},\Vdash)\to(c_{1}^{\prime},c_{2}^{\prime},\Vdash^{\prime})$
is a _target-identity_ if $c_{2}$ and $c_{2}^{\prime}$ are the same object and
if $f_{2}$ is the identity morphism.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Remark 4.12.

We remark that the target-identities form a wide subcategory and are stable
under products and exponentiation.

##  5 From well-pointed locally finite CCCs to finite sets

We now recall the definition of the class of CCCs $\mathbf{C}$ for which we
will show that $\mathbf{C}$-recognizable languages coincide with our other
definitions of regular languages of $\lambda$-terms. Recall that in a CCC
$\mathbf{C}$, a _point_ of an object $c$ is a morphism $1\to c$ from the
terminal object to $c$.

######  Definition 5.1.

A CCC is said to be:

  * •

_well-pointed_ if every morphism is determined by its action on points of its
domain;

  * •

_locally finite_ if all its hom-sets are finite sets.

We start by introducing the following constructions, which will help us to use
partial surjections.

######  Definition 5.2.

Let $\mathbf{C}$ be a category with a terminal object. We define the following
full subcategories of $\mathbf{C}$:

  * •

${\mathbf{C}}_{\geq 1}$ containing the objects $c$ that have at least one
point; we call these objects _inhabited_ ,

  * •

${\mathbf{C}}_{\leq 1}$ containing the objects $c$ that have at most one
point,

  * •

${\mathbf{C}}_{=1}$ containing the objects $c$ that have exactly one point.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

When instantiated to the CCC $\mathbf{Lam}$ of simple types and
$\lambda$-terms, the notion of inhabited object coincides with the usual
notion of inhabited simple type.

######  Proposition 5.3.

If $\mathbf{C}$ is a CCC, then the category ${\mathbf{C}}_{\geq 1}$ is a sub-
CCC of $\mathbf{C}$.

The proof is in Appendix B.

######  Proposition 5.4.

If $\mathbf{E}$ is a well-pointed CCC, then the category ${\mathbf{E}}_{\leq
1}$ is a sub-CCC of $\mathbf{E}$. Moreover, the category ${\mathbf{E}}_{=1}$
is equivalent to the terminal category.

The proof is in Appendix B. We now prove the interesting fact that inhabited
objects characterize the recognized languages of $\lambda$-terms in a well-
pointed CCC.

######  Proposition 5.5.

If $\mathbf{E}$ is a well-pointed CCC, then a language of $\lambda$-terms is
$\mathbf{E}$-recognizable if and only if it is ${\mathbf{E}}_{\geq
1}$-recognizable.

######  Proof 5.6.

Let $\mathbf{E}$ be a well-pointed CCC. By Proposition 5.3,
${\mathbf{E}}_{\geq 1}$ is a sub-CCC of $\mathbf{E}$ so any language which is
${\mathbf{E}}_{\geq 1}$-recognizable is $\mathbf{E}$-recognizable, as
explained in Remark 2.5.

We now show that the only language recognized by ${\mathbf{E}}_{\leq 1}$ is
the empty and full languages. Let $A$ be a simple type and $c$ be an object of
${\mathbf{E}}_{\leq 1}$. As $\mathbf{E}$ is well-pointed and by Proposition
5.4, we know that $\llbracket A\rrbracket_{c}$ belongs to ${\mathbf{E}}_{\leq
1}$, which means that $\mathbf{C}(1,\llbracket A\rrbracket_{c})$ is empty or a
singleton, so
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{c}(A){}{}$
contains at most the empty and full languages, which are the same when $A$ is
not inhabited.

The empty and full languages are recognized by any CCC, so in particular by
${\mathbf{E}}_{\geq 1}$. Therefore, all $\mathbf{E}$-recognizable languages
are ${\mathbf{E}}_{\geq 1}$-recognizable.

######  Example 5.7.

  * •

The category ${\mathbf{FinSet}}_{\geq 1}$ is the CCC of _non-empty_ finite
sets.

  * •

An implicative semilattice is a meet-semilattice such that each meet operation
has an upper adjoint. Implicative semilattices are CCCs, however, they are
degenerate and so never distinguish different $\lambda$-terms of the same
type.

Another way to understand this fact is to remark that their full subcategory
of inhabited objects is the terminal category.

Next, we introduce the basic partial relations at which we will interpret the
$\lambda$-calculus.

######  Definition 5.8.

Let $\mathbf{E}$ be a well-pointed locally finite CCC and $\mathbf{R}$ be the
CCC of logical relations from $\mathbf{FinSet}$ to $\mathbf{E}$. For any
object $e$ of $\mathbf{E}$, we consider the triple

$T_{e}\quad:=\quad(\mathbf{E}(1,e),e,\sim_{e})\qquad\text{where $\sim_{e}$ is
the identity relation of $\mathbf{E}(1,e)$.}$

which extends to a functor $T:\mathbf{E}\to\mathbf{R}$.

We now prove a converse to Lemma 4.10 in the present case.

######  Proposition 5.9.

Let $\mathbf{E}$ be a well-pointed locally finite CCC whose objects are all
inhabited and $\mathbf{R}$ be the CCC of logical relations from
$\mathbf{FinSet}$ to $\mathbf{E}$. Then, the full subcategory of partial
surjections is a sub-CCC of $\mathbf{R}$.

We provide two proofs of this proposition. The first one constructs the CCC by
hand, see Appendix B. The other one uses the squeezing technique, see Appendix
D.

######  Theorem 5.10 (claimed in [DBLP:books/hal/Salvati15, Lemma 20]).

For every well-pointed locally finite CCC $\mathbf{E}$, any
$\mathbf{E}$-recognizable language is $\mathbf{FinSet}$-recognizable.

######  Proof 5.11.

Let $A$ be a simple type and $L$ be a language of $\lambda$-terms of type $A$
which is $\mathbf{E}$-recognizable. By Proposition 5.5, it is
${\mathbf{E}}_{\geq 1}$-recognizable. Let $e$ be an object of
${\mathbf{E}}_{\geq 1}$ such that
$L\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{e}(A){}{}$.
We consider the object $T_{e}=(\mathbf{E}(1,e),e,\sim_{e})$ from Definition
5.8, whose relation is a partial surjection. The object $\llbracket
A\rrbracket_{T_{e}}$ is of the form $(\llbracket
A\rrbracket_{\mathbf{E}(1,e)},\llbracket A\rrbracket_{e},\sim_{e}^{A})$, where
the relation $\sim_{e}^{A}$ is a partial surjection, as explained in Remark
2.5.

Let $F$ be a subset of $\mathbf{E}(1,\llbracket A\rrbracket_{e})$ such that
$L$ is
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}$.
We consider the subset $F^{\prime}$ of $\llbracket
A\rrbracket_{\mathbf{E}(1,e)}$ defined as the inverse image

$F^{\prime}\quad:=\quad\\{q\in\llbracket
A\rrbracket_{\mathbf{E}(1,e)}\mid\exists q^{\prime}\in F\text{ s.t.
}q\sim_{e}^{A}q^{\prime}\\}$

By the fundamental lemma of logical relations, for $\lambda$-term $t$ of type
$A$, we have

$\left\llbracket
t\right\rrbracket_{\mathbf{E}(1,e)}\sim_{e}^{A}\left\llbracket
t\right\rrbracket_{e}\ .$

which proves that
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F^{\prime}}{}{}$.
Moreover, as $\sim_{e}^{A}$ is a functional relation, we get the converse
inclusion. This proves that $L$ is $\mathbf{FinSet}$-recognizable.

##  6 From finite sets to -terms

In this section, we apply the squeezing construction of Definition 4.8 on a
CCC of logical relations to show that every $\mathbf{FinSet}$-recognizable
language is syntactically regular, through an encoding of finite sets into the
simply typed $\lambda$-calculus. To achieve that, we need to change slightly
of setting, by moving from finite sets to finite ordinals. This will make it
possible to define the functor
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(-)}{}{}$
without ambiguity.

Therefore, we consider the category $\mathbf{FinOrd}$ whose objects are
natural numbers and whose morphisms are the set-theoretic maps between the
associated finite cardinals
$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\langle}n{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\rangle}{}{}:=\\{1,\dots,n\\}$.
The inclusion of $\mathbf{FinOrd}$ in $\mathbf{FinSet}$ is a fully faithful
functor that is essentially surjective, henceforth we get an equivalence
between $\mathbf{FinOrd}$ and $\mathbf{FinSet}$ using the axiom of choice. In
particular, $\mathbf{FinOrd}$ is a CCC that recognizes the same languages as
$\mathbf{FinSet}$.

### The encoding of finite sets and its squeezing structure

We take $\mathbf{R}$ to be the CCC of logical relations from $\mathbf{Lam}$ to
$\mathbf{FinOrd}$. We recall that the objects of $\mathbf{R}$ are therefore
triples $R=(B,n,\Vdash)$ where $B$ is a simple type, $n$ is a natural number
and $\Vdash$ is a subset of the product
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(B){}{}\times{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\langle}n{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rangle}{}{}$.
A morphism of $\mathbf{R}$ is a pair of morphisms of $\mathbf{Lam}$ and
$\mathbf{FinOrd}$ which respect the relations.

######  Definition 6.1.

We define the functor
${\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\operatorname{Fin}}({-})}{}{}:\mathbf{FinOrd}\to\mathbf{Lam}$
as
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}:=\mathbbmss{o}^{n}\Rightarrow\mathbbmss{o}$
and, for every $f:n\to n^{\prime}$, the $\lambda$-term
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(f)}{}{}:{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}\to{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n^{\prime})}{}{}$
is

$\lambda(p:{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}).\,\lambda(x:\mathbbmss{o}^{n^{\prime}}).\,p\
\langle x_{f(1)},\,\dots,\,x_{f(n)}\rangle\ .$

######  Remark 6.2.

As $\mathbf{FinOrd}$ is equivalent to the free cocartesian category and
${\mathbf{Lam}}^{\textrm{op}}$ is cocartesian, we get a functor
$n\mapsto\mathbbmss{o}^{n}$. The composition of the two functors

${\mathbf{FinOrd}}$${{{\mathbf{Lam}}^{\textrm{op}}}}$${\mathbf{Lam}}$$\scriptstyle{n\mapsto\mathbbmss{o}^{n}}$$\scriptstyle{(-)\Rightarrow\mathbbmss{o}}$

is precisely the functor
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}({-})}{}{}$.

Our goal is now to exhibit a squeezing structure on $\mathbf{R}$ in order to
show Theorem 6.5. We consider the target-identities for the two wide
subcategories of the structure. We now define the following family of objects.

######  Definition 6.3.

For any natural number $n$, we define the object
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{n}{}{}$
as

$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\operatorname{Bij}}_{n}{}{}\quad:=\quad\left({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{},n,{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{n}{}{}\right)$

where
$\mathrel{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{n}{}{}}$
is the bijection between the sets
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}){}{}$
and
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\langle}n{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rangle}{}{}$
defined as

$\mathrel{\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\Vdash}_{n}{}{}}\quad:=\quad\\{(\pi_{i},i):1\leq
i\leq n\\}\qquad\text{with\leavevmode\nobreak\ $\pi_{i}$
the\leavevmode\nobreak\ $\lambda$-term\leavevmode\nobreak\
$\lambda(x:\mathbbmss{o}^{n}).\,x_{i}$}\ .$

This assignment extends to a functor
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{(-)}{}{}:\mathbf{FinOrd}\to\mathbf{R}$.

######  Proposition 6.4.

There is a squeezing structure on the CCC $\mathbf{R}$ such that:

  * •

the left and right morphisms are the target-identities of $\mathbf{R}$,

  * •

for any object $c=(B,n,\Vdash)$ of $\mathbf{R}$, the objects $L_{c}$ and
$R_{c}$ are both equal to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{n}{}{}$.

The proof is in Appendix D. Proposition 6.4 shows that we have a sub-CCC
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$
of the CCC of logical relations from $\mathbf{Lam}$ to $\mathbf{FinOrd}$,
whose objects are tuples $(B,n,\Vdash)$ such that there exists $\lambda$-terms
$u:{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}\to
B$ and
$v:B\to{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}$
lifting to the two following target-identities:

$\immediate\immediate\immediate\leavevmode\hbox to166.21pt{\vbox
to17.42pt{\pgfpicture\makeatletter\hbox{\hskip 83.10251pt\lower-8.75955pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-83.10251pt}{-8.65971pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
35.808pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.50246pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${{\left({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{},n,{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{n}{}{}\right)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
35.808pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 47.29451pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.989pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{(B,n,\Vdash)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
23.29454pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-11.28651pt}{-6.15971pt}\pgfsys@lineto{35.91347pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{36.11345pt}{-6.15971pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{2.4066pt}{-2.05695pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{(u,\operatorname{Id}_{n})}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\text{and}\quad\immediate\immediate\immediate\leavevmode\hbox
to166.21pt{\vbox to17.42pt{\pgfpicture\makeatletter\hbox{\hskip
83.10251pt\lower-8.75955pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-83.10251pt}{-8.65971pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
23.29454pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.989pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{(B,n,\Vdash)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
23.29454pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 59.80797pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.50246pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${{\left({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{},n,{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{n}{}{}\right)}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
35.808pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-36.31343pt}{-6.15971pt}\pgfsys@lineto{10.88655pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.08653pt}{-6.15971pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.43881pt}{-2.05695pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{(v,\operatorname{Id}_{n})}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\ .$

### Encoding recognizability by finite sets

We have shown in Proposition 6.4 that we have a squeezing structure on the CCC
of logical relations $\mathbf{R}$ from $\mathbf{Lam}$ to $\mathbf{FinOrd}$. We
now show how to use this structure, culminating in the link established in
Theorem 6.5 between $\mathbf{FinOrd}$-recognizable and syntactically regular
languages.

######  Theorem 6.5.

If a language is $\mathbf{FinSet}$-recognizable, then it is syntactically
regular.

######  Proof 6.6.

Let $A$ be a simple type and
$L\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}$
be any $\mathbf{FinSet}$-recognizable language. There exists a finite set $Q$
and a subset
$F\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\langle}\llbracket
A\rrbracket_{n}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rangle}{}{}$
such that

$L\ =\
\\{t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}\mid\left\llbracket
t\right\rrbracket_{n}\in F\\}\ .$

We take $n$ to be the cardinality of $Q$ and note $\chi:\llbracket
A\rrbracket_{n}\to 2$ the characteristic function associated to the subset
$F$. By applying the functor
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{(-)}{}{}$,
we get a morphism of relations

${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{\chi}{}{}:=({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(\chi)}{}{}\,,\,\chi)\quad:\quad\left({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(\llbracket
A\rrbracket_{n})}{}{},\llbracket
A\rrbracket_{n},{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{\llbracket
A\rrbracket_{n}}{}{}\right)\ \longrightarrow\
\left({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(2)}{}{},2,{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{2}{}{}\right)\
.$

The interpretation $\llbracket
A\rrbracket_{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{n}{}{}}$
is of the form
$(A[{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}],\llbracket
A\rrbracket_{n},\mathrel{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}^{A}_{n}{}{}})$
as explained in Remark 2.5. As it is an object of
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{R}){}{}$,
it has a target-identity into
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{\llbracket
A\rrbracket_{n}}{}{}$. By composing this morphism with
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Bij}}_{\chi}{}{}$,
we obtain a morphism

$(r\,,\,\chi)\quad:\quad(A[{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}],\llbracket
A\rrbracket_{n},\mathrel{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}^{A}_{n}{}{}})\
\longrightarrow\
\left({{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(2)}{}{},2,{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{2}{}{}\right)\
.$

By the fundamental lemma of logical relations, we get that, for every
$\lambda$-term $t$ of type $A$,

$t[{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}]\mathrel{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}^{A}_{n}{}{}}\left\llbracket
t\right\rrbracket_{n}\qquad\text{on which we apply $(r,\chi)$ to get}\qquad r\
t[{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}]\mathrel{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Vdash}_{2}{}{}}\chi(\left\llbracket
t\right\rrbracket_{n})$

which states that $r\
t[{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Fin}}(n)}{}{}]=_{\beta\eta}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{true}}}{}{}$
if and only if $\chi(\left\llbracket t\right\rrbracket_{n})$ is $1$. This
proves that $r$ recognizes the language
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}$
given by
$F\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\langle}\llbracket
A\rrbracket_{n}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rangle}{}{}$,
and so that $L$ is syntactically regular.

##  7 Regular languages

In this section, we want to point out a few consequences of the equivalence
previously proved through Theorem 3.2, Theorem 5.10 and Theorem 6.5. Using
these theorems, the following definition of regular languages is well-defined.

######  Definition 7.1.

Let $A$ be a simple type. A _regular language_ of $\lambda$-terms of type $A$
is a subset
$L\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}(A){}{}$
such that one of the following equivalent propositions holds:

  * •

$L$ is syntactically regular;

  * •

$L$ is $\mathbf{C}$-recognizable, for some non-degenerate, well-pointed and
locally finite CCC $\mathbf{C}$;

  * •

$L$ is $\mathbf{FinSet}$-recognizable.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

We denote by
$\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\operatorname{Reg}}(A){}{}$
the set of regular languages of $\lambda$-terms of type $A$.

######  Remark 7.2.

Note that $\mathbf{FinSet}$ recognizes all the regular languages of
$\lambda$-terms. In that sense, it plays the same role as the monoid

$M\ :=\ \\{f:\mathbb{N}\to\mathbb{N}\mid\exists N\in\mathbb{N},\forall n\geq
N,f(n)=n\\}\quad\text{with the composition of functions}$

which recognizes all the regular languages of finite words as all finite
monoids can be embedded into $M$. Such a monoid cannot be finite; however, $M$
is a _locally finite monoid_ , i.e. all its finitely generated submonoids are
finite (this is a standard notion, see e.g. [grilletsemigroups, §V.5]).

In the case of finite words, recognizability by finite monoids and locally
finite monoids are equivalent when the alphabet is finite. In the case of
$\lambda$-terms however, finite CCCs are all degenerate whereas the locally
finite case yields regular languages of $\lambda$-terms, with some additional
conditions.

######  Proposition 7.3.

The set
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Reg}}(A){}{}$
of regular languages of $\lambda$-terms of some simple type $A$ is a Boolean
algebra.

This fact boils down to stability by union or intersection. It is proved in
[DBLP:conf/wollic/Salvati09, Theorem 8] using intersection types and in
[entics:12280, Proposition 2.5] using logical relations. We provide another
proof, showing that it is a direct consequence of our results.

######  Proof 7.4.

Using any of the three conditions of Definition 7.1, it is clear that regular
languages are closed under complement.

The product CCC $\mathbf{FinSet}\times\mathbf{FinSet}$ is non-degenerate,
well-pointed and locally finite. It comes with two projections which are both
CCC functors $\mathbf{FinSet}\times\mathbf{FinSet}\to\mathbf{FinSet}$. Let $Q$
and $Q^{\prime}$ be two finite sets; we consider the object $(c,c^{\prime})$
of $\mathbf{FinSet}\times\mathbf{FinSet}$. As explained in Remark 2.5, for any
simple type $A$, we get that
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{Q}(A){}{}\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{(Q,Q^{\prime})}(A){}{}$
and
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{Q^{\prime}}(A){}{}\subseteq{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{(Q,Q^{\prime})}(A){}{}$.

Moreover,
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{(Q,Q^{\prime})}(A){}{}$
is a Boolean algebra. This shows that the intersection of a language in
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{Q}(A){}{}$
with another in
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{Q^{\prime}}(A){}{}$
can be taken in
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Rec}}_{(Q,Q^{\prime})}(A){}{}$,
so it is still a regular language. Therefore,
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\operatorname{Reg}}(A){}{}$
is a Boolean algebra.

We now point out two other consequences of the equivalence in Definition 7.1.

  * •

As stated in the introduction, Statman’s finite completeness theorem tells us
that singleton languages of $\lambda$-terms, taken modulo
$\beta\eta$-conversion, are regular languages. It has multiple proofs, see
[statman-dowek-1992] for proof directly in the finite standard model,
[DBLP:conf/wollic/Salvati09] using intersection types,
[DBLP:journals/iandc/KobeleS15] in the model of complete lattices and
[DBLP:journals/ipl/SrivathsanW12] using Böhm trees.

These results are usually proved in one CCC. Using Theorem 3.2, Theorem 5.10
and Theorem 6.5, we get that the singleton languages are recognized by any
non-degenerate, well-pointed and locally finite CCC and are also syntactically
regular.

  * •

Some CCCs satisfying these three conditions are the coKleisli categories of a
model of linear logic, see [mellies_2009]. In [HOParity], a notion of higher-
order automaton is presented, which recognizes a language of $\lambda$-terms
of a given simple type. The run-trees for these non-deterministic automata are
defined using an intersection type system, which is an equivalent way of
presenting the semantic interpretation $\left\llbracket-\right\rrbracket$ of
the simply typed $\lambda$-calculus in the coKleisli category
$\mathbf{ScottL}_{!}$ of the Scott model of linear logic. Using the
equivalence proved in the present article, a language is recognized by a
higher-order automaton, i.e. $\mathbf{ScottL}_{!}$-recognizable, if and only
if it satisfies one of the conditions of Definition 7.1.

##  8 Conclusion and future perspectives

In this article, we have shown that every non-degenerate, well-pointed and
locally finite CCCs recognizes exactly Salvati’s regular languages of
$\lambda$-terms [DBLP:conf/wollic/Salvati09], and that those also coincide
with syntactically regular languages. This is evidence for the robustness of
this notion, and therefore of the dual notion of profinite $\lambda$-term
introduced in [entics:12280].

Among the aforementioned conditions, non-degeneracy is needed to recognize
non-trivial languages, and local finiteness is clearly crucial: in the case of
finite words and trees, regularity is closely related to recognition by
finitary structures. What about well-pointedness? In other words, one question
that remains open is the following: is there a locally finite CCC that
recognizes languages of $\lambda$-terms that are not regular, i.e. not
recognizable by $\mathbf{FinSet}$? For example, sequential algorithms famously
form a locally finite CCC which is _not_ well-pointed, cf.
[DBLP:books/daglib/0093287-amadio-curien, Chapter 14]; we would like to
understand its recognition power.

As explained in Example 2.2, the regular languages of $\lambda$-terms of type
${{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{Church}}}}_{n}{}{}$
for some natural number $n$ are exactly the usual regular languages of the
finite words associated by the Church encoding. It is possible to encode words
in other calculi, like the non-commutative affine $\lambda$-calculus in which
case a syntactic approach analogous to Definition 2.9 yields the star-free
languages, see [iatlc1]. Moreover, gluing techniques have been studied for
other calculi, see [DBLP:conf/tlca/Hasegawa99] for the linear case. One can
therefore wonder whether it is possible to develop a semantic approach à la
Salvati, analogous to Definition 2.1, for other calculi.

## References

  * [1] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher.  Categorical reconstruction of a reduction free normalization proof.  In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS ’95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182–199. Springer, 1995.  doi:10.1007/3-540-60164-3_27.
  * [2] Roberto M. Amadio and Pierre-Louis Curien.  Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 1998.  doi:10.1017/CBO9780511983504.
  * [3] Robert Atkey.  Syntax for free: Representing syntax with binding using parametricity.  In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 35–49. Springer, 2009.  doi:10.1007/978-3-642-02273-9_5.
  * [4] Mikołaj Bojańczyk.  Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic.  CoRR, abs/2008.11635, 2020.  arXiv:2008.11635.
  * [5] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota.  Automata theory in nominal sets.  Logical Methods in Computer Science, 10(3), 2014.  doi:10.2168/LMCS-10(3:4)2014.
  * [6] Antonio Bucciarelli.  Logical relations and lambda theories.  In Advances in Theory and Formal Methods of Computing, proceedings of the 3rd Imperial College Workshop, pages 37–48, 1996.
  * [7] Thomas Ehrhard.  The Scott model of linear logic is the extensional collapse of its relational model.  Theoretical Computer Science, 424:20–45, 2012.  doi:10.1016/j.tcs.2011.11.027.
  * [8] Marcelo Fiore.  Semantic analysis of normalisation by evaluation for typed lambda calculus.  Mathematical Structures in Computer Science, 32(8):1028–1065, 2022\.  doi:10.1017/S0960129522000263.
  * [9] Jean-Yves Girard.  The Blind Spot: Lectures on logic.  European Mathematical Society, September 2011.  doi:10.4171/088.
  * [10] Charles Grellois.  Semantics of linear logic and higher-order model-checking.  PhD thesis, Université Paris 7, April 2016.  URL: https://hal.science/tel-01311150.
  * [11] Pierre A. Grillet.  Semigroups. An introduction to the structure theory.  Chapman & Hall/CRC Pure and Applied Mathematics. Dekker, 1995.  doi:10.4324/9780203739938.
  * [12] Masahito Hasegawa.  Logical predicates for intuitionistic linear type theories.  In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA’99, L’Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 198–212. Springer, 1999.  doi:10.1007/3-540-48959-2_15.
  * [13] Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva.  Tree Automata as Algebras: Minimisation and Determinisation.  In Markus Roggenbach and Ana Sokolova, editors, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), volume 139 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:22, Dagstuhl, Germany, 2019. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  doi:10.4230/LIPIcs.CALCO.2019.6.
  * [14] Gerd G. Hillebrand and Paris C. Kanellakis.  On the expressive power of simply typed and let-polymorphic lambda calculi.  In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 253–263. IEEE Computer Society, 1996.  doi:10.1109/LICS.1996.561337.
  * [15] Naoki Kobayashi.  Model checking higher-order programs.  Journal of the ACM, 60(3):20:1–20:62, 2013.  doi:10.1145/2487241.2487246.
  * [16] Naoki Kobayashi.  10 years of the higher-order model checking project (extended abstract).  In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 2:1–2:2. ACM, 2019\.  doi:10.1145/3354166.3354167.
  * [17] Gregory M. Kobele and Sylvain Salvati.  The IO and OI hierarchies revisited.  Information and Computation, 243:205–221, 2015.  doi:10.1016/j.ic.2014.12.015.
  * [18] Paul-André Melliès.  Categorical Semantics of Linear Logic.  In P.-L. Curien, H. Herbelin, J.-L. Krivine, and P.-A. Melliès, editors, Interactive models of computation and program behaviour, volume 27 of Panoramas et Synthèses. Société Mathématique de France, 2009.  URL: https://smf.emath.fr/publications/semantique-categorielle-de-la-logique-lineaire.
  * [19] Paul-André Melliès.  Higher-order parity automata.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, Reykjavik, Iceland, June 2017. IEEE.  doi:10.1109/LICS.2017.8005077.
  * [20] John C. Mitchell and Andre Scedrov.  Notes on sconing and relators.  In Egon Börger, Gerhard Jäger, Hans Kleine Büning, Simone Martini, and Michael M. Richter, editors, Computer Science Logic, 6th Workshop, CSL ’92, San Miniato, Italy, September 28 - October 2, 1992, Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 352–378. Springer, 1992.  doi:10.1007/3-540-56992-8_21.
  * [21] Lê Thành Dũng Nguyễn.  Implicit automata in linear logic and categorical transducer theory.  PhD thesis, Université Paris XIII, 2021.  URL: https://hal.science/tel-04132636.
  * [22] Lê Thành Dũng Nguyễn and Cécilia Pradic.  Implicit automata in typed $\lambda$-calculi I: aperiodicity in a non-commutative logic.  In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 135:1–135:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPIcs.ICALP.2020.135.
  * [23] C.-H. Luke Ong.  On model-checking trees generated by higher-order recursion schemes.  In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81–90. IEEE Computer Society, 2006.  doi:10.1109/LICS.2006.38.
  * [24] C.-H. Luke Ong.  Higher-order model checking: An overview.  In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 1–15. IEEE Computer Society, 2015.  doi:10.1109/LICS.2015.9.
  * [25] Gordon D. Plotkin.  Recursion does not always help.  In Fairouz Kamareddine, editor, A Century since Principia’s Substitution Bedazzled Haskell Curry. In Honour of Jonathan Seldin’s 80th Anniversary. College Publications, 2023.  arXiv:2206.08413.
  * [26] Simona Ronchi Della Rocca.  Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper).  In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1–2:7, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  doi:10.4230/LIPIcs.TYPES.2016.2.
  * [27] Sylvain Salvati.  Recognizability in the simply typed lambda-calculus.  In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, volume 5514 of Lecture Notes in Computer Science, pages 48–60. Springer, 2009.  doi:10.1007/978-3-642-02261-6_5.
  * [28] Sylvain Salvati.  Lambda-calculus and formal language theory.  Habilitation à diriger des recherches, Université de Bordeaux, 2015\.  URL: https://hal.science/tel-01253426.
  * [29] B. Srivathsan and Igor Walukiewicz.  An alternate proof of Statman’s finite completeness theorem.  Information Processing Letters, 112(14-15):612–616, 2012.  doi:10.1016/j.ipl.2012.04.014.
  * [30] Richard Statman.  Completeness, invariance and lambda-definability.  Journal of Symbolic Logic, 47(1):17–26, 1982.  doi:10.2307/2273377.
  * [31] Richard Statman.  On the $\lambda Y$ calculus.  Annals of Pure and Applied Logic, 130(1-3):325–337, 2004.  doi:10.1016/j.apal.2004.04.004.
  * [32] Richard Statman and Gilles Dowek.  On Statman’s finite completeness theorem, 1992.  arXiv:2309.03602.
  * [33] Kazushige Terui.  Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus.  In 23rd International Conference on Rewriting Techniques and Applications (RTA’12), pages 323–338, 2012.  doi:10.4230/LIPIcs.RTA.2012.323.
  * [34] Sam van Gool, Paul-André Melliès, and Vincent Moreau.  Profinite lambda-terms and parametricity.  Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 – Proceedings of MFPS XXXIX, November 2023.  doi:10.46298/entics.12280.
  * [35] Igor Walukiewicz.  Automata theory and higher-order model-checking.  ACM SIGLOG News, 3(4):13–31, 2016.  doi:10.1145/3026744.3026745.

##  Appendix A The regular language of affine untyped terms

The goal of this appendix is to provide a detailed explaination of Example
2.4. We first introduce a grammar for the simply typed $\lambda$-terms of type
UntypedTerms through the following notion of scoped term.

######  Definition A.1.

We consider untyped terms with de Bruijn indices, given by the grammar

$u,v\quad::=\quad\textup{{var}}_{i}\text{ for
$i\in\mathbb{N}^{*}$}\mid\textup{{abs}}(u)\mid\textup{{app}}(u,v)$

where we write $\textup{{abs}}(-)$ for the abstraction to distinguish it from
the simply typed $\lambda$-abstraction.

For any natural number $n$ and untyped term $u$, we define the judgment
$n\vdash u$ by induction with the rules

$\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
15.22969pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{$1\leq i\leq
n$}}}\hbox{\hbox{\hbox{}\hbox{}}\hbox{$n\vdash\textup{{var}}_{i}$}}\par}\par}}}$}\qquad\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
1.13898pt\hbox{}}\vbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hbox{\hbox{\hbox{}\hbox{$n+1\vdash
u$}}\hbox{$n\vdash\textup{{abs}}(u)$}}\par}\par}}}$}\qquad\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
8.14012pt\hbox{}}\vbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$n\vdash u$}}\hbox{$n\vdash
v$}}}}\hbox{$n\vdash\textup{{app}}(u,v)$}}\par}\par}}}$}\ .$

The judgment $n\vdash u$ has at most one derivation. We call a scoped term any
pair of $n$ and $u$ such that $n\vdash u$ is derivable.

In the rest of the appendix, we will simply say that $n\vdash u$ is a scoped
term whenever this judgment is derivable. We now give the encoding of scoped
terms into the simply typed $\lambda$-calculus.

######  Definition A.2.

Let us consider a fixed sequence of simply typed variables
$x_{k}:\mathbbmss{o}$ for $k\in\mathbb{N}$. We define the context $\Gamma_{n}$
as
$\ell:(\mathbbmss{o}\Rightarrow\mathbbmss{o})\Rightarrow\mathbbmss{o},a:\mathbbmss{o}\Rightarrow\mathbbmss{o}\Rightarrow\mathbbmss{o},x_{1}:\mathbbmss{o},\dots,x_{n}:\mathbbmss{o}$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

For any natural number $n$ and untyped term $u$, we consider the encoding
$n\vdash u$ of a scoped term defined by induction as

$n\vdash\textup{{var}}_{i}$
---
$\displaystyle:=\quad x_{n+1-i}$ $n\vdash\textup{{abs}}(u)$
---
$\displaystyle:=\quad\ell\ (\lambda(x_{n+1}:\mathbbmss{o}).\
\hbox{\set@color$n+1\vdash
u$}\ooalign{\raisebox{6.83331pt}{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rule{18.13885pt}{0.5pt}}}\cr\leavevmode\closebox\closebox})$
$n\vdash\textup{{app}}(u,v)$
---
$\displaystyle:=\quad a\ (\hbox{\set@color$n\vdash
u$}\ooalign{\raisebox{6.83331pt}{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rule{18.13885pt}{0.5pt}}}\cr\leavevmode\closebox\closebox})\
(\hbox{\set@color$n\vdash
v$}\ooalign{\raisebox{6.83331pt}{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rule{18.13885pt}{0.5pt}}}\cr\leavevmode\closebox\closebox})$

which is such that $\Gamma_{n}\vdash\hbox{\set@color$n\vdash
u$}\ooalign{\raisebox{6.83331pt}{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rule{18.13885pt}{0.5pt}}}\cr\leavevmode\closebox\closebox}:\mathbbmss{o}$.

Using normalization for the simply typed $\lambda$-calculus, we can claim the
following fact.

######  Claim 3.

For every natural number $n$, the encoding of scoped terms $n\vdash u$ into
the open $\lambda$-terms $n\vdash u$ of type $\mathbbmss{o}$ in context
$\Gamma_{n}$, taken modulo $\beta\eta$-conversion, is bijective.

In particular, the encoding induces a bijection between the set
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}){}{}$
and the set of closed untyped terms, i.e. the $u$ such that $0\vdash u$ is a
scoped term.

######  Definition A.3.

For any scoped term $n\vdash u$ and $1\leq i\leq n$, we define the natural
number $\textup{{occ}}_{i}(n\vdash u)$, the number of occurences of the
$i^{\text{th}}$ variable, by induction as:

$\displaystyle\textup{{occ}}_{i}(n\vdash\textup{{var}}_{j})\quad$
$\displaystyle:=\quad\text{$1$ if $i=j$ otherwise $0$}$
$\displaystyle\textup{{occ}}_{i}(n\vdash\textup{{abs}}(u))\quad$
$\displaystyle:=\quad\textup{{occ}}_{i+1}(n+1\vdash u)$
$\displaystyle\textup{{occ}}_{i}(n\vdash\textup{{app}}(u,v))\quad$
$\displaystyle:=\quad\textup{{occ}}_{i}(n\vdash u)+\textup{{occ}}_{i}(n\vdash
v)\ .$

When the scoped term $n\vdash u$ is clear from context, we will simply write
$\textup{{occ}}_{i}$.

######  Definition A.4.

For any finite set $Q$ and functions $f_{\textup{{abs}}}:(Q\Rightarrow Q)\to
Q$ and $f_{\textup{{app}}}:Q\to Q\Rightarrow Q$, we interpret any scoped term
$n\vdash u$ as its semantics

$n\vdash
u\qquad\rightsquigarrow\qquad\immediate\immediate\immediate{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0.7,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0,0}\rrparenthesis}{}{}\quad:\quad
Q^{n}\longrightarrow Q$

which is the set-theoretic function defined, for $q_{1},\dots,q_{n}\in Q$, by
induction as:

$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{var}}_{i}\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[q_{1},\dots,q_{n}]\quad$
$\displaystyle:=\quad q_{i}$
$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{abs}}(u)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[q_{1},\dots,q_{n}]\quad$
$\displaystyle:=\quad
f_{\textup{{abs}}}(q\mapsto{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[q,q_{1},\dots,q_{n}])$
$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{app}}(u,v)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[q_{1},\dots,q_{n}]\quad$
$\displaystyle:=\quad
f_{\textup{{app}}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[q_{1},\dots,q_{n}])({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash v\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[q_{1},\dots,q_{n}])\
.$

We write the arguments of the function
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}$
between square brackets $[$ and $]$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

######  Remark A.5.

The semantics of Definition A.4 factor through the encoding of Definition A.2
in the simply typed $\lambda$-calculus and its semantic interpretation as for
all $q_{1},\dots,q_{n}\in Q$,

${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}(q_{1},\dots,q_{n})\quad=\quad\left\llbracket\,\hbox{\set@color$n\vdash
u$}\ooalign{\raisebox{6.83331pt}{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rule{18.13885pt}{0.5pt}}}\cr\leavevmode\closebox\closebox}\,\right\rrbracket_{Q}(f_{\textup{{abs}}})(f_{\textup{{app}}})(q_{n},\dots,q_{1})\
.$

We now instantiate Definition A.4 with the following values of $Q$,
$f_{\textup{{abs}}}$ and $f_{\textup{{app}}}$:

  * •

$Q$ is the set $\\{0,1,\infty\\}\times\\{\bot,\top\\}$, with its product
monoid structure. For any $q\in Q$, we write $q_{1}\in\\{0,1,\infty\\}$ and
$q_{2}\in\\{\bot,\top\\}$ for its two components.

  * •

$f_{\textup{{abs}}}$ is the function $(Q\Rightarrow Q)\to Q$ defined as

$g\quad\longmapsto\quad(g(0,\top)_{1}\ ,\
g(0,\top)_{2}\,\wedge\,(g(1,\top)_{1}\neq\infty))$

  * •

$f_{\textup{{app}}}$ is the curried monoid product of $Q$, i.e. the function
$Q\to(Q\Rightarrow Q)$ defined as

$(n,b)\quad\longmapsto\quad(n^{\prime},b^{\prime})\mapsto(n+n^{\prime},b\wedge
b^{\prime})\ .$

######  Proposition A.6 (Left part of the tuple).

For any scoped term $n\vdash u$ and any elements $k_{1},\dots k_{n}$ of
$\\{0,1,\infty\\}$, we have

${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}\quad=\quad\textup{{occ}}_{1}\cdot
k_{1}+\dots+\textup{{occ}}_{n}\cdot k_{n}$

where the product $\cdot:\mathbb{N}\times\\{0,1,\infty\\}\to\\{0,1,\infty\\}$
comes from the monoid structure of $\\{0,1,\infty\\}$.

######  Proof A.7.

We verify this by induction on the scoped term $n\vdash u$.

$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{var}}_{i}\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}$
$\displaystyle\ :=\ k_{i}$ $\displaystyle\ =\ \textup{{occ}}_{1}\cdot
k_{1}+\dots+\textup{{occ}}_{n}\cdot k_{n}$
$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{abs}}(u)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}$
$\displaystyle\ :=\
f_{\textup{{abs}}}\left((k,b)\mapsto{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k,b)\,,\,(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]\right)_{1}$
$\displaystyle\ =\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}$
$\displaystyle\ =\ \textup{{occ}}_{1}\cdot k_{1}+\dots+\textup{{occ}}_{n}\cdot
k_{n}$
$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{app}}(u,v)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}$
$\displaystyle\ :=\
f_{\textup{{app}}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)])({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash v\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)])_{1}$
$\displaystyle\ =\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}\
+\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash v\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k_{1},\top)\,,\,\dots\,,\,(k_{n},\top)]_{1}$
$\displaystyle\ =\ \textup{{occ}}_{1}\cdot k_{1}+\dots+\textup{{occ}}_{n}\cdot
k_{n}$

In the abs case, the last equality is obtained by remarking that
$\textup{{occ}}_{1}(n+1\vdash u)$ is multiplied by $0$ and that
$\textup{{occ}}_{i+1}(n+1\vdash
u)=\textup{{occ}}_{i}(n\vdash\textup{{abs}}(u))$ for $i\geq 1$.

We introduce the following definition.

######  Definition A.8.

We define the property of a scoped term to be _affine in its bound variables_
by induction as follows:

  * •

$n\vdash\textup{{var}}_{i}$ is always affine in its bound variables,

  * •

$n\vdash\textup{{abs}}(u)$ is affine in its bound variables if and only if

$\textup{{occ}}_{1}(n+1\vdash u)\ \leq\ 1\quad\text{and}\quad\text{$n+1\vdash
u$ is affine in its bound variables}$

  * •

$n\vdash\textup{{app}}(u,v)$ is affine in its bound variables if and only if

$n\vdash u$ and $n\vdash v$ are both affine in their bound variables.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

A $\lambda$-term
$t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}){}{}$
will said to be _affine_ when the closed untyped term $0\vdash u$ bijectively
associated to $t$ by 3 is affine in its bound variables.

######  Proposition A.9 (Right part of the tuple).

For any scoped term $n\vdash u$, we have

${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}\quad=\quad
b$

where $b$ is $\top$ if and only if the scoped term $n\vdash u$ is affine in
its bound variables.

######  Proof A.10.

We prove this by induction on the scoped term $n\vdash u$.

  * •

For any $1\leq i\leq n$, $n\vdash\textup{{var}}_{i}$ is always affine in its
bound variables, and we always have

${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{var}}_{i}\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}\
=\ \top\ .$

  * •

For any scoped term $n+1\vdash u$, we have

$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{abs}}(u)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$
$\displaystyle\ :=\
f_{\textup{{abs}}}((k,b)\mapsto{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(k,b)\,,\,(0,\top)\,,\,\dots\,,\,(0,\top)])_{2}$
$\displaystyle\ =\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$
$\displaystyle\qquad\wedge\quad{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(1,\top)\,,\,(0,\top)\,,\,\dots\,,\,(0,\top)]_{1}\neq\infty$
$\displaystyle\ =\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun+1\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$
$\displaystyle\qquad\wedge\quad\textup{{occ}}_{1}(n+1\vdash u)\leq 1\ .$

where the last step comes from Proposition A.6. By the induction hypothesis on
the scoped term $n+1\vdash u$, we get that $n\vdash\textup{{abs}}(u)$ is
affine in its bound variables if and only if
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{abs}}(u)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$
is $\top$.

  * •

For any scoped terms $n\vdash u$ and $n\vdash v$, we have

$\displaystyle{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{app}}(u,v)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$
$\displaystyle\ :=\
f_{\textup{{app}}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)])({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash v\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)])_{2}$
$\displaystyle\ =\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}\
\wedge\
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash v\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$

which shows, by the induction hypotheses on $n\vdash u$ and $n\vdash v$, that
$n\vdash\textup{{app}}(u,v)$ is affine in its bound variables if and only if
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mun\vdash\textup{{app}}(u,v)\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}[(0,\top)\,,\,\dots\,,\,(0,\top)]_{2}$
is $\top$.

######  Theorem A.11.

The language of closed affine untyped terms is regular in $\mathbf{FinSet}$.

######  Proof A.12.

We consider the language

$L\ :=\
\\{t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}){}{}\mid\text{$t$
is
{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}affine}}\\}\
.$

By definition,
$t\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\Lambda}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}){}{}$
is affine if and only if $0\vdash u$ is affine in its bound variables, where
$0\vdash u$ is the unique scoped term such that $t=\hbox{\set@color$0\vdash
u$}\ooalign{\raisebox{6.83331pt}{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rule{18.13885pt}{0.5pt}}}\cr\leavevmode\closebox\closebox}$,
given by 3. Moreover, by Proposition A.9, we have that $0\vdash u$ is affine
in its bound variables if and only if

${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mu0\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}_{2}\quad=\quad\top$

and, by Remark A.5,
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\llparenthesis}\mkern
2.0mu0\vdash u\mkern
2.0mu{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\rrparenthesis}{}{}_{2}=\left\llbracket
t\right\rrbracket_{Q}(f_{\textup{{abs}}})(f_{\textup{{app}}})$. Therefore, if
we define the subset $F$ of
$\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}\rrbracket_{Q}$
as

$F\quad:=\quad\\{s\in\llbracket{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\textsf{{UntypedTerms}}}{}{}\rrbracket_{Q}\mid
s(f_{\textup{{abs}}})(f_{\textup{{app}}})_{2}=\top\\}$

we get that
$L={\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}L}_{F}{}{}$
and therefore that $L$ is $\mathbf{FinSet}$-recognizable.

##  Appendix B Sub-CCC proofs

Throughout the article, we construct new CCCs as full subcategories of other
CCCs which verify some stability properties. A sub-CCC is a sub-category whose
inclusion functor is a CCC functor. More precisely, this construction is
justified by the following claim:

######  Claim 4.

Let $\mathbf{C}$ be a CCC and $\mathbf{D}$ be a full subcategory of
$\mathbf{C}$. If:

  * •

the terminal object of $\mathbf{C}$ belongs to $\mathbf{D}$,

  * •

the objects of $\mathbf{D}$ are stable under cartesian products,

  * •

the objects of $\mathbf{D}$ are stable under exponentiation,

then $\mathbf{D}$ is a sub-CCC of $\mathbf{C}$.

### Proof of Theorem 4.9

By definition of a squeezing structure, we have the following facts:

  * •

The terminal object $1$ of $\mathbf{C}$ is an object of
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$.

  * •

If $c$ and $c^{\prime}$ belong to
${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathbf{Sqz}}(\mathbf{C}){}{}$,
then $c\times c^{\prime}$ still does. Indeed, we have the following morphisms:

$L_{c\times c^{\prime}}\overset{\operatorname{l}}{\longrightarrow}L_{c}\times
L_{c^{\prime}}\overset{\operatorname{l}}{\longrightarrow}c\times
c^{\prime}\qquad\text{and}\qquad c\times
c^{\prime}\overset{\operatorname{r}}{\longrightarrow}R_{c}\times