Semantic analysis of normalisation by evaluation for typed lambda calculus

Abstract

This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper, the analysis is refined further by considering intensional Kripke relations (in the form of Artin–Wraith glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed metatheory. A normalisation-by-evaluation program in a dependently typed functional programming language is synthesised.

1. Introduction

Normalisation by evaluation for typed lambda calculus was first considered by Berger and Schwichtenberg (1991) from a type and proof theoretic viewpoint, and later investigated from the point of view of logic (Berger, 1993), type theory (Coquand, 1994), category theory (Altenkirch et al., 1995; Čubrić et al., 1997; Reynolds, 1998) and partial evaluation (Danvy, 1998; Filinski, 1999). This work gives a new categorical and algebraic perspective on the topic.

Outline. Normalisation by evaluation will be broadly viewed as the technique of giving semantics in (metalanguages for) non-standard models from which normalisation information can be extracted (Martin-Lof 1975). In this light, we will investigate the following problems.

1. I. Extensional normalisation problem: To define normal terms and establish that every term $\beta\eta$ -equals one in normal form.That is, writing $\mathscr{L}_{\tau}(\Gamma)$ for the set of terms of type $\tau$ in context $\Gamma$ , to identify a set of normal terms $\mathscr{N}_{\tau}(\Gamma) \subseteq \mathscr{L}_{\tau}(\Gamma)$ and show that for every term $t\in\mathscr{L}_{\tau}(\Gamma)$ , there exists a normal term $N\in\mathscr{N}_{\tau}(\Gamma)$ such that $t ={}_{\beta\eta} N$ .

2. II. Intensional normalisation problem: To define, and prove the correctness of, a normalisation function associating normal forms to terms. More precisely, to construct functions

   \begin{equation*} \mathsf{nf}_{\tau,\Gamma}: \mathscr{L}_{\tau}(\Gamma) \rightarrow \mathscr{N}_{\tau}(\Gamma)\end{equation*}
   satisfying the following three properties.

   1. (1) For all normal terms $N\in\mathscr{N}_{\tau}(\Gamma)$ , the syntactic equality $\mathsf{nf}_{\tau,\Gamma}(N)$ $= N$ holds.

   2. (2) For all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ , the semantic equality $\mathsf{nf}_{\tau,\Gamma}(t) ={}_{\beta\eta} t$ holds.

   3. (3) For all pair of terms $t,t'\in\mathscr{L}_{\tau}(\Gamma)$ , if $t={}_{\beta\eta} t'$ then $\mathsf{nf}_{\tau,\Gamma}(t) = \mathsf{nf}_{\tau,\Gamma}(t')$ . In the context of normalisation by evaluation, the correctness condition (1) has seldom been considered – the exception being (Reynolds 1998). However, it is both natural and interesting. For instance, together with the correctness condition (3) it implies that $\beta\eta$ -equal normal terms are syntactically equal, which in turn, together with the correctness condition (2), entails the stronger version of extensional normalisation that every term $\beta\eta$ -equals a unique normal term.

These problems will be, respectively, dealt with in Parts I and II of the paper. Part I provides a unifying view of definability and normalisation leading to an extensional normalisation result. This analysis, besides unifying the two hitherto unrelated problems of definability and normalisation, motivates and elucidates the notions of neutral and normal terms, which are here distilled from semantic considerations. Part II shows that an intensional view of Part I amounts to the traditional technique of normalisation by evaluation. This development leads to a treatment of normalisation by evaluation via the Artin–Wraith glueing construction, finally formalising the observation that normalisation by evaluation is closely related to categorical glueing (Coquand and Dybjer, 1997).

More in detail, the paper is organised as follows. Section 2.1 briefly recalls the syntax and categorical semantics of the typed lambda calculus. Section 2.2 presents an analysis of the lambda definability result of Jung and Tiuryn via Kripke logical relations (Jung and Tiuryn 1993) leading to an extensional normalisation result. Section 3.1 describes the rudiments of a theory of typed abstract syntax with variable binding which is used to put the typed lambda calculus in an algebraic framework. This algebraic view is exploited in Section 3.2 to structure the development of an intensional version of Section 2.2 culminating in the technique of normalisation by evaluation.

Related work. The treatment of extensional normalisation presented here is similar to Tait’s approach to strong normalisation via computability predicates (Girard, 1972; Tait, 1967) for the typed lambda calculus and also to Krivine’s approach to normalisation Krivine, (1993), Chapter III for the untyped lambda calculus. The precise relationships need to be investigated.

The analysis of normalisation by evaluation pursued here is categorical and, as such, is related to Altenkirch et al. (1995); Altenkirch et al. (2001), Čubrić et al. (1997), Reynolds (1998).

The approach of Čubrić et al. (1997) is in the context of so-called $\mathcal{P}$ -category theory; which is, roughly, a version of category theory equipped with an intensional notion of equality formalised by partial equivalence relations. The intensional information needed for the purpose of normalisation will be captured here in the context of traditional category theory via Artin–Wraith glueing.

In Altenkirch et al. (1995), normalisation by evaluation is reconstructed categorically in a model obtained via an ad hoc twisted-glueing construction. This model embodies objects with both syntactic and semantic components and translations between them essentially encoding a correctness predicate. In contrast, we adopt a purely semantic view, working with intensional logical relations in models given by the traditional categorical-glueing construction (Wraith, 1974).

Another important point of departure between this work and the other categorical ones is the algebraic treatment of the subject, which led to a deeper understanding of the normalisation function.

2. Part I

2.1 Typed lambda calculus

For the purpose of establishing notations, we briefly recall the syntax and semantics of the typed lambda calculus. For details see, e.g., Lambek and Scott (1986), Crole (1994), Taylor (1999).

Syntax. The types of the simply-typed lambda calculus are given by the grammar

(1) \begin{equation}\begin{array}{rcl}\tau& ::= & \theta \mid \texttt{1} \mid \tau_1 * \tau_2 \mid \tau_1 \texttt{=}\!\!\texttt{>} \tau_2\end{array}\end{equation}

where $\theta$ ranges over base types. We write $\widetilde{\mathrm{T}}$ for the set of simple types generated by a set of base types T.

The grammar for the terms is

\begin{equation*}\begin{array}{rcl}t& ::= & x \mid \langle{}\rangle \mid \pi_1(t) \mid \pi_2(t) \mid \langle{t_1,t_2}\rangle \mid t(t') \mid \lambda{x:\tau}t\end{array}\end{equation*}

where x ranges over (a countably infinite set of) variables. The notion of free and bound variables are standard. As usual, we will identify terms up to the renaming of bound variables.

Typing contexts, with types in a set $\mathcal{T}$ , are defined as functions $V\rightarrow \mathcal{T}$ where the domain of the context, V, is a finite subset of the set of variables. Under this view, for a variable x, a type $\tau$ , and a context $\Gamma$ , we let $(x:\tau) \in \Gamma$ stand for $x\in\mathrm{dom}(\Gamma)$ and $\Gamma(x) = \tau$ . For distinct variables $x_i$ ( $i=1,n$ ), we use the notation $\langle{x_i:\tau_i}\rangle_{i=1,n}$ for the context $\{ x_1,\ldots, x_n \} \rightarrow \mathcal{T}$ mapping $x_i$ to $\tau_i$ . For a context $\Gamma$ , a variable x, and a type $\tau$ , the notation $\Gamma, x:\tau$ presupposes $x \not\in \mathrm{dom}(\Gamma)$ and denotes the context $\mathrm{dom}(\Gamma)\cup\{x\} \rightarrow \mathcal{T}$ mapping every $y \in \mathrm{dom}(\Gamma)$ to $\Gamma(y)$ , and x to $\tau$ .

The well-typed terms $\Gamma \vdash t: \tau$ in context (where $\Gamma$ is a typing context, t is a term and $\tau$ is a type) are given by the usual rules; see Figure 1.

Figure 1. Well-typed terms.

Semantics. The appropriate mathematical universes for giving semantics to the typed lambda calculus are cartesian closed categories (Crole, 1994; Lambek and Scott, 1986; Taylor, 1999); i.e, categories with terminal object, binary products and exponentials (for which we, respectively, use the notation 1, $\times$ , and $\Rightarrow$ ).

For an interpretation $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ of base types in a cartesian closed category, we let $\textbf{s}[\![_]\!]: \widetilde{\mathrm{T}} \rightarrow \mathcal{S}$ be the extension to simple types as prescribed by a chosen cartesian closed structure. That is, $\textbf{s}[\![\theta]\!] = \textbf{s}(\theta)$ (for $\theta \in \mathrm{T}$ ), $\textbf{s}[\![\texttt{1}]\!] = 1$ , and $\textbf{s}[\![{\tau*\tau'}]\!] = \textbf{s}[\![\tau]\!] \times \textbf{s}[\![{\tau'}]\!]$ and $\textbf{s}[\![{\tau\texttt{=}\!\!\texttt{>}\tau'}]\!] = \textbf{s}[\![\tau]\!] \Rightarrow \textbf{s}[\![{\tau'}]\!]$ (for $\tau, \tau' \in \widetilde{\mathrm{T}}$ ). As usual, the interpretation of types is extended to contexts by setting $\textbf{s}[\![\Gamma]\!] = \prod_{x\in\mathrm{dom}(\Gamma)} \textbf{s}[\![{\Gamma(x)}]\!]$ for all contexts $\Gamma$ . Finally, the semantics of a term $\Gamma \vdash t: \tau$ as a morphism $\textbf{s}[\![\Gamma]\!] \rightarrow \textbf{s}[\![\tau]\!]$ in $\mathcal{S}$ is denoted $\textbf{s}[\![{\Gamma \vdash t: \tau}]\!]s$ .

2.2 From definability to normalisation

Kripke relations were introduced by Jung and Tiuryn in (1993) for the purpose of characterising lambda definability. We will analyse this result and provide a corresponding extensional normalisation result.

Kripke relations. For a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ , a $\mathbb{C}$ -Kripke relation R of arity $\boldsymbol{\sigma}$ over an object A of $\mathcal{S}$ is a family $\{ R(c) \subseteq \mathcal{S}(\boldsymbol{\sigma}(c),A)\}_{c \in \mid{\,\mathbb{C}\,}\mid}$ satisfying the following condition.

(Monotonicity) For every $\rho: c' \rightarrow c$ in $\mathbb{C}$ and every $a: \boldsymbol{\sigma}(c) \rightarrow A$ in R(c), the map $a \circ \boldsymbol{\sigma}(\rho): \boldsymbol{\sigma}(c') \rightarrow A$ is in R(c’).

In other words, a $\mathbb{C}$ -Kripke relation R of arity $\boldsymbol{\sigma}$ over an object A is a unary predicate over the $\mathbb{C}^\mathrm{op}$ -variable set of A-valued morphisms $\mathcal{S}(\boldsymbol{\sigma}(\_),A): \mathbb{C}^\mathrm{op} \rightarrow \textbf{Set}$ in the functor category $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$ of $\mathbb{C}^\mathrm{op}$ -variable sets, referred to as presheaves.

The category of Kripke relations $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ of arity $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ has objects given by pairs (R,A) consisting of an object A of $\mathcal{S}$ and a $\mathbb{C}$ -Kripke relation of arity $\boldsymbol{\sigma}$ over A, and morphisms $f: (R,A) \rightarrow (R',A')$ given by maps $f: A \rightarrow A'$ in $\mathcal{S}$ such that, for all $a: \boldsymbol{\sigma}(c) \rightarrow A$ in R(c), the composite $f \circ a: \boldsymbol{\sigma}(c) \rightarrow A'$ is in R’(c). Composition and identities are as in $\mathcal{S}$ .

Example 1. The category of $\mathbb{C}$ -Kripke relations of arity the unique functor to the terminal category is (isomorphic to) the complete Heyting algebra of subterminal objects of the presheaf topos $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$ .

The following proposition is well-known (see, e.g., Alimohamed 1995; Ma and Reynolds 1992).

Proposition 2. Let $\mathbb{C}$ be a small category and let $\mathcal{S}$ be a cartesian closed category. For a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ , the category of Kripke relations $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ is cartesian closed and the forgetful functor $\underline{K}\langle{\boldsymbol{\sigma}}\rangle \rightarrow \mathcal{S}: (R,A) \mapsto A$ preserves the cartesian closed structure strictly.

The cartesian closed structure of $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ is given as follows.

1. (Products) The terminal object is $(\top,1)$ where 1 is terminal in $\mathcal{S}$ and where $\top(c) = \{ \boldsymbol{\sigma}(c) \rightarrow 1\}$ for all c in $\mathbb{C}$ . The product $(R,A)\times(R',A')$ of (R,A) and (R’,A’) is

where is the product of A and A’ in $\mathcal{S}$ , and where $a: \boldsymbol{\sigma}(c) \rightarrow A \times A'$ is in $(R \wedge R')(c)$ iff $\pi \circ a: \boldsymbol{\sigma}(c) \rightarrow A$ is in R(c) and $\pi' \circ a: \boldsymbol{\sigma}(c) \rightarrow A'$ is in R’(c).

1. (Exponentials) The exponential $(R,A)\Rightarrow(R',A')$ of (R,A) and (R’,A’) is

where is the exponential of A and A’ in $\mathcal{S}$ , and where ${f: \boldsymbol{\sigma}(c) \rightarrow A \Rightarrow A'}$ is in $(R \supset R')(c)$ iff for every $\rho: c' \rightarrow c$ in $\mathbb{C}$ and $a: \boldsymbol{\sigma}(c') \rightarrow A$ in R(c’), the composite $\varepsilon \circ \langle{f \circ \boldsymbol{\sigma}(\rho) , a}\langle: \boldsymbol{\sigma}(c') \rightarrow A'$ is in R’(c’).

The Fundamental Lemma of logical relations is a consequence of Proposition 2

Lemma 3. (Fundamental Lemma (Plotkin 1973; Statman 1985)). For an interpretation of base types $\mathcal{I}: \mathrm{T} \rightarrow \underline{K}\langle{\boldsymbol{\sigma}}\rangle: \theta \mapsto (\mathscr{R}_\theta,\mathcal{I}_0(\theta))$ , the interpretation

\begin{equation*}\mathcal{I}_0[\![{\Gamma \vdash t: \tau}]\!]: \mathcal{I}_0[\![{\Gamma}]\!] \rightarrow \mathcal{I}_0[\![{\tau}]\!]in \mathcal{S}\end{equation*}

of a term $\Gamma \vdash t: \tau$ yields a morphism $\mathcal{I}[\![{\Gamma}]\!] \rightarrow \mathcal{I}[\![{\tau}]\!]$ in $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ ; that is, for $\mathcal{I}[\![\Gamma]\!]= (\mathscr{R}_\Gamma,\mathcal{I}_0[\![\Gamma]\!])$ and $\mathcal{I}[\![\tau]\!] = (\mathscr{R}_\tau,\mathcal{I}_0[\![\tau]\!])$ , the following diagram

commutes in $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\!$ (for a necessarily unique natural map $\mathscr{R}_\Gamma \rightarrow \mathscr{R}_\tau$ ).

Definability. The definability result of Jung and Tiuryn (1993) uses Kripke relations varying over a poset of contexts ordered by context extension. Here, however, to parallel the development with the one to follow in Part II, we will consider Kripke relations varying over a category of contexts and context renamings.

Definition 4. For a set of types $\mathcal{T}$ , we let $\mathbb{F}{}\!\downarrow\!\mathcal{T}$ be the category with objects given by contexts $\Gamma$ with types in $\mathcal{T}$ , and with morphisms $\Gamma \rightarrow \Gamma'$ given by type-preserving context renamings; that is, by functions $\rho: \mathrm{dom}(\Gamma) \rightarrow \mathrm{dom}(\Gamma')$ such that for all variables $x \in \mathrm{dom}(\Gamma)$ , the types $\Gamma(x)$ , and $\Gamma'(\rho x)$ are equal. We write $\mathbb{F}{}[\mathcal{T}]$ for $(\mathbb{F}{}\!\downarrow\!\mathcal{T})^\mathrm{op}$ .

With respect to an interpretation $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ of base types in a cartesian closed category, we write $\textbf{s}[\![{\_}[\![$ for the canonical semantic functor $\mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathcal{S}$ interpreting contexts and their renamings. This is explicitly given by

for all $\rho: \Gamma \rightarrow \Gamma'$ in $\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}$ .

For every type $\tau \in \widetilde{\mathrm{T}}$ , the definability relation

\begin{equation*}\mathscr{D}_\tau(\Gamma)=\{ \ \textbf{s}[\![{\Gamma \vdash t: \tau }]\!] \mid \Gamma \vdash t: \tau \ \}\subseteq \mathcal{S}(\textbf{s}[\![\Gamma]\!],\textbf{s}[\![\tau]\!])\end{equation*}

is an $\mathbb{F}{}[\widetilde{\mathrm{T}}]$ -Kripke relation of arity $\textbf{s}[\![{\_}]\!]: \mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathcal{S}$ over $\textbf{s}[\![{\tau}]\!]$ , and the family of definability relations $\{ \mathscr{D}_\tau\}s_{\tau \in \widetilde{\mathrm{T}}}$ has the following logical characterisation.

Lemma 5 (Definability Lemma (Alimohamed 1995; Jung and Tiuryn 1993)). Let $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ be an interpretation of base types in a cartesian closed category. Setting $\mathscr{R}_\theta = \mathscr{D}_\theta$ for all base types $\theta \in \mathrm{T}$ and letting $\mathscr{R}_\tau$ be given by the cartesian closed structure of the category of Kripke relations $\underline{K}{\textbf{s}[\![{\_}]\!]: \mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathcal{S}}$ for the other types $\tau \in \widetilde{\mathrm{T}}$ , it follows that $\mathscr{R}_\tau = \mathscr{D}_\tau$ for all types $\tau \in \widetilde{\mathrm{T}}$ .

The usual proof of the Definability Lemma is by induction on the structure of types using the explicit description of the cartesian closed structure in categories of Kripke relations given above; see Jung and Tiuryn (1993), Alimohamed (1995) (and Fiore and Simpson 1999 for the case with sum types). However, there is a more conceptual argument based on establishing that the definability relations satisfy the following closure properties:

s which is, in effect, what the usual calculations really amount to.

The above analysis can be refined further. Indeed, the fact that neither of the following inclusions

(2) \begin{equation} \mathscr{D}_\tau \subseteq \mathscr{R}_\tau \subseteq \mathscr{D}_\tau\end{equation}

in isolation is strong enough to re-establish the inductive hypothesis in the Definability Lemma, suggests considering a more general situation in which the Kripke logical relations $\mathscr{R}_\tau$ are bounded by possibly distinct Kripke relations (unlike the situation in (2)).

We are thus led to the following Basic Lemma. Notice the mixed-variance treatment of exponentiation. This is akin to Krivine’s approach to normalisation for the untyped lambda calculus using adapted pairs of subsets of lambda terms Krivine (1993), Chapter III, pp. 33–39.

Lemma 6 (Basic Lemma). Consider an interpretation $\mathcal{I}_0: \mathrm{T} \rightarrow \mathcal{S}$ of base types in a cartesian closed category $\mathcal{S}$ .

With respect to a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ , let $\langle{ (\mathscr{A}_\tau,\mathcal{I}_0[\![{\tau}]\!])}\rangle_{\tau\in\widetilde{\mathrm{T}}}$ and $\langle{ ( \mathscr{B}_\tau,\mathcal{I}_0[\![{\tau}]\!] ) }\rangle_{\tau\in\widetilde{\mathrm{T}}}$ be two families of Kripke relations in $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ indexed by types such that

For a family of Kripke relations $\langle{ ( \mathscr{R}_\theta , \mathcal{I}_0[\![\theta]\!] ) }\rangle_{\theta\in\mathrm{T}}$ in $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ indexed by base types, let $\langle{ ( \mathscr{R}_\tau , \mathcal{I}_0[\![{\tau}]\!] ) }\rangle_s{\tau\in\widetilde{\mathrm{T}}}$ be the family of Kripke relations indexed by types induced by the cartesian closed structure of $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ .

If $\mathscr{A}_\theta \subseteq \mathscr{R}_\theta \subseteq \mathscr{B}_\theta$ for all base types $\theta \in \mathrm{T}$ , then

1. 1. $\mathscr{A}_\tau \subseteq \mathscr{R}_\tau \subseteq \mathscr{B}_{\tau}$ for all types $\tau \in \widetilde{\mathrm{T}}$ , and thus

2. 2. for all terms $\Gamma\vdash t:\tau$ (with $\Gamma=\langle{x_i:\tau_i}\rangle_{i=1,n})$ and morphisms $a_i: \boldsymbol{\sigma}(c) \rightarrow \mathcal{I}_0[\![{\tau_i}]\!]$ in $\mathscr{A}_{\tau_i}(c)$ $(1 \leq i \leq n, c \in \mid{\mathbb{C}}\mid)$ , we have that $\mathcal{I}_0[\![{\Gamma \vdash t: \tau}]\!] \circ \langle{a_1,\ldots,a_n}\rangle: \boldsymbol{\sigma}(c) \rightarrow \mathcal{I}_0[\![{\tau}]\!]$ is in $\mathscr{B}_\tau(c)$ .

Proof. The proof of the first part is by induction on the structure of types. This uses the facts that

\begin{equation*}R\subseteq\top \mathrm{for all} (R,1) \mathrm{in} \underline{K}\langle{\boldsymbol{\sigma}}\rangle\end{equation*}

and that, for Kripke relations $(R_i,A_i)$ and $(R'_i,A_i)$ in $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ ( $i=1,2$ ),

\begin{equation*}\mathrm{if} R_1 \subseteq R'_1 \mathrm{and} R_2 \subseteq R'_2 \mathrm{then}(R_1\wedge R_2) \subseteq (R'_1\wedge R'_2) \mathrm{and}(R'_1\supset R_2) \subseteq (R_1\supset R'_2)\end{equation*}

which follows from the functoriality of binary products and exponentials using the observation that, for (R,A) and (R’,A) in $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$ ,

\begin{equation*}R \subseteq R'\mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} \mathrm{id}_A: (R,A) \rightarrow (R',A)\mbox{ in $\underline{K}\langle{\boldsymbol{\sigma}}\rangle$}.\end{equation*}

The proof of the second part follows from considering the interpretation $\mathcal{I}: \mathrm{T} \rightarrow \underline{K}\langle{\boldsymbol{\sigma}}\rangle$ mapping a base type $\theta$ to the Kripke relation $( \mathscr{R}_\theta , \mathcal{I}_0[\![\theta]\!])$ and noticing that, by the first part and the Fundamental Lemma of logical relations, the diagram below in $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$

(3)

commutes, where for $\Gamma = \langle{ x_i:\tau_i }\rangle_{i=1,n}$ , $\mathscr{A}_\Gamma = \mathscr{A}_{\tau_1}\wedge\ldots\wedge\mathscr{A}_{\tau_n}$ and $\mathscr{R}_\Gamma = \mathscr{R}_{\tau_1}\wedge\ldots\wedge\mathscr{R}_{\tau_n}$ .

The Basic Lemma yields the Definability Lemma by considering $\mathscr{A}_\tau = \mathscr{D}_\tau = \mathscr{B}_\tau$ in the category of Kripke relations $\underline{K}{\textbf{s}[\![{\_}]\!]: \mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathcal{S}}$ for the given interpretation $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ . We will now see that the Basic Lemma can be also applied to obtain an extensional normalisation result (see Lemma 9).

Normalisation. For an interpretation $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ of base types in a cartesian closed category, we aim at defining families $\{ ( \mathscr{DM}_\tau , \textbf{s}[\![{\tau}]\!] ) \}_{\tau\in\widetilde{\mathrm{T}}}$ and $\{ ( \mathscr{DN}_\tau , \textbf{s}[\![{\tau}]\!] )\}_{\tau\in\widetilde{\mathrm{T}}}$ of $\mathbb{F}{}[\widetilde{\mathrm{T}}]$ -Kripke relations of arity $\textbf{s}[\![{\_}]\!]: \mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathcal{S}$ of definable morphisms such that

so that, by the second part of the Basic Lemma, we get (setting $\mathscr{R}_\theta = \mathscr{DM}_\theta$ for all $\theta \in \mathrm{T}$ , and $a_i = \pi_i: \textbf{s}[\![\Gamma]\!] \rightarrow \textbf{s}[\![{\tau_i}]\!]$ for $\Gamma = \langle{x_i:\tau_i}\rangle_{i=1,n}$ ) that, for all terms $\Gamma \vdash t: \tau$ ,

(4) \begin{equation} {\textbf{s}[\![{\Gamma \vdash t: \tau}]\!]: \textbf{s}[\![\Gamma]\!] \rightarrow \textbf{s}[\![{\tau}]\!]\mathrm{is in} \mathscr{DN}_\tau(\Gamma).}\end{equation}

The above will be achieved by distilling the semantic closure properties (i)–(vii) into two syntactic typing systems $\vdash_{\mathscr{M}}$ and $\vdash_{\mathscr{N}}$ with respect to which the definitions

(5)

(6)

will provide the required Kripke relations (see Proposition 8). The conditions (i)–(vii) amount, roughly, to the following properties.

• The system $\vdash_{\mathscr{M}}$ should contain variables (condition (vii)), and be closed under projections (condition (ii)) and under the application to terms in the system $\vdash_{\mathscr{N}}$ (condition (iv)).

• The system $\vdash_{\mathscr{N}}$ should contain the unit (condition (i)) and should be closed under pairing (condition (iii)) and under abstraction (condition (v)).

• Every term of base type in the system $\vdash_{\mathscr{M}}$ should be in the system $\vdash_{\mathscr{N}}$ (condition (vi)).

Formally, the systems are given by the rules in Figure 2.

Figure 2. Neutral and normal terms.

Thus, from purely semantic considerations, we have synthesised the notions of neutral normal forms (viz., those derivable in the system $\vdash_{\mathscr{M}}$ ) and of long $\beta\eta$ -normal forms (viz., those derivable in the system $\vdash_{\mathscr{N}}$ ), henceforth, respectively, referred to as neutral and normal terms, and characterised as follows.

Proposition 7.

1. 1. (Neutral terms)

   

2. 2. (Normal terms)

   • $\Gamma\vdash_{\mathscr{N}} t:\texttt{1} \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} t = \langle{}\rangle$

   • $\Gamma\vdash_{\mathscr{N}} t:\tau_1*\tau_2 \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} [ \ \exists\ \Gamma\vdash_{\mathscr{N}} N_1:\tau_1\, , \Gamma \vdash_{\mathscr{N}} N_2:\tau_2 .\ t = \langle{N_1,N_2}\rangle \ ]$

   • $\Gamma\vdash_{\mathscr{N}} t:\tau\texttt{=}\!\!\texttt{>}\tau' \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} [ \ \exists\ \Gamma,x:\tau\vdash_{\mathscr{N}} N:\tau'.\ t = \lambda{x:\tau}N \ ]$

   • For $\theta$ a base type, $\Gamma\vdash_{\mathscr{N}} t:\theta \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} \Gamma\vdash_{\mathscr{M}} t:\theta$ .

Neutral and normal terms are closed under context renamings and thereby semantically induce Kripke relations.

Proposition 8. Let $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ be an interpretation of base types in a cartesian closed category. For all types $\tau\in\widetilde{\mathrm{T}}$ , the definitions (5) and (6), respectively, yield $\mathbb{F}{}[\widetilde{\mathrm{T}}]$ -Kripke relations $\mathscr{DM}_\tau$ and $\mathscr{DN}_\tau$ of arity $\textbf{s}[\![{\_}]\!]: \mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathcal{S}$ satisfying conditions (i)–(vii).

Proof. The first part is a corollary of the facts that

(7)

and

(8)

The second part follows by the construction of the systems $\vdash_{\mathscr{M}}$ and $\vdash_{\mathscr{N}}$ .

From Proposition 8, we have (4) and therefore, from (6) and Proposition 7(2), we obtain the following Extensional Normalisation Lemma.

Lemma 9 (ExtensionalNormalisation Lemma). Let $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ be an interpretation of base types in a cartesian closed category. For every term $\Gamma \vdash t: \tau$ , there exists a long $\beta\eta$ -normal term $\Gamma \vdash_{\mathscr{N}} N: \tau$ such that

in $\mathcal{S}$ .

Specialising the Extensional Normalisation Lemma for the canonical interpretation of types in the free cartesian closed category generated by them, we obtain the following syntactic result (Streicher 1998).

Corollary 10. Every simply typed term is $\beta\eta$ -equal to one in long $\beta\eta$ -normal form.

The above does not give information about the long $\beta\eta$ -normal form associated to a term because Kripke relations are extensional predicates. What is needed instead for this purpose is a notion of intensional Kripke relation in which the extension of the predicate is witnessed (or realised). Technically, this amounts to revisiting the development in categories obtained by the Artin–Wraith glueing construction (Wraith 1974). This will be done in Part II. To do it at an appropriate abstract, syntax-independent level, we will first consider the typed lambda calculus algebraically.

3. Part II

3.1 Algebraic typed lambda calculus

We provide an algebraic setting for the syntax and semantics of the typed lambda calculus following and extending the theory of Fiore et al. (1999). In particular, we describe the typed abstract syntax of simply typed and of neutral and normal terms as initial algebras and show how the usual semantics corresponds to unique algebra homomorphisms from the initial (term) algebras to suitable semantic algebras.

3.1.1 Syntax

Categories of contexts, which we study next, play a crucial role in describing abstract syntax with variable binding; see Fiore et al. (1999) for further details.

Free (co)cartesian categories. The category of untyped contexts and renamings $\mathbb{F}{}$ with objects given by finite subsets of (the countably infinite set of) variables and morphisms given by all functions is the free cocartesian category on one generator.

More generally, the free cocartesian category over a set $\mathcal{T}$ can be described as the comma category $\mathbb{F}{}\!\downarrow\!\mathcal{T}$ of contexts with types in the set $\mathcal{T}$ and type-preserving context renamings. (That is, $\mathbb{F}{}\!\downarrow\!\mathcal{T}$ is the category with objects given by maps $\Gamma: V \rightarrow \mathcal{T}$ where V is in $\mathbb{F}{}$ , and with morphisms $\rho: \Gamma \rightarrow \Gamma'$ given by functions $\rho: \mathrm{dom}(\Gamma) \rightarrow \mathrm{dom}(\Gamma')$ such that $\Gamma = \Gamma' \circ \rho$ .) The initial object $(0 \rightarrow \mathcal{T})$ in $\mathbb{F}{}\!\downarrow\!\mathcal{T}$ is the empty context; whilst the coproduct in $\mathbb{F}{}\!\downarrow\!\mathcal{T}$ is

As before, we write $\mathbb{F}{}[\mathcal{T}]$ for $(\mathbb{F}{}\!\downarrow\!\mathcal{T})^\mathrm{op}$ . Further, we write $\langle{\_}\rangle: \mathcal{T} \rightarrow \mathbb{F}{}[\mathcal{T}]$ for the universal embedding (mapping $\tau$ to $(1 \tau \mathcal{T})$ ) and exhibiting $\mathbb{F}{}[\mathcal{T}]$ as the free cartesian category over $\mathcal{T}$ .

Typed abstract syntax with variable binding. The semantic universe on which to consider the algebras for the typed lambda calculus over a set of base types T is the functor category $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ of $\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}$ -variable sets, referred to as (covariant) presheaves. (Recall that $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ has objects given by functors $\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}} \rightarrow \textbf{Set}$ and morphisms $\varphi: P \rightarrow P'$ given by natural transformations; that is, families of functions $\varphi = \{ \varphi_\Gamma: P(\Gamma) \rightarrow P'(\Gamma)\}_{\Gamma\in\mid{\,\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}\,}\mid}$ such that $\varphi_{\Gamma'} \circ P(\rho) = P'(\rho) \circ \varphi_\Gamma$ for all $\rho:\Gamma\rightarrow\Gamma'$ in $\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}$ .)

The structure of $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ allowing the interpretation of variables and binding operators is described below.

• The presheaf of variables of type $\tau \in \widetilde{\mathrm{T}}$ is

  (9) \begin{equation} \mathrm{V}_{\tau} = \textbf{y}\langle\tau\rangle\end{equation}
  in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ where is the Yoneda embedding. Hence, $\mathrm{V}_{\tau}(\Gamma) \cong \{ x \mid (x:\tau) \in \Gamma \}$ .

• For every type $\tau \in \widetilde{\mathrm{T}}$ , the parameterisation functor ${\_}\times\langle\tau\rangle: \mathbb{F}{}[\widetilde{\mathrm{T}}] \rightarrow \mathbb{F}{}[\widetilde{\mathrm{T}}]$ induces the following situation

  (10)

  
  Thus, in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ , the exponential $P^{\mathrm{V}_{\tau}}$ of the presheaf $\mathrm{V}_{\tau}$ and a presheaf P can be explicitly described as $P({\_}+\langle{\tau}\rangle)$ .

Hence, $P^{\mathrm{V}_{\tau}}(\Gamma) \cong P(\Gamma+\langle{\tau}\rangle)$ .

A typed lambda algebra over a set of base types T is a $\widetilde{\mathrm{T}}$ -sorted algebra with carrier given by a family $\{ \mathscr{X}_\tau\}_{\tau\in\widetilde{\mathrm{T}}}$ of presheaves in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ equipped with the following operations:

Informally, one thinks of the sets $\mathscr{X}_\tau(\Gamma)$ ( $\tau\in\widetilde{\mathrm{T}}$ , $\Gamma \in \mid{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}\mid$ ) as the $\tau$ -sorted elements of the algebra $\mathscr{X}$ in the context $\Gamma$ . Note that under this interpretation the abstraction operation corresponds to a natural family of mappings

\begin{equation*}\mathscr{X}_{\tau'}(\Gamma+\langle{\tau}\rangle)\rightarrow\mathscr{X}_{\tau\texttt{=}\!\!\texttt{>}\tau'}(\Gamma)\end{equation*}

associating an element of sort $\tau'$ in the context $\Gamma+\langle{\tau}\rangle$ (that is, the context $\Gamma$ extended with a fresh variable of type $\tau$ ) with an element of sort $\tau\texttt{=}\!\!\texttt{>}\tau'$ in the context $\Gamma$ .

In the tradition of categorical algebra, the category of typed lambda algebras can be defined as the category of $\Sigma$ -algebras for a signature endofunctor $\Sigma$ on $(\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}})^{\widetilde{\mathrm{T}}}$ . This endofunctor is induced by the above operations as follows, for $\theta\in\mathrm{T}$ and $\tau,\tau'\in\widetilde{\mathrm{T}}$ :

\begin{equation*}\begin{array}{lcll}(\Sigma\mathscr{X})_\theta& = & \mathrm{V}_{\theta} + \mathrm{E}_{\theta}(\mathscr{X})\\[2mm](\Sigma\mathscr{X})_\texttt{1}& = & \mathrm{V}_{\texttt{1}} + 1 + \mathrm{E}_{\texttt{1}}(\mathscr{X})\\[2mm](\Sigma\mathscr{X})_{\tau*\tau'}& = & \mathrm{V}_{\tau*\tau'} + (\mathscr{X}_\tau \times \mathscr{X}_{\tau'}) + \mathrm{E}_{\tau*\tau'}(\mathscr{X})\\[2mm](\Sigma\mathscr{X})_{\tau\texttt{=}\!\!\texttt{>}\tau'}& = & \mathrm{V}_{\tau\texttt{=}\!\!\texttt{>}\tau'} + (\mathscr{X}_{\tau'})^{\mathrm{V}_{\tau}} + \mathrm{E}_{\tau\texttt{=}\!\!\texttt{>}\tau'}(\mathscr{X})\end{array}\end{equation*}

where

\begin{equation*}\begin{array}{cl}\mathrm{E}_{\tau}(\mathscr{X})\; = \; \coprod_{\tau'\in\widetilde{\mathrm{T}}}\: \mathscr{X}_{\tau*\tau'} + \mathscr{X}_{\tau'*\tau} + (\mathscr{X}_{\tau'\texttt{=}\!\!\texttt{>}\tau}\times\mathscr{X}_{\tau'})\end{array}\end{equation*}

is the signature endofunctor corresponding to the projections and application operations onto $\tau$ .

The initial $\Sigma$ -algebra $\mathscr{L}_= \{ \mathscr{L}_{\tau}\}_{\tau\in\widetilde{\mathrm{T}}}$ with its structure

(11) \begin{equation}\begin{array}{rcl}\mathrm{V}_{\theta} + \mathrm{E}_{\theta}(\mathscr{L}_)&\cong&\mathscr{L}_{\theta}\\[2mm]\mathrm{V}_{\texttt{1}} + 1 +\mathrm{E}_{\texttt{1}}(\mathscr{L})& \cong &\mathscr{L}_{\texttt{1}}\\[2mm]\mathrm{V}_{\tau*\tau'} +(\mathscr{L}_{\tau} \times \mathscr{L}_{\tau'}) + \mathrm{E}_{\tau*\tau'}(\mathscr{L})& \cong &\mathscr{L}_{\tau*\tau'}\\[2mm]\mathrm{V}_{\tau\texttt{=}\!\!\texttt{>}\tau'} +(\mathscr{L}_{\tau'})^{\mathrm{V}_{\tau}} +\mathrm{E}_{\tau\texttt{=}\!\!\texttt{>}\tau'}(\mathscr{L})& \cong &\mathscr{L}_{\tau\texttt{=}\!\!\texttt{>}\tau'}\end{array}\end{equation}

can be explicitly described as the family of presheaves of terms

\begin{equation*}\mathscr{L}_{\tau}(\Gamma) = \{ \ t \mid \Gamma \vdash t: \tau \ \}\end{equation*}

with presheaf action given by variable renaming (that is, by the mapping associating $\Gamma \vdash t: \tau$ to $\Gamma' \vdash t[^{\rho x}\!/_{x}]_{x\in\mathrm{dom}(\Gamma)}: \tau$ for any $\rho: \Gamma \rightarrow \Gamma'$ in $\mathbb{F}\!\downarrow\!\widetilde{\mathrm{T}}$ ), and with operations

\begin{equation*}\begin{array}{lcl}\textsf{var}_\tau & : & \mathrm{V}_{\tau} \rightarrow \mathscr{L}_{\tau}\\[2mm]\textsf{unit}_\texttt{1} & : & 1 \rightarrow \mathscr{L}_{\texttt{1}}\\[2mm]\textsf{fst}^{(\tau')}_\tau & : & \mathscr{L}_{\tau*\tau'} \rightarrow \mathscr{L}_{\tau}\\[2mm]\textsf{snd}^{(\tau')}_\tau & : & \mathscr{L}_{\tau'*\tau} \rightarrow \mathscr{L}_{\tau}\\[2mm]\textsf{pair}_{\tau*\tau'} & : & \mathscr{L}_{\tau} \times \mathscr{L}_{\tau'} \rightarrow \mathscr{L}_{\tau*\tau'}\\[2mm]\textsf{app}^{(\tau')}_\tau & : & \mathscr{L}_{\tau'\texttt{=}\!\!\texttt{>}\tau} \times \mathscr{L}_{\tau'} \rightarrow \mathscr{L}_{\tau}\\[2mm]\textsf{abs}_{\tau\texttt{=}\!\!\texttt{>}\tau'} & : & (\mathscr{L}_{\tau'})^{\mathrm{V}_{\tau}} \rightarrow \mathscr{L}_{\tau\texttt{=}\!\!\texttt{>}\tau'}\end{array}\end{equation*}

corresponding to the typing rules in Figure 1.

A full theory of typed abstract syntax with variable binding incorporating substitution along the lines of Fiore et al. (1999) can be developed (see, e.g., Fiore and Hur 2010; Fiore and Szamozvancev 2022). This is however not necessary for the purposes of the paper.

The notions of neutral and normal terms are given by mutual induction (see Figure 2) and, as such, the associated algebraic notion corresponds to considering a signature endofunctor on the product category $(\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}})^{\widetilde{\mathrm{T}}} \times (\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}})^{\widetilde{\mathrm{T}}}$ . This endofunctor, with components $\langle{\Sigma_1,\Sigma_2}\rangle$ , is defined below:

\begin{equation*}\left\{\begin{array}{rcl}(\Sigma_1(\mathscr{X},\mathscr{Y}))_\tau= \mathrm{V}_{\tau} + \mathrm{E}_{\tau}(\mathscr{X},\mathscr{Y})\end{array}\right.\qquad\qquad\left\{\begin{array}{lcl}(\Sigma_2(\mathscr{X},\mathscr{Y}))_\theta& = & \mathrm{V}_{\theta} + \mathrm{E}_{\theta}(\mathscr{X},\mathscr{Y})\\[2mm](\Sigma_2(\mathscr{X},\mathscr{Y}))_\texttt{1}& = & 1\\[2mm](\Sigma_2(\mathscr{X},\mathscr{Y}))_{\tau*\tau'}& = &\mathscr{Y}_\tau \times \mathscr{Y}_{\tau'}\\[2mm](\Sigma_2(\mathscr{X},\mathscr{Y}))_{\tau\texttt{=}\!\!\texttt{>}\tau'}& = &(\mathscr{Y}_{\tau'})^{\mathrm{V}_{\tau}}\end{array}\right.\end{equation*}

where

\begin{equation*}\textstyle\mathrm{E}_{\tau}(\mathscr{X},\mathscr{Y}) = \coprod_{\tau'\in\widetilde{\mathrm{T}}}\: \mathscr{X}_{\tau*\tau'} + \mathscr{X}_{\tau'*\tau} + (\mathscr{X}_{\tau'\texttt{=}\!\!\texttt{>}\tau}\times\mathscr{Y}_{\tau'})\end{equation*}

for $\theta\in\mathrm{T}$ and $\tau,\tau'\in\widetilde{\mathrm{T}}$ .

We write $(\mathscr{M},\mathscr{N})$ for the initial $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra with structure, for $\theta\in\mathrm{T}$ and $\tau,\tau'\in\widetilde{\mathrm{T}}$ , as follows:

(12) \begin{equation} \left\{\begin{array}{rcl}\mathrm{V}_{\tau} + \mathrm{E}_{\tau}(\mathscr{M},\mathscr{N})& \cong &\mathscr{M}_{\tau}\end{array}\right.\qquad\qquad\left\{\begin{array}{rcl}\mathrm{V}_{\theta} + \mathrm{E}_{\theta}(\mathscr{M},\mathscr{N})& \cong &\mathscr{N}_{\theta}\\[2mm]1& \cong &\mathscr{N}_{\texttt{1}}\\[2mm]\mathscr{N}_{\tau} \times \mathscr{N}_{\tau'}& \cong &\mathscr{N}_{\tau*\tau'}\\[2mm](\mathscr{N}_{\tau'})^{\mathrm{V}_{\tau}}& \cong &\mathscr{N}_{\tau\texttt{=}\!\!\texttt{>}\tau'}\end{array}\right.\end{equation}

Note that we have an isomorphism

(13) \begin{equation} \textsf{norm} \, : \, \mathscr{M}_{\theta} \cong \mathrm{V}_{\theta} + \mathrm{E}_{\theta}(\mathscr{M},\mathscr{N}) \cong \mathscr{N}_{\theta}\end{equation}

for all $\theta\in\mathrm{T}$ .

Explicitly, the presheaves $\mathscr{M}_\tau$ and $\mathscr{N}_{\tau}$ can be, respectively, described as the neutral and normal terms

\begin{equation*}\begin{array}{l}\mathscr{M}_\tau(\Gamma)\ = \ \{\, M\ \mid\ \Gamma \vdash_{\mathscr{M}} M: \tau\, \}\end{array}\qquad\qquad\begin{array}{r}\mathscr{N}_{\tau}(\Gamma)\ = \ \{\, N\ \mid\ \Gamma \vdash_{\mathscr{N}} N: \tau\, \}\end{array}\end{equation*}

with presheaf action given by variable renaming (recall (7) and (8)), and with operations

(14) \begin{equation} \ \left\{\begin{array}{lcl}\textsf{var}_\tau& \ : &\mathrm{V}_{\tau} \rightarrow \mathscr{M}_{\tau}\\[2mm]\textsf{fst}^{(\tau')}_\tau& \ : &\mathscr{M}_{\tau*\tau'} \rightarrow \mathscr{M}_{\tau}\\[2mm]\textsf{snd}^{(\tau')}_\tau& \ : &\mathscr{M}_{\tau'*\tau} \rightarrow \mathscr{M}_{\tau}\\[2mm]\textsf{app}^{(\tau')}_\tau& \ : &\mathscr{M}_{\tau'\texttt{=}\!\!\texttt{>}\tau} \times \mathscr{N}_{\tau'} \rightarrow \mathscr{M}_\tau\end{array}\right.\qquad\qquad\left\{\begin{array}{lcl}\textsf{var}_\theta& \!\! : &\mathrm{V}_{\theta} \rightarrow \mathscr{N}_{\theta}\\[2mm]\textsf{fst}^{(\tau')}_\theta& \!\! : &\mathscr{M}_{\theta*\tau'} \rightarrow \mathscr{N}_{\theta}\\[2mm]\textsf{snd}^{(\tau')}_\theta& \!\! : &\mathscr{M}_{\tau'*\theta} \rightarrow \mathscr{N}_{\theta}\\[2mm]\textsf{app}^{(\tau')}_\theta& \!\! : &\mathscr{M}_{\tau'\texttt{=}\!\!\texttt{>}\theta} \times \mathscr{N}_{\tau'} \rightarrow \mathscr{N}_{\theta}\\[2mm]\textsf{unit}_\texttt{1}& \!\! : &1 \cong \mathscr{N}_{\texttt{1}}\\[2mm]\textsf{pair}_{\tau*\tau'}& \!\! : &\mathscr{N}_{\tau} \times \mathscr{N}_{\tau'} \cong \mathscr{N}_{\tau*\tau'}\\[2mm]\textsf{abs}_{\tau\texttt{=}\!\!\texttt{>}\tau'}& \!\! : &(\mathscr{N}_{\tau'})^{\mathrm{V}_{\tau}} \cong \mathscr{N}_{\tau\texttt{=}\!\!\texttt{>}\tau'}\end{array}\right.\end{equation}

corresponding to the typing rules in Figure 2.

Note that every $\Sigma$ -algebra $\mathscr{X}$ induces a canonical $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra structure on the pair $(\mathscr{X},\mathscr{X})$ and hence, by initiality, homomorphic interpretations $(\mathscr{M},\mathscr{N}) \rightarrow (\mathscr{X},\mathscr{X})$ . Applying this observation to the initial $\Sigma$ -algebra $\mathscr{L}$ , we obtain the embeddings $\mathscr{M} \rightarrowtail \mathscr{L}$ and $\mathscr{N} \rightarrowtail \mathscr{L}$ of neutral and normal terms into terms.

Structural induction. Initial algebras have the following associated structural induction principle (Lehmann and Smyth 1981).

Let $\alpha: FA \rightarrow A$ be an initial algebra for an endofunctor F, if the subobject $m: P \rightarrowtail A$ satisfies the closure property of being a sub F-algebra of A, in the sense that the diagram

(15)

commutes for a (necessarily unique) map $FP \rightarrow P$ , then $m: P \rightarrowtail A$ is an isomorphism.

For the initial $\Sigma$ -algebra $\mathscr{L}$ (resp. the initial $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra $(\mathscr{M},\mathscr{N})$ ), the structural induction principle corresponds, in elementary terms, to proving a property of terms (resp. of neutral and normal terms) by induction (resp. simultaneous induction) on their derivation. The structural induction principle for the initial $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra $(\mathscr{M},\mathscr{N})$ features in the proof of Theorem 21.

3.1.2 Semantics

As we will see below, every interpretation of base types in a cartesian-closed category induces a canonical semantic typed lambda algebra with respect to which the unique algebra homomorphism from the initial (term) algebra is the usual semantics of simply typed terms.

Nerve functor. Every functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ induces the following situation

(16)

where $\langle\boldsymbol{\sigma}\rangle(A) = \mathcal{S}(\boldsymbol{\sigma}(\_),A)$ and where $(\underline{\boldsymbol{\sigma}}_\Gamma)_{\Gamma'} = \boldsymbol{\sigma}_{\Gamma',\Gamma}: \mathbb{C}(\Gamma',\Gamma) \rightarrow \mathcal{S}(\boldsymbol{\sigma}(\Gamma'),\boldsymbol{\sigma}(\Gamma))$ . We refer to $\langle\boldsymbol{\sigma}\rangle: \mathcal{S} \rightarrow \textbf{Set}^{\mathbb{C}^\mathrm{op}}$ as the $\boldsymbol{\sigma}$ -nerve functor and to the presheaf $\langle\boldsymbol{\sigma}\rangle(A)$ as the $\boldsymbol{\sigma}$ -nerve of A.

Two important properties of nerve functors follow.

Proposition 11. For a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ where $\mathbb{C}$ is small, the nerve functor $\langle\boldsymbol{\sigma}\rangle: \mathcal{S} \rightarrow \textbf{Set}^{\mathbb{C}^\mathrm{op}}$ preserves limits. Further, for $\boldsymbol{\sigma}$ and $\mathbb{C}$ cartesian and $\mathcal{S}$ cartesian closed, it also commutes with exponentiation by representables in the sense that there is a canonical natural isomorphism

for all $\Gamma \in \mid\mathbb{C}\mid$ .

Proof. The first part is well-known and follows from the canonical natural isomorphism

\begin{equation*}\begin{array}{rcl}\mathcal{S}(\boldsymbol{\sigma}(\Gamma),L)& \cong &\lim_{\Delta\in\mathbb{D}}\: \mathcal{S}(\boldsymbol{\sigma}(\Gamma),D(\Delta))\\[2mm]f & \mapsto & \langle{\, \pi_\Delta \circ f \,}\rangle_{\Delta\in\mathbb{D}}\end{array}\quad\qquad(\Gamma\in\mathbb{C})\end{equation*}

available for any diagram $D: \mathbb{D} \rightarrow \mathcal{S}$ with limit $\langle{\, \pi_\Delta: L \rightarrow D(\Delta) \,}\rangle_{\Delta\in\mathbb{D}s}$ in $\mathcal{S}$ .

For the second part, note that for we have the following situation (generalising (10))

from which it follows that naturally in $\Delta\in\mathbb{C}$ . We thus obtain a canonical isomorphism

\begin{equation*}\begin{array}{rcl}(\langle\boldsymbol{\sigma}\rangle A)^{\textbf{y}(\Gamma)}(\Delta)& \cong & (\langle\boldsymbol{\sigma}\rangle A)(\Delta\times\Gamma)\ = \ \mathcal{S}(\boldsymbol{\sigma}(\Delta\times\Gamma),A)\\[2mm]& \cong & \mathcal{S}(\boldsymbol{\sigma}(\Delta)\times\boldsymbol{\sigma}(\Gamma),A)\\[2mm]& \cong & \mathcal{S}(\boldsymbol{\sigma}(\Delta),\boldsymbol{\sigma}(\Gamma)\Rightarrow A)\ = \ \langle\boldsymbol{\sigma}\rangle(\boldsymbol{\sigma}(\Gamma)\Rightarrow A)(\Delta)\end{array}\end{equation*}

natural in $\Gamma,\Delta\in\mathbb{C}$ and $A\in\mathcal{S}$ .

Initial algebra semantics. Using the nerve functor $\langle{\textbf{s}[\![{\_}]\!]}\rangle : \mathcal{S} \rightarrow \textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ induced by the cartesian extension $\textbf{s}[\![{\_}]\!]:\mathbb{F}[\widetilde{\mathrm{T}}]\rightarrow\mathcal{S}$ of an interpretation $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ of base types in a cartesian closed category, the operations

\begin{equation*}\begin{array}{lcl}\pi_1& : &\textbf{s}[\![{\tau}]\!] \times \textbf{s}[\![{\tau'}]\!]\rightarrow\textbf{s}[\![{\tau}]\!]\\[2mm]\pi_2& : &\textbf{s}[\![{\tau'}]\!] \times \textbf{s}[\![{\tau}]\!]\rightarrow\textbf{s}[\![{\tau}]\!]\\[2mm]\varepsilon& : &(\textbf{s}[\![{\tau}]\!] \Rightarrow \textbf{s}[\![{\tau'}]\!])\times\textbf{s}[\![{\tau}]\!]\rightarrow\textbf{s}[\![{\tau'}]\!]\end{array}\end{equation*}

in $\mathcal{S}$ can be lifted to $\textbf{Set}^{\mathbb{F}\!\downarrow\!\widetilde{\mathrm{T}}}$ to provide a semantic typed lambda algebra structure on the family

(17)

The operations are as follows:

(18)

(Note that item 1 relies on diagram (16) while items 2, 5, 6, and 7 rely on Proposition. Similar applications of this proposition will be used throughout without further reference.)

By initiality, the semantic typed lambda algebra induces semantic homomorphic interpretations $\ell: \mathscr{L} \rightarrow \mathscr{C}$ and $(m,n): (\mathscr{M},\mathscr{N}) \rightarrow (\mathscr{C},\mathscr{C})$ . These are related as shown below

(19)

Indeed, by the initiality of $(\mathscr{M},\mathscr{N})$ , (19) directly follows from the fact that the homomorphism property of $\ell: \mathscr{L} \rightarrow \mathscr{C}$ amounts to the commutativity of the diagrams in Appendix A and that the homorphism property of $(m,n): (\mathscr{M},\mathscr{N}) \rightarrow (\mathscr{C},\mathscr{C})$ amounts to the commutativity of the diagrams in Appendix B.

Explicitly, for $\tau\in\widetilde{\mathrm{T}}$ , the mapping $\ell_{\tau}: \mathscr{L}_{\tau} \rightarrow \mathscr{C}_{\tau}$ is the standard semantic interpretation of terms

(20)

whilst $m_{\tau}: \mathscr{M}_\tau \rightarrow \mathscr{C}_{\tau}$ and $n_{\tau}: \mathscr{N}_{\tau} \rightarrow \mathscr{C}_{\tau}$ are, respectively, the semantic interpretations of neutral and normal terms.

3.2 Normalisation by evaluation via categorical glueing

We will now see how, by working with intensional Kripke relations, the analysis of normalisation given in Section 2.2 amounts to normalisation by evaluation. As in that section, we will work with semantic models of (covariant) presheaves in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ over nerves induced by interpretations $\textbf{s}$ of the set of base types T in arbitrary cartesian closed categories (see (24)). This level of generality allows the definition of normalisation functions $\textbf{s}-\textsf{nf}_{\tau}: \mathscr{L}_{\tau} \rightarrow \mathscr{N}_{\tau}$ ( $\tau\in\widetilde{\mathrm{T}}$ ) in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ over the $\textbf{s}[\![{\_}]\!]$ -nerve of $\textbf{s}[\![{\tau}]\!]$ (Corollary 20) that are parametric on the interpretation $\textbf{s}$ . Crucially, the normalisation functions will be shown to be parametrically polymorphic, in the sense of being interpretation independent (Corollary 22). This is methodologically important. Firstly, as in Corollary 10, the consideration of the universal interpretation of base types into the free cartesian closed category over them leads to our solution of the intensional normalisation problem (see the discussions after Corollaries 20 and 22 in § Normalisation function below) stated in Introduction. Secondly, the consideration of the trivial interpretation of base types in the trivial cartesian closed category leads to a normalisation algorithm from which a normalisation program is synthesised (see § Normalisation algorithm below).

Intensional Kripke relations. The category of intensional $\mathbb{C}$ -Kripke relations of arity $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ is defined as the glueing of $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$ and $\mathcal{S}$ along the nerve functor $\langle\boldsymbol{\sigma}\rangle: \mathcal{S} \rightarrow \textbf{Set}^{\mathbb{C}^\mathrm{op}}$ . That is, as the comma category $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ of objects given by triples (P,p,A) with $P\in\mid{\textbf{Set}^{\mathbb{C}^\mathrm{op}}}\mid$ , $A\in\mid{\mathcal{S}}\mid$ , and $p: P \rightarrow \langle\boldsymbol{\sigma}\rangle(A)$ in $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$ , and of morphisms $(P,p,A) \rightarrow (P',p',A')$ given by pairs

such that the diagram

commutes.

Example 12. The category of intensional $\mathbb{C}$ -Kripke relations of arity the unique functor to the terminal category is (isomorphic to) the presheaf topos $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$ .

As it is well-known (see, e.g., Crole 1994; Lambek and Scott 1986; Taylor 1999), for $\mathcal{S}$ cartesian closed, the glueing category $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ is also cartesian closed. Indeed, the cartesian closed structure of $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ is given as follows.

1. (Products) The terminal object is (1,t,1) where t is the unique map . The binary product $(P,p,A)\times(Q,q,B)$ of (P,p,A) and (Q,q,B) is $(P\times Q,r,A\times B)$ where r is the composite .

2. (Exponentials) The exponential $(P,p,A)\Rightarrow(Q,q,B)$ of (P,p,A) and (Q,q,B) is $(R,r,A\Rightarrow B)$ in the pullback diagram

   (21)

   
   where the map $\langle\boldsymbol{\sigma}\rangle(A\Rightarrow B) \rightarrow (\langle\boldsymbol{\sigma}\rangle B)^{(\langle\boldsymbol{\sigma}\rangle A)}$ is the exponential transpose of the composite

Explicitly, one may take R(c) to be

(22)

with r projecting pairs onto their first component.

Proposition 13. Let $\mathbb{C}$ be a small category and let $\mathcal{S}$ be a cartesian closed category. For a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ , the glueing category $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ is cartesian closed and the forgetful functor $\pi : {\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle} \rightarrow \mathcal{S} : (P,p,A)\mapsto A$ preserves the cartesian closed structure strictly.

Remark. The category of $\mathbb{C}$ -Kripke relations $\underline{K}\boldsymbol{\sigma}$ is a full subcategory of the glueing category $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle{\boldsymbol{\sigma}}\rangle$ via the mapping . On the other hand, every glued object (P,f,A) has an associated Kripke relation given by the extension of the map f (as shown in the diagram below, where $\mathrm{im}(f)$ denotes the image of f)

and the mapping $\mathrm{im}: (P,f,A) \mapsto (\mathrm{im}(f),A)$ exhibits $\underline{K}\boldsymbol{\sigma}$ as a reflective subcategory of $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ . For $\mathcal{S}$ cartesian closed, as can be readily seen from the explicit descriptions of finite products in $\underline{K}\boldsymbol{\sigma}$ and $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ , the reflection $\mathrm{im}: \underline{K}\boldsymbol{\sigma} \to \textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ preserves the cartesian structure and, therefore, $\underline{K}\boldsymbol{\sigma}$ is an exponential ideal of $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ (as can also be readily seen from the descriptions of exponentials in $\underline{K}\boldsymbol{\sigma}$ and $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ ). Thus, for (P,p,A) and (Q,q,A) in $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ , there are inclusions

\begin{equation*} \mathrm{im}( \ (P,p,A)\Rightarrow\!(Q,q,B) \ )(c) \ \subseteq \ ( \ \mathrm{im}(P,p,A) \!\supset \mathrm{im}(Q,q,B) \ )(c) \qquad(\,c\in\mid{\mathbb{C}}\mid\,)\end{equation*}

where

\begin{equation*}\begin{array}{l} \mathrm{im}( \ (P,p,A)\Rightarrow\!(Q,q,B) \ )(c) \\[2.5mm] \quad = \left\{\begin{array}{l|l} f: \boldsymbol{\sigma}(c)\to A\Rightarrow B & \begin{array}{l} \exists\, \varphi : \textbf{y}(c)\times P\to Q.\ \forall\, \rho: c'\to c.\ \forall\, a\in P(c').\ \\[1mm] \quad q_{c'}(\varphi_{c'}(\rho,a)) = \varepsilon \circ \langle{ f\circ \boldsymbol{\sigma}(\rho) , p_{c'}(a) }\rangle \end{array} \end{array}\right\} \end{array}\end{equation*}

and

\begin{equation*}\begin{array}{l} ( \ \mathrm{im}(P,p,A) \!\supset \mathrm{im}(Q,q,B) \ ) (c) \\[2.5mm] \quad = \left\{\begin{array}{l|l} f: \boldsymbol{\sigma}(c)\to A\Rightarrow B & \begin{array}{l} \forall\, \rho: c'\to c.\ \forall\, a\in P(c').\ \exists\, b\in Q(c').\ \\[1mm] \quad q_{c'}(b) = \varepsilon \circ \langle{ f\circ \boldsymbol{\sigma}(\rho) , p_{c'}(a) }\rangle \end{array} \end{array}\right\}\ .\end{array}\end{equation*}

These inclusions may be strict; as it happens, for instance, when $\mathbb{C}^\mathrm{op}=\mathbb{F}{}$ (the category of untyped contexts and renamings), $\boldsymbol{\sigma}$ is the unique functor to the trivial cartesian closed category, $Q=\textbf{y}(1)$ (for a singleton context 1), $P=\mathrm{im}(Q\to\langle\boldsymbol{\sigma}\rangle(1))$ , and $c=0$ (the empty context). Indeed, in this situation, $(P\Rightarrow\!\!Q)(c)\cong\textbf{Set}^{\mathbb{F}{}}(P,Q)=\emptyset$ whilst $(\mathrm{im}(p)\supset\mathrm{im}(q))(c)=(P\supset P)(c)=\{\mathrm{id}\}$ . Thus, in general, the reflection $\mathrm{im}: \underline{K}\boldsymbol{\sigma} \to \textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ does not preserve exponentials.

Now, note that (16) induces the embedding

extending both the Yoneda embedding and the functor $\boldsymbol{\sigma}:\mathbb{C}\rightarrow\mathcal{S}$

and satisfying the following extended form of the Yoneda Lemma (which we will use in § Normalisation function below).

Lemma 14 (Extended Yoneda Lemma). For a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ where $\mathbb{C}$ is a small category, the natural transformation

where $[{\_,=}]$ denotes the hom-functor of the glueing category $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ , is an isomorphism making the following diagram

commute.

Proof. Follows from the fact that, for $\varphi: \textbf{y}(\Gamma) \rightarrow P$ in $\textbf{Set}^{\mathbb{C}^\mathrm{op}}$ and $f: \boldsymbol{\sigma}(\Gamma) \rightarrow A$ in $\mathcal{S}$ , the diagram

commutes if and only if $f = p_\Gamma(\varphi_\Gamma(\mathrm{id}_\Gamma))$ .

Proposition 15. For a functor $\boldsymbol{\sigma}: \mathbb{C} \rightarrow \mathcal{S}$ where $\mathbb{C}$ is small, $\mathbb{C}$ and $\boldsymbol{\sigma}$ are cartesian, and $\mathcal{S}$ is cartesian closed, we have that preserves products and that the exponential $(P,p,A)^{\overline{\textbf{y}}(\Gamma)}$ in $\textbf{Set}^{\mathbb{C}^\mathrm{op}}\!\downarrow\!\langle\boldsymbol{\sigma}\rangle$ can be described as $(P^{\textbf{y}(\Gamma)},p',\boldsymbol{\sigma}(\Gamma)\texttt{=}\!\!\texttt{>} A)$ where p’ is the composite

Proof. The first part follows from the commutativity of for all $\Gamma,\Delta\in\mid\mathbb{C}\mid$ .

For the second part, since the exponential $(P,p,A)^{\overline{\textbf{y}}(\Gamma)}$ is given by pulling back the map $p^{\textbf{y}(\Gamma)}: P^{\textbf{y}(\Gamma)} \rightarrow (\langle\boldsymbol{\sigma}\rangle A)^{\textbf{y}(\Gamma)}$ along the composite

(recall (21)), where f is the exponential transpose of

it will be enough to show that the composite

is the identity. This is indeed the case as follows from the commutativity of the diagram below

where

(23) \begin{equation} e_P\, : \,P(\_\times\Gamma)\times\textbf{y}(\Gamma) \rightarrow P(\_)\, : \,(x,\rho) \mapsto (P\langle{\mathrm{id},\rho}\rangle)(x)\end{equation}

denotes the counit of the adjunction $\_ \times \textbf{y}(\Gamma) \dashv \textbf{Set}^{(\_\times\Gamma)^\mathrm{op}}: \textbf{Set}^{\mathbb{C}^\mathrm{op}} \rightarrow \textbf{Set}^{\mathbb{C}^\mathrm{op}}$ .

Glueing syntax and semantics. Let $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ be an interpretation of base types in a cartesian closed category. The embedding restricted to types $\tau\in\widetilde{\mathrm{T}}$ yields the glued object

glueing the syntax and semantics of variables. In the same spirit, glueing the syntax and semantics of neutral and normal terms (see (19)), we obtain the glued objects

in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

Having constructed the -algebra structure on $(\mathscr{C},\mathscr{C})$ by lifting the semantic operations in $\mathcal{S}$ (recall (17) and (18)), the homomorphism property of the semantic interpretation $(m,n):(\mathscr{M},\mathscr{N}) \rightarrow (\mathscr{C},\mathscr{C})$ (see Appendix B) entails the two propositions below, which show how the algebraic operations on the initial $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra $(\mathscr{M},\mathscr{N})$ and on the semantic $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra $(\mathscr{C},\mathscr{C})$ can be glued to yield operations in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ on the pair of families of glued objects $( \{ \mu_{\tau}\}_{\tau\in\widetilde{\mathrm{T}}}\ ,\ \{ \eta_{\tau}\}_{\tau\in\widetilde{\mathrm{T}}} )$ .

Proposition 16. Let $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ be an interpretation of base types in a cartesian closed category

1. 1. For $\tau, \tau' \in \widetilde{\mathrm{T}}$ , the pair of maps

   
   constitute a map $\nu_{\tau} \rightarrow \mu_{\tau}$ in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

2. 2. For $\tau, \tau' \in \widetilde{\mathrm{T}}$ , the pair of maps

   
   constitute a map $\mu_{\tau*\tau'} \rightarrow \mu_{\tau}$ in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

3. 3. For $\tau, \tau' \in \widetilde{\mathrm{T}}$ , the pair of maps

   
   constitute a map $\mu_{\tau'*\tau} \rightarrow \mu_{\tau}$ in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

4. 4. For $\tau, \tau' \in \widetilde{\mathrm{T}}$ , the pair of maps

   
   constitute a map $\mu_{\tau'\texttt{=}\!\!\texttt{>}\tau} \times \eta_{\tau'} \rightarrow \mu_{\tau}$ in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

Proof. Items 1, 2, 3, and 4, respectively, follow from (B1), (B2), (B3), and (B4) in Appendix B.

Proposition 17. Let $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ be an interpretation of base types in a cartesian closed category.

1. 1. For a base type $\theta \in \mathrm{T}$ , the pair of isomorphisms

   
   constitute an isomorphism in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

2. 2. The pair of isomorphisms

   
   constitute an isomorphism in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

3. 3. For $\tau, \tau' \in \widetilde{\mathrm{T}}$ , the pair of isomorphisms

   
   constitute an isomorphism in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

4. 4. For $\tau, \tau' \in \widetilde{\mathrm{T}}$ , the pair of isomorphisms

   
   constitute an isomorphism in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ .

Proof. Items 1, 2, 3, and 4, respectively, follow from (B1–B8), (B9), (B10), and (B11) (relying on Proposition 15) in Appendix B.

Note that the above operations on glued objects are given by pairs of syntactic operations together with their associated semantic meaning in the case of neutral terms (Proposition 16) and together with the identity in the case of normal terms (Proposition 17).

Normalisation by evaluation. Let $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ be an interpretation of base types in a cartesian closed category. Consider the interpretation

(24)

By Proposition 13, the semantics of terms induced by $\overline{\textbf{s}}$ in $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle$ extends the semantics induced by $\textbf{s}$ in $\mathcal{S}$ ; that is, the denotation $\overline{\textbf{s}}[\![{\Gamma\vdash t:\tau}]\!]$ is a pair of the form

\begin{equation*}(\ \textbf{s}'[\![{\Gamma\vdash t:\tau}]\!] \ , \ \textbf{s}[\![{\Gamma\vdash t:\tau}]\!])\end{equation*}

such that, letting

the diagram

commutes for all $\Gamma=\langle{x_i:\tau_i}\rangle_{i=1,n}$ .

We now aim at defining maps such that

(25)

commutes; so that, for all terms $\Gamma\vdash t:\tau(\Gamma=\langle{x_i:\tau_i}\rangle_{i=1,n}$ ), the diagram below

will commute (diagram (3) of the Basic Lemma (Lemma 6)) and, hence, the evaluation of the horizontal top composite at the tuple $\langle{\textsf{var}_{\tau_i}(x_i)}\rangle_{i=1,n}$ of the variables in the context $\Gamma$ will yield a normal term in $\mathscr{N}_{\tau}(\Gamma)$ with the same semantics as the given term t (compare the Extensional Normalisation Lemma (Lemma 9) and see Corollary 20 below). Moreover, as we will show below (see Corollary 19), the long $\beta\eta$ -normal forms associated to two $\beta\eta$ -equal terms will be the same.

The abstract way to define the maps in (25) – which in the literature on normalisation by evaluation are either referred to as unquote and quote or as reflect and reify – is by defining maps

that project in $\mathcal{S}$ onto identities (see Proposition 18 below). The definition of these maps is by induction on the structure of types relying on Propositions 16 and 17 as follows:

1. 1. For a base type $\theta \in \mathrm{T}$ , we define $\text{u}_{\theta} = \mathrm{id}_{\mu_\theta}$ and .

2. 2. We let $\text{u}_{\texttt{1}} = (\mu_\texttt{1} \rightarrow 1)$ and .

3. 3. For types $\tau,\tau'\in\widetilde{\mathrm{T}}$ , we define

   
   as the pairing of the maps and let be the composite
   

4. 4. For types $\tau,\tau'\in\widetilde{\mathrm{T}}$ , we define

   
   as the exponential transpose of the map
   
   and let be the composite
   
   where $\mathrm{v}_\tau=(\textsf{var}_\tau,\mathrm{id}):\nu_{\tau}\rightarrow\mu_{\tau}$ .

Proposition 18 below yields (25) as a corollary.

Proposition 18. For every type $\tau\in\widetilde{\mathrm{T}}$ , we have the identities

\begin{equation*}\pi(\text{u}_{\tau}) \ = \ \mathrm{id}_{\textbf{s}[\![{\tau}]\!]} \ = \ \pi(\mathrm{q}_{\tau})\end{equation*}

for $\pi$ the forgetful functor $\textbf{Set}^{\mathbb{F}\downarrow\tilde{T}}\downarrow\langle\textbf{s}[\![{\_}]\!]\rangle \rightarrow \mathcal{S}$ .

Proof. The proof is by induction on the structure of types.

1. (1) For a base type $\theta \in \mathrm{T}$ , by definition of $\text{u}_{\theta}$ and $\mathrm{q}_{\theta}$ .

2. (2) $\pi(\text{u}_{\texttt{1}}) = \pi(\mathrm{q}_{\texttt{1}}) = \mathrm{id}_{1}$ by definition of $\text{u}_{\texttt{1}}$ and $\mathrm{q}_{\texttt{1}}$ .

3. (3) For types $\tau,\tau'\in\widetilde{\mathrm{T}}$ ,

   
   and
   

4. (4) For types $\tau,\tau'\in\widetilde{\mathrm{T}}$ ,

   
   and hence
   
   further
   
   

Normalisation function. Every interpretation $\textbf{s}: \mathrm{T} \rightarrow \mathcal{S}$ of base types in a cartesian closed category, induces a normalisation function $\textbf{s}-\textsf{nf}_{\tau}: \mathscr{L}_{\tau} \rightarrow \mathscr{N}_{\tau}$ in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ defined as the composite

where $\overline{\ell}$ denotes the semantics of terms induced by the interpretation of (24) and where

for

Explicitly

,

for all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ .

Having the same denotation, $\beta\eta$ -equal terms are identified by the normalisation function.

Corollary 19. Let $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ be an interpretation of base types in a cartesian closed category. For every pair of terms t,t’ in $\mathscr{L}_{\tau}(\Gamma)$ , if $t ={}_{\beta\eta} t'$ then $\textbf{s}-\textsf{nf}_{\tau,\Gamma}\textbf{s}(t) = \textbf{s}-\textsf{nf}_{\tau,\Gamma}\textbf{s}(t')$ in $\mathscr{N}_{\tau}(\Gamma)$ . Further, as a consequence of Proposition 18 (see also (25)), we have that a term and its associated normal form have the same semantics.

Corollary 20. For every interpretation $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ of base types in a cartesian closed category, the diagram

commutes for all types $\tau\in\widetilde{\mathrm{T}}$ .

Considering the universal interpretation $\textbf{f}: \mathrm{T} \rightarrow \mathcal{F}_{\mathrm{ccc}}[\mathrm{T}]$ of the set of base types T into the free cartesian closed category $\mathcal{F}_{\mathrm{ccc}}[\mathrm{T}]$ over them, by Corollary, we have that

(26) \begin{equation} t ={}_{\beta\eta} \textbf{f}-\textsf{nf}_{\tau,\Gamma}\textbf{f}(t)\end{equation}

and hence, by Corollary 19, that

\begin{equation*}\textbf{s}-\textsf{nf}_{\tau,\Gamma}(t)=\textbf{s}-\textsf{nf}_{\tau,\Gamma}(\textbf{f}-\textsf{nf}_{\tau,\Gamma}(t))\end{equation*}

for all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ . Thus, the normalisation function $\textbf{f}-\textsf{nf}_{\tau}$ is idempotent and therefore fixes some normal terms. In fact, as we will see below (see (29) in Theorem 21), all normalisation functions $\textbf{s}-\textsf{nf}_{\tau}$ fix all normal terms: that is,

(27) \begin{equation}\mbox{for all $N \in \mathscr{N}_{\tau}(\Gamma)$, $\textbf{s}-\textsf{nf}_{\tau,\Gamma}(N) = N$.}\end{equation}

This fixed-point property is important: from it and Corollary 19 it follows that

• for all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ and normal terms $N\in\mathscr{N}_{\tau}(\Gamma)$ , if $t ={}_{\beta\eta} N$ then $\textbf{s}-\textsf{nf}_{\tau,\Gamma}(t) = N$ , and

• for every pair of normal terms $N,N' \in \mathscr{N}_{\tau}(\Gamma)$ , if $N ={}_{\beta\eta} N'$ then $N = N'$ ;

so that, further using Corollary 20 in the form (26), we have that

• for all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ , $\textbf{s}-\textsf{nf}_{\tau,\Gamma}(t) = \textbf{f}-\textsf{nf}_{\tau,\Gamma}(t)$ .

Thus, the fixed-point property (27) allows one to conclude that: all interpretations induce the same normalisation function $\mathsf{nf}_\tau: \mathscr{L}_{\tau} \rightarrow \mathscr{N}_{\tau}$ such that, for every term $t\in\mathscr{L}_{\tau}(\Gamma)$ , one has that $\mathsf{nf}_{\tau,\Gamma}(t)\in\mathscr{N}_{\tau}(\Gamma)$ is the unique normal term $\beta\eta$ -equal to t.

We now establish (27). The appropriate induction hypothesis to proceed by induction on the structure of neutral and normal terms is stated in the theorem below.

Theorem 21. For every interpretation $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ of base types in a cartesian closed category, the diagrams

(28)

and

(29)

commute for all types $\tau \in \widetilde{\mathrm{T}}$ .

Proof. The proof uses the induction principle associated to the initial $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra $(\mathscr{M},\mathscr{N})$ (see (15)) by considering the equalisers

of (28) and (29), respectively, and showing that the family

is a sub $\langle{\Sigma_1,\Sigma_2}\rangle$ -algebra, from which it follows that $\iota_{\tau}$ and $\jmath_{\tau}$ are isomorphisms and hence that (28) and (29) commute. The details are spelled out in Appendix 7.

Remark. In elementary terms, the above categorical proof amounts to establishing the identities

and

for $M\in\mathscr{M}_\tau(\Gamma)$ and $N\in\mathscr{N}_{\tau}(\Gamma)$ , by simultaneous induction on the derivation of neutral and normal terms (Reynolds 1998).

The commutativity of diagram (29) amounts to property (27) and hence, as explained above, all normalisation functions coincide.

Corollary 22. For every interpretation $\textbf{s}:\mathrm{T}\rightarrow\mathcal{S}$ of base types in a cartesian closed category and for the universal interpretation $\textbf{f}: \mathrm{T} \rightarrow \mathcal{F}_{\mathrm{ccc}}[\mathrm{T}]$ of base types into the free cartesian closed category over them, the identity

holds.

Summarising, we have obtained normalisation functions

\begin{equation*}\mathsf{nf}_{\tau,\Gamma}: \mathscr{L}_{\tau}(\Gamma) \rightarrow \mathscr{N}_{\tau}(\Gamma)\quad(\tau\in\widetilde{\mathrm{T}}, \Gamma\in\mid{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}\mid)\end{equation*}

satisfying the correctness properties below.

• For all context renamings $\rho: \Gamma \rightarrow \Gamma'$ in $\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}$ ,

  \begin{equation*}(\mathsf{nf}_{\tau,\Gamma}\ t)[\rho] = \mathsf{nf}_{\tau,\Gamma'}(t[\rho])\end{equation*}
  for every term $t \in \mathscr{L}_{\tau}(\Gamma)$ .

• For all normal terms $N\in\mathscr{N}_{\tau}(\Gamma)$ ,

  \begin{equation*}\mathsf{nf}_{\tau,\Gamma}(N) = N.\end{equation*}

• For all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ ,

  \begin{equation*}\mathsf{nf}_{\tau,\Gamma}(t)={}_{\beta\eta} t.\end{equation*}

• For all terms $t,t'\in\mathscr{L}_{\tau}(\Gamma)$ ,

  \begin{equation*}\mathrm{if} t={}_{\beta\eta} t' \mathrm{then}\mathsf{nf}_{\tau,\Gamma}(t) = \mathsf{nf}_{\tau,\Gamma}(t').\end{equation*}

Normalisation algorithm. The simplest description of the normalisation function from which to extract an algorithm is the one induced by the trivial interpretation $\textbf{t}$ of base types in the trivial cartesian closed category as, in this case, the glueing category $\textbf{Set}^{\mathbb{F}{} \!\downarrow\!\widetilde{\mathrm{T}}}\!\downarrow\!\langle{\textbf{t}[\![{\_}]\!]}\rangle$ is simply (isomorphic to) the presheaf category $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ (recall Example 12). In fact, previous categorical analysis of normalisation by evaluation have centred around this interpretation (Altenkirch et al. 1995; Reynolds 1998).

Explicitly, the unquote and quote maps

(30)

in $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ , with respect to the interpretation of base types $\textbf{s}: \theta \mapsto \mathscr{M}_\theta$ , are (in the internal language of $\textbf{Set}^{\mathbb{F}{}\!\downarrow\!\widetilde{\mathrm{T}}}$ ) as follows:

and the normalisation function is given by

(31) \begin{equation} \mathsf{nf}_s{\tau,\Gamma}(t)=\mathrm{q}_{\tau} ( \textbf{s}[\![{\Gamma\vdash t:\tau}]\!]\, \langle{\text{u}_{\tau_i}(\textsf{var}_{\tau_i}\,x_i)}\rangle_{i=1,n} )\end{equation}

for all terms $t\in\mathscr{L}_{\tau}(\Gamma)$ where $\Gamma=\langle{x_i:\tau_i}\rangle_{i=1,n}$ .

These functions can be directly implemented, for instance, in metalanguages supporting abstract syntax with variable binding, like HOAS (Pfenning and Elliot 1988), Fresh O’Caml (Fresh O’Caml www.cl.cam.ac.uk/ amp12/fresh-ocaml/), the Scope-and-Type Safe Universe of Syntaxes with Binding (Allais et al. 2021), and the SOAS Framework (Fiore and Szamozvancev 2022). Indeed, for concreteness, we here synthesise an elementary implementation in Agda considered as a dependently typed functional programming language. ¹

Syntax. We consider simple types over a countably infinite set of base types (see (1)):

Typing contexts (Definition 4) are inductively generated by context extension from an empty context:

We then have a family of variable indices (recall (9)) given as follows:

for which context renamings (Definition 4) are considered:

The abstract syntax of simply typed terms (see (11)) is implemented by the inductive family below:

Analogously, the abstract syntax of neutral and normal terms (see (12) and (14)) is implemented by the following mutually inductive families:

Their presheaf actions (recall (7) and (8)) will be needed:

Note the treatment of abstraction guaranteeing fresh bindings.

Semantics. We implement the presheaf semantics of types induced by the interpretation of base types as neutral terms (see (24)). Note that for higher types, the implementation glosses over the naturality condition required of presheaf exponentials (see (22)).

The semantic interpretation of terms (see (20)) follows:

Normalisation by evaluation. The unquote and quote functions (see (30)) are implemented:

Remark. A technical point to note is that the implementation of arises from the functorial action of presheaf exponentiation (in particular with respect to the evaluation map (23)), which in this case instatiates to the equivalent expression .

Finally, the normalisation function (see (31)) is

4. Conclusion

We have given a new categorical view of normalisation by evaluation for typed lambda calculus, both for extensional and intensional normalisation problems.

Extensional normalisation was obtained from a basic lemma unifying definability and normalisation. Our analysis has the important methodological consequence of providing guidance when looking for normal forms. Indeed, a basic lemma based on the definability result of Fiore and Simpson (1999) via Grothendiek logical relations led to syntactic counterparts of the normal forms of Altenkirch et al. (2001) and has been applied to establish extensional normalisation for the typed lambda calculus with empty and sum types (Balat et al. 2004). Along this line of research, one can study normalisation for other calculi for which definability results based on Kripke relations have been obtained – as classical linear logic (Streicher 2000), for instance.

The approach to normalisation by evaluation presented in the paper is novel, chiefly, in the following respects.

• The refinement from the extensional setting to the intensional one leading to the formalisation of normalisation by evaluation via categorical glueing.

• The use of an algebraic framework to structure both the development and proofs culminating in the definition of the normalisation function within a simply typed metatheory.

• The synthesis of a normalisation-by-evaluation program in a dependently typed functional programming language.

The obtained abstract normalisation algorithm synthesises various concrete implementations. Its specialisation to particular implementations of abstract syntax directly yields normalisation programs for concrete syntactic representations. In particular, we have provided a normalisation-by-evaluation program for the type-and-scope safe, intrinsically typed encoding of typed lambda terms (Allais et al. 2021; Altenkirch and Reus 1999; Benton et al. 2012). How the abstract setting is related to representations of binding based on generating globally unique identifiers, say as in Filinski (2001), needs to be investigated.

The role of categorical glueing in our analysis is reminiscent of realisability. It would be interesting to understand whether there are connections to the modified realisability approach of Berger (1993).