--- abstract: 'We give a formal treatment of simple type theories, such as the simply-typed $\lambda$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $\lambda$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $\beta$- and $\eta$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.' bibliography: - 'fscd21.bib' title: Abstract clones for abstract syntax --- Introduction ============ The abstract concept of type theory is crucial in the study of programming languages. However, while it is generally appreciated that the concrete syntax associated to a type theory is peripheral to its fundamental structure, conventional techniques for working with type theories and proving properties thereof are predominantly syntactic. The primary reason for this incongruity is that, though abstract frameworks for defining and reasoning about general classes of type theories have been developed (e.g. @fiore2010algebraic [@fiore2010second; @arkor2020algebraic; @fiore2013multiversal; @hirschowitz2010modules; @ahrens2016modules; @ahrens2019modular; @hirschowitz2020modules], there called *second-order abstract syntax*), the mathematical prerequisites are significant and often appear unapproachable to those without a firm category theoretic background. This is regrettable, because these general techniques alleviate much of the rote associated to syntactic proofs, such as those for adequacy, normalization, and the admissibility of substitution. It so happens that there exists in the mathematical folklore an approach that is particularly well-suited to capturing the essential structure of simple type theories and yet requires essentially no experience with category theory to employ fruitfully: this is the formalism of *abstract clones* (often simply called *clones*) with algebraic structure. The structure of an abstract clone captures the notion of a context-indexed family of terms, closed under variable projection and substitution; equipping clones with algebraic structure permits the expression of variable-binding operators, like the $\lambda$-abstraction operator familiar from $\lambda$-calculi. It is known amongst cognoscenti that abstract clones might be employed for this purpose: for instance, Fiore, Plotkin, and Turi @fiore1999abstract proved that abstract clones are equivalent to their notion of *substitution monoids*, which represent families of (unityped) terms with an associated capture-avoiding substitution operation; later, Fiore and Mahmoud @mahmoud2011second [@fiore2014functorial] proved that abstract clones with algebraic structure are equivalent to the *$\Sigma$-monoids* of Fiore et al., which extend substitution monoids with second-order (<span>i.e.</span> variable binding) algebraic structure. In a separate line of inquiry, Hyland @hyland2012classical uses abstract clones with algebraic structure to give a modern treatment of the unityped $\lambda$-calculus. However, it does not appear that abstract clones have previously been expressly proposed for the study of simple type theories (in fact, the definition of a typed abstract clone with algebraic structure is absent from the literature). Here, we give an exposition of the use of abstract clones with algebraic structure in defining simple type theories and proving various of their properties. After setting up the relevant definitions (\[sec:clones\]), we describe how simple type theories can be modelled by algebras of second-order presentations (\[sec:second-order\]). We then show that free algebras exist, giving an abstract description of the syntax of the type theory (\[sec:free-algebras\]). We derive an induction principle @lehmann1981algebraic that enables abstract reasoning about the syntax (\[sec:induction\]), and show that this is powerful enough to prove non-trivial properties of type theories, in particular using logical relations (\[sec:logical-relations\]). We also compare the clone-theoretic framework to other approaches (\[comparison\]). Though we do not expect our treatment to be surprising to experts familiar with prior categorical developments, it is an important perspective in the understanding of simple type theories and deserves explication. Though we occasionally make reference to category theory throughout the paper, knowledge of category theory is not necessary to understand the content. Abstract clones and first-order presentations {#sec:clones} ============================================= A typed (or *multisorted*) *abstract clone* @taylor1993abstract, henceforth simply *clone*, encapsulates the structure of terms in simple contexts, closed under variables and substitution. Informally, for each context $x_1 : {A}_1, \ldots, x_n : {A}_n$ and type $B$, where ${A}_1$ to ${A}_n$ are types (or *sorts*), a clone ${{\mathbf{X}}}$ specifies a set of terms $X({A}_1, \ldots, {A}_n; B)$, each element of which is considered a term of type $B$ in the context $x_1 : {A}_1, \ldots, x_n : {A}_n$. It also specifies terms $\var_i$ representing the projection of the variable $x_i$ from the context, and functions ${\mathsf{subst}_{\Gamma; A_n, \dots, A_n; B}} : X({A}_1, \dots, {A}_n; B) \times X(\Gamma; {A}_1) \times \cdots \times X(\Gamma; {A}_n) \to X(\Gamma; B)$ representing simultaneous substitution: $$\begin{aligned} t \in X({A}_1, \ldots, {A}_n; B) \quad &\textit{represents} \quad x_1 : {A}_1, \ldots, x_n : {A}_n \vdash t : B \\ \var[{A}_1, \ldots, {A}_n]_i \in X({A}_1, \ldots, {A}_n; {A}_i) \quad &\textit{represents} \quad x_1 : {A}_1, \ldots, x_n : {A}_n \vdash x_i : {A}_i \\ {\mathsf{subst}_{\Gamma; A_1, \dots, A_n; B}}(t, u_1, \ldots, u_n) \quad &\textit{represents} \quad \Gamma \vdash {t \{x_1 \mapsto u_1, \ldots, x_n \mapsto u_n\}} : B\end{aligned}$$ The clone ${{\mathbf{X}}}$ is required to satisfy laws expressing that (1) substituting variables for themselves does nothing; (2) applying a substitution to a variable results in the term corresponding to that variable in the substitution; and (3) substitution is associative. We fix a set $S$ of types (sorts). We denote by $S^*$ the free monoid on $S$, <span>i.e.</span> lists of elements of $S$. Conceptually, contexts $x_1 : {A}_1, \ldots, x_n : {A}_n$ are given by elements $[{A}_1, \ldots, {A}_n] \in S^*$, since variable names carry no information. We write ${\diamond}\in S^*$ for the empty context, and $\Gamma, \Xi$ for the concatenation of $\Gamma \in S^*$ and $\Xi \in S^*$. For contexts $\Gamma, \Delta \in S^*$, where $\Delta = [{A}_1, \ldots, {A}_n]$, we define $X(\Gamma; \Delta) = \prod_{i\leq n} X(\Gamma; {A}_i)$. We call the elements ${\boldsymbol\sigma}\in X(\Gamma; \Delta)$ *substitutions*; a substitution is therefore a tuple $\boldsymbol{\sigma} = (\sigma_1, \ldots, \sigma_n)$ of terms $\sigma_i \in X(\Gamma; {A}_i)$. \[def:clone\] An *$S$-sorted clone* ${{\mathbf{X}}}= (X, \var, {\mathsf{subst}_{}})$ consists of - for each context $\Gamma \in S^*$ and sort ${A}\in S$, a set $X(\Gamma; {A})$ of *terms*; - for each context $\Gamma \in S^*$, a tuple $\var[\Gamma] \in X(\Gamma; \Gamma)$ of *variables*; - for each pair of contexts $\Gamma, \Delta \in S^*$ and sort ${A}\in S$, a *substitution function* $\textstyle {\mathsf{subst}_{\Gamma; \Delta; {A}}} : X (\Delta; {A}) \times X (\Gamma; \Delta) \to X (\Gamma; {A}) $, which we write as ${t [\boldsymbol\sigma]} = {\mathsf{subst}_{\Gamma; \Delta; {A}}}(t,\boldsymbol\sigma)$; such that $$\begin{aligned} {\var[{A}_1, \dots, A_n]_i [\boldsymbol\sigma]} &= \sigma_i &&\text{for each $\boldsymbol\sigma \in X(\Gamma; A_1, \dots, A_n)$ and $i \leq n$} \\ {t [\var[\Gamma]]} &= t &&\text{for each $t \in X (\Gamma; {A})$} \\ {t [{\sigma'_1 [\boldsymbol\sigma]},\dots,{\sigma'_m [\boldsymbol\sigma]}]} &= {({t [\boldsymbol\sigma']}) [\boldsymbol\sigma]} &&\text{for each $t \in X (\Xi; {A})$, $\boldsymbol\sigma' \in X (\Delta;\Xi)$, $\boldsymbol\sigma \in X (\Gamma; \Delta)$} \end{aligned}$$ A *clone homomorphism* $f : {{\mathbf{X}}}\to {{\mathbf{X}}}'$ consists of a function $f_{\Gamma; {B}} : X (\Gamma; {B}) \to X'(\Gamma; {B})$ for each context $\Gamma \in S^*$ and sort ${B}\in S$, such that the following hold, where $\Delta = [{A}_1, \ldots, {A}_n] \in S^*$: $$\begin{aligned} f_{\Delta; {A}_i} (\var[\Delta]_i) &= {\var[\Delta]_i}' &&\text{for each $i \leq n$} \\ f_{\Gamma; {B}} ({t [\boldsymbol\sigma]}) &= {(f_{\Delta; {B}}(t)) [f_{\Gamma; {A}_1}(\sigma_1), \dots, f_{\Gamma; {A}_n}(\sigma_n)]}\mathrlap{'} &&\text{for each $t \in X (\Delta; {B})$, $\boldsymbol\sigma \in X (\Gamma; \Delta)\!$} \end{aligned}$$ We write ${{\mathbf{Clone}}(S)}$ for the category of $S$-sorted clones and homomorphisms. We extend every clone homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{X}}}'$ to act on substitutions as follows, where $\Delta = [{A}_1, \ldots, {A}_n] \in S^*$: $$\begin{aligned} f_{\Gamma; \Delta} & : X(\Gamma; \Delta) \to X'(\Gamma; \Delta) & f_{\Gamma; \Delta}&(\boldsymbol\sigma) = (f_{\Gamma; {A}_1}(\sigma_1), \dots, f_{\Gamma; {A}_n}(\sigma_n))\end{aligned}$$ We denote by ${{\mathbf{Var}}_{S}}$ the $S$-sorted *clone of variables*, whose family of terms is given by ${\mathsf{Var}_{S}} ({A}_1, \ldots, {A}_n; {B}) = \{i \mid {A}_i = {B}\}$; whose variables are given by $\var[\Gamma]_i = i$; and whose substitution is given by $i[\boldsymbol\sigma] = \sigma_i$. ${{\mathbf{Var}}_{S}}$ is the initial object in ${{\mathbf{Clone}}(S)}$: for any $S$-sorted clone ${{\mathbf{X}}}$, there is a unique homomorphism ${\triangleright}: {{\mathbf{Var}}_{S}} \to {{\mathbf{X}}}$ given by ${\triangleright}_{\Gamma; {B}}(i) = \var[\Gamma]_i$. \[eg-monoid\] The terms of any universal algebra @birkhoff1935structure form a *monosorted* clone (<span>i.e.</span> an $S$-sorted clone for which $S$ is a singleton $\{ * \}$). The sets of terms, along with the variables and substitution function, exactly match the classical notions. For instance, monoids form a clone $\mathbf{Mon}$, where $\mathrm{Mon}(\underbrace{*, \ldots, *}_n; *)$ is the free monoid on $n$ elements. \[example:stlcclone\] Let ${\mathsf{Ty}}$ be the set of sorts freely generated by a base type ${{\mathsf{b}}}\in {\mathsf{Ty}}$ and function types $(A {\Rightarrow}B) \in {\mathsf{Ty}}$ for $A, B \in {\mathsf{Ty}}$ (precisely, ${\mathsf{Ty}}$ is the free magma on $\{ {{\mathsf{b}}}\}$). The terms of the simply typed $\lambda$-calculus (STLC) form a ${\mathsf{Ty}}$-sorted clone ${{\mathbf{{\Lambda}}}}$. Consider terms generated by the following rules: $$\begin{prooftree}[center=false] \infer0{\Gamma, x : A, \Delta \vdash x : A} \end{prooftree} \qquad \begin{prooftree}[center=false] \hypo{\Gamma \vdash f : A {\Rightarrow}B} \hypo{\Gamma \vdash a : A} \infer2{\Gamma \vdash {{\mathsf{app}}}\,f\,a : B} \end{prooftree} \qquad \begin{prooftree}[center=false] \hypo{\Gamma, x : A \vdash t : B} \infer1{\Gamma \vdash \lambda x : A.\,t : A {\Rightarrow}B} \end{prooftree}$$ (We write ${{\mathsf{app}}}$ to distinguish application of $\lambda$-terms from application of mathematical functions. We also use named variables for readability, identifying $\alpha$-equivalent terms.) Capture-avoiding simultaneous substitution ${t \{x_i \mapsto u_i\}}_i$ of terms is defined in the usual way by recursion on $t$: $$\begin{gathered} {x_j \{x_i \mapsto u_i\}}_i = u_j \qquad {({{\mathsf{app}}}\,f\,a) \{x_i \mapsto u_i\}}_i = {{\mathsf{app}}}\,({f \{x_i \mapsto u_i\}}_i) \,({a \{x_i \mapsto u_i\}}_i) \\ {(\lambda x : A.\,t) \{x_i \mapsto u_i\}}_i = \lambda y : A.\,({t \{x_1\mapsto u_1, \dots, x_n\mapsto u_n, x\mapsto y\}}) \end{gathered}$$ The clone ${{\mathbf{{\Lambda}}}}$ has sets of terms $ {\Lambda}(A_1, \dots, A_n; B) = \{ x_1 : A_1, \dots, x_n : A_n \vdash t : B \} $, variables $\var[\Gamma]_i = x_i$, and substitution ${t [\boldsymbol\sigma]} = {t \{x_i \mapsto \sigma_i\}}_i$. There is a related ${\mathsf{Ty}}$-sorted clone ${{\mathbf{{\Lambda_{\beta\eta}}}}}$ of STLC terms up to $\beta\eta$-equality, defined by quotienting the sets of terms associated to ${{\mathbf{{\Lambda}}}}$ by the equivalence relation ${\approx}_{\beta\eta}$, where $\Gamma \vdash t {\approx}_{\beta\eta} t' : A$ is the congruence relation generated by the following rules: $$\begin{prooftree} \hypo{\Gamma, x : A \vdash t : B} \hypo{\Gamma \vdash u : A} \infer2[$(\beta)$]{\Gamma \vdash {{\mathsf{app}}}\,(\lambda x : A.\,t)\,u {\approx}_{\beta\eta} {t \{x \mapsto u\}} : B} \end{prooftree} \qquad \begin{prooftree} \hypo{\Gamma \vdash t : A {\Rightarrow}B} \infer1[$(\eta)$]{\Gamma \vdash t {\approx}_{\beta\eta} \lambda x : A.\,{{\mathsf{app}}}\,t\,x : A{\Rightarrow}B} \end{prooftree}$$ \[remark-simple-type-theories\] We shall only consider abstract clones with *sets* of types. However, as illustrated by the previous example, the types in a simple type theory often have algebraic structure themselves. By considering only the underlying set of types, the algebraic structure is forgotten. This simplifies the development, at the cost of some loss of expressivity. By specifying a (monosorted) clone of types, rather than a set, one recovers exactly the *simple type theories* of Arkor and Fiore @arkor2020algebraic. ${{\mathbf{Clone}}(S)}$ is a cartesian category, permitting us to combine clones pointwise. The terminal object ${\mathbf{1}}$ is the unique clone in which every set of terms is a singleton. The binary product ${{\mathbf{X}}}_1 \times {{\mathbf{X}}}_2$ has sets of terms given by products of sets $ (X_1 \times X_2)(\Gamma; {A}) = X_1(\Gamma; {A}) \times X_2(\Gamma; {A}) $, variables $\var[\Gamma]_i = (\var[\Gamma]_i, \var[\Gamma]_i)$, and substitution $ (t_1, t_2)[(\sigma_{11}, \sigma_{21}), \dots, (\sigma_{1n}, \sigma_{2n})] = (t_1[\boldsymbol\sigma_1] ,t_2[\boldsymbol\sigma_2]) $. \[clones-form-a-variety\] $S$-sorted abstract clones form a *variety* in the sense of universal algebra; this means that ${{\mathbf{Clone}}(S)}$ is the category of models for a (multisorted) algebraic theory. Such categories are well-behaved, and several of the properties we mention throughout the paper (such as being cartesian) follow abstractly from this observation. We often choose to be more explicit for ease of comprehension, but make note where this abstract perspective is helpful. Substitution and context extension {#subst-and-renaming} ---------------------------------- We briefly consider the structure of substitutions $\boldsymbol\sigma$ in $S$-sorted clones ${{\mathbf{X}}}$, in particular to define various substitutions that we use below, and to characterize context extension in clones. If $\boldsymbol\sigma \in X(\Gamma; \Delta)$ and $\boldsymbol\sigma' \in X(\Delta; \Xi)$ are substitutions, then their *composition* $(\boldsymbol\sigma' \boldsymbol{\circ}\boldsymbol\sigma) \in X(\Gamma; \Xi)$ is the substitution $(\sigma'_1[\boldsymbol\sigma], \dots, \sigma'_m[\boldsymbol\sigma])$, where $m$ is the length of $\Xi$. The three equations in the definition of a clone () equivalently state (1 & 2) that $\var$ is the (left- and right-) unit for composition ($ \var[\Delta] {\circ}\boldsymbol\sigma ~=~\boldsymbol\sigma ~=~\boldsymbol\sigma {\circ}\var[\Gamma] $); and (3) that composition is associative ($ \boldsymbol\sigma'' {\circ}(\boldsymbol\sigma' {\circ}\boldsymbol\sigma) ~=~(\boldsymbol\sigma'' {\circ}\boldsymbol\sigma') {\circ}\boldsymbol\sigma $). In fact, this perspective underlies the connection between abstract clones and cartesian multicategories (which may be considered categories whose morphisms have multiple inputs, corresponding to each of the variables in a context): we elaborate on this connection in . We call the substitutions ${\boldsymbol\rho}\in {\mathsf{Var}_{S}}(\Gamma; \Delta)$ *variable renamings*. This is justified by observing that ${\boldsymbol\rho}$ selects a variable in the context $\Delta$ for each variable in $\Gamma$. If $t \in X(\Delta; {A})$ is a term in some clone ${{\mathbf{X}}}$, then ${t [{\triangleright}{\boldsymbol\rho}]} \in X(\Gamma; {A})$ corresponds to the term in which the variables in $t$ have been renamed according to ${\boldsymbol\rho}$. A special case of renaming is *weakening* $ \wk[\Gamma]_{\Xi} = (1, \dots, n) \in {\mathsf{Var}_{S}}(\Gamma, \Xi; \Gamma) $. Using weakening and composition, we may define the *lifting* of a substitution $\boldsymbol\sigma \in X(\Gamma; \Delta)$ to a larger context: $${\mathsf{lift}_{\Xi}} (\boldsymbol\sigma) ~=~(\boldsymbol\sigma {\circ}({\triangleright}\wk[\Gamma]_{\Xi}) , {\triangleright}(n+1, \dots, n+m)) ~\in~X(\Gamma, \Xi; \Delta, \Xi)$$ where $n$ is the length of $\Gamma$ and $m$ is the length of $\Xi$. Context extension induces the following operation on clones. Given an $S$-sorted clone ${{\mathbf{X}}}$ and context $\Xi \in S^*$, we let ${{\Uparrow^{\Xi}}} {{\mathbf{X}}}$ be the $S$-sorted clone with terms $({{\Uparrow^{\Xi}}} X)(\Gamma; {A}) = X(\Gamma, \Xi; {A})$, variables $(\var[\Gamma, \Xi]_{i})_{i \le n} \in X(\Gamma, \Xi; \Gamma)$, and substitution $ {t [{\boldsymbol\sigma},{\triangleright}(n+1, \dots, n+m)]} \in X(\Gamma, \Xi; {A}) $ for $t \in X(\Delta, \Xi; {A})$ and ${\boldsymbol\sigma}\in X(\Gamma, \Xi; \Delta)$, where $n$ is the length of $\Gamma$ and $m$ is the length of $\Xi$. This satisfies a universal property as follows. Weakening forms a homomorphism $\weaken[\Xi]_{{{\mathbf{X}}}} : {{\mathbf{X}}}\to {{\Uparrow^{\Xi}}} {{\mathbf{X}}}$ that sends $t \in X(\Gamma; {A})$ to ${t [{\triangleright}\wk[\Gamma]_{\Xi}]} \in X(\Gamma, \Xi; {A})$. Then, for every homomorphism $g : {{\Uparrow^{\Xi}}} {{\mathbf{X}}}\to {{\mathbf{Y}}}$, we obtain a homomorphism $g {\circ}\weaken[\Xi]_{{{\mathbf{X}}}} : {{\mathbf{X}}}\to {{\mathbf{Y}}}$ and a substitution $g_{{\diamond}; \Xi} (\var[\Xi]) \in Y({\diamond}; \Xi)$. Together, these uniquely determine $g$: to give a homomorphism $g$ is just to give a homomorphism ${{\mathbf{X}}}\to {{\mathbf{Y}}}$ and a closed term $\sigma_i$ for each extra variable from $\Xi$. (From the perspective of algebraic theories, context extension ${{\Uparrow^{\Xi}}} {{\mathbf{X}}}$ corresponds to the construction of the *polynomial* @lambek1988higher or *simple slice category* @jacobs1999categorical over $\Xi$.) \[context-extension-up\] For each clone homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{Y}}}$ and substitution $\boldsymbol\sigma \in Y({\diamond}; \Xi)$, there is a unique homomorphism $g : {{\Uparrow^{\Xi}}} {{\mathbf{X}}}\to {{\mathbf{Y}}}$ such that $g {\circ}\weaken[\Xi]_{{{\mathbf{X}}}} = f$ and $g_{{\diamond}; \Xi} (\var[\Xi]) = \boldsymbol\sigma$. Suppose $g$ is such a homomorphism. Then, for each $t \in X(\Gamma, \Xi; A)$, we have $ g_{\Gamma; A}(t) = {(g_{\Gamma, \Xi; A}(\weaken[\Xi]_{{{\mathbf{X}}}}(t))) [\var[\Gamma], (g_{{\diamond}; \Xi}(\var[\Xi])) {\circ}{\triangleright}\wk[{\diamond}]_\Gamma]} = {(f_{\Gamma, \Xi; A}(t)) [\var[\Gamma], {\boldsymbol\sigma}{\circ}{\triangleright}\wk[{\diamond}]_{\Gamma}]} $, where the first equality uses preservation of variables and substitution by $g$, and the second uses the assumptions on $g$. Hence, $g$ is unique when it exists. For existence, define $ g_{\Gamma; A}(t) = {(f_{\Gamma, \Xi; A}(t)) [\var[\Gamma], {\boldsymbol\sigma}{\circ}{\triangleright}\wk[{\diamond}]_{\Gamma}]} $. Substitutions $\boldsymbol\sigma \in Y({\diamond}; \Xi)$ are in natural bijection with homomorphisms ${{\Uparrow^{\Xi}}}{{\mathsf{Var}_{S}}} \to {{\mathbf{Y}}}$, and so equivalently states that ${{\Uparrow^{\Xi}}} {{\mathbf{X}}}$ is the coproduct of ${{\mathbf{X}}}$ and ${{\Uparrow^{\Xi}}}{{\mathsf{Var}_{S}}}$. (This contrasts with presheaf-based frameworks @fiore1999abstract [@hofmann1999semantical], in which context extension is exponentiation.) First-order presentations ------------------------- Clones describe collections of terms closed under variable projection and substitution. We will frequently be interested in clones equipped with extra structure, so as, for example, to interpret the operations of a given type theory. *Presentations* permit the axiomatization of clones that interpret various operations, subject to sets of axioms; while the *algebras* for a given presentation are exactly those clones that satisfy the axiomatization. Later, we will see how clones may be freely generated from presentations, allowing one to define a clone simply by specifying its generating operators and axioms. Our treatment of first-order presentations is the classical notion of presentation for multisorted universal algebra @birkhoff1970heterogeneous [@goguen1985completeness]. An *$S$-sorted first-order signature* $\Sigma$ consists of a set $\Sigma(\Gamma; {B})$ for each $(\Gamma; {B}) \in S^* \times S$. We call the elements ${\mathsf{o}} \in \Sigma (\Gamma; {B})$ the *$(\Gamma; {B})$-ary operators*. *Terms over $\Sigma$* are generated by the following rules: $$\begin{prooftree}[center=false] \infer0{\Gamma, x : {A}, \Delta \vdash x : {A}} \end{prooftree} \qquad \begin{prooftree}[center=false] \hypo{\Gamma \vdash t_1 : {A}_1} \hypo{\cdots} \hypo{\Gamma \vdash t_n : {A}_n} \infer3[\ \textnormal{(${\mathsf{o}} \in \Sigma ({A}_1, \dots, {A}_n; {B})$)}]{\Gamma \vdash {{\mathsf{o}}}(t_1, \dots, t_n) : {B}} \end{prooftree}$$ An *$({A}_1, \dots, {A}_n; {B})$-ary term* $t$ over $\Sigma$ is a term $x_1 : {A}_1, \dots, x_n : {A}_n \vdash t : {B}$, and an *$(\Gamma; {B})$-ary equation* over $\Sigma$ is a pair $(t, u)$ of $(\Gamma; {B})$-ary terms. An *$S$-sorted first-order presentation* ${{\mathbf{\Sigma}}}= (\Sigma, E)$ consists of an $S$-sorted first-order signature $\Sigma$ and, for each $(\Gamma; {B}) \in S^* \times S$, a set $E (\Gamma; {B})$ of $(\Gamma; {B})$-ary equations. Observe that the operators of a signature correspond to terms in the logic specified below (namely, first-order equational logic). In particular, a $(\Gamma; {B})$-ary operator ${\mathsf{o}}$, where $\Gamma = [{A}_1, \ldots, {A}_n] \in S^*$, may be thought of either as a function ${\mathsf{o}} : {A}_1, \ldots, {A}_n \to {B}$, or as a term $x_1 : {A}_1, \ldots, x_n : {A}_n \vdash {\mathsf{o}} : B$. These perspectives are complementary, and mirror the practice in categorical logic of representing terms by morphisms. \[def:first-order-logic\] If $\Gamma \vdash u_i : {A}_i$ for $i \leq n$ and $x_1 : {A}_1, \dots x_n : {A}_n \vdash t : {B}$ are terms over an $S$-sorted first-order signature $\Sigma$, their substitution $\Gamma \vdash {t \{x_1 \mapsto u_1, \ldots, x_n \mapsto u_n\}} : {B}$ is defined by recursion on $t$ in the usual way. The *equational logic* over an $S$-sorted first-order presentation ${{\mathbf{\Sigma}}}= (\Sigma, E)$ consists of the following rules for the congruence of ${\approx}$ under operations and substitution, together with reflexivity, symmetry and transitivity of ${\approx}$: $$\begin{gathered} \begin{prooftree}[center=false] \hypo{\Gamma \vdash t_1\,{{\approx}}\,u_1\,{:}\,{A}_1} \hypo{\cdots} \hypo{\Gamma \vdash t_n\,{{\approx}}\,u_n\,{:}\,{A}_n} \infer3[\ \textnormal{(${\mathsf{o}} \in \Sigma ({A}_1, \dots, {A}_n; {B})$)}]{\Gamma \vdash {\mathsf{o}}(t_1, \dots, t_n) {\approx}{\mathsf{o}}(u_1, \dots, u_n) : {B}} \end{prooftree} \\[2ex] \begin{prooftree}[center=false] \hypo{\Gamma \vdash t'_1 {\approx}u_1' : {A}_1} \hypo{\cdots} \hypo{\Gamma \vdash t'_n {\approx}u_n' : {A}_n} \infer3 [\ \textnormal{($(t, u) \in E ({A}_1, \dots, {A}_n; {B})$)}] {\Gamma \vdash {t \{x_i \mapsto t'_i\}}_i {\approx}{u \{x_i \mapsto u'_i\}}_i : {B}} \end{prooftree} \end{gathered}$$ The terms over $\Sigma$ form a clone ${{\mathbf{Term}}^{{{\mathbf{\Sigma}}}}} = ({\mathsf{Term}^{{{\mathbf{\Sigma}}}}}, \var, {\mathsf{subst}_{}})$, where ${\mathsf{Term}^{{{\mathbf{\Sigma}}}}} (\Gamma; {A})$ is the set of ${\approx}$-equivalence classes of $(\Gamma; {A})$-ary terms; the variables are $\var[\Gamma]_i = x_i$; and substitution is ${t [\boldsymbol\sigma]} = {t \{x_i \mapsto \sigma_i\}}_i$. A clone ${{\mathbf{X}}}$ is *presented by* ${{\mathbf{\Sigma}}}$ when ${{\mathbf{Term}}^{{{\mathbf{\Sigma}}}}}$ is isomorphic to ${{\mathbf{X}}}$ in ${{\mathbf{Clone}}(S)}$ (that is, when there are homomorphisms ${{\mathbf{Term}}^{{{\mathbf{\Sigma}}}}} \rightleftarrows {{\mathbf{X}}}$ that are mutually inverse). A clone may have many different presentations: for instance, the clone $\mathbf{Mon}$ of monoids () may be presented by a unit and a binary multiplication operation, or by an $n$-ary multiplication operation for each $n \in \mathbb N$ (subject to suitable axioms). \[example:global-state\] Fix a finite set $V = \{v_1, \dots, v_k\}$ of *values*. The ${\mathsf{Ty}}$-sorted presentation ${{{\mathbf{\Sigma}}}^{{\mathbf{GS}}}_{V}}$ of *global $V$-valued state* has a $\smash{(\underbrace{{{\mathsf{b}}},\dots,{{\mathsf{b}}}}_k; {{\mathsf{b}}})}$-ary operator ${\mathsf{get}}$, a $({{\mathsf{b}}}; {{\mathsf{b}}})$-ary operator ${\mathsf{put}}_{v_i}$ for each $i \leq k$, and equations $$\begin{aligned} x : {{\mathsf{b}}}\vdash {\mathsf{get}} ({\mathsf{put}}_{v_1}(x), \dots, {\mathsf{put}}_{v_k}(x)) &{\approx}x : {{\mathsf{b}}}&& \\ x_1 : {{\mathsf{b}}}, \dots, x_k : {{\mathsf{b}}}\vdash {\mathsf{put}}_{v_i} ({\mathsf{get}}(x_1, \dots, x_k)) &{\approx}{\mathsf{put}}_{v_i}(x_i) : {{\mathsf{b}}}&&\text{for each $i \leq k$} \\ x : {{\mathsf{b}}}\vdash {\mathsf{put}}_{v_i} ({\mathsf{put}}_{v_j}(x)) &{\approx}{\mathsf{put}}_{v_j}(x) : {{\mathsf{b}}}&&\text{for each $i, j \leq k$} \end{aligned}$$ Informally, the term ${\mathsf{get}}(t_1, \dots, t_n)$ gets the current value $v_i$ of the state and then continues as $t_i$, while the term ${\mathsf{put}}_{v_i}(t)$ sets the state to $v_i$ and then continues as $t$. (In \[example:stlc-initial\] below, we combine this presentation with the STLC to obtain a call-by-name calculus with global state. In call-by-name calculi, effects occur at base types, so it is only necessary to axiomatize ${\mathsf{get}}$ and ${\mathsf{put}}_{v_i}$ operators for ${{\mathsf{b}}}\in {\mathsf{Ty}}$, rather than for all types.) We denote by ${{\mathbf{GS}}_{V}}$ the clone ${{\mathbf{Term}}^{{{{\mathbf{\Sigma}}}^{{\mathbf{GS}}}_{V}}}}$ arising from the presentation ${{{\mathbf{\Sigma}}}^{{\mathbf{GS}}}_{V}}$. Second-order presentations {#sec:second-order} ========================== Just as first-order presentations describe algebraic structure, second-order presentations describe binding algebraic structure @fiore1999abstract. Variable-binding operators are prevalent in type theory: for instance, the $\lambda$-abstraction operator of the STLC, ${\mathsf{let}}\text{-}{\mathsf{in}}$ expressions in functional programming languages, and case-splitting in calculi with sum types. Second-order presentations are similar to first-order presentations, except that each operator must describe its binding structure, <span>i.e.</span> how many variables (and of what types) it binds in each operand. Hence, while first-order arities have the form $({A}_1, \dots, {A}_n; {B}) \in S^*\times S$, second-order arities have the form $ ((\Delta_1; {A}_1), \dots, (\Delta_n; {A}_n); {B}) \in (S^* \times S)^* \times S $. Operators of such an arity take $n$ arguments of types ${A}_1, \dots {A}_n$ and produce terms of type ${B}$: the length of the context $\Delta_i \in S^*$ is the number of variables bound by the $i$^th^ argument; and the argument types are given by the list $\Delta_i$. First-order operators may be expressed as second-order operators that bind no variables. An *$S$-sorted second-order signature* @fiore1999abstract [@fiore2010second] consists of a set $\Sigma(\Psi; {B})$ for each $(\Psi;{B}) \in (S^*\times S)^* \times S$. We call the elements ${\mathsf{o}} \in \Sigma (\Psi; {B})$ the *$(\Psi; {B})$-ary operators*. The ${\mathsf{Ty}}$-sorted second-order signature ${\Sigma^{{\Lambda}}}$ of the STLC consists of an $(({\diamond}; A {{\Rightarrow}} B), ({\diamond};A); B)$-ary operator ${\mathsf{app}}$ and an $((A; B); (A {{\Rightarrow}} B))$-ary operator ${\mathsf{abs}}$ for each $A, B \in {\mathsf{Ty}}$. Thus each application operator ${\mathsf{app}}$ has two arguments, neither of which bind variables; and each $\lambda$-abstraction operator ${\mathsf{abs}}$ has one argument, which binds one variable. Just as the axioms of first-order presentations are expressed in first-order equational logic, the axioms of second-order presentations are expressed in the second-order equational logic of Fiore and Hur @fiore2010second. Second-order equational logic extends the first-order setting with *metavariables* @aczel1978general [@hamana2004free; @fiore2008second], which conceptually stand for parameterized placeholders for terms. Each variable $x : {A}$ in first-order logic has an associated type ${A}\in S$; correspondingly, each metavariable ${\textsl{\textsc{m}}}: ({A}_1, \ldots, {A}_n; {A})$ has an associated context and type (called *second-order arities* in @arkor2020algebraic). ${\textsl{\textsc{m}}}$ may be thought of as a variable parameterized by $n$ terms of types ${A}_1$ through ${A}_n$; a nullary ($n = 0$) metavariable behaves like an ordinary variable. There are several alternative ways to describe second-order equational logic @arkor2020higher, but we follow Fiore and Hur @fiore2010second in associating to each term both a variable context and a metavariable context: a metavariable context $\Psi$ is a list of context–sort pairs $(\Delta; {A}) \in S^* \times S$. The judgment $\Psi~|~\Delta \vdash t : {A}$ expresses that the term $t$ has sort ${A}$ in variable context $\Delta$ and metavariable context $\Psi$. Below, we write $\vec x$ for a list $x_1, \dots, x_n$ of variables, $\vec x.\,t$ to indicate binding of the variables $\vec x$ in $t$, and write $\vec x : \Delta$ as an abbreviation of $x_1 : {A}_1, \dots, x_n : {A}_n$ for $\Delta = [{A}_1, \dots, {A}_n]$. Suppose $S$ is a set and $\Sigma$ is an $S$-sorted second-order signature. *Terms over $\Sigma$* are generated by the following rules for variables, metavariables, and operators: $$\begin{gathered} \begin{prooftree} \infer0{\Psi~|~\Gamma, x : {A}, \Delta \vdash x : {A}} \end{prooftree} \\ \begin{prooftree} \hypo{\Psi, {\textsl{\textsc{m}}}: ({A}_1, \dots, {A}_n; {B}), \Phi~|~\Gamma \vdash t_1 : A_1} \hypo{\mspace{-12mu}\cdots\mspace{-12mu}} \hypo{\Psi, {\textsl{\textsc{m}}}: ({A}_1, \dots, {A}_n; {B}), \Phi~|~\Gamma \vdash t_n : A_n} \infer3{\Psi, {\textsl{\textsc{m}}}: ({A}_1, \dots, {A}_n; {B}), \Phi~|~\Gamma \vdash {\textsl{\textsc{m}}}(t_1, \dots, t_n) : {B}} \end{prooftree} \\ \begin{prooftree} \hypo{\Psi~|~\Gamma, \vec x_1 : \Delta_1 \vdash t_1 : {A}_1} \hypo{\mspace{-16mu}\cdots\mspace{-16mu}} \hypo{\Psi~|~\Gamma, \vec x_n : \Delta_n \vdash t_n : {A}_n} \infer3[\textnormal{(${\mathsf{o}}\in\Sigma((\Delta_1;{A}_1),\dots,(\Delta_n;{A}_n);{B})$)}] {\Psi~|~\Gamma \vdash {\mathsf{o}} ((\vec x_1.\,t_1) , \dots, (\vec x_n.\,t_n)) : {B}} \end{prooftree} \end{gathered}$$ A *$((\Delta_1; {A}_1), \dots, (\Delta_n; {A}_n); {B})$-ary term* over $\Sigma$ is a term ${\textsl{\textsc{m}}}_1 : (\Delta_1, {A}_1), \dots, {\textsl{\textsc{m}}}_n : (\Delta_n; {A}_n)~|~{\diamond}$ $\vdash t : {B}$, and a *$(\Psi; {B})$-ary equation* is a pair $(t, u)$ of $(\Psi; {B})$-ary terms. An *$S$-sorted second-order presentation* ${{\mathbf{\Sigma}}}= (\Sigma, E)$ consists of an $S$-sorted second-order signature $\Sigma$ and, for each $(\Psi; {B}) \in (S^* \times S)^* \times S$, a set $E (\Psi; {B})$ of $(\Psi; {B})$-ary equations over $\Sigma$. Multisorted second-order presentations may essentially be taken as a definition of *simple type theory* (modulo the subtlety regarding type operators described in ): just as the informal notion of *algebra* was formalized through the framework of universal algebra @birkhoff1935structure, so second-order presentations facilitate a precise, formal definition of simple type theory @arkor2020algebraic. \[example:stlcpres\] The operators of the signature ${\Sigma^{{\Lambda}}}$ of the STLC present the following rules: $$\begin{prooftree} \hypo{\Psi~|~\Gamma \vdash f : A {\Rightarrow}B} \hypo{\Psi~|~\Gamma \vdash a : A} \infer2{\Psi~|~\Gamma \vdash {\mathsf{app}}(f, a) : B} \end{prooftree} \qquad \begin{prooftree} \hypo{\Psi~|~\Gamma, x : A \vdash t : B} \infer1{\Psi~|~\Gamma \vdash {\mathsf{abs}}(x.\,t) : A {\Rightarrow}B} \end{prooftree}$$ We can then give, for each $A, B \in {\mathsf{Ty}}$, an $((A; B), ({\diamond}; A); B)$-ary equation for $\beta$-equality, and an $(({\diamond}; A{{\Rightarrow}}B); (A{{\Rightarrow}}B))$-ary equation for $\eta$-equality: $$\begin{array}{rr@{~}c@{~}ll@{\qquad\quad~}r} {\textsl{\textsc{m}}}_1 : (A; B), {\textsl{\textsc{m}}}_2 : ({\diamond}; A)~|~{\diamond}\vdash& {\mathsf{app}}({\mathsf{abs}}(x.\,{\textsl{\textsc{m}}}_1(x)), {\textsl{\textsc{m}}}_2()) &{\approx}& {\textsl{\textsc{m}}}_1({\textsl{\textsc{m}}}_2()) &: B &(\beta) \\ {\textsl{\textsc{m}}}: ({\diamond}; A {{\Rightarrow}} B)~|~{\diamond}\vdash& {\mathsf{abs}}(x.\,{\mathsf{app}}({\textsl{\textsc{m}}}(), x)) &{\approx}& {\textsl{\textsc{m}}}() &: A {\Rightarrow}B &(\eta) \end{array}$$ The signature ${\Sigma^{{\Lambda}}}$ together with these equations forms the ${\mathsf{Ty}}$-sorted second-order presentation ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$ of the STLC with $\beta\eta$-equality. Note that second-order equations permit the expression of *axiom schemata*, as axioms containing metavariables (in both the traditional and precise sense of the term "metavariable") @fiore2013multiversal [@arkor2020algebraic]. Without second-order equations, one would have to add $\beta$ and $\eta$ equations for each instantiation of the metavariables in the rules above. If $(\Psi~|~\Gamma \vdash u_i : {A}_i)_i$ and $\Psi~|~x_1 : {A}_1, \dots, x_n : {A}_n \vdash t : {B}$ are terms over an $S$-sorted second-order signature $\Sigma$, then their *substitution* $\Psi~|~\Gamma \vdash {t \{x_i \mapsto u_i\}}_i : {B}$ is defined by recursion on $t$: $$\begin{gathered} {x_j \{x_i \mapsto u_i\}}_i = u_j \qquad {{\textsl{\textsc{m}}}(t_1, \dots t_m) \{x_i \mapsto u_i\}}_i = {\textsl{\textsc{m}}}({t_1 \{x_i \mapsto u_i\}}_i, \dots, {t_m \{x_i \mapsto u_i\}}_i) \\ {{\mathsf{o}}((\vec{y_1}.\,t_1), \dots, {\mathsf{o}}(\vec{y_k}.\,t_k)) \{x_i \mapsto u_i\}}_i = {\mathsf{o}}((\vec{y_1}.\,{t_1 \{x_i \mapsto u_i\}}_i), \dots, (\vec{y_k}.\,{t_k \{x_i \mapsto u_i\}}_i)) \end{gathered}$$ (On the right-hand side of the definition on operators, the terms $t_i$ are weakened, and we omit from the substitution variables that are mapped to themselves.) If instead we have terms $ (\Psi~|~\Gamma, \vec x_i : \Delta_i \vdash u_i : {A}_i)_i $ and $ {\textsl{\textsc{m}}}_1 : (\Delta_1; {A}_1), \dots, {\textsl{\textsc{m}}}_n : (\Delta_n; {A}_n)~|~\Gamma' \vdash t : {B}$ then their *metasubstitution* $ \Psi~|~\Gamma, \Gamma' \vdash {t \{{\textsl{\textsc{m}}}_i \mapsto (\vec {x_i}.\,u_i)\}}_i : {B}$ is defined using ordinary substitution by recursion on $t$: $$\begin{gathered} {x \{{\textsl{\textsc{m}}}_i \mapsto (\vec {x_i}.\,u_i)\}}_i = x \qquad {{\textsl{\textsc{m}}}_j(t_1, \dots, t_m) \{{\textsl{\textsc{m}}}_i {\mapsto} (\vec {x_i}.\,u_i)\}}_i = {u_j \{x_{jk} \mapsto {t_k \{{\textsl{\textsc{m}}}_i {\mapsto} (\vec {x_i}.\,u_i)\}}_i\}}_k \\ {{\mathsf{o}}((\vec{y_1}.\,t_1), \dots, (\vec{y_k}.\,t_k)) \{{\textsl{\textsc{m}}}_i \mapsto (\vec {x_i}.\,u_i)\}}_i \\\qquad = {\mathsf{o}}( (\vec{y_1}.\,{t_1 \{{\textsl{\textsc{m}}}_i \mapsto (\vec {x_i}.\,u_i)\}}_i), \dots, (\vec{y_k}.\,{t_k \{{\textsl{\textsc{m}}}_i \mapsto (\vec {x_i}.\,u_i)\}}_i)) \end{gathered}$$ Algebras -------- The algebras for a presentation are the abstract clones interpreting each of the operations of the signature, subject to the axioms of the presentation. In other words, a presentation is a specification of structure, while the algebras are the realizations, or models, of that structure. For instance, in the first-order setting, the algebras for the presentation of monoids form (set-theoretic) monoids. An *algebra* $({{\mathbf{X}}}, {\llbracket {-} \rrbracket})$ for an $S$-sorted second-order signature $\Sigma$ (called "presentation clones" in @mahmoud2011second) consists of an $S$-sorted clone ${{\mathbf{X}}}$ and, for each context $\Gamma$ and $((\Delta_1; {A}_1), \dots, (\Delta_n; {A}_n); {B})$-ary operator ${\mathsf{o}}$, a function $ {\llbracket {\mathsf{o}} \rrbracket}_\Gamma : \prod_i X (\Gamma, \Delta_i; {A}_i) \to X (\Gamma; {B}) $ such that, for all substitutions $\boldsymbol\sigma \in X (\Xi; \Gamma)$ and tuples of terms $(t_i \in X (\Gamma, \Delta_i; {A}_i))_i$, $${({\llbracket {\mathsf{o}} \rrbracket}_{\Gamma}(t_1, \dots, t_n)) [\boldsymbol\sigma]} = {\llbracket {\mathsf{o}} \rrbracket}_{\Xi}( {t_1 [{\mathsf{lift}_{\Delta_1}} \boldsymbol\sigma]} , \dots, {t_n [{\mathsf{lift}_{\Delta_n}} \boldsymbol\sigma]})$$ A *homomorphism* $f : ({{\mathbf{X}}}, {\llbracket {-} \rrbracket}) \to ({{\mathbf{X}}}', {\llbracket {-} \rrbracket}')$ of $\Sigma$-algebras is a homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{X}}}'$ of clones such that, for all ${\mathsf{o}} \in \Sigma((\Delta_1; {A}_1), \dots, (\Delta_n; {A}_n); {B})$ and $(t_i\in X(\Gamma,\Delta_i;{A}_i))_i$, $$\textstyle f_{\Gamma; {B}}({\llbracket {\mathsf{o}} \rrbracket}_{\Gamma} (t_1, \dots, t_n)) ~=~ {\llbracket {\mathsf{o}} \rrbracket}'_{\Gamma} (f_{\Gamma,\Delta_1; {A}_1} t_1, \dots, f_{\Gamma,\Delta_n; {A}_n} t_n)$$ The interpretation of operators in a $\Sigma$-algebra $({{\mathbf{X}}}, {\llbracket {-} \rrbracket})$ extends to an interpretation $ {\llbracket t \rrbracket}_{\Gamma} : \prod_i X (\Gamma, \Delta_i; {A}_i) \to X (\Gamma, \Xi ; {B}) $ of each term $ {\textsl{\textsc{m}}}_1 : (\Delta_1; {A}_1), \dots, {\textsl{\textsc{m}}}_n : (\Delta_n; {A}_n) ~|~\vec x : \Xi \vdash t : {B}$ as follows (where $n$ is the length of $\Gamma$): $$\begin{aligned} {\llbracket x_i \rrbracket}_{\Gamma}(\boldsymbol\sigma) &= \var[\Gamma, \Xi]_{n + i} \\ {\llbracket {\textsl{\textsc{m}}}_i(t_1, \dots, t_m) \rrbracket}_{\Gamma}(\boldsymbol\sigma) &= {\sigma_i [\var[\Gamma, \Xi]_1 ,\dots ,\var[\Gamma, \Xi]_n ,{\llbracket t_1 \rrbracket}_{\Gamma}(\boldsymbol\sigma) ,\dots ,{\llbracket t_m \rrbracket}_{\Gamma}(\boldsymbol\sigma)]} \\ {\llbracket {\mathsf{o}}((\vec x_1.\,t_1), \dots, (\vec x_m.\,t_m)) \rrbracket}_{\Gamma}(\boldsymbol\sigma) &= {\llbracket {\mathsf{o}} \rrbracket}_{\Gamma, \Xi} ({\llbracket t_1 \rrbracket}_{\Gamma}(\boldsymbol\sigma), \dots, {\llbracket t_m \rrbracket}_{\Gamma}(\boldsymbol\sigma))\end{aligned}$$ \[algebra-for-sop\] An algebra $({{\mathbf{X}}}, {\llbracket {-} \rrbracket})$ for a second-order presentation ${{\mathbf{\Sigma}}}= (\Sigma, E)$ is a $\Sigma$-algebra such that, for all equations $(t, u) \in E(\Psi; {A})$ and contexts $\Gamma$, we have ${\llbracket t \rrbracket}_{\Gamma} = {\llbracket u \rrbracket}_{\Gamma}$. We let ${{\mathbf{\Sigma}}}{\operatorname{{\mathbf{-Alg}}}}$ be the category of ${{\mathbf{\Sigma}}}$-algebras and all $\Sigma$-algebra homomorphisms between them. \[example:stlc-algebras\] An algebra for the presentation ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$ of the STLC with $\beta\eta$-equality consists of a ${\mathsf{Ty}}$-sorted clone ${{\mathbf{X}}}$ and functions $${\llbracket {\mathsf{app}} \rrbracket}_{\Gamma} : X(\Gamma; A {\Rightarrow}B) \times X(\Gamma; A) \to X(\Gamma; B) \qquad {\llbracket {\mathsf{abs}} \rrbracket}_{\Gamma} : X(\Gamma, A; B) \to X(\Gamma; A {\Rightarrow}B)$$ that commute with substitution and satisfy $$\begin{aligned} {\llbracket {\mathsf{app}} \rrbracket}_{\Gamma} ({\llbracket {\mathsf{abs}} \rrbracket}_{\Gamma} (t),\,t') &= {t [\var[\Gamma], t']} &&\text{for}~t \in X (\Gamma, A; B), t' \in X (\Gamma; A) \tag{$\beta$}\label{eq:algebra-beta} \\ {\llbracket {\mathsf{abs}} \rrbracket}_{\Gamma} ({\llbracket {\mathsf{app}} \rrbracket}_{\Gamma, A} ({t [{\triangleright}\wk[\Gamma]_{A}]}, \var[\Gamma, A]_{n + 1})) &= t &&\text{for}~t \in X (\Gamma; A{{\Rightarrow}}B) \tag{$\eta$} \end{aligned}$$ For each set $Z$ we have a set-theoretic interpretation of the STLC, which forms a ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra $({\mathcal M}_Z, {\mathcal M}_Z{\llbracket {-} \rrbracket})$ as follows. Define interpretations ${\mathcal M}_Z{\llbracket A \rrbracket} \in {{\mathbf{Set}}}$ of each sort $A \in {\mathsf{Ty}}$ recursively by setting ${\mathcal M}_Z{\llbracket {{\mathsf{b}}}\rrbracket} = Z$ and ${\mathcal M}_Z{\llbracket A {\Rightarrow}B \rrbracket} = {{\mathbf{Set}}}({\mathcal M}_Z{\llbracket A \rrbracket}, {\mathcal M}_Z{\llbracket B \rrbracket})$ (where ${{\mathbf{Set}}}(Y, Y')$ is the set of functions $Y \to Y'$). We then have a ${\mathsf{Ty}}$-sorted clone ${\mathcal M}_Z$, where the sets of terms are given by $ {\mathcal M}_Z(A_1, \ldots, A_n; B) = {{\mathbf{Set}}}(\prod_i {\mathcal M}_Z{\llbracket A_i \rrbracket},{\mathcal M}_Z{\llbracket B \rrbracket}) $, the variables by projections $\var[\Gamma]_i = \pi_i$, and substitution by $f[\boldsymbol\sigma] = (\xi \mapsto f (\sigma_1(\xi), \dots, \sigma_n(\xi)))$. This forms a ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra, with interpretations of the operators given by function application and currying. More generally, the interpretation of the STLC in any cartesian-closed category ${\mathbf{C}}$ with a specified object $Z \in {\mathbf{C}}$ forms a ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra taking $ {\mathcal M}_Z(A_1, \dots, A_n; B) = {\mathbf{C}}(\prod_i {\mathcal M}_Z{\llbracket A_i \rrbracket}, {\mathcal M}_Z{\llbracket B \rrbracket}) $ to be the sets of terms, where ${\mathcal M}_Z{\llbracket {{\mathsf{b}}}\rrbracket} = Z$ and ${\mathcal M}_Z{\llbracket A {\Rightarrow}B \rrbracket} = {{\mathcal M}_Z{\llbracket B \rrbracket}}^{{\mathcal M}_Z{\llbracket A \rrbracket}}$. The cartesian structure of ${{\mathbf{Clone}}(S)}$ lifts to ${{\mathbf{\Sigma}}}{\operatorname{{\mathbf{-Alg}}}}$ for every presentation ${{\mathbf{\Sigma}}}$: the clone ${\mathbf{1}}$ uniquely forms a ${{\mathbf{\Sigma}}}$-algebra, and the product $({{\mathbf{X}}}_1, {\llbracket {-} \rrbracket}_1) \times ({{\mathbf{X}}}_2, {\llbracket {-} \rrbracket}_2)$ is the clone ${{\mathbf{X}}}_1 \times {{\mathbf{X}}}_2$ equipped with interpretations $ {\llbracket {\mathsf{o}} \rrbracket}_{\Gamma}((\sigma_{11}, \sigma_{21}), \dots, (\sigma_{1n}, \sigma_{2n})) = ({\llbracket {\mathsf{o}} \rrbracket}_{1,\Gamma}(\boldsymbol\sigma_1) ,{\llbracket {\mathsf{o}} \rrbracket}_{2,\Gamma}(\boldsymbol\sigma_2)) $. Free algebras {#sec:free-algebras} ============= Second-order $S$-sorted presentations ${{\mathbf{\Sigma}}}$ can be viewed as descriptions of simple type theories for which $S$ is the set of types. In particular, the operators specify the term formers of the type theory (such as $\lambda$-abstraction, or application). From this perspective, the syntax of the type theory described by ${{\mathbf{\Sigma}}}$ is the *initial* ${{\mathbf{\Sigma}}}$-algebra: there is a unique $\Sigma$-algebra homomorphism from the algebra formed by the syntax to any other algebra, given by induction on terms. More generally, given the syntax of an existing theory in the form of a clone ${{\mathbf{X}}}$, the *free* ${{\mathbf{\Sigma}}}$-algebra on ${{\mathbf{X}}}$ is given by augmenting ${{\mathbf{X}}}$ by the operators and equations of ${{\mathbf{\Sigma}}}$; or, from another perspective, augmenting the type theory described by ${{\mathbf{\Sigma}}}$ with the operations specified by ${{\mathbf{X}}}$. For example, the free ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra on ${{\mathbf{GS}}_{V}}$ () may be seen as the STLC extended by additional term formers (${\mathsf{get}}$ and ${\mathsf{put}}_{v_1}, \dots, {\mathsf{put}}_{v_k}$) representing the side-effects of global state. \[def:free-algebra\] Suppose ${{\mathbf{\Sigma}}}= (\Sigma, E)$ is an $S$-sorted second-order presentation and ${{\mathbf{X}}}$ is an $S$-sorted clone. A ${{\mathbf{\Sigma}}}$-algebra $F_{{{\mathbf{\Sigma}}}}{{\mathbf{X}}}$ equipped with a clone homomorphism $\eta_{{{\mathbf{X}}}} : {{\mathbf{X}}}\to F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}$ is the *free ${{\mathbf{\Sigma}}}$-algebra* on ${{\mathbf{X}}}$ if, for any other ${{\mathbf{\Sigma}}}$-algebra $({{\mathbf{Y}}}, {\llbracket {-} \rrbracket})$ and clone homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{Y}}}$, there is a unique $\Sigma$-algebra homomorphism ${f^\dagger} : F_{{\mathbf{\Sigma}}}{{\mathbf{X}}}\to ({{\mathbf{Y}}}, {\llbracket {-} \rrbracket})$ such that ${f^\dagger} {\circ}\eta_{{{\mathbf{X}}}} = f$. The *initial ${{\mathbf{\Sigma}}}$-algebra* is the free ${{\mathbf{\Sigma}}}$-algebra on ${\mathsf{Var}_{S}}$. \[example:stlc-initial\] Recall the presentation ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$ of the STLC with $\beta\eta$-equality from \[example:stlcpres\]. The initial ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra is the clone ${{\mathbf{{\Lambda_{\beta\eta}}}}}$ of STLC terms up to ${\approx}_{\beta\eta}$ (\[example:stlcclone\]), with the operators ${\mathsf{app}}$ and ${\mathsf{abs}}$ interpreted as $$\begin{aligned} ((f, a) \mapsto {{\mathsf{app}}}\,f\,a) &: {\Lambda_{\beta\eta}}(\Gamma; A {\Rightarrow}B) \times {\Lambda_{\beta\eta}}(\Gamma; A) \to {\Lambda_{\beta\eta}}(\Gamma; B) \\ (t \mapsto \lambda x : A.\,t) &: {\Lambda_{\beta\eta}}(\Gamma, A; B) \to {\Lambda_{\beta\eta}}(\Gamma; A {\Rightarrow}B) \end{aligned}$$ The free ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra on the clone ${{\mathbf{GS}}_{V}}$ of global $V$-valued state (\[example:global-state\]) can be described as follows for $V = \{v_1, \dots, v_k\}$. The underlying ${\mathsf{Ty}}$-sorted clone is defined in the same way as ${{\mathbf{{\Lambda_{\beta\eta}}}}}$, but with the following additional term formers and equations (omitting the typing constraints on equations). $$\begin{array}{l} \begin{prooftree}[center=false] \hypo{\Gamma \vdash t_1 : {{\mathsf{b}}}} \hypo{\cdots} \hypo{\Gamma \vdash t_k : {{\mathsf{b}}}} \infer3{\Gamma \vdash {{\mathsf{get}}}(t_1, \dots, t_k) : {{\mathsf{b}}}} \end{prooftree} \\[1ex] \begin{prooftree}[center=false] \hypo{\Gamma \vdash t : {{\mathsf{b}}}} \infer1[\ \textnormal{($i \leq k$)}]{\Gamma \vdash {{\mathsf{put}}}_{v_i}(t) : {{\mathsf{b}}}} \end{prooftree} \end{array} \qquad \begin{array}{r@{~{\approx}_{\beta\eta}~}lr} {{\mathsf{get}}}({{\mathsf{put}}}_{v_1}(t), \dots, {{\mathsf{put}}}_{v_k}(t)) &t \\[0.5ex] {{\mathsf{put}}}_{v_i} ({{\mathsf{get}}}(t_1, \dots, t_k)) &{{\mathsf{put}}}_{v_i}(t_i) &(i \leq k) \\[0.5ex] {{\mathsf{put}}}_{v_i} ({{\mathsf{put}}}_{v_j}(t)) &{{\mathsf{put}}}_{v_j}(t) &(i,k \leq k) \end{array}$$ This forms a ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra in the same way as ${{\mathbf{{\Lambda_{\beta\eta}}}}}$ above. The morphism $\eta_{{{\mathbf{GS}}_{V}}}$ is given by $ \eta_{{{\mathbf{GS}}_{V}}} ({\mathsf{get}} (t_1, \dots, t_k)) = {\mathsf{get}} (\eta_{{{\mathbf{GS}}_{V}}}(t_1), \dots, \eta_{{{\mathbf{GS}}_{V}}}(t_k)) $ and $ \eta_{{{\mathbf{GS}}_{V}}} ({\mathsf{put}}_{v_i}(t)) = {\mathsf{put}}_{v_i} (\eta_{{{\mathbf{GS}}_{V}}}(t)) $. If ${{\mathbf{\Sigma}}}'$ is a first-order presentation, the free ${{\mathbf{\Sigma}}}$-algebra on ${{\mathbf{Term}}^{{{\mathbf{\Sigma}}}'}}$ is closed under the operators of ${{\mathbf{\Sigma}}}'$: each ${\mathsf{o}} \in {{\mathbf{\Sigma}}}'({A}_1, \dots, {A}_n; {B})$ induces a term $\eta({\mathsf{o}}(x_1,\dots, x_n)) \in F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}({A}_1, \dots, {A}_n; {B})$ and hence functions $ (\boldsymbol\sigma~\mapsto~{\eta({\mathsf{o}}(\vec x)) [\boldsymbol\sigma]}) \,:\, F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}(\Gamma; {A}_1, \dots, {A}_n) \to F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}(\Gamma; {B}) $. We show that free algebras for any signature, and on any clone, exist, by constructing them explicitly. Existence of these free algebras facilitates the developments in the next sections. However, note that we do not rely on the explicit description: after this section, we reason about free algebras solely using the universal property in . This is important, as we wish to reason about type theories independently of their syntax, which leads to greatly simplified proofs. (It is also possible to prove the existence of free algebras entirely abstractly using a monadicity theorem and , avoiding concrete syntax.) $$\begin{gathered} \SwapAboveDisplaySkip \begin{prooftree}[center=false] \infer0{\Gamma, x : {A}, \Delta \vdash_{{{\mathbf{X}}}} x : {A}} \end{prooftree} \qquad \begin{prooftree}[center=false] \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_1 : {A}_1} \hypo{\cdots} \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_n : {A}_n} \infer3[\ \textnormal{($f \in X({A}_1,\dots,{A}_n;{B})$)}] {\Gamma \vdash_{{{\mathbf{X}}}} {f}(t_1, \dots, t_n) : {B}} \end{prooftree} \\[1ex] \begin{prooftree}[center=false] \hypo{\Gamma, \vec x_1 : \Delta_1 \vdash_{{{\mathbf{X}}}} t_1 : {A}_1} \hypo{\mspace{-1mu}\cdots\mspace{-1mu}} \hypo{\Gamma, \vec x_n : \Delta_n \vdash_{{{\mathbf{X}}}} t_n : {A}_n} \infer3 [\ \textnormal{(${\mathsf{o}} \in \Sigma((\Delta_1; {A}_1), \dots, (\Delta_n; {A}_n); {B})$)}] {\Gamma \vdash_{{{\mathbf{X}}}} {\mathsf{o}}((\vec x_1.\,t_1), \dots, (\vec x_n.\,t_n)) : {B}} \end{prooftree} \end{gathered}$$ $$\begin{gathered} \begin{prooftree}[center=false] \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_1 {\approx}u_1 : {A}_1} \hypo{\cdots} \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_n {\approx}u_n : {A}_n} \infer3[\ \textnormal{($f \in X({A}_1, \dots, {A}_n; {B})$)}] {\Gamma \vdash_{{{\mathbf{X}}}} {f} (t_1, \dots, t_n) {\approx}{f} (u_1, \dots, u_n) : {B}} \end{prooftree} \\ \begin{prooftree}[center=false] \hypo{\Gamma, \vec x_1 : \Delta_1 \vdash_{{{\mathbf{X}}}} t_1 {\approx}u_1 : {A}_1} \hypo{\mspace{-1mu}\cdots\mspace{-1mu}} \hypo{\Gamma, \vec x_n : \Delta_n \vdash_{{{\mathbf{X}}}} t_n {\approx}u_n : {A}_n} \infer3 [\textnormal{(${\mathsf{o}} \in \Sigma ((\Delta_1;{A}_1), \dots; {B})$)}] {\Gamma \vdash_{{{\mathbf{X}}}} {\mathsf{o}}((\vec x_1.\,t_1), \dots, (\vec x_n.\,t_n)) {\approx}{\mathsf{o}}((\vec x_1.\,u_1), \dots, (\vec x_n.\,u_n)) : {B}} \end{prooftree} \\[2ex] \begin{prooftree}[center=false] \hypo{\Gamma, \vec x_1{:}\Delta_1 \vdash_{{{\mathbf{X}}}} t_1 {\approx}u_1:{A}_1} \hypo{\mspace{-12mu}\cdots\mspace{-12mu}} \hypo{\Gamma, \vec x_n{:}\Delta_n \vdash_{{{\mathbf{X}}}} t_n {\approx}u_n:{A}_n} \infer3 [\textnormal{($(t',u') \in E((\Delta_1;{A}_1), \dots; {B})$)}] {\Gamma \vdash_{{{\mathbf{X}}}} {t' \{{\textsl{\textsc{m}}}_i \mapsto (\vec x_i.\,t_i)\}}_i {\approx}{u' \{{\textsl{\textsc{m}}}_i \mapsto (\vec x_i.\,u_i)\}}_i : {B}} \end{prooftree} \\[2ex] \begin{prooftree}[center=false] \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_1 : {A}_1} \hypo{\cdots} \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_n : {A}_n} \infer3[\textnormal{($i \leq n$)}]{\Gamma \vdash_{{{\mathbf{X}}}} {t_i {\approx}\var[{A}_1,\dots,{A}_n]_i}(t_1,\dots,t_n) : {B}} \end{prooftree} \\ \begin{prooftree}[center=false] \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_1 : {A}_1} \hypo{\cdots} \hypo{\Gamma \vdash_{{{\mathbf{X}}}} t_n : {A}_n} \infer3 {\Gamma \vdash_{{{\mathbf{X}}}} {f} ({\sigma_1}(t_1, \dots, t_n) , \dots , {\sigma_{k}}(t_1, \dots, t_n)) {\approx}({{f [\boldsymbol\sigma]}})(t_1, \dots, t_n) : {B}} \end{prooftree} \tag{$f \in X({A}'_1, \dots, {A}'_k; {B}), \boldsymbol\sigma \in X({A}_1, \dots, {A}_n; {A}_1', \dots, {A}'_k)$} \end{gathered}$$ In universal algebra, free algebras of first-order presentations are constructed in two steps: by first closing a sort-indexed set $X$ of constants under the operators of the presentation; and then quotienting the terms by the equations of the presentation. gives the analogous construction in the second-order setting. First, we construct terms $\Gamma \vdash_{{{\mathbf{X}}}} t : {B}$ from variables, the terms of the clone $f \in X({A}_1, \dots, {A}_n; {B})$ (viewed as function symbols), and the operators of the presentation ${{\mathbf{\Sigma}}}$. Second, we quotient by the equivalence relation ${\approx}$ generated by congruence, the equations of ${{\mathbf{\Sigma}}}$ (using metasubstitution), and rules imposing compatibility with the clone structure of ${{\mathbf{X}}}$. The clone $F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}$ has terms $ F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}(\Gamma; {B}) = \{\Gamma \vdash_{{{\mathbf{X}}}} t : {B}\}/{\approx}$, with variables and substitution defined in the evident way; the homomorphism $\eta_{{{\mathbf{X}}}} : {{\mathbf{X}}}\to F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}$ sends $t \in X(\Gamma; {B})$ to $x_1 : A_1, \ldots, x_n : A_n \vdash_{{{\mathbf{X}}}} t(x_1, \dots, x_n) : {B}$, where $\Gamma = [{A}_1, \ldots, {A}_n]$. For every $S$-sorted second-order presentation ${{\mathbf{\Sigma}}}$ and $S$-sorted clone ${{\mathbf{X}}}$, the free ${{\mathbf{\Sigma}}}$-algebra $F_{{\mathbf{\Sigma}}}{{\mathbf{X}}}$ exists. The forgetful functor ${{\mathbf{\Sigma}}}{\operatorname{{\mathbf{-Alg}}}}\to {{\mathbf{Clone}}(S)}$ therefore has a left adjoint (in fact, it is monadic). Induction over second-order syntax {#sec:induction} ================================== We now describe how the formalism of abstract clones may be used to prove properties of simple type theories. To begin, we consider predicates over abstract clones, which are predicates over the terms of the type theory induced by the clone, closed under the structural operations of variable projection and substitution. Below, we extend each family of subsets $P(\Gamma; {A}) \subseteq Y(\Gamma; {A})$ to contexts by defining $P(\Gamma; {A}_1,\dots,{A}_n)$ to be the set of all substitutions $\boldsymbol\sigma \in Y(\Gamma; {A}_1,\dots,{A}_n)$ such that $\sigma_i \in P(\Gamma; {A}_i)$ for all $i \leq n$. A *predicate* $P$ over an $S$-sorted clone ${{\mathbf{X}}}$ consists of a subset $P(\Gamma; {A}) \subseteq X(\Gamma; {A})$ for each $(\Gamma; {A}) \in S^* \times S$ such that, for all contexts $\Gamma = [{A}_1, \ldots, {A}_n]$ and $i \leq n$, we have $\var[\Gamma]_i \in P(\Gamma; {A}_i)$, and, for all $t \in P(\Delta; {B})$ and $\boldsymbol\sigma \in P(\Gamma; \Delta)$, we have ${t [\boldsymbol\sigma]} \in P(\Gamma; {B})$. Closure under variables and under substitution imply that $P$ forms a clone ${{\mathbf{P}}}$ whose inclusion ${{\mathbf{P}}}\hookrightarrow {{\mathbf{X}}}$ into ${{\mathbf{X}}}$ is a clone homomorphism. Predicates over $S$-sorted clones are equivalently the subobjects in ${{\mathbf{Clone}}(S)}$, and are hence closed under arbitrary conjunction, existential quantification, and quotients of equivalence relations. (This follows from , since varieties are exact categories @barr1971exact [Theorem 5.11], and all exact categories enjoy these properties.) They are also closed under context extension: if $P$ is a predicate over ${{\mathbf{X}}}$ and $\Xi$ is a context, then ${{\Uparrow^{\Xi}}} P$ is a predicate over ${{\Uparrow^{\Xi}}} {{\mathbf{X}}}$. We present a meta-theorem for establishing properties of simple type theories. \[Induction principle for second-order syntax\] \[thm:induction\] Suppose that $({{\mathbf{Y}}}, {\llbracket {-} \rrbracket})$ is an algebra for an $S$-sorted second-order presentation ${{\mathbf{\Sigma}}}$, that $f : {{\mathbf{X}}}\to {{\mathbf{Y}}}$ is a clone homomorphism from an $S$-sorted clone ${{\mathbf{X}}}$, and that $P$ is a predicate over ${{\mathbf{Y}}}$. If - for all operators ${\mathsf{o}} \in \Sigma((\Delta_1;{A}_1), \dots, (\Delta_n;{A}_n); {B})$, contexts $\Gamma \in S^*$, and tuples of terms $(t_i \in P(\Gamma, \Delta_i; {A}_i))_i$ we have ${\llbracket {\mathsf{o}} \rrbracket}_\Gamma (t_1, \dots, t_n) \in P(\Gamma; {B})$; - for all terms $t \in X(\Gamma; {A})$ we have $f_{\Gamma; {A}}(t) \in P(\Gamma; {A})$, then, for all free terms $t \in (F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}) (\Gamma; {A})$, we have ${f^\dagger}_{\Gamma; {A}}(t) \in P(\Gamma; {A})$. The predicate $P$ is closed under operators, so the interpretations of operators in ${{\mathbf{Y}}}$ make ${{\mathbf{P}}}$ into a ${{\mathbf{\Sigma}}}$-algebra. The image of $f$ is contained in $P$, so $f$ forms a clone homomorphism ${{\mathbf{X}}}\to {{\mathbf{P}}}$. By the universal property of the free algebra $F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}$, we therefore have an algebra homomorphism $F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}\to {{\mathbf{P}}}$. This necessarily sends $t \in (F_{{{\mathbf{\Sigma}}}}{{\mathbf{X}}})(\Gamma; {A})$ to ${f^\dagger}_{\Gamma; {A}}(t) \in P(\Gamma;{A})$. We give two corollaries of this induction principle. The first is for proving properties of closed terms, which take the form of families of subsets $P ({A}) \subseteq Y({\diamond}; {A})$. Given such a family $P$, let $P({A}_1,\dots, {A}_n)$ be the set of all $\boldsymbol\sigma \in Y({\diamond}; {A}_1,\dots,{A}_n)$ such that $\sigma_i \in P({A}_i)$ for all $i \leq n$, and define a predicate ${P^{\sharp}}$ over ${{\mathbf{Y}}}$ by $ {P^{\sharp}} (\Gamma; {A}) = \{ t \in Y(\Gamma; {A}) \mid \forall \boldsymbol\sigma \in P(\Gamma).\,{t [\boldsymbol\sigma]} \in P ({A}) \} $. Applying the induction principle above to ${P^{\sharp}}$ gives us the following. \[corollary:closed-terms\] Suppose that ${{\mathbf{\Sigma}}}$ is an $S$-sorted second-order presentation, that $({{\mathbf{Y}}}, {\llbracket {-} \rrbracket})$ is a ${{\mathbf{\Sigma}}}$-algebra, and that $(P ({A}) \subseteq Y ({\diamond}; {A}))_{{A}\in S}$ is a family of subsets. For every $S$-sorted clone ${{\mathbf{X}}}$ and clone homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{Y}}}$, if - for every operator ${\mathsf{o}} \in \Sigma ((\Delta_1;{A}_1),\dots, (\Delta_n;{A}_n); {B})$ and tuple $ (t_i \in {P^{\sharp}} (\Delta_i;{A}_i))_{i \leq n} $ of terms, we have ${\llbracket {\mathsf{o}} \rrbracket}_{{\diamond}}(t_1, \dots, t_n) \in P ({B})$; - for every term $t \in X (\Gamma; {B})$, we have $f_{\Gamma; {B}}(t) \in {P^{\sharp}} (\Gamma; {B})$, then, for every type ${A}\in S$ and free term $t \in (F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}) ({\diamond}; {A})$, we have ${f^\dagger}_{{\diamond}; {A}}(t) \in P ({A})$. ${P^{\sharp}}({\diamond}; {A}) = P({A})$, so it suffices to apply \[thm:induction\] to the predicate ${P^{\sharp}}$. We therefore check the two assumptions of that theorem. Closure of ${P^{\sharp}}$ under $f$ is immediate; and ${P^{\sharp}}$ is closed under operators because, if $(t_i \in {P^{\sharp}}(\Gamma, \Delta_i; {A}_i))_i$ and $\boldsymbol\sigma \in P(\Gamma)$, then $ {t_i [{\mathsf{lift}_{\Delta_i}} \boldsymbol\sigma]} \in {P^{\sharp}}(\Delta_i; {A}_i) $ for all $i \leq n$, so that $ {{\llbracket {\mathsf{o}} \rrbracket}_{\Gamma}(t_1, \dots, t_n) [\boldsymbol\sigma]} = {\llbracket {\mathsf{o}} \rrbracket}_{{\diamond}}( {t_1 [{\mathsf{lift}_{\Delta_1}}\boldsymbol\sigma]}, \dots, {t_n [{\mathsf{lift}_{\Delta_n}}\boldsymbol\sigma]}) \in P({B}) $. Families of subsets $P({A}) \subseteq X({\diamond}; {A})$ are closed under arbitrary conjunction and disjunction, complements, and universal and existential quantification. They form a *tripos* @hyland1980tripos [@pitts2002tripos], and hence a model of higher-order logic over ${{\mathbf{Clone}}(S)}$; the tripos-theoretic methods of Hofmann @hofmann1999semantical carry over in this way to the setting of abstract clones. The second corollary is for families of subsets $P(\Gamma; {A}) \subseteq Y(\Gamma; {A})$ that are not known to be closed under substitution. (In some cases proving closure under substitution requires an induction over terms, but induction over terms is what this section is meant to enable.) Analogously to the construction ${P^{\sharp}}$ for predicates over closed terms, we define a predicate ${P^{\flat}}$ over ${{\mathbf{Y}}}$ by $ {P^{\flat}} (\Gamma; {A}) = \{ t \in Y(\Gamma; {A}) \mid \forall \Delta, \boldsymbol\sigma \in P(\Delta; \Gamma).\, {t [\boldsymbol\sigma]} \in P (\Delta; {A}) \} $. \[corollary:open-terms\] Suppose that ${{\mathbf{\Sigma}}}$ is an $S$-sorted second-order presentation, that $({{\mathbf{Y}}}, {\llbracket {-} \rrbracket})$ is a ${{\mathbf{\Sigma}}}$-algebra, and that $(P (\Gamma;{A}) \subseteq Y (\Gamma;{A}))_{(\Gamma;{A})\in S^*\times S}$ is a family of subsets. For every $S$-sorted clone ${{\mathbf{X}}}$ and homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{Y}}}$, if - for every context $\Gamma$ we have $\var[\Gamma] \in P(\Gamma; \Gamma)$; - for every context $\Gamma$, operator ${\mathsf{o}} \in \Sigma ((\Delta_1;{A}_1),\dots,(\Delta_n;{A}_n);{B})$, and tuple of terms $ (t_i \in {P^{\flat}}(\Gamma, \Delta_i; {A}_i))_i $ we have $ {\llbracket {\mathsf{o}} \rrbracket}_\Gamma(t_1, \dots, t_n) \in {P^{\flat}}(\Gamma; {B}) $; - for every term $t \in X (\Gamma; {B})$ we have $f_{\Gamma; {B}}(t) \in {P^{\flat}} (\Gamma; {B})$, then, for every free term $t \in (F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}) (\Gamma; {A})$, we have ${f^\dagger}_{\Gamma; {A}}(t) \in P (\Gamma; {A})$. We can apply \[thm:induction\] to ${P^{\flat}}$ because it is closed under operators and under $f$. Hence ${f^\dagger}_{\Gamma; {A}}(t) \in {P^{\flat}} (\Gamma; {A})$ for each $t \in (F_{{{\mathbf{\Sigma}}}} {{\mathbf{X}}}) (\Gamma; {A})$, and so $\var[\Gamma] \in P(\Gamma; \Gamma)$ implies that $ {f^\dagger}_{\Gamma; {A}}(t) = {({f^\dagger}_{\Gamma; {A}}(t)) [\var[\Gamma]]} \in P(\Gamma; {A}) $. The above corollaries are designed to enable logical relations arguments, in which the fundamental lemma is proven using an induction hypothesis that quantifies over substitutions. In particular, in \[corollary:open-terms\] we require ${P^{\flat}}$ to be closed under the operators, rather than $P$. There is a third corollary that instead requires closure of $P$ under operators (this would essentially be the principle of induction on $\Gamma \vdash_{{{\mathbf{X}}}} t : {A}$), but this is less useful for our purposes. Logical relations {#sec:logical-relations} ================= We provide two extended examples of proofs using the induction principles of the previous section, both involving the presentation ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$ of the STLC with $\beta\eta$-equality. The first is a proof of the adequacy of the set-theoretic model of the STLC, which uses induction on closed terms; the second is a proof that every STLC term is $\beta\eta$-equal to one in normal form, using induction on open terms. Both examples are logical relations proofs, the former using ordinary logical relations and the latter using Kripke relations @jung1993new. Though both properties are known to hold, these proofs in particular illustrate that our induction principles are powerful enough to justify logical relations arguments. We include a proof of normalization for the STLC with global state in , as a further motivating example. Closed terms and adequacy ------------------------- We say that a model ${\mathcal M}$ of the STLC is *adequate* when, for all closed terms $t$ and $u$ of the base type ${{\mathsf{b}}}$, if ${\mathcal M}{\llbracket t \rrbracket} = {\mathcal M}{\llbracket u \rrbracket}$, then $t$ and $u$ are equal up to $\beta\eta$-equality. (In adequate models, equality of denotations implies observational equivalence for terms of arbitrary types.) We first show that we can perform logical relations arguments for the STLC using our induction principle: specifically \[corollary:closed-terms\]. Fix a ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra $({{\mathbf{Y}}}, {\llbracket {-} \rrbracket})$, homomorphism $f : {{\mathbf{X}}}\to {{\mathbf{Y}}}$ from some clone ${{\mathbf{X}}}$, and a subset $P({{\mathsf{b}}}) \subseteq Y({\diamond}; {{\mathsf{b}}})$ of closed terms of base type. We extend $P$ to a family of subsets $P(A) \subseteq Y({\diamond}; A)$ in the standard way for logical relations: $$ P(A {\Rightarrow}B) = \{t \in Y({\diamond}; A {{\Rightarrow}} B) \mid \forall a \in P(A).\,{\llbracket {\mathsf{app}} \rrbracket}_{{\diamond}}(t, a) \in P(B)\}$$ Applying \[corollary:closed-terms\] to $P$ gives us the following: \[lemma:lr-closed\] If, for every context $\Gamma$ and term $t \in X(\Gamma; {B})$, we have $f_{\Gamma; {B}}(t) \in {P^{\sharp}}(\Gamma; {B})$, then, for every free term $t \in (F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{X}}})({\diamond}; {A})$, we have ${f^\dagger}_{{\diamond}; A}(t) \in P({A})$. The only non-trivial assumption of \[corollary:closed-terms\] is closure under operators. Closure under ${\mathsf{app}}$ is immediate from the definition of the logical relation. Closure under ${\mathsf{abs}}$ holds because, if $t \in {P^{\sharp}}(A; B)$, then, for all $a \in P(A)$, we have $ {\llbracket {\mathsf{app}} \rrbracket}_{{\diamond}}({\llbracket {\mathsf{abs}} \rrbracket}_{{\diamond}}(t), a) = t[a] \in P(B) $ using the \[eq:algebra-beta\] law, so that ${\llbracket {\mathsf{abs}} \rrbracket}_{{\diamond}}(t) \in P(A {\Rightarrow}B)$. Note that if terms are generated only by $\lambda$-abstraction and application then there are no closed terms of base type. For a more interesting example, we therefore consider the STLC with booleans (where the base type ${{\mathsf{b}}}$ is the type of booleans). Consider the ${\mathsf{Ty}}$-sorted first-order presentation ${{{\mathbf{\Sigma}}}_{{\mathbf{Bool}}}}$ with two $({\diamond}; {{\mathsf{b}}})$-ary operators ${\mathsf{true}}$, ${\mathsf{false}}$, and, for each ${A}\in {\mathsf{Ty}}$, a $({{\mathsf{b}}}, {A}, {A}; {A})$-ary operator ${\mathsf{ite}}$ ("if-then-else"), along with two equations: $$\begin{gathered} y : {A}, z : {A}\vdash {\mathsf{ite}}({\mathsf{true}}(), y, z) {\approx}y : {A}\qquad y : {A}, z : {A}\vdash {\mathsf{ite}}({\mathsf{false}}(), y, z) {\approx}z : {A}\end{gathered}$$ Let ${{\mathbf{Bool}}}$ be the ${\mathsf{Ty}}$-sorted clone that is presented by ${{{\mathbf{\Sigma}}}_{{\mathbf{Bool}}}}$. Consider the free ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra $F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}} {{\mathbf{Bool}}}$, and the ${{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}$-algebra ${\mathcal M}_{\mathbb B}$ (as defined in ) with ${\mathbb B}= \{{\mathrm{tt}}, {\mathrm{ff}}\}$. The former should be thought of as containing the terms of the STLC with booleans (we make this precise below); the latter is the usual model in ${{\mathbf{Set}}}$. Both have clone homomorphisms from ${{\mathbf{Bool}}}$: the free algebra has $\eta_{{{\mathbf{Bool}}}} : {{\mathbf{Bool}}}\to F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}} {{\mathbf{Bool}}}$; the model ${\mathcal M}_{\mathbb B}$ has the unique $g : {{\mathbf{Bool}}}\to {\mathcal M}_{\mathbb B}$ such that $$\begin{gathered} g_{\Gamma; {{\mathsf{b}}}} ({\mathsf{true}}()) = \zeta \mapsto {\mathrm{tt}}\qquad g_{\Gamma; {{\mathsf{b}}}} ({\mathsf{false}}()) = \zeta \mapsto {\mathrm{ff}}\\ g_{\Gamma; {A}} ({\mathsf{ite}}(t_1,t_2,t_3)) = \zeta \mapsto \begin{cases} g_{\Gamma;{A}}(t_2)(\zeta) &\text{if}~g_{\Gamma;{{\mathsf{b}}}}(t_1)(\zeta) = {\mathrm{tt}}\\ g_{\Gamma;{A}}(t_3)(\zeta) &\text{if}~g_{\Gamma;{{\mathsf{b}}}}(t_1)(\zeta) = {\mathrm{ff}}\end{cases}\end{gathered}$$ The algebra homomorphism ${g^\dagger} : F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{Bool}}}\to {\mathcal M}_{\mathbb B}$ gives the interpretation of STLC terms in the model. Define a subset $ P({{\mathsf{b}}}) \subseteq (F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{Bool}}}\times {\mathcal M}_{\mathbb B})({\diamond}; {{\mathsf{b}}}) = (F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{Bool}}})({\diamond}; {{\mathsf{b}}}) \times {\mathbb B}$ by $$P({{\mathsf{b}}}) = \{(\eta_{{{\mathbf{Bool}}}}({\mathsf{true}}()),{\mathrm{tt}}) , (\eta_{{{\mathbf{Bool}}}}({\mathsf{false}}()),{\mathrm{ff}})\}$$ This extends to a logical relation $P$ by the definition on function types above and, by a simple proof, satisfies the precondition of \[lemma:lr-closed\], where the clone homomorphism $f$ is $ {\langle\eta_{{{\mathbf{Bool}}}}, g\rangle} : {{\mathbf{Bool}}}\to F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{Bool}}}\times {\mathcal M}_{\mathbb B}$. Hence, for all $t \in (F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{Bool}}})({\diamond}; A)$, we have $ (t, {g^\dagger}_{{\diamond}; {A}}(t)) = {{\langle\eta_{{{\mathbf{Bool}}}}, g\rangle}^\dagger}_{{\diamond}; {A}}(t) \in P({A}) $. When ${A}= {{\mathsf{b}}}$ this immediately implies, for all $t, t' \in (F_{{{{\mathbf{\Sigma}}}^{{\Lambda_{\beta\eta}}}}}{{\mathbf{Bool}}})({\diamond}; {{\mathsf{b}}})$, that if ${g^\dagger}_{{\diamond}; {{\mathsf{b}}}}(t) = {g^\dagger}_{{\diamond}; {{\mathsf{b}}}}(t')$ then $t = t'$. This last property is seen to be adequacy of the set-theoretic model ${\mathcal M}_{\mathbb B}$ as follows. Let ${{\mathbf{{\Lambda_{\beta\eta{\mathbf{Bool}}}}}}}$ be the ${\mathsf{Ty}}$-sorted clone that is defined in the same way as ${{\mathbf{{\Lambda_{\beta\eta}}}}}$ (\[example:stlcclone\]) but with additional term formers and equations (omitting the typing constraints on equations): $$\begin{array}{l} \begin{prooftree}[center=false]
{'source': 'arXiv_out/2105'}