Free Σ-monoids:
A Higher-Order Syntax with Metavariables
Makoto Hamana
Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp

Abstract. The notion of Σ-monoids is proposed by Fiore, Plotkin andTuri, to give abstract algebraic model of languages with variable binding
and substitutions. In this paper, we give a free construction of Σ-monoids.
The free Σ-monoid over a given presheaf serves a well-structured term
language involving binding and substitutions. Moreover, the free Σ-monoid
naturally contains interesting syntactic objects which can be viewed as“metavariables” and “environments”. We analyse the term language ofthe free Σ-monoid by relating it with several concrete systems, especiallythe λ-calculus extended with contexts.

1

Introduction

In theory of programming languages, we often use some extension of the λcalculus. When we develop such a theory, we usually use a formal language
consisting of both λ-calculus and its meta-language. For example, when we write
like “for a term λx.M · · · ”, this “M ” is a metavariable denoting some λ-term
and is not a (object) variable of the λ-calculus. Since we can also instantiate
this M by substitution at the meta-level, we can see that an operation similar tothe β-reduction also happens at the meta-level. Sato et al. proposed a series of
λ-calculi that formalises both the object-level and such a notion of meta-levels[SSB99, SSK01, SSKI03].
A natural question is what is a good semantics of such a kind of calculus,
and clearly existing semantics of the λ-calculus has not covered this object/meta
features. This is an interesting mathematical problem. We also expect that it may
be a step to theoretical foundation of meta-programming features consideredin the traditional declarative languages (such as Lisp’s quote and backquote,
Prolog’s assert) and also revisited recently in the modern programming languages(such as MetaML, FreshML, Boost C++ Library etc.)
This paper shows that the notion of free Σ-monoids can provide a unified viewof the structure of object and meta-levels in syntax. The structure of Σ-monoids
is an abstract algebraic model of syntax with variable binding and substitutions
proposed by Fiore, Plotkin and Turi [FPT99]. Although the notion of meta-level
was originally not considered for Σ-monoids, we will see that the free constructionof them explored here can naturally induce the notions of object and meta-levels.
Moreover, the syntax extracted from the free Σ-monoids can be used to analyse
W.-N. Chin (Ed.): APLAS 2004, LNCS 3302, pp. 348–363, 2004.
c Springer-Verlag Berlin Heidelberg 2004°

Free Σ-monoids: A Higher-Order Syntax with Metavariables

349

and relate existing work on extensions of λ-calculus enriched by several new
constructs: contexts, metavariables, and environments.
Organisation and results. Our contribution of this paper is summarised asfollows.
(i). To give an explicit free construction MΣ of Σ-monoid (Sect. 3), and show it
is a monad (Sect. 4).
(ii). To show the free Σ-monoid MΣ X naturally has two-level substitution structure (Sect. 5.1):• the Σ-monoid multiplication β gives capture-avoiding substitution, and• the monad multiplication µ gives possibly capturing substitution.
(iii). The generators X of the free Σ-monoid can be seen as “metavariables” inthe sense of Sato et al. [SSKI03]. (Sect. 5.1).
(iv). To show a link between Plotkin’s staged variables [Plo00] and variables decorated with substitutions in contextual calculi [Tal93, Mas99, HO01, San98,
SSK01] via a Kan extension (Sect. 5.2, 5.3).
(v). The construct dxeht1 , . . . , tl i in the free Σ-monoid which is naturally arisenby the free construction can be seen as an “explicit environment” in thesense of Sato, Sakurai and Burstall [SSB99] (Sect. 5.4).
How to read the paper. This paper is based on the work on semantics ofabstract syntax with variable binding by Fiore el al. [FPT99] in the frameworkof categorical algebra. Basic knowledge of category theory is assumed for reading
Sect. 2-4, especially monoids, monads and algebras (e.g. [Mac71] Chap. VI, VII).
But the construction of free Σ-monoid (Sect. 3.1 (I)) is purely syntactic, so one
can understand it without the knowledge of category theory. Also, in Sect. 5,
we see how the notion of Σ-monoids gives a unifying point of view on various
syntactic manipulations and constructs, as variable binding, holes of contexts,
explicit environments, and substitution of object and meta-variables by terms.
So, the reader who is interested in these syntactic aspect can start from Sect. 5
after the preliminaries of Sect. 2.

2

Preliminaries

2.1

Matavariables and Object Variables

In this paper, we precisely distinguish “object-level variables” and “meta-levelvariables”. Before going to the main part, we firstly explain this distinction to
avoid confusion.
For example, consider the following λ-term in a certain mathematical context:
λa.λb.M a

350

Makoto Hamana

where M is a λ-term. At the level of text, this M is a meta-level variable “M ”.
The variable a itself is an actual object-level variable “a” 1 . Moreover, there isalso an important difference between metavariables and object variables in viewof substitutions. If we substitute a term bb for the (object) variable a in the above
term, this is actually impossible because usually we assume “capture-avoiding
substitutions” in the λ-calculus, i.e.
(λa.λb.M a)[a := bb] = (λa0 .λb.M a0 )[a := bb] = λa0 .λb.M a0 .
But the situation in the case of metavariables differs. If we want to substitute aterm bb for M , we have(λa.λb.M a){M 7→ bb} = λa.λb.(bb)awhere {− 7→ −} denotes a meta-level substitution. In this case, although the(object) variable b is captured by the binder, usually it does not matter.
If we view these phenomena at the extra meta-level (i.e. meta-meta-level),these two classes of variables are classified by the distinction of substitutions:capture-avoiding and possibly capturing. We use the notions of “object variables” and “metavariables” in this sense (cf. [SSKI03]) and use the following
terminology: metavariable or simply variable for the notion of metavariable, andobject variable for the notion of object-level variable.
We do not call “object variable” simply variable except for a particular casein this paper.
2.2

Binding Algebras

Now we are going to technical preliminary. We review the notion of binding
algebras by Fiore, Plotkin, and Turi. For detail, see [FPT99].
A binding signature Σ is consisting of a set Σ of function symbols with anarity function a : Σ → N∗ . A function symbol of arity hn1 , . . . , nl i, denoted byf : hn1 , . . . , nl i, has l arguments and binds ni variables in the i-th argument(1 ≤ i ≤ l).
Example 1. The signature of the λ-calculus has a function symbol λ of arity
h1i, viz. λ-abstraction with one argument and binding one variable, and function
symbol @ of arity h0, 0i, viz. application with two arguments and binding no variables. Hereafter, we refer to this signature as “the signature of the λ-calculus”.
The free Σ-monoid we will give in this paper consists of terms constructedby this kind of binding signature. For example, by using the construction rules(I) in Sect. 3.1, the term λ([1]ovar(1)) can be constructed. This is an encodingof the λ-term λx.x by the method of de Bruijn levels [FPT99], where [-] denotes
a binder and ovar(i) an object variable i.
1

Indeed, this can also be seen as a metavariable a denoting some object-level variable.
But assuming a itself is an object variable is simpler and there is no difference inreasoning about them (cf. [Pit03])

Free Σ-monoids: A Higher-Order Syntax with Metavariables

351

Let F be the category which has finite cardinals n = {1, . . . , n} (n is possibly 0) as objects, and all functions between them as arrows m → n. This is
the category of object variables by the method of de Bruijn levels (i.e. natural
numbers) and their renamings. The functor category SetF plays an central rolein this paper. The objects of it are functors F → Set and the arrows are naturaltransformations between them. An object A ∈ SetF is often called a presheaf .
We define the functor δ : SetF → SetF as follows: for L ∈ SetF , n ∈ F, ρ ∈arr F,(δL)(n) = L(n + 1), (δL)(ρ) = L(ρ + id1 ).
To a binding signature Σ, we associate the signature functor Σ : SetF → SetF
given byaYΣA ,
δ ni A.
f :hn1 ,...,nl i∈Σ 1≤i≤l

A Σ-binding algebra (or simply Σ-algebra) is a pair (A, α) consisting of a presheaf
A ∈ SetF and a map2 α = [fA ]f ∈Σ : ΣA - A called algebra structure, wherefA is an operation
fA : δ n1 A×. . .×δ nl A - A
defined for each function symbol f : hn1 , . . . , nl i ∈ Σ.
Define the presheaf V ∈ SetF by
V(n) = n;V(ρ) = ρ(ρ : m → n ∈ F).

In [FPT99], this V is called “the presheaf of variables”. More precisely, this Vmeans the presheaf of object variables.
Proposition 2. ([FPT99]) (SetF , •, V) forms a monoidal category [Mac71],
where the monoidal product is defined as follows. For presheaves A and B,a(A • B)(n) , (A(m)×B(n)m )/ ∼(1)m∈N

where ∼ is the equivalence relation generated by(t; uρ1 , . . . , uρm ) ∼ (A(ρ)(t); u1 , . . . , ul )for ρ : m → l ∈ F. The arrow part of A • B is defined by(A • B)(ρ)(t; u1 , . . . , ul ) , (t; B(ρ)(u1 ), . . . , B(ρ)(ul ))for ρ : n → k ∈ F. This is certainly well-defined because the equivalence relation∼ is preserved by the map (A • B)(ρ).
Here and throughout this paper, we use the following notation.
Notation 3. An element of A(m)×B(n)m is denoted by (t; u1 , . . . , um ) wheret ∈ A(m) and u1 , . . . , um ∈ B(m). A representative of an equivalence class in
A • B(n) is also denoted by this notation.
2[ ] denotes a copair of coproducts.

352

Makoto Hamana

3

Free Σ-monoids

Definition 4. Let Σ be a signature functor with strength st defined by a binding
signature. A Σ-monoid consists of a monoid object [Mac71] M = (M, η : V →M, µ : M • M → M ) in the monoidal category (SetF , •, V) with a Σ-binding
algebra α : ΣM → M such thatstΣµΣ(M ) • M - Σ(M • M ) - ΣM
α•M

?
M •M

µ

α
?
- M

commutes; a morphism of Σ-monoids (M, α) - (M 0 , α0 ) is a morphism in SetF
which is both Σ-algebra homomorphism and monoid morphism. This defines thecategory Σ-Mon of Σ-monoids.
Theorem 5. ([FPT99]) A free Σ-algebra TV over V is an initial Σ-monoid,
with the multiplication given in [Prop. 3.5 of [FPT99]]
A natural question is an existence of a free Σ-monoid . This means whether
is there a Σ-monoid which is freely generated from a given arbitrary X ∈ SetF
and has universality. TV is an example of it but is not a full answer because thisΣ-monoid is only generated3 from a particular presheaf.
Now, our aim is to give a free Σ-monoid, denoted by MΣ X, generated fromarbitrary X ∈ SetF . In the following, we explicitly construct it with substitution monoidal structure as a “language” equipped with the feature of variablebinding and substitutions. In contrast to V of the presheaf of object variables,
we will show that the presheaf X of generators is regarded as the presheaf ofmetavariables, which was not considered in [FPT99]. The actual situation will
be clear in Sect. 5.
Remark 6. Notice that the relationship between the notions of free Σ-algebra
and free Σ-monoid is not a simple implication. Namely, although TV is a freeΣ-algebra over V (equivalently, an initial V + Σ-algebra), it is not a free Σmonoid over V. Correctly, TV is a free Σ-monoid over 0 ∈ SetF of the empty
set functor, i.e. in our notation, TV = MΣ 0. This is easily checked because theexplicit construction of TV ([FPT99] Sect. 2) is the same as the construction (I)of MΣ X without using the rule (¨) (because of X = 0) below.
3.1

Construction

Let Σ be a binding signature and X an arbitrary presheaf in SetF . We constructthe Σ-monoid MΣ X by the following four steps and show that it is free.
3

See Remark 6.

Free Σ-monoids: A Higher-Order Syntax with Metavariables

353(I) The presheaf MΣ X. First we define the set M̄Σ X(n) indexed by n ∈ N by
the following construction rules (by starting from the first rule).
i ∈ V(n)ν(n)
ovar(i) ∈ M̄Σ X(n)f : hi1 , . . . il i ∈ Σ t1 ∈ M̄Σ X(n+i1 ) · · · tl ∈ M̄Σ X(n+il )fMΣ X (n)f ([n+1, . . . , n+i1 ]t1 , . . . , [n+1, . . . , n+il ]tl ) ∈ M̄Σ X(n)x ∈ X(l) t1 , . . . , tl ∈ M̄Σ X(n)(¨)
dxeht1 , . . . , tl i ∈ M̄Σ X(n)Note that any l ∈ N with X(l) 6= ∅ is possible to apply the rule (¨) because X
is a functor F → Set. So, l is possibly 0, i.e. if x ∈ X(0), dxehi ∈ M̄Σ X(n) for
all n ∈ N.
Notation 7. We often simply write dxe for dxehovar(1), . . . , ovar(l)i. Since thebinders are clear from the arity of function symbol f ∈ Σ, we often abbreviatef ([n+1, . . . , n+i]t1 , . . . , [n+1, . . . , n+l]tl ) as just f (t1 , . . . , tl ).
.
Define the equivalence relation = on M̄Σ X(n) generated by context (by function symbols in Σ) closure of “the axiom”.
dxehtρ1 , . . . , tρl i = dX(ρ)(x)e ht1 , . . . , tm i
(2)for every ρ : l → m ∈ F, x ∈ X(l), t1 , . . . , tm ∈ M̄Σ X(n) (so, for example,.
f (dxeht2 , t1 i) = f (dX(ρ)(x)e ht1 , t2 i)). The presheaf MΣ X ∈ SetF is defined by.
MΣ X(n) , M̄Σ X(n) / =, and for ρ : n → n0 ∈ F, the arrow part is defined bystructural induction (see Theorem 8):
MΣ X(ρ)(ovar(i)) = ovar(ρ(i))
MΣ X(ρ)(f (t1 , . . . , tl )) = f (MΣ X(ρ)(t1 ), . . . , MΣ X(ρ)(tl ))MΣ X(ρ)(dxeht1 , . . . , tl i) = dxehMΣ X(ρ)(t1 ), . . . , MΣ X(ρ)(tl )i.
The most important point of this construction is the invention of the rule(¨), and the related construct dxeht1 , . . . , tn i and axiom (2). Syntactic meaningsof this construct will be discussed in detail in Sect. 5. The idea of rule (¨) comesfrom a construction of free symmetric multicategory. If the reader is familiar withcategorical type theory, this rule may be able to be understood as the (formal)
composition of arrows with the principle of “substitution as composition”.
(II) Σ-algebra. MΣ X has the V + Σ-algebra structure[ ν, [fMΣ X ]f ∈Σ ] : V + (ΣMΣ X)- MΣ X

where the maps ν, fMΣ X are defined by the construction rule of the presheafM̄Σ X (the mappings from the upper to the lower in the construction rules).
Define the map σ : X • MΣ X → MΣ X by(x; t1 , . . . , tl )- dxeht1 , . . . , tl i354

Makoto Hamana.
This is well-defined because it maps a ∼-equivalnce class to a =-equivalnce class.
So this is also an algebra structure. Moreover, we can show the following.
Theorem 8. (MΣ X, [ ν, [fMΣ X ]f ∈Σ , σ ]) is an initial (V + Σ + X • −)-algebra.
Proof. This is proved by strandard argument of showing uniquness and structural induction.
utHence, we can use structual induction on terms of MΣ X (e.g. when we define
a map whose domain is MΣ X).
Remark 9. A (V +Σ+X •−)-algebra always satisfies “the axiom” (2) although
it is simply an algebra defined by an signature functor (i.e. it is not defined as a
(Σ, E)-algebra). This is because the functor X • − is defined by a quotient.

(III) Monoid. We construct the monoid (MΣ X, ν, β) in the monoidal category(SetF , •, V). The unit ν : V → MΣ X is already defined in (I). The multiplication
β : MΣ X •MΣ X → MΣ X is defined inductively as follows. Here, [n+1, . . . , n+k]t
is abbreviated as [n+~k]t.
a- MΣ X(n)β(n) :MΣ X(m)×MΣ X(n)m / ∼mβ(n)(ovar(i); ~t) = tiβ(n)(dxehs1 , . . . , sl i; ~t) = dxehβ(n)(s1 ; ~t), . . . , β(n)(sl ; ~t)i (x ∈ X(l))β(n)(f ([n+ i~1 ]s1 , . . . , [n+ ~il ]sl ); ~t)= f ([n+ i~1 ] β(n+i1 )(s1 ; upi (~t), ovar(n+1), . . . , ovar(n+i1 )), . . .
1(3)[n+ ~il ] β(n+il )(sl ; upil (~t), ovar(n+1), . . . , ovar(n+il ))where f : hi1 , . . . , il i ∈ Σ and ~t denotes t1 , . . . , tm , and the weakening map fromMΣ X(n) to MΣ X(n+i) is defined by upi , MΣ (idn +wi ) where wi : 0 → i. Thisis well-defined, and the naturality of β follows from the definitions of MΣ X(ρ).
The isomorphisms V • MΣ X ∼= MΣ X, MΣ X • V ∼= MΣ X, (MΣ X • MΣ X) •MΣ X ∼
M
X
•
(M
X
•
M
X)
of
monoidaredefinedby= ΣΣΣ(i; ~t) 7→ ti , (t; 1, . . . , l) 7→ t((s; ~t); ~u) 7→ (s; (t1 ; ~u), . . . , (tl ; ~u))The inverse mappings are obvious except for u `: MΣ X → V • MΣ X. This u isdefined by t 7→ (1; t) because in V • MΣ X(n) = m m×MΣ X(n)m / ∼, always(i; t1 , . . . , tl ) ∼ (1; ti )holds by taking ρ : 1 → m, 1 7→ i in the definition of ∼; thus u is an isomorphism.
The monoid laws are proved by induction on the terms in MΣ X.

Free Σ-monoids: A Higher-Order Syntax with Metavariables

355(IV) Σ-monoid. The remaining task is to show that the monoid (MΣ X, ν, β)makes the following diagram of Σ-monoid law commutative. The strength st is
the one defined in [FPT99].
stΣβΣ(MΣ X) • MΣ X - Σ(MΣ X • MΣ X) - ΣMΣ X
α • MΣ X?
MΣ X • MΣ X

βα?
- MΣ X

Instantiating this diagram at n ∈ F and chasing an element, this eventually
becomes the equality
β(n)(f ([n+ i~1 ]s1 , . . . , [n+ ~il ]sl ); ~t)= f ([n+ i~1 ] β(n+i1 )(s1 ; upi (~t), ovar(n+1), . . . , ovar(n+i1 )), . . .)1

In fact, this is true because it is nothing but the equation (3) 4 in the definitionof β. Hence, we have the following.
Proposition 10. (MΣ X, ν, β) is a Σ-monoid.
3.2

Universality

Definition 11. An assignment φ : X → A is a morphism of SetF whose target
A has a Σ-monoid structure (A, ν̃, β̃).
Then, this is extended to a Σ-monoid morphism φ∗ : MΣ X → A as follows.
MΣ X(n)ovar(i)f (t1 , . . . , tl )- A(n)- ν̃(n)(i)- fA (φ∗ (n+i1 )(t1 ), . . . , φ∗ (n+il )(tl ))dxeht1 , . . . , tl i- β̃(n)( φ(l)(x); φ∗ (n)(t1 ), . . . φ∗ (n)(tl ) )where f : hi1 , . . . , il i ∈ Σ. Checking this is certainly a Σ-monoid morphism isstraightforward.
Lemma 12.
Let φ : X → A and ψ : X → B be assignments. For a Σ-monoid morphism h : B → A
such that φ = h ◦ ψ in SetF , the right diagram
commutes in Σ-Mon.

MΣ X

ψ ∗-

@
@@
φ∗ R

B
h
?
A

Proof. Instantiating the diagram at n ∈ F, use induction on the structure ofterms.
ut
4This just expresses an inductive application of β, i.e. roughly, β(n)(f (s1 , . . . , sl ); ~t) =f (β(n + i1 )(s1 ; ~t), . . . , β(n + il )(sl ; ~t)).

356

Makoto Hamana

Finally, we show the Σ-monoid MΣ X has the following universality, whichmeans freeness.
Proposition 13.
Let A be a Σ-monoid and φ : X → A an
assignment. Then, there exists a unique Σmonoid morphism φ̂ that makes the right diagram commutative where η X (n) maps x to
dxe.

X

ηX
MΣ X
@@
@
φR

φ̂
?
A

Proof. Actually, such φ̂ exists by taking φ̂ = φ∗ . For uniqueness, take B = MΣ X
in Lemma 12.
ut
Theorem 14. (MΣ X, ν, β) is the free Σ-monoid over X ∈ SetF .
This universality can be rephrased as an adjunction:
Corollary 15. The functor U : Σ-Mon → SetF that forgets the Σ-monoid
structure has the left adjoint MΣ , i.e. there is an adjunction
F

Set ¾

4

MΣ ⊥
U

Σ-Mon

Free Σ-Monoid Construction is a Monad

By Corollary 15 and the basic theorem of category theory (every adjunction givesa monad [Mac71]), we know that U MΣ gives a monad on SetF . We state thiswith the usual identification regarding MΣ as the endofunctor U MΣ on SetF .
Theorem 16. (MΣ , η, µ) is a monad on SetF .
It is valuable to concretely describe this monad and show the theorem toknow the internal structure of the language given by the free Σ-monoid. So, in
this section, we explicitly show that MΣ gives a monad on SetF .
Functor. First, we describe the functor MΣ : SetF → SetF . In Sect. 3.1 (I),
we have defined the object part of MΣ by giving the construction of the freeΣ-monoid over a presheaf X. Now, we define the arrow part: for φ : X → Y ∈arr SetF , MΣ (φ) : MΣ X → MΣ Y is defined as follows:MΣ φ(n)(ovar(i)) = ovar(i)MΣ φ(n)(f (t1 , . . . , tl )) = f (MΣ φ(n + i1 )(t1 ), . . . , MΣ φ(n + il )(tl ))MΣ φ(n)(dxeht1 , . . . , tl i) = dφ(n)(x)ehMΣ φ(n)(t1 ), . . . , MΣ φ(n)(tl )iwhere f : hi1 , . . . , il i ∈ Σ.
Unit. The unit η : Id → MΣ is defined by η X (n) : X(n) → MΣ X(n), x 7→ dxe.

Free Σ-monoids: A Higher-Order Syntax with Metavariables

357

Multiplication. The multiplication µ : MΣ ◦ MΣ → MΣ is defined byµX (n) : MΣ (MΣ X)(n)ovar(i)f (t1 , . . . , tl )dseht1 , . . . , tl i

- MΣ X(n)- ovar(i)- f (µX (n + i1 )(t1 ), . . . , µX (n + il )(tl ))- β(n)(s; µX (n)(t1 ), . . . µX (n)(tl ))where f : hi1 , . . . , il i ∈ Σ, and s ∈ MΣ X(m), t1 , . . . , tl ∈ MΣ MΣ X(n).
Monad laws. We write M for MΣ for simplicity. The unit laws of the monad isproved straightforwardly by induction of terms in M X(n). The associative lawof the monad is also proved by induction, but more cumbersome. The associative
law at X ∈ SetF and n ∈ F isM M M X(n)M µX (n)-µM X (n)?
M M X(n)µX (n)M M X(n)µX (n)?
- M X(n)Namely, we need to prove the equationµX (n) ◦ M µX (n) (w) = µX (n) ◦ µM X (n) (w)(4)

for all w ∈ M M M X(n). We proceed by induction on the structure of w. The
cases w = ovar(i), f (~t) are straightforward chasing. The case w = dseh~ti is again
cumbersome. For simplicity, hereafter we omit subscripts and the component
parameter n of the natural transformations µ, β. By using M µ as an arrow partof the functor MΣ defined above, the equation (4) becomes
lhs = µ(M µ(dseh~ti)) = µ( dµ(s)ehM µ(~t)i )I.H.
= β( µ(s); µ(M µ(~t)) ) = β( µ(s); µµ(~t) ),rhs = µ( β(s; µ(~t)) ).

So, we need to proveβ( µ(s); µµ(~t) ) = µ( β(s; µ(~t)) ).

(5)

Conceptually, this means a commutation of the monoid multiplication β andthe monad multiplication µ. This point will be discussed with a relationship tocontextual calculi in Sect. 5.2. The equation (5) is proved again by induction on
the structure of s ∈ M M X(n). The case s = uh~v i is the most complicated case,but a careful equational calculation shows it. Hence, we have shown Th. 16.
A structure similar to this monoad MΣ and monoid MΣ X is also consideredby Ghani and Uustalu [GU03] from the viewpoint of combination of two signatures. They used finitary monads in the category [Set, Set]f of finitary functors,

358

Makoto Hamana

instead of monoids in SetF , to model substitutions. This finitary monad approachis equivalent to monoid approach in SetF used here because the equivalence of
categories [Set, Set]f ' SetF . Hence, our MΣ can also be seen as a structure
having monads in two-levels, i.e. it induces the monads on [Set, Set]f and on
Set.

5

Analysis on the Term Language of Free Σ-monoids

5.1

Multiplications as Substitution operations

An intuition of the multiplication µ of the monad MΣ is the operation that“erases” (or “collapse”) all the outermost brackets “d−e”. This operation canalso be considered as a substitution. Because, for example, performing the multiplicationµX (n)(f (dte)) = f (t)can be rewritten as “applying a substitution”µX (n)( f (d∗e){∗ 7→ t} ) = f (t)Here, the notation f (d e){ 7→ } is another representation of an element ofMΣ ◦ MΣ , which is a syntactic form of (suspended) substitution. Although we
can more rigorously define this identification, we keep this informal for simplicity.
There are two important properties of µ as substitution by this understanding. We state this:(i). µ performs a substitution of metavariables.
(ii). µ performs a possibly capturing substitution.
The above examples shows (i). Why this is metavariable substitution isthat the construct dte is considered as a metavariable in MΣ (MΣ X) (or ∗, t
are metavariables in MΣ X). In this case, the generators MΣ X is considered as
metavariables.
Interestingly and importantly, we see that µ has the property (ii). For example, we haveµX (0)( λ([1]dovar(1)e) ) = λ([1]ovar(1))
by using the signature of the λ-calculus given in Example 1. Here, the object
variable 1 is captured by the binder “[1]”.
Notice that this kind of capturing cannot happen in the case of the Σ-monoid
multiplication β : MΣ X • MΣ X → MΣ X. Consider a similar try:β( λ([1]ovar(1)); ovar(2) ).
This expresses that we want to replace the object variable ovar(a) inside λ withthe free object variable ovar(b). But actually the term is not well-formed, i.e.
(λ([1]ovar(1)); ovar(2)) 6∈ MΣ X • MΣ X(2).
Hence, we state the following by the definition of β and this observation:(iii). β performs a substitution of object variables.
(iv). β performs a capture-avoiding substitution.

Free Σ-monoids: A Higher-Order Syntax with Metavariables

5.2

359

Staged Variables and a Construction of a Presheaf ofMetavariables

We have obtained a construction of the free Σ-monoid MΣ X over X ∈ SetF andshown that MΣ is a monad. As a consequence, we can think of X as a kind of“variables” as in the case of first-order universal algebra.
But what is a presheaf X of variables? In the case of first-order universal
algebra, elements in the set X of generators can be just considered as syntactic
constants of variables. In the case of binding algebra, this is not so simple,
because X itself is a presheaf. One may guess that the component X(n) for eachn is a set of variables. This seems feasible but what is a concrete meaning ofa “variable” x in a particular component X(n) is still not clear, especially weshould know the meaning of the index n. Also, since X must be a functor, weneed to consider the functoriality of X.
A hint to answer this problem can be found in Plotkin’s “Metalanguage forprogramming with bound object variables” [Plo00]. He considered the notion of“staged variables” for this metalanguage. Let us see this notion by adapting it
for our term language. A variable x has a “stage” n that is a set {1, . . . , n} of
object variables, and it is denoted by x : n. A typing judgment
x:n `t:nmeans that as usual, t depends on a variable x, and also the term t depends only
on object variables in n. A staged variable x : n is a variable which means that
it is only instantiated by a term having free object variables from 1 to n. The
staged variables forms an N-indexed set X by setting x ∈ X(n) iff x : n.
An N-indexed set X is “almost” a presheaf in SetF . But clearly it is not
sufficient because it lacks the arrow part. So, we need to seek some canonicalway of constructing a presheaf X 0 ∈ SetF from an N-indexed set X of staged
variables.
Fortunately, there is a construction for it. The category of N-index sets canbe expressed as the presheaf category SetN (by considering N as a discrete
category). Thus, this problem can be abstracted to that of finding a constructionof a presheaf in SetF from a given presheaf in SetN . This can be obtained bya Kan extension. Namely, for the inclusion functor J, we have the left Kan
extension:
J N
F¡¡ LanJ X
¡
?ª
Set

X

We write this extension as X̂ ∈ SetF and calculate it as follows. By the coend
formula of the left Kan extension (where “·” denotes a copower) [Mac71] anddiscreteness of N, we have
Z k∈NaX̂(n) = (LanJ X)(n) = (F(Jk, −) · X(k))(n) =F(k, n)×X(k)
k∈N

360

Makoto Hamana

with the obvious arrow part. We use the last coproduct formula as a definitionof X̂ for a given N-indexed set X of staged variables.
5.3

Variables Decorated with Substitutions

Next, we consider syntactic meaning of “variables” in X̂(n). Now we know that
an element of X̂(n) is a pair (ξ, x) where x : k (i.e. x ∈ X(k)) and ξ : k → n ∈ F.
So, we use the notationxξ ∈ X̂(n)and call this syntactic construct a variable with renamer [Ham01, Ham03] whereξ is a renamer, because ξ is a renaming function on object variables.
By the term construction rule in Sect. 3.1 (I), the above variable with renamerxξ becomes the term.
dxξ e = dxξ ehovar(1), . . . , ovar(n)i = dxehovar(ξ1), . . . , ovar(ξk)i ∈ MΣ X̂(n).
where we are using “the axiom” (2). (In particular, if ξ : 0 → n, dxξ e = dxehi ∈MΣ X̂(n)). Hence, a variable with renamer is merely a particular form of theconstruct dxeh· · ·i. Or, one may call it a variable decorated with substitution.
One may seem that this is merely a semantically derived object, or this has no
actual computational usefulness. However, it is not true. The same syntactic construct, a variable decorated with substitution, has appeared in several extended
λ-calculus for computing with contexts [Tal93, Mas99, HO01, San98, SSK01](also, the same construct is appeared in the series of work based on Nominal
Logic [Pit03], e.g. “suspension” construct in [UPG03]). Their extensions of λcalculus with contexts have the feature of “hole variables” meaning holes of contexts. In these calculi, the notion of “holes decorated with substitutions” plays
an essential role to ensure commutativity of β-reduction and hole-filling operation. This problem will be clear by the following argument by Sands [San98] on
failure of naive extension of the λ-calculus with holes. Later, we will see that
this relates to the free Σ-monoid.
Consider the λ-calculus extended with the hole ¤ syntactically. If we consider
this extended λ-calculus naively, we have the following kind of reduction:(λx.¤)y →β ¤.
But this is not adequate, since filling the hole with x does not commute withthis β-reduction:(λx.¤)I- ¤β−red.

fill with x?
(λx.x)I- I
β−red.

6≡

fill with x
?
x

(6)

Notice that the operation of filling a hole allows the capture of the variable x by
the binder, which is the main feature of contextual calculi. The problem of theFree Σ-monoids: A Higher-Order Syntax with Metavariables

361

above non-commutativity is due to the fact that the reduction step “forgets” theterm I. So, the solution in contextual calculi is to syntactically decorate holes
with explicit substitutions, so that e.g.
(λx.¤)I →β ¤{I/x} .

(7)Then, by using this modified β-reduction, the above diagram commutes because
the both reductions go to I.
Interestingly, the above diagram has already appeared in this paper. In the
proof of monad law in Sect. 4, we encountered the equation (5)β( µ(s); µµ(~t) ) = µ( β(s; µ(~t)) ).
This is diagrammatically,(s; µ(~t)) ∈ M M X • M M X

β

µ•µ

?
MX • MX

β

- MMX
µ
?
- MX

and we have proved that it commutes. We claim that this is nothing but thecommutativity of the diagram (6). The reason is as follows. We have seen that
our metavariables allow possibly capturing substitution in Sect. 5.1. Namely,
our metavariables behave exactly the same as holes in contextual calculi. Thismeans that the substitution operation µ of metavariables can be seen as theoperation of filling holes. And since β-reduction is a replacement of object-levelvariables, it corresponds to the substitution of object variables by the monoid
multiplication β. Hence, the commutativity (5) of β and µ is the same as thediagram (6)5 . This means the diagram (6) is an instance of monad law of thefree Σ-monoid.
More concretely, Sands’ discussion can be formulated in our term language.
Assume the beta-axiom of the λ-calculus by using the binding signature of λcalculus:
λ([1]dM e)@dN e = β(dM e; dN e)
where metavariables M ∈ X(1) and N ∈ X(0). Then, using the metavariable∗ ∈ X(1), we haveλ([1]d∗e)@I = β(d∗e; I) = d∗ehIi.
By regarding the bound object variable 1 as x and the metavariable d∗e as ¤,this precisely corresponds to the reduction (7).
This is an interesting link between the notions used in the different areas. We
have seen that Plotkin’s notion of staged variables naturally induces the notionof decorated variables that has been used for computing with contextual holes.
5

So, our implicit intension of naming β the Σ-monoid multiplication is this similarity
to β-reduction. Notice also that β-reduction is a substitution of object-level variables.

362

5.4

Makoto Hamana

Explicit Environments

As we have seen, we can consider the Σ-monoid MΣ X as a “language” having thefeatures of binding, substitutions, and metavariables. It is not only practicallyshown, but also theoretically justified, i.e. it has the desired universal property(Th. 13). Hence, we summarise it formally:
Definition 17. A higher-order syntax with metavariables is specified by• a given binding signature Σ, and• an indexed set X(n) of staged variables6 for each n ∈ N.
The presheaf MΣ X̂ of terms` is constructed by the construction rules (I) in Section 3.1 where X̂(n) = k∈N F(k, n)×X(k). Then, terms are expressed as thefollowing BNF:
MΣ X̂(n) 3 t ::= ovar(i) | f (t1 , . . . , tl ) | dxeht1 , . . . , tl i
X(l) 3 x
where i ∈ n.
This syntax is standard7 except for the seemingly exotic constructdxeht1 , . . . , tl i. We call this construct an explicit environment which follows theterminology in Sato, Sakurai and Burstall’s λ-calculus with “explicit environments” [SSB99]. Namely, dxeht1 , . . . , tl i can be seen as a first-class representationof an environment (i.e. a list of (variable,value)-pairs).
Because the sequence part always means substitutes of object variables from
1 to l, informally a term dxeht1 , . . . , tl i meansdxe h1 7→ t1 , . . . , l 7→ tl i.
This is a “suspended” substitution because the substitution process does not
happen before instantiating the variable x. Our understanding is that a term
dxeht1 , . . . , tl i is an explicit environment having a “placeholder” d e that is named“x” and it waits for an actual term to evaluate (by the multiplication µ) underthe environment ht1 , . . . , tl i.
Acknowledgments. The discussion with Masahiko Sato on the role of metavariables in “calculi of metavariables” was an important step of this work; I would
like to thank him. I also thank Neil Ghani, and the anonymous referees for useful comments. This work is supported by the JSPS Grant-in-Aid for Scientific
Research (16700005).
6
7

These are metavariables.
By regarding ovar(i) as an object variable.

Free Σ-monoids: A Higher-Order Syntax with Metavariables

363

References[FPT99] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In
Proc. 14th Annual Symposium on Logic in Computer Science, pages 193–202,
1999.
[GU03] N. Ghani and T. Uustalu. Explicit substitutions and higher order syntax.
In Proceedings of 2nd ACM SIGPLAN Workshop on Mechanized Reasoning
about Languages with Variable Binding, MERLIN’03, pages 135–146, 2003.
[Ham01] M. Hamana. A logic programming language based on binding algebras. In
4th International Symposium on Theoretical Aspects of Computer Software(TACS 2001), LNCS 2215, pages 243–262, 2001.
[Ham03] M. Hamana. Term rewriting with variable binding: An initial algebra approach. In Proceedings of Fifth ACM-SIGPLAN International Conference
on Principles and Practice of Declarative Programming (PPDP2003), pages
148–159. ACM Press, 2003.
[HO01] M. Hashimoto and A. Ohori. A typed context calculus. Theoretical Computer
Science, 266:249–271, 2001.
[Mac71] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971.
[Mas99] Ian A. Mason. Computing with contexts. Higher-Order and Symbolic Computation, 12(2):171–201, 1999.
[Pit03] A. M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186:165–193, 2003.
[Plo00] G. Plotkin. Another meta-language for programming with bound names modulo renaming. In Winter Workshop in Logics, Types and Rewriting, HeriotWatt University, February 2000. Lecture slides.
[San98] D. Sands. Computing with contexts: A simple approach. In Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II),
volume 10 of Electronic Notes in Theoretical Computer Science, 1998.
[SSB99] M. Sato, T. Sakurai, and R. Burstall. Explicit environments. In In Proceedings of TLCA’99, LNCS 1581, pages 340–354, 1999.
[SSK01] M. Sato, T. Sakurai, and Y. Kameyama. A simply typed context calculus
with first-class environments. In 5th International Symposium on Functionaland Logic Programming (FLOPS 2001), LNCS 2024, pages 359–374, 2001.
[SSKI03] M. Sato, T. Sakurai, Y. Kameyama, and A. Igarashi. Calculi of metavariables. In Computer Science Logic and 8th Kurt Gödel Colloquium(CSL’03 & KGC), LNCS 2803, pages 484–497, 2003.
[Tal93] C. L. Talcott. A theory of binding structures and applications to rewriting.
Theoretical Computer Science, 112(1):99–143, 1993.
[UPG03] C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal unification. In Computer
Science Logic and 8th Kurt Gödel Colloquium (CSL’03 & KGC), LNCS 2803,
pages 513–527, 2003.