Abstract Syntax and Variable Binding

(Extended Abstract)

Marcelo Fiore

COGS Univ. of Sussex

<marcelo@cogs.susx.ac.uk>

Gordon Plotkin

LFCS Univ. of Edinburgh

<gdp@dcs.ed.ac.uk>

Daniele Turi LFCS Univ. of Edinburgh

                <dt@dcs.ed.ac.uk>

Abstract

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with both a (binding) algebra and a substitution structure compatible with each other. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

Introduction

It has long been recognised that the essential syntactical structure of programming languages is not that given by their concrete or surface syntax—as expressed, say, by a language description in BNF oriented to parsing: there the parse trees contain much information useless for language processing. Rather, the deep structure of a phrase should reflect its semantic import.

McCarthy [23] coined the term abstract syntax for such structures, which are typically given as trees with their top node labelled by the main semantic constituent, or, equivalently, by terms of first-order logic. Abstract syntax has both synthetic and analytic aspects: the former concerns the constructors needed to form phrases, the latter the destructors (predicates and selectors) needed to take them apart [21]. Burstall [6] contributed structural recursion—a generalised form of primitive recursion—to analytic syntax, with an associated principle of structural induction.

The algebraic point of view of ADJ [14] (see also [33]) regards abstract syntax as the initial algebra (of the constructors) and semantics as the unique homomorphism to a semantic algebra (the model). Structural recursion then arises from initiality. The categorical view regards the algebras as those of an associated signature functor: the initial algebra has an isomorphism as structure map and its inverse is analytic syntax. Finally, in the recursive type view [33], the initial algebra is obtained as the solution to a recursive (set) equation; this leads one to a treatment of syntax within programming languages as exemplified in the ML/LCF approach [15].

The first-order view can be problematic. For example, when dealing with context-sensitive aspects of syntax, it does not account satisfactorily for variable binding, with its allied notions of scope, free and bound occurrences, α-equivalence, production of fresh variables, and substitution (e.g., in λ-calculus, CCS with value passing, π-calculus, logical quantifiers and integrals). Useful context-sensitive extensions of BNF certainly exists, such as attribute grammars and van Wijngaarden grammars; however, as in the first-order case, they do not themselves give an account of deep structure.

One proposal for an abstract treatment, originating with Church [7], is that of higher-order abstract syntax; there one uses the binding apparatus provided by the typed λ-calculus to express all other forms of binding—see [30, 26, 31, 29]. Now, normal forms (of ground type) play the rôle of first-order terms, but with first-order signatures being replaced by second-order ones. (The binding analogue of trees is provided by the term graphs first introduced by Wadsworth—see, e.g., [17].) A form of analytic syntax is given by matching or unification in associated logic programming languages [26, 31]. In implementations, de Bruijn’s terms [9] are used to provide “α-equivalence normal forms.”

Unfortunately, in the higher-order abstract syntax approach, many of the desirable properties mentioned above, such as accounts of structural recursion and induction, and recursive equations for abstract syntax, are missing, or at least not fully developed (see [25, 24, 10]).

In this paper, we provide a (categorical) algebraic view of syntax with variable binding. The analogue to universal algebra is the theory of binding algebras originating in the work of Aczel [1]— see also [20, 32, 37]. We replace algebras over sets by binding algebras over variable sets. Formally, variable sets are (covariant) presheaves and the fundamental idea is to turn contexts into the “index category” of the presheaves.

We obtain a notion of binding signature in which binding is again expressed by second-order types, but now using a special presheaf of variables or, equivalently, by a first-order signature extended with a notion of differentiation (cf. [16]). Binding algebras are then presheaves equipped with operations corresponding to the signature; our models are such algebras additionally equipped with a compatible substitution structure.

Abstract syntax is the initial such model, with the algebra structure obtained as the solution to a recursive presheaf equation and substitution defined by an associated structural recursion. The unique homomorphism from the syntax to another model (initial algebra semantics) preserves, besides the constructors, the extra substitution structure.

Organisation of the paper. We start in Section 1 by advocating the use of the category of (covariant) presheaves Set^{𝔽} as a suitable mathematical universe in which to deal with syntax with variable binding. The index category 𝔽 is a skeleton of the category of finite sets and functions; it provides a notion of cartesian context allowing for exchange, weakening, and contraction. The structure of Set^{𝔽} relevant to modelling variable binding is studied in detail.

The study of signatures with variable binding in our framework is carried out in Section 2. Our main result here is that the presheaf of terms (with binders) associated to a (binding) signature has an abstract universal characterisation as a free algebra over a presheaf of variables. This result is exploited in two directions: to give implementations of abstract syntax (with variable binding) à la de Bruijn, and to provide semantics by initiality. These two applications are exemplified using the λ-calculus.

Section 3 is devoted to substitution. We treat both single-variable and simultaneous substitution. The former is handled by introducing the notion of substitution algebra; the latter first by the elementary abstract clones and then, yet more abstractly, as certain monoids in the category of presheaves. The three presentations are shown to be equivalent. We also define two “categorical programs” for substitution by structural recursion.

In Section 4, we define the category of models of a signature; the presheaf of terms is the initial such model. We exemplify the corresponding initial algebra semantics again using the λ-calculus. This semantics automatically verifies the semantic substitution lemma.

Finally, in Section 5 we give a taste of multisorted syntax with binding by considering the simple case of two-sorted syntax over a single variable type. This allows one to deal with languages such as CCS with value passing [27] and the π-calculus [28].

Future work. Various directions for further work are possible; we mention but a few here. First, the syntactic counterpart of our treatment of substitution by categorical structural recursion (i.e., parameterised initiality) will be worked out. In particular, we envisage a type theory based on the internal language of our semantic universe for manipulating abstract syntax with binding. Again, structural induction principles for reasoning about abstract syntax with binding should be available within our framework.

Second, the investigation of more sophisticated syntax in our setting will be pursued. The simply typed λ-calculus can be easily accommodated; various linear settings (in contrast to the cartesian one explored here) also seem to fit; type theories with dependent types are yet to be tackled.

Third, theories of operational semantics with binding will be developed along the lines of [36]. Preliminary results indicate that some interesting syntactic formats of well-behaved operational rules for languages with variable binding can be obtained.

Fourth, connections between our approach and the general theory of substitution provided by clubs [18, 19] will be investigated.

1 The universe of types

We present the universe of types within which we work. Our intent is to consider a notion of type broad enough to encompass syntax with variable binding (and, more generally, algebras for binding signatures) in a framework with rich type structure (i.e., type constructors and operations on types). To motivate our choice we start by examining the structure of the set of λ-terms.

Λ. In the course of our discussion we will consider the set of (untyped) λ-terms Λ_{Var} given by the following grammar.

\begin{aligned}x ∈ Var & ::= & x_{i} (i ∈ ℕ^{+}) , \\ t ∈ Λ_{Var} & ::= & x | λx.t′ | t_{1}t_{2} . \end{aligned}

In untyped settings, the treatment of the operator λ as a binder is typically dealt with by introducing the notion of free/bound variable. However, as is well-known and commonly used in typed settings, this information may be presented by judgements, consisting of a term together with a context, subject to a well-formedness condition. To simplify the exposition we will consider the following wellformedness rules which provide canonical representatives for α-equivalence classes of λ-terms by the method of de Bruijn levels [9].

\frac{1 ≤ i ≤ n}{x_{1}, …, x_{n} ⊢ x_{i}}  \frac{x_{1}, …, x_{n}, x_{n+1} ⊢ t}{x_{1}, …, x_{n} ⊢ λx_{n+1}.t} ; \frac{x_{1}, …, x_{n} ⊢ t_{1}  x_{1}, …, x_{n} ⊢ t_{2}}{x_{1}, …, x_{n} ⊢ t_{1}t_{2}} (1)

Conceptually, the passage from the approach based on free/bound variables to the one based on contexts consists in turning the free-variable function FV : Λ_{Var} [figure]P(Var) into extra structure on terms. As we will see, the latter viewpoint is important for bringing out the structure of the type Λ of λ-terms (up to α-equivalence). As a first step in this direction notice that contexts stratify λ-terms up to α-equivalence. Indeed, for all n ∈ ℕ, we have a bijective correspondence

Λ_{ℓ}(n) ≅ Λ_{α}(n) : t [figure] [t]_{α}  (2)

where

Λ_{ℓ}(n) =^{def} { t ∈ Λ_{Var} | x_{1}, …, x_{n} ⊢ t } ,

Λ_{α}(n) =^{def} { [t]_{α} | t ∈ Λ_{Var} ∧ FV(t) ⊆ { x_{1}, …, x_{n} } } .

Next, note that the well-formedness rules (1) induce (and in fact correspond to) the following bijection: for all n ∈ ℕ,

n + Λ_{ℓ}(n + 1) + Λ_{ℓ}(n) × Λ_{ℓ}(n) [figure: ≅]Λ_{ℓ}(n) (3)
\xymatrix{i ∈ n \ar@{|->}[r] & x_{i}}
\xymatrix{t ∈ Λ_{ℓ}(n + 1) \ar@{|->}[r] & λx_{n+1}.t}
\xymatrix{(t_{1}, t_{2}) ∈ Λ_{ℓ}(n) × Λ_{ℓ}(n) \ar@{|->}[r] & t_{1}t_{2}}

where, by abuse of notation, we write n for the set { 1, …, n }.

To conclude the analysis of the structure of Λ we first need to examine the structure of contexts.

The structure of contexts. The notion of context relevant to this paper is that of (untyped) cartesian context. This is reflected in the operations which we allow for context manipulation. Considering the set { 1, …, m } as a generic abstract context with m variables, these operations are

exchange  s_{n} : n + 2 [figure] n + 2
weakening  w_{n} : n [figure] n + 1
contraction  c_{n} : n + 2 [figure] n + 1

(4)

with their intuitive definitions (see (5) below). Closing the above operations under composition we obtain all functions from m to n (m, n ∈ ℕ). Thus, we take the category of cartesian contexts 𝔽 to be the full subcategory of Set with objects { 1, …, n } (n ∈ ℕ). (Note that 𝔽 is isomorphic to the category of finite cardinals and functions.) A conceptual description of the category 𝔽 is as the free cocartesian category on one object (see e.g. [22, § VIII.4, Lemma 1]). As such, it may be understood as being generated from an initial object (the generic abstract empty context) by an operation of context extension, (−)+1, with a generic abstract context with one variable, 1. Following this viewpoint, we will henceforth consider the category 𝔽 as equipped with a chosen coproduct structure

n [figure: ^{old^{n}}] n + 1 [figure: ^{new^{n}}] 1 .

The operations in (4) can be thus described as follows: s_{n} = id_{n}+s, w_{n} = id_{n}+w, and c_{n} = id_{n}+c where

s =^{def} [new_{1}, old_{1}] : 2 [figure] 2 ,
w =^{def} old_{0} : 0 [figure] 1 ,
c =^{def} [id_{1}, id_{1}] : 2 [figure] 1 .

(5)

We are now in a position to spell out the structure of Λ.

The structure of Λ. Since contexts stratify terms, it follows that the operations on contexts act on them. Indeed, every function ρ : m [figure] n in 𝔽 (thought of as a renaming of variables) induces an action

\xymatrix{Λ_{ℓ}(m) \ar[d]^{def}_{≅} \ar[r]^{Λ_{ℓ}(ρ)} & Λ_{ℓ}(n) \\ Λ_{α}(m) \ar[r]_{Λ_{α}(ρ)} & Λ_{α}(n) \ar[u]_{≅}}

where Λ_{α}(ρ) : t [figure] t{x_{ρ1}/x_{1}, …, x_{ρm}/x_{m}}, which is functorial in the sense that

Λ_{ℓ}(id_{n}) = id_{Λ_{ℓ}(n)} , Λ_{ℓ}(ρ′∘ρ) = Λ_{ℓ}(ρ′)∘Λ_{ℓ}(ρ) ,

for all n ∈ 𝔽 and for all ρ : n [figure] n′ and ρ′ : n′ [figure] n′′ in 𝔽. That is, Λ_{ℓ} is an object of the presheaf category

F =^{def} Set^{𝔽} ,

which we take to be our universe of types. Following common usage, these types are referred to as presheaves. Clearly, Λ_{α} is a presheaf in F. The presheaf of variables Var is given, for n ∈ 𝔽 and ρ in 𝔽, by

Var(n) = { x_{1}, …, x_{n} } , Var(ρ) : x_{i} [figure] x_{ρi} .

For a slightly more involved example consider the presheaf L : 𝔽 [figure] Set with L(n) given by the left hand side of the bijection (3) and equipped with the functorial action

L(ρ) =^{def} ρ + Λ_{ℓ}(ρ + id_{1}) + Λ_{ℓ}(ρ) × Λ_{ℓ}(ρ) (6)

for every ρ in 𝔽.

An important non-syntactic example is provided by the presheaf of operations (from A to B) ⟨A, B⟩ for objects A, B in a cartesian category C:

\begin{matrix}⟨A, B⟩(n) = C(A^{n}, B) \\ ⟨A, B⟩(ρ) : f [figure] f⟨π_{ρ1}, …, π_{ρ_{m}}⟩ \end{matrix}  (7)

for n ∈ 𝔽 and ρ : m [figure] n in 𝔽. In particular, the presheaf ⟨A, A⟩ is the clone of operations on A.

Recall that a map f : A [figure]B between presheaves A and B in F is a so-called natural transformation given by an indexed family of functions { f_{n} : A(n) [figure]B(n) in Set }_{n∈𝔽} subject to the following naturality condition: for all ρ : m [figure] n in 𝔽,

f_{n} ∘ A(ρ) = B(ρ) ∘ f_{m} .

The bijection (2) yields an isomorphism of presheaves Λ_{ℓ} ≅ Λ_{α} in F. More interestingly, notice that the particular implementation of λ-terms (up to α-equivalence) adopted in our exposition by the method of de Bruijn levels is reflected in the mathematical structures under consideration. Indeed, the bijection (3) yields a natural isomorphism of presheaves L ≅ Λ_{ℓ} in F if and only if the chosen coproduct structure on 𝔽 is taken to be the one with old_{n}(i) = i (1 ≤ i ≤ n) and new_{n} = n + 1 (cf. the rule for λ-introduction in (1)). We will see in the next section that an implementation of λ-terms (up to α-equivalence) by the method of de Bruijn indices [9] is also available in our framework.

We conclude with a description of the type constructors and the operations on types (cf. [11]) in the universe F that will be needed in the rest of the paper. As an application, we will show how type constructors may be used to provide a structural definition of the presheaf L of (6).

The structure of F. The category F is a wellknown and interesting topos (see [22, § VIII.4]). Many of the constructions that follow in this and later sections can be cast in the language of topos theory. However, we do not emphasise this viewpoint here; rather we adopt a presentation that generalises to other contexts.

\underline{Sums, products, and exponentials:} F is a complete and cocomplete cartesian closed category, with limits and colimits computed pointwise (see [22]).

\underline{V:} The presheaf (of abstract variables) V ∈ F is obtained by embedding the generic abstract context with one variable in 𝔽 into F via Yoneda. Explicitly, V is the embedding of 𝔽 in Set given by

V(n) = n (n ∈ 𝔽) ; V(ρ) = ρ (ρ in 𝔽) .

\underline{δ:} The type constructor (for context extension) δ : F [figure] F is obtained from the operation of context extension (−)+1 : 𝔽 [figure] 𝔽 by precomposition:

δ( ) =^{def} ( ) ∘ ((−)+1) .

In elementary terms, for A ∈ F, the presheaf δA is given, for n ∈ 𝔽 and ρ in 𝔽, by

(δA)(n) = A(n + 1) , (δA)(ρ) = A(ρ + id_{1}) ; and, for f : A [figure] B in F, the map δf : δA [figure] δB is given by

(δf)_{n} = f_{n+1} : A(n + 1) [figure] B(n + 1) (n ∈ 𝔽) .

Thus, intuitively, an element of type δA in the context n is an element of type A in the extended context n + 1.

The operations on contexts extend from 𝔽 to F in the same vein. For instance, the operations in (5) respectively give rise to the natural transformations swap : δ^{2} [figure: .]δ^{2}, up : Id [figure: .]δ, contract : δ^{2} [figure: .] δ with the following explicit descriptions: for A ∈ F and n ∈ 𝔽,

swap_{A,n} = A(s_{n}) : A(n + 2) [figure] A(n + 2) ,
up_{A,n} = A(w_{n}) : A(n) [figure] A(n + 1) ,
contract_{A,n} = A(c_{n}) : A(n + 2) [figure] A(n + 1) .

Note that, as the passage from 𝔽 to F is given by precomposition, it preserves equational structures. In particular, the monad ((−)+1, { w_{n} }, { c_{n} }) on 𝔽 yields the monad (δ, up, contract) on F.

We examine some properties of δ. First we note that, by construction, δ has both a left and a right adjoint; hence it preserves both limits and colimits (as a simple calculation will also show). These adjoints are given by the following natural bijective correspondences

\begin{matrix}X [figure] δA \\ X × V [figure] A \end{matrix}  \begin{matrix}δA [figure] Y \\ A [figure] ⟨V + 1, Y ⟩ \end{matrix}  (8)

Second, observe that the first correspondence above shows that δ(−) ≅^{.} (−)^{V}, and states that the elements of type δA in the context X are the elements of type A in the extended context X ×V. Finally, we note the important fact that the diagram

V [figure: old] δV [figure: new] 1  (9)

is a coproduct in F.

It should be clear that the type L of (6) equals the structured type V + δΛ_{ℓ} + Λ_{ℓ} × Λ_{ℓ}. We will show in the next section that the inductive type μX.V + δX + X × X characterises the presheaf Λ of λ-terms (up to α-equivalence).

2 Binding algebras

We show that the universe F provides a suitable setting for modelling binding signatures and their algebras. In particular, we obtain a characterisation of syntax with variable binding by initiality, which generalises the well-known result for the first-order case [14]. This yields a notion of abstract syntax with variable binding for which an initial algebra semantics is available.

Syntax with variable binding. A binding signature [32] Σ = (O, a) consists of a set of operations O equipped with an arity function a : O [figure] ℕ^{∗}. An operator of arity ⟨n_{1}, …, n_{k}⟩ has k arguments and binds n_{i} variables in the i-th argument (1 ≤ i ≤ k). For instance, the signature of the λ-calculus has an operator of arity ⟨1⟩, viz. λabstraction with one argument and binding one variable, and an operator of arity ⟨0, 0⟩, viz. application with two arguments and binding no variables.

The terms associated to a signature over a set of variables (ranged over by x) are given by the following grammar.

\begin{matrix}t ∈ T_{Σ} \\ ::= x | o((x_{1}, …, x_{n_{1}}).t_{1}, …, (x′_{1}, …, x′_{n_{k}}).t_{k}) \end{matrix}

where o is an operator of arity ⟨n_{1}, …, n_{k}⟩. Obvious definitions for free/bound variables and α-equivalence apply to these terms.

Analogous to the case of the λ-calculus, for any signature, there is a presheaf of terms (up to α-equivalence) TV_{α} ∈ F given by

TV_{α}(n) =^{def} { [t]_{α} | FV(t) ⊆ { x_{1}, …, x_{n} } }

TV_{α}(ρ) : t [figure] t{x_{ρ1}/x_{1}, …, x_{ρm}/x_{m}}

for every n ∈ 𝔽 and ρ : m [figure] n in 𝔽.

Abstract syntax with variable binding. To give the abstract characterisation of TV_{α} we consider the notion of binding algebra associated to a binding signature. Recalling that an operator of arity ⟨n_{i}⟩_{1≤i≤k} binds n_{i} variables in the i-th argument and that δ is a type constructor for context extension it is natural to interpret an operation of arity ⟨n_{1}, …, n_{k}⟩ on a presheaf A ∈ F as a map δ^{n_{1}}(A) × … × δ^{n_{k}}(A) [figure] A, and hence to define a Σ-algebra over a presheaf A ∈ F as a map

∐_{\begin{matrix}o∈O \\ a(o)=⟨n_{i}⟩_{1≤i≤k} \end{matrix}} δ^{n_{1}}(A) × … × δ^{n_{k}}(A) [figure]A .

Thus, to a signature Σ = (O, a) we associate the functor Σ : F [figure] F given by

Σ(X) =^{def} ∐_{\begin{matrix}o∈O \\ a(o)=⟨n_{i}⟩_{1≤i≤k} \end{matrix}} ∏_{1≤i≤k} δ^{n_{i}}(X) , (10)

and define the category of algebras associated to the signature Σ as the category Σ-Alg, with objects given by algebras h : ΣA [figure]A and morphisms f : (A, h) [figure](A′, h′) given by maps f : A [figure] A′ that are homomorphic in the sense that f ∘ h = h′ ∘ Σ(f). This approach fits into the paradigm of categorical algebra [4, 5]. However we remark that the general theory allows for the treatment of more sophisticated notions of signature (that may incorporate equational theories); they will not be considered in this extended abstract.

As is well-known (see e.g. [4]), the forgetful functor Σ-Alg [figure]F : (A, h) [figure]A has a left adjoint providing the free Σ-algebra on a presheaf; which, for a presheaf X ∈ F, is an initial X + Σ-algebra.

The presheaf of terms TV_{α} of a signature Σ = (O, a) has a syntactic algebra structure [τ^{(o)}]_{o∈O} given, at stage n, by the mapping sending the tuple of terms ⟨t_{i}⟩_{1≤i≤k} to the term

o( (x_{new(1)}, …, x_{new(n_{i})}).t_{i} {x_{1}/x_{old(1)}, …, x_{n}/x_{old(n)}} )_{1≤i≤k} ,

where new(j) = new_{n+j−1} (1 ≤ j ≤ n_{i}) and old(j) = old_{n}(j) (1 ≤ j ≤ n).

Theorem 2.1 The presheaf of terms TV_{α} associated to a signature Σ (equipped with the syntactic algebra structure) is a free Σ-algebra on the presheaf of variables V.

Rather than proving this general result here we show how it may be used to implement abstract syntax. To this end recall that the underlying presheaf of a free Σ-algebra on a presheaf X may be computed as the union of the chain

0 ⊆ X + Σ(0) ⊆ X + Σ(X + Σ(0)) ⊆ ⋯

obtained by iterating the functor X + Σ on the empty presheaf 0.

In the particular case of the free algebra Λ on the presheaf of variables V for the signature of the λ-calculus Σ_{λ}(X) = δX + X × X this calculation amounts to the following inductive definitions: Λ(n) = { t | n ⊢ t } (n ∈ 𝔽) where

\frac{1 ≤ i ≤ n}{n ⊢ var(i)}  \frac{n + 1 ⊢ t}{n ⊢ lam(t)}  \frac{n ⊢ t_{1}  n ⊢ t_{2}}{n ⊢ app(t_{1}, t_{2})}

and, for ρ : m [figure] n in 𝔽,

Λ(ρ)(t) = case t of

[figure: var(i); var( ρi )]
[figure: lam(t′); lam( Λ(ρ + id_{1})(t) )]
\xymatrix{app(t1, t2) \ar@{=>}[r] & app( Λ(ρ)(t_{1}), Λ(ρ)(t_{2}) ) .}

This abstract view yields particular implementations of λ-terms according to different choices of the coproduct structure on the category 𝔽. For instance, if old_{n}(i) = i + 1 (1 ≤ i ≤ n) and new_{n} = 1 (n ∈ ℕ) then the presheaf Λ implements λ-terms by the method of de Bruijn indices; as one can notice, for example, from the fact that, for ρ : m [figure] n in 𝔽,

Λ(ρ)(lam(var i)) = \{ \begin{matrix}lam(var 1) & , if i = 1 . \\ lam(var ρi) & , otherwise . \end{matrix}

(The reader may wish to consider examples involving swap and up.) Of course, the implementation of λ-terms by the method of de Bruijn levels is obtained by choosing old_{n}(i) = i (1 ≤ i ≤ n) and new_{n} = n + 1 (n ∈ ℕ).

A glance at initial algebra semantics. In order to consider interpretations of the λ-calculus let fold : D^{D} ◁ D : unfold be a retraction in a cartesian closed category C [34].

The clone of operations ⟨D, D⟩ ∈ F (see (7)) admits a canonical interpretation of variables π : V [figure] ⟨D, D⟩ given by

[figure: n; C(D^{n}, D); i; π_{i}^{(n)} ,]

and may be equipped with an algebra structure δ⟨D, D⟩ + ⟨D, D⟩ × ⟨D, D⟩ [figure] ⟨D, D⟩ as follows

\begin{matrix}C(D^{n+1}, D) & [figure] & C(D^{n}, D) \\ (f : D^{n+1} [figure] D) & [figure] & fold ∘ λλ(f) , \end{matrix}

\xymatrix{C(D^{n}, D) × C(D^{n}, D) \ar[r] & C(D^{n}, D)}
(f, x : D^{n} [figure] D) [figure]ev ∘ ⟨unfold ∘ f, x⟩ .

As Λ is the free Σ_{λ}-algebra on V, it follows from Theorem 2.1 that π has a unique homomorphic extension [[−]] : Λ [figure] ⟨D, D⟩ characterised as

\xymatrix{V + δΛ + Λ × Λ \ar[d]_{V+δ[[−]]+[[−]]×[[−]]} \ar[r]^{[var,lam,app]}_{≅} & Λ \ar[d]^{[[−]]} \\ V + δ⟨D, D⟩ + ⟨D, D⟩ × ⟨D, D⟩ \ar[r] & ⟨D, D⟩ & ,}

and which can be easily shown to be the traditional compositional interpretation function Λ(n) [figure] C(D^{n}, D) (n ∈ ℕ) of λ-terms [34].

3 Substitution

A program for substitution. To motivate the more abstract development to follow, and to link our approach to programming, we start by writing a (categorical) recursive program for substituting λ-terms in the type theory of F.

Let Λ (the presheaf of λ-terms) be the free algebra on the presheaf of variables V for the signature of the λ-calculus Σ_{λ} (see Theorem 2.1 and the discussion after it). We aim at defining an operation

σ : δΛ × Λ [figure] Λ

that, roughly speaking, given a pair (t, u) consisting of a term t with a new variable (i.e., a term in an extended context) and a term u, substitutes u for the new variable in t. Using that

δΛ = δV + δδΛ + δΛ × δΛ

(since Λ = μX.V + δX + X × X and δ preserves sums and products) we can define a recursive program for σ by case analysis on its first argument. The definition is as follows σ(t, u) = case t of

[figure: x : δV; β(x, u)]
[figure: t′ : δδΛ; lam( δσ(swap t′, up u) )]
\xymatrix{t_{1}, t_{2} : δΛ \ar@{=>}[r] & app( σ(t_{1}, u), σ(t_{2}, u) )}

(11)

where, using that δV = V + 1 (see (9)), the basic substitution β : δV × TV [figure] TV is defined as

β(x, u) = case x of [figure: old(y); var(y); new; u; .]

Put in elementary terms, the natural family σ_{n} : Λ(n + 1) × Λ(n) [figure] Λ(n) (n ∈ 𝔽) is given by

σ_{n}(t, u) = case t of

var(i)  [figure]case i of [figure: old_{n}(j); var(j); new_{n}; u]
[figure: lam(t′); lam( σ_{n+1}(swap_{n} t′, up_{n} u) )]
\xymatrix{app(t_{1}, t_{2}) \ar@{=>}[r] & app( σ_{n}(t_{1}, u), σ_{n}(t_{2}, u) ) & .}

Note that the substitution σ_{n}(lam(t′), u) proceeds by swapping (the indices for) the binding and the new variables in t′ ∈ Λ(n + 2), and by subsequently using the substitution operation σ_{n+1} with the weakened argument up_{n}(u) (where indices are shifted appropriately).

As we show below, the above definition of substitution amounts to a definition by structural recursion. Note that in the traditional approach to substitution (see, for example, [3]) welldefinedness needs to be established separately because of α-equivalence.

Definition of substitution by structural recursion. For a signature Σ, let ϕ_{X} : ΣTX [figure] TX be a free Σ-algebra over the presheaf X. To define a substitution operation

σ : δ(TV) × TV [figure] TV

for the presheaf of terms TV by structural recursion we proceed as follows. First, with the aid of the following exchange natural isomorphisms

δ^{n}(δX) ≅ (X^{V})^{V×···×V} ≅ (X^{V×···×V})^{V} ≅ δ(δ^{n}X)

we define a distributive law ψ : Σδ ≅^{.} δΣ of the endofunctor Σ over the monad δ in an obvious way. Second, we observe that this construction yields the following situation

\xymatrix{F \ar[d]^{≅^{.}}|{∘}_{δ} \ar[r]^{V+Σ(−)} & F \ar[d]|{∘}^{δ} \\ F \ar[r]_{δV+Σ(−)} & F & ;}

from which, by the uniformity property of the fixed-point operator (see [12, Theorem 7.3.12 (6)]), it follows that the Σ-algebra

Σδ(TV) ≅^{ψ_{TV}} δΣ(TV) [figure: δϕ_{V}]δ(TV)

is free over δV. Finally, using that Σ has a strength str : Σ(A)×X [figure] Σ(A×X), we let σ be the unique homomorphic extension of the basic substitution β. That is, we define σ to be the unique map such that the diagram

\xymatrix{Σ(δ(TV)) × TV \ar[r]^{str} \ar[d]^{≅}_{ψ_{TV}×id} & Σ(δ(TV) × TV) \ar[r]^{Σσ} & ΣTV \ar[dd]^{ϕ_{TV}} \\ δΣ(TV) × TV \ar[d]_{δϕ_{V}×id} \\ δ(TV) × TV \ar@{-->}[rr]^{σ} &  & TV \\ δV × TV \ar@{-->}[urr]_{β} \ar[u]^{δη_{V}×id}}

commutes, where the map η_{V} : V [figure]TV, coercing variables into terms, is the universal arrow associated to the free algebra TV.

Substitution algebras. We show that the operations σ obtained as above obey the laws of substitution. To this end we introduce an axiomatisation of single-variable substitution, whose justification is provided by Theorem 3.3 below.

Definition 3.1 A substitution algebra X = (X, φ, ν) consists of a presheaf X ∈ F equipped with two operations φ : δX × X [figure] X (a substitution) and ν : 1 [figure] δX (a generic new variable) such that:

1. u : X ⊢ φ(ν, u) = u .

2. t, u : X ⊢ φ(up(t), u) = t .

3. t : δ^{2}X ⊢ δφ(t, ν) = contract(t) .

4. t : δ^{2}X , u : δX , v : X ⊢ φ(δφ(t, u), v) = φ(δφ(swap(t), up(v)), φ(u, v)) .

The axioms have the following intuitive reading. Axiom 1 says that substituting for the generic new variable has the expected result. Axiom 2 says that substituting for a variable that is not in a term does not affect the term. Axiom 3 says that substituting the generic new variable in a term is like performing a contraction. Axiom 4 is a version of the substitution lemma.

Theorem 3.2 For every signature Σ, the structure (TV, σ, ⌜η_{V}⌝) is a substitution algebra.

Clones. Substitution algebras axiomatise singlevariable substitution. Here we show that they are equivalent to the following axiomatisation of simultaneous substitution by abstract clones (familiar, in the concrete case, from universal algebra— cf. [8, page 132]).

An (abstract) clone X = (X, μ, π) consists of a family X = {X_{n}}_{n∈ℕ} of sets, a family π = {π_{i}^{(n)} ∈ X_{n} | 1 ≤ i ≤ n}_{n∈ℕ} of distinguished elements, and a family

μ = {μ_{m}^{(n)} : X_{n} × (X_{m})^{n} [figure] X_{m}}_{n,m∈ℕ}

of operations such that, for every element t of X_{n}, every n-tuple u⃗ = (u_{1}, …, u_{n}) of elements of X_{m}, and every m-tuple v⃗ of elements of X_{l}, the following three axioms hold:

\begin{matrix}μ_{m}(π_{i}; u⃗) = u_{i} , μ_{n}(t; π_{1}, …, π_{n}) = t , \\ μ_{l}(μ_{m}(t; u⃗); v⃗) = μ_{l}(t; μ_{l}(u_{1}; v⃗), …, μ_{l}(u_{n}; v⃗)) \end{matrix} (12)

An example of a clone is given by taking: for X_{n} the set TV(n) of terms (in a context of n variables) with respect to a given signature; for π_{i}^{(n)} the variable x_{i}^{(n)} in TV(n); and for μ_{m}^{(n)} the simultaneous substitution of terms

σ_{m}^{(n)} : TV(n) × TV(m)^{n} [figure] TV(m) .

We write σ_{m}(t; u⃗) in infix notation and with no indices as t [u⃗]. Then the three axioms in (12) amount to the following familiar properties of substitution:

\begin{matrix}x_{i}[u⃗] = u_{i} , t [x_{1}, …, x_{n}] = t , \\ t [u⃗][v⃗] = t [u_{1}[v⃗], …, u_{n}[v⃗]] . \end{matrix}

(The last identity is the syntactic substitution lemma—cf. [3, page 27].)

For every object C of a cartesian category C, the clone of operations ⟨C, C⟩ on C as defined after (7) yields another example of an (abstract) clone: X_{n} = C(C^{n}, C) is then the set of operations on C of arity n, π_{i}^{(n)} is the i-th projection π_{i} : C^{n} [figure] C, and μ_{m} is given by composition.

We remark that, just like clones of operations, abstract clones X = (X, μ, π) are presheaves, with X(n) =^{def} X_{n} and with action on renamings

ρ : n [figure] m given by X(ρ)(t) =^{def} μ_{m}(t; π_{ρ1}, …, π_{ρn}).

Both clones and substitution algebras, together with the evident homomorphisms, form categories.

Theorem 3.3 The categories of substitution algebras and of clones are equivalent.

Monoids in F. There are several equivalent categorical formulations of clones; e.g., as Lawvere theories, or as finitary monads, or as one-object cartesian multicategories. (See [13] for an elementary presentation of the connection between substitution and Lawvere theories.) Here we recall that clones (and thus also substitution algebras) are equivalent to monoids in F with respect to a suitable monoidal structure. This compact and abstract presentation is very convenient for reasoning about the structure of substitution and its interplay with Σ-algebras. In particular, it allows us to define the simultaneous substitution of terms by structural recursion.

The monoidal structure we consider is given by a (highly non-symmetric) tensor ‘•’ of presheaves with unit V. For every presheaf Y, the functor • Y is the left adjoint of the endofunctor ⟨Y, ⟩ on F:

\begin{matrix}X • Y [figure] Z \\ X [figure] ⟨Y, Z⟩ \end{matrix}  (13)

An explicit description of this tensor is given by the following coend: for presheaves X and Y,

(X • Y)(m) =^{def} (∐_{n∈ℕ} X(n) × Y (m)^{n})_{/≈}

= {(t; u⃗) | n ∈ ℕ, t ∈ X(n), u⃗ ∈ Y (m)^{n}}_{/≈}

where ≈ is the equivalence relation generated by

(t; u_{1}, …, u_{n}) ∼ (t′; u′_{1}, …, u′_{n′})

iff there exists ρ : n [figure] n′ such that X(ρ)(t) = t′ and u_{i} = u′_{ρi}. For example, for X = Λ,

\begin{matrix}(x_{1}x_{2}; u_{1}, u_{2}) ∼ (x_{2}x_{3}; u, u_{1}, u_{2}) \\ ∼ (x_{1}x_{3}; u_{1}, u, u_{2}) ∼ (x_{2}x_{1}; u_{2}, u_{1}) \end{matrix}

and (x_{1}x_{1}; u) ∼ (x_{1}x_{2}; u, u), for all u_{1}, u_{2}, and u in Λ(m). Generalising these examples, one can see that canonical representatives of (X • Y)(m) are given, up to a generalised form of α-conversion, by the tuples in an equivalence class which appear at the least stage n.

A monoid X = (X, μ, π) in F = (F, •, V) consists of a presheaf X, a unit π : V [figure]X, and a multiplication μ : X • X [figure] X such that the following diagrams commute.

\xymatrix{V • X \ar[r]^{π•id} \ar[dr]_{≅} & X • X \ar[d]^{μ} & X • V \ar[l]_{id•π} \ar[dl]^{≅} \\  & X}

\xymatrix{(X • X) • X \ar[d]_{μ•id} \ar[rr]^{≅} &  & X • (X • X) \ar[d]^{id•μ} \\ X • X \ar[r]_{μ} & X & X • X \ar[l]^{μ}}

The three isomorphisms in the above diagrams act as follows:

\begin{matrix}(i; u⃗) [figure] u_{i} , (t; 1, …, n) [figure] t , \\ ((t; u⃗); v⃗) [figure] (t; (u_{1}; v⃗), …, (u_{n}; v⃗)) . \end{matrix}

(Note that every equivalence class of X • V contains a tuple of the form (t; 1, …, n).)

The monoids in F, with morphisms f : (X, μ, π) [figure] (X′, μ′, π′) given by maps f : X [figure] X′ such that f ∘ μ = μ′ ∘ (f • f) and f ∘ π = π′, form a category Mon(F) with initial object V = (V, V•V ≅ V, id_{V}). Similarly, one defines the category Mon(C) of monoids in any monoidal category C = (C, ⊗, I).

Proposition 3.4 The categories of clones and of monoids in F = (F, •, V) are equivalent.

A program for simultaneous substitution. Let F be an endofunctor on a monoidal closed category C = (C, ⊗, I). If F has a strength st_{X,Y} : F (X) ⊗ Y [figure] F (X ⊗ Y), then its free algebras are also parametrically free with respect to ⊗. In particular, if F has a free algebra ϕ_{I} : F T I [figure] T I over I, then there is a unique map σ : T I ⊗ T I [figure] T I making the following diagram commutative

\xymatrix{F (T I) ⊗ T I \ar[d]_{ϕ_{I}⊗id} \ar[r]^{^{st^{T I,T I}}} & F (T I ⊗ T I) \ar[r]^{F σ} & F T I \ar[d]^{ϕ_{I}} \\ T I ⊗ T I \ar@{-->}[rr]_{σ} &  & T I \\ I ⊗ T I \ar[u]^{η_{I}⊗id} \ar[urr]_{≅}}

where η_{I} is the universal arrow corresponding to the free algebra T I. That is, σ is the unique (parametric) homomorphic extension of I ⊗ T I [figure: ∼] T I.

Proposition 3.5 Under the above hypotheses, T I = (T I, σ, η_{I}) is a monoid in C.

The adjunction (13) shows that F = (F, •, V) is closed. Moreover, endofunctors corresponding to first-order signatures are strong with respect to • in the obvious way; for instance, for binary operations, the strength maps (t_{1}, t_{2}; u⃗) to ((t_{1}; u⃗), (t_{2}; u⃗)). Moving on to binding signatures, one has to prove δ strong. This holds in the category V/F of pointed presheaves; indeed, δ restricts to an endofunctor on V/F (via up : Id [figure]δ) and it has a strength st_{X,Y} (m) : (δX • Y)(m) [figure] δ(X • Y)(m) which acts as follows,

(t; u⃗) [figure] (t; [up_{m}(u⃗), π_{new_{m}}^{(m+1)}]) ,

where π : V [figure]Y is the point of Y. In particular, the free Σ-algebra TV over V has a point η_{V} =^{def} var : V [figure] TV given by the insertion of the variables (mapping i to x_{i}). The above proposition then yields the following:

Corollary 3.6 Let Σ be a signature and let TV be its free algebra over V. Then (TV, σ, η_{V}) is a monoid in F, where σ : TV • TV [figure]TV is the unique homomorphic extension of V • TV [figure: ∼] TV.

The above σ is defined by structural recursion. For instance, for the λ-calculus σ : Λ • Λ [figure] Λ is defined as follows: for all (t; u⃗) in (Λ • Λ)(m),

σ_{m}(t; u⃗) = case t of

[figure: var(i); u_{i}]
[figure: lam(t′); lam( σ_{m+1}(t′; [up_{m}(u⃗), var(new_{m})] )]
\xymatrix{app(t_{1}, t_{2}) \ar@{=>}[r] & app( σ_{m}(t_{1}; u⃗), σ_{m}(t_{2}; u⃗) )}

Taking old_{n}(i) = i + 1 (1 ≤ i ≤ n) and new_{n} = 1 we get de Bruijn’s definition of substitution [9] for indices, while old_{n}(i) = i (1 ≤ i ≤ n) and new_{n} = n + 1 give the definition for levels.

Note that, in the absence of binding, the above specialises to the usual substitution. For instance, consider the expressions given by the grammar

e ∈ E ::= x | n | e_{1} plus e_{2} | e_{1} times e_{2} . (14)

The corresponding presheaf E is the carrier of the free algebra over V of the endofunctor Σ_{e}X =^{def} ℕ + X^{2} + X^{2} on F; its monoid multiplication σ_{E} : E • E [figure] E given by Proposition 3.6 is then the usual substitution of expressions (with contexts).

4 Initial algebra semantics

The key to initial algebra semantics for syntax with variable binding is the definition of a category of presheaves equipped with both a Σ-algebra and a monoid structure compatible with each other. Of course, we expect this category to have the free Σ-algebra TV with monoid structure given by Corollary 3.6 as an initial object.

For any strong endofunctor F on C = (C, ⊗, I), let F -Mon(C) be the category with objects given by F -monoids, i.e., quadruples X = (X, μ, π, h), where (X, μ, π) is a monoid in C and (X, h) is an F -algebra such that

\xymatrix{F (X) ⊗ X \ar[d]_{h⊗id} \ar[r]^{^{st^{X,X}}} & F (X ⊗ X) \ar[r]^{F μ} & F X \ar[d]^{h} \\ X ⊗ X \ar[rr]_{μ} &  & X} (15)

commutes; morphisms are maps of C which are both F -algebra and monoid homomorphisms.

Theorem 4.1 Let F, T I, σ, η_{I}, and ϕ_{I} be as in Proposition 3.5. Then T I = (T I, σ, η_{I}, ϕ_{I}) is an initial F -monoid.

This result, together with Corollary 3.6, ensures that we can take Σ-monoids as our category of models for a signature Σ; the type of terms TV is then the initial such model. We remark that Σ-monoids and the commutativity of the diagram (15) specialise, respectively, to the models and the uniformity condition given in [2].

We call the unique morphism TV [figure] 𝔐 from the initial Σ-monoid TV to a Σ-monoid 𝔐 the initial algebra semantics corresponding to 𝔐. By definition of morphism in Σ-Mon(F), it is compositional, it preserves the variables and it always satisfies the semantic substitution lemma [35, Lemma 4.6].

Consider, for example, the λ-calculus. For 𝔐 = (𝔐, μ, π, [abs, ·]) to be a Σ_{λ}-monoid the following should hold: for all d in 𝔐(n) and e⃗ in 𝔐(m)^{n},

μ_{m}(abs(d); e⃗) = abs(μ_{m+1}(d; [up(e⃗), π_{new_{m}}^{(m+1)}]) ,

μ_{m}(d_{1} · d_{2}; e⃗) = μ_{m}(d_{1}; e⃗) · μ_{m}(d_{2}; e⃗) .

The initial algebra semantics of the λ-calculus with respect to such a model 𝔐 is then the unique morphism [[ ]] : Λ [figure] 𝔐 such that:

[[λx.t]] = abs[[t]] , [[tu]] = [[t]] · [[u]] ,
[[x_{i}^{(n)}]] = [[π_{i}^{(n)}]] ,
[[t [u_{1}, …, u_{n}]]] = μ_{m}([[t]]; [[u_{1}]], …, [[u_{n}]]) .

In particular, one can easily verify that the model ⟨D, D⟩ for the λ-calculus defined at the end of Section 2 is a Σ_{λ}-monoid and that the corresponding initial algebra semantics is the desired one.

Another example is provided by the syntax for expressions in (14). For instance, one can take as model the clone of operations on the natural numbers ⟨ℕ, ℕ⟩, together with the canonical algebra structure Σ_{e}⟨ℕ, ℕ⟩ [figure] ⟨ℕ, ℕ⟩ given by addition and multiplication in ℕ. Again, it is easy to check that this forms a Σ_{e}-monoid. The corresponding initial algebra semantics E : E [figure]⟨ℕ, ℕ⟩ verifies, apart from compositionality and preservation of variables, the semantic substitution lemma for expressions:

E[[e[e_{1}, …, e_{n}]]] = E[[e]] ∘ ⟨E[[e_{1}]], …, E[[e_{n}]]⟩ .

Using substitution algebras instead of monoids one can define an equivalent category of Σ-substitution algebras consisting of quadruples X = (X, φ, ν, h), where (X, φ, ν) is a substitution algebra and (X, h) is a Σ-algebra such that

\xymatrix{Σ(δ(X)) × X \ar[r]^{^{str^{δX,X}}} \ar[d]^{≅}_{ψ_{X}×id} & Σ(δ(X) × X) \ar[r]^{Σφ} & ΣX \ar[dd]^{h} \\ δΣ(X) × X \ar[d]_{δh×id} \\ δ(X) × X \ar[rr]_{φ} &  & X}

commutes; morphisms are maps of F which are both Σ-algebra and substitution algebra homomorphisms.

Theorem 4.2 The categories of Σ-substitution algebras and Σ-monoids in F are equivalent.

5 A sketch of multi-sorted syntax

The above approach extends to multi-sorted signatures. In this extended abstract we shall only consider a special case which allows us to deal with two-sorted languages and a single type of variables. Examples are languages à la CCS [27] passing expressions along channels c ∈ C, with one sort given by expressions e ∈ E as in (14) and another sort (with expression variables only) given by process terms such as:

p ∈ Π ::= nil | p_{1} ∥ p_{2} | c?x.p | c!e.p | [e_{1} =e_{2}] p

(16)

There is thus a substitution of expressions in expressions e[e_{1}, …, e_{n}] and a substitution of expressions in process terms which we denote by p⌊e_{1}, …, e_{n}⌋. We can account for this as follows.

Every monoid M = (M, μ, π) in F defines a monad • M on F. The algebras of this monad give the desired form of two-sorted substitution. Formally, a ( • M)-algebra is a (right) action of the monoid M = (M, μ, π), i.e., a presheaf A and a map α : A•M [figure] A such that the following two diagrams commute.

\xymatrix{A • M \ar[d]_{α} & A • V \ar[l]_{id•π} \ar[dl]^{≅} \\ A}

\xymatrix{(A • M) • M \ar[d]_{α•id} \ar[rr]^{≅} &  & A • (M • M) \ar[d]^{id•μ} \\ A • M \ar[r]_{α} & A & A • M \ar[l]^{α}}

Equationally, for all a in A(n), u⃗ in M(m)^{n}, and v⃗ in M(l)^{m},

\begin{matrix}α_{m}(a; π_{1}, …, π_{n}) = a , \\ α_{l}(α_{m}(a; u⃗); v⃗) = α_{l}(a; μ_{l}(u_{1}; v⃗), …, μ_{l}(u_{1}; v⃗)) . \end{matrix}

Note the occurrence of μ in the second law.

For example, for objects A and B in a cartesian category C, the monoid ⟨A, A⟩ has a canonical action on ⟨A, B⟩ given by composition in C: for all f : A^{n} [figure] B and g_{i} : A^{m} [figure] A,

(f; g_{1}, …, g_{n}) [figure] f ∘ ⟨g_{1}, …, g_{n}⟩ .

For A = B, this specialises to the clone of operations on A. In particular, we have an action ⟨ℕ, P⟩ • ⟨ℕ, ℕ⟩ [figure] ⟨ℕ, P⟩ for any set P.

One can form the category Act(F) of monoid actions in F; the morphisms

(f, g) : (A • M [figure: α] A) [figure] (A′ • M′ [figure: α′] A′)

are pairs of maps f : A [figure] A′ and g : M [figure] M′ such that g is a monoid morphism and f ∘α = (α′•g)∘f. In the vein of the previous section it is natural to combine Σ-algebras h : ΣA [figure]A and actions α : A • M [figure] A by requiring that the diagram

\xymatrix{Σ(A) • M \ar[d]_{h•id} \ar[r]^{^{st^{A,M}}} & Σ(A • M) \ar[r]^{Σα} & ΣA \ar[d]^{h} \\ A • M \ar[rr]_{α} &  & A}

commutes. The corresponding category, with morphisms given by maps which are both Σ-algebra and action homomorphisms, is denoted by Σ-Act(F).

The analogue of Corollary 3.6 for actions can be established by observing that for every M-action α : A • M [figure]A, the compos-

ite \xymatrix{ΣA • M \ar[r]^{^{st^{A,M}}} & Σ(A • M) \ar[r]^{Σα} & ΣA} is also an M-action. This means that st is a distributive law which lifts Σ to an endofunctor Σ̃ on Act(F) such that its category of algebras Σ̃-Alg is exactly Σ-Act(F). Therefore, the forgetful functor Σ-Act(F) [figure] Act(F) has a left adjoint

F Σ̃ : Act(F) [figure] Σ-Act(F) .

If ϕ_{A} : ΣT A [figure]A is the free Σ-algebra over A and η_{A} : A [figure] T A is the corresponding universal arrow, F Σ̃ maps an M-action α : A • M [figure] A to the unique parametric homomorphism γ extending the composite η_{A} ∘ α : A • M [figure] T A; that is,

\xymatrix{Σ(T A) • M \ar[d]_{ϕ_{A}•id} \ar[r]^{^{st^{T A,M}}} & Σ(T A • M) \ar[r]^{Σγ} & ΣT A \ar[d]^{ϕ_{A}} \\ T A • M \ar@{-->}[rr]_{γ} &  & T A}

For example, consider the presheaf Π of process terms corresponding to (16), i.e., the initial algebra Σ_{p}Π ≅ Π of the endofunctor

Σ_{p}X =^{def} 1 + X^{2} + C × δX + C × E × X + E^{2} × X .

Then F Σ̃_{p} maps the initial action 0•E [figure: ∼] 0 of the monoid of expressions E to the following Σ_{p}-action (initial in the fiber of Σ_{p}-actions over E):

\xymatrix{Σ_{p}Π • E \ar[d]_{≅} \ar[r]^{^{st^{Π,E}}} & Σ_{p}(Π • E) \ar[r]^{Σ_{p}γ} & Σ_{p}Π \ar[d]^{≅} \\ Π • E \ar@{-->}[rr]_{γ} &  & Π}

Writing p⌊e⃗⌋ for γ_{m}(p; e⃗), the fact that γ is an E-action amounts to the identities:

p⌊x_{1}^{(n)}, …, x_{n}^{(n)}⌋ = p ,

p⌊e⃗⌋⌊d⃗⌋ = p⌊e_{1}[d⃗], …, e_{n}[d⃗]⌋ .

We do not expand on the corresponding initial algebra semantics here. Let us just remark that one can consider a Σ_{p}-action of ⟨ℕ, ℕ⟩ over ⟨ℕ, P⟩, where P is the final solution in Set of the domain equation X ≅ B(X), for a suitable behaviour endofunctor B. The initial algebra semantics D : Π [figure] ⟨ℕ, P⟩ is the intended semantics of the language and it satisfies, besides compositionality, the identity

D[[p⌊e_{1}, …, e_{n}⌋]] = D[[p]] ∘ ⟨E[[e_{1}]], …, E[[e_{n}]]⟩ .

Another example where Σ-actions can be used is the π-calculus [28]: its substitution can be seen as an action of the initial monoid V (of names/variables) on the syntax.

Our exposition focussed on simultaneous substitution, however single-variable substitution can also be treated in this setting. This is achieved by taking M to be a substitution algebra and by considering maps of type δA × M [figure] A verifying evident variants of the axioms 2, 3 and 4 for substitution algebras.

Acknowledgements. We are grateful to John Power especially for his suggestion of working with algebras over presheaves.

References

[1] P. Aczel. A general Church-Rosser theorem. Unpublished manuscript, 1978.

[2] P. Aczel. Frege structures and the notions of proposition, truth and set. In J. Barwise et al., editors, The Kleene Symposium, pages 31–60. North-Holland, 1980.

[3] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1984. Revised edition.

[4] M. Barr and C. Wells. Toposes, Triples and Theories. Springer-Verlag, 1985.

[5] F. Borceux. Handbook of Categorial Algebra. Cambridge University Press, Cambridge, 1994.

[6] R. M. Burstall. Proving properties of programs by structural induction. The Computer Journal, 12(1):41–48, 1969.

[7] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[8] P. Cohn. Universal Algebra. Harper & Row, 1965.

[9] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381–391, 1972.

[10] J. Despeyroux, F. Pfenning, and C. Schuermann. Primitive recursion for higher-order abstract syntax. LNCS, 1210, 1997.

[11] M. Fiore, E. Moggi, and D. Sangiorgi. A fullyabstract model for the π-calculus. In Proc. Eleventh IEEE Symp. on Logic In Computer Science, 1996.

[12] M. P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations Series. Cambridge University Press, 1996.

[13] J. Goguen. What is unification? In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Equations, Vol. 1, Algebraic Techniques, pages 217–261. Academic Press, 1989.

[14] J. Goguen, J. Thatcher, and E. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R. Yeh, editor, Current Trends in Programming Methodology, volume IV, pages 80–149. Prentice Hall, 1978.

[15] M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.

[16] A. Joyal. Foncteurs analytiques et espèces de structures. In Combinatoire énumerative, volume 1234 of Lecture Notes in Mathematics, pages 126– 159. Springer Verlag, 1987.

[17] W. Kahl. Relational treatment of term graphs with bound variables. Logic Journal of the IGPL, 6(2):259–303, 1998.

[18] G. Kelly. An abstract approach to coherence. In Coherence in Categories, volume 281 of Lecture Notes in Mathematics, pages 106–147. Springer-Verlag, 1972.

[19] G. Kelly. Clubs and data-type constructors. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 163–190. Cambridge University Press, 1992.

[20] J. W. Klop. Combinatory Reduction Systems. PhD thesis, University of Utrecht, 1980. Published as Mathematical Center Tract 129.

[21] P. Landin. A λ-calculus approach. In Advances in Programming and Non-Numerical Computation, pages 97–141. Pergammon Press, 1966.

[22] S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic: a first introduction to topos theory. Universitext. Springer-Verlag, 1992.

[23] J. McCarthy. Towards a mathematical science of computation. In IFIP Congress 1962, pages 21– 28. North-Holland, 1963.

[24] R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 434–445, Warsaw, Poland, 29 June–2 July 1997. IEEE Computer Society Press.

[25] D. Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Informal Proceedings of the Logical Frameworks BRA Workshop, June 1990. Available as UPenn CIS technical report MS-CIS-90-59.

[26] D. Miller and G. Nadathur. A logic programming approach to manipulating formulas and programs. In S. Haridi, editor, IEEE Symposium on Logic Programming, pages 379–388, San Francisco, Sept. 1987.

[27] R. Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer-Verlag, 1980.

[28] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1–77, Sept. 1992.

[29] T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 342–349, 1991.

[30] B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf type theory: an introduction. Clarendon, 1990.

[31] F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the SIGPLAN ’88 Symposium on Language Design and Implementation, Atlanta, Georgia, pages 199–208. ACM Press, 1988.

[32] G. Plotkin. An illative theory of relations. In R. Cooper et al., editors, Situation Theory and its Applications, number 22 in CSLI Lecture Notes, pages 133–146. Stanford University, 1990.

[33] D. Scott. The lattice of flow diagrams. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pages 311–366. Springer-Verlag, Berlin, 1971.

[34] D. Scott. Relating theories of the λ-calculus. In J. Hindley and J. Seldin, editors, To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism, pages 403–450. Academic Press, 1980.

[35] R. Tennent. Semantics of Programming Languages. Prentice Hall, New York, 1991.

[36] D. Turi and G. Plotkin. Towards a mathematical operational semantics. In Proc. 12^{th} LICS Conf. IEEE, Computer Society Press, 1997.

[37] S. Yong. A Framework for Binding Operators. PhD thesis, LFCS, Edinburgh, 1992.