Principles for Functional Abstract Syntax

Thierry Despeyroux^{1}, André Hirschowitz^{2}

1 INRIA-Sophia Antipolis, B.P 93, F-06902 Sophia Antipolis Cedex, France

                    thierry.despeyroux@sophia.inria.fr

2 CNRS, URA 168, University of Nice, F-06108 Nice Cedex 2, France

                    andre.hirschowitz@sophia.inria.fr

Abstract In this paper, we give a new, categorical definition for firstorder and higher-order abstract syntax (that we call functional abstract syntax), and we state the corresponding induction, separation and recursion principles. We also present a practical application of functional abstract syntax by means of syntactical editing.

Introduction

As compared to concrete syntax, abstract syntax focuses on the tree structure of terms. Indeed, this structure is suited for "syntax-oriented" edition, as well as for semantics specification. It is also the relevant part of the syntax for metatheoretical reasoning about the object language: an omnipresent ingredient of such reasoning is the principle of induction on the tree structure, together with the companion separation and recursion principles.

Accordingly, trees play a central role in a generic programming environment like Centaur [1].

- Concerning edition: once an abstract syntax is declared, a corresponding editor is generated; this editor acts as client of a (generic) tree processor which receives terms (encoded as trees) together with commands or queries, and returns trees or booleans;

- Concerning semantics: the philosophy of "natural semantics" is precisely to specify semantics in terms of elementary (tree) constructions of the language;

- Concerning meta-level reasoning: from a syntax+semantics specification, a Coq file is generated, making available the desired induction and companion principles [15].

The trees concerned in the above processes may contain variables: substitution and unification are two fundamental and delicate operations on these trees.

Recent works on the semantics of programming languages and on proof development systems have shown the need to incorporate the notion of binding into abstract syntax, from which emerged what is called higher-order abstract syntax [13]. Higher-order abstract syntax has already been used in some systems such as λ-Prolog [10,11] or Elf [12]. In higher-order abstract syntax, objectlevel constructions are interleaved with basic meta-level constructions, namely abstraction and application. The corresponding tree structure for terms breaks bindings, and admits sub-trees with "free" variables.

In the present work, we study a slightly different tree structure for terms of a higher-order abstract syntax (that we call rather functional abstract syntax), which we claim better suited for a higher-level handling of the three above mentioned tasks of edition, semantics specification and meta-theoretical reasoning. The main feature of our higher-order (functional) trees is that they represent functions: bindings are inherited by sub-terms so that there are no free variables. Accordingly, each of our trees is labeled with a refined meta-level functional type: in low-level language, this functional type keeps track of the ordering of the variables, and of their types, especially in case of variables which eventually do not occur. In other words, our approach replaces low-level basic constructions (namely constructors of the syntax and variables) by their higher-order (functional) counterpart, which we call higher-order constructors and higher-order projections respectively, and which govern higher-order induction and companion principles suited for higher-order meta-theoretical reasoning. As for edition, we specify what should be a functional syntax-oriented editor.

All our definitions are settled in the language of categories. In particular, we start with a categorical definition of functional abstract syntax. Indeed, while some formal definitions of first-order abstract syntax are available (for example through order-sorted algebra in [5,4,8]), higher-order abstract syntax has been considered till now rather as a methodology. Note that abstract syntax as implemented in LF [6] for instance, avoids products by an extensive use of curryfication (as we plan to explain elsewhere, this is one main obstacle for the implementation of higher-order semantics in this system). Instead of mimicing this implementation, we reinsert products in the picture, linking tightly our definitions to the familiar framework of cartesian (closed) categories. Roughly speaking, we define an abstract syntax as a free cartesian (closed in the higher-order case) category. At this point, we had to select a precise notion or cartesian (closed) category, namely to decide for instance whether the product were defined (or commutative, or associative) up to isomorphism or strictly. Here we have departed from the usual track and experienced to identify canonically isomorphic objects as much as possible. Finally, we had to give a convincing definition for freeness of a CCC. For this we have followed a standard track, namely we have built a left-adjoint for a forgetful functor. The correspondence between cartesian closed categories and the semantics of typed λ-calculi has been widely studied (see for example [14]). This is because the notion of category captures and integrates perfectly the notions of function and application. Here we take these notions as fully understood, and build our notion of syntax upon them, thus selecting special kinds of CCCs.

In the study of a first-order abstract syntax, constant use is made of the induction, separation and recursion principles, which roughly say:

- what is true for the terminals and stable by the constructors is true for any term of the syntax

- two terms with different head constructors are different, as well as two terms with the same head constructor but different sons (in some place)

- in order to define a function on terms, it is sufficient to specify it on terminals, and to give, for each constructor, a recursion formula in terms of the sons and the value of the function on these sons.

The extension of these three principles to the higher-order case is not straightforward, because in this case, the sons are no more ground terms, but functional ones. Our approach is to consider the functional terms altogether, and to extend naturally the action of the constructors of our syntax to these functional terms. We call these extensions higher-order constructors and use them systematically to express our three principles. Since we consider functional terms, when de-structuring trees, we eventually meet bound variables. In our approach, these are functional constructions which we call higher-order projections and these are the second new ingredient in our three principles. We give special attention to the second-order case, which is the most usual, where we give alternative versions of the induction and recursion principles. These alternative principles are apparently weaker, but they have the advantage of being expressible “in ground terms”.

This paper does not give the proofs of the described properties. This may be done by giving an explicit description of the terms of the categories using trees of composable arrows as it is done in [9] p. 50 for strings of composable arrows.

After a first section devoted to our categorical definitions and three sections devoted to the above discussed principles in the first-order, second-order and general cases, we present what could be a practical application of functional abstract syntax by means of syntax-oriented editing.

1 Categorical Preliminaries

The definitions of FOAS (first-order abstract syntax) and HOAS (higher-order abstract syntax) need some preliminary definitions on graphs and categories.

1.1 First-Order Case

In the following, we will write “category” for what is usually called small category (objects from a set), and “Category” for categories that are not necessarily small.

A cartesian graph is a graph (see [9] p.10) whose set of vertices is a commutative monoïd (see [9] p.2). We say that a cartesian graph is free if so is the monoïd of its vertices. We will also call a free cartesian graph a factorial graph.

A morphism of cartesian graphs is a morphism of graphs which induces on vertices a morphism of monoïds. The Category FG of factorial graphs is included in the Category of cartesian graphs ([14]).

We will consider here that a cartesian category is a category with distinguished products (see [14] p.18).

We call factorial category a cartesian category X where the product makes obj(X) into a free commutative monoïd (in such a way that the categorical identification between A × B and B × A is the identity).

We call base of a factorial category X the set of indecomposable elements (that we call atomic) of obj(X) (The neutral element is not in the base.)

A morphism of factorial categories is a functor which induces on objects a morphism of monoïds such that the following diagram (of trifunctors) commutes:

[figure: Hom(X, A × B) ≃ Hom(X, A) × Hom(X, B); Hom(F (X), F (A × B)) =; Hom(F (X), F (A) × F (B)) →^{∼} Hom(F (X), F (A)) × Hom(F (X), F (B))]

The factorial categories form a Category FC and we have a forgetful functor FC → FG.

Proposition 1. This functor admits a left adjoint F_{FC} : G ⇒ F_{FC}(G).

Definition 2. If G is a factorial graph, we say that F_{FC}(G) is the first-order abstract syntax (FOAS) associated with G, and we call first-order abstract syntax (FOAS) any factorial category isomorphic to F_{FC}(G) for some factorial graph G.

We say that a factorial graph G is simple if the target of any of its arrows is a base object.

Proposition 3. Any FOAS is isomorphic to a FOAS associated with a simple graph.

Example Let P_{1}...P_{n} be a set of names (to be understood as type or phylum names), and consider a set names c_{1}, ..., c_{m} for arrows in the monoïd generated by the P_{i}’s :

c_{i} : P_{1}^{a_{i,1}} × ... × P_{n}^{a_{i,n}} → P_{b_{i}}

(to be understood as a set of operators given by their signatures). This form a simple factorial graph, and thus specifies a FOAS.

The objects of this category correspond to the terms (trees) of the abstract syntax. Ground terms are objects of type P_{1}^{0} × ... × P_{n}^{0} → P_{j} for some j.

To fix ideas, let us take the set of names {Nat} containing only one element, and the three operators

zero : Nat^{0} → Nat

succ : Nat → Nat

plus : Nat^{2} → Nat

We write s(zero) a ground term of the category of type Nat^{0} → Nat. λa:Nat.plus(a,s(zero)) is a functional term (also called scheme) of type Nat → Nat. With our representation of FOAS, the sons of a functional term are themselves functional; in the present example λa:Nat.a and λa:Nat.s(zero).

1.2 Higher-Order Case

For the higher-order case, the structure of monoïd is not sufficient. We call higher-order monoïd (HO-monoïd) a commutative monoïd (E, ×, 1) endowed with a second composition law → satisfying the four following conditions:

A → (B × C) = (A → B) × (A → C)
B → (C → A) = (B × C) → A
1 → A = A
A → 1 = 1.

A morphism of HO-monoïds is a morphism of monoïds which also respects the second law. HO-monoïds form a Category HOM and the forgetful functor HOM → Sets admits a left adjoint functor F_{HOM}.

We call free HO-monoïd a HO-monoïd isomorphic to F_{HOM}(S) for some set S. We call base of a free HO-monoïd the (unique) minimal set of generators and we say that elements of the base are atomic.

In a HO-monoïd M there is a notion of normal form: any element of M different from 1 and from the atomic elements decomposes in a unique way (up to order) as a product of indecomposable (for ×) elements, and any indecomposable element can be expressed in a unique way as U → V with V atomic [2].

We call factorial closed graph a graph whose set of vertices is a HOmonoïd.

A morphism of factorial closed graphs is a morphism of graphs which induces on vertices a morphism of HO-monoïds.

Factorial closed graphs form a Category FCG.

A cartesian closed category is a cartesian category with (distinguished) exponentiation (see [9] p.95).

A factorial closed category is a cartesian closed category X where product and exponentiation make objects(X) into a free HO-monoïd in such a way that the four structural (Yoneda) isomorphisms between:

A → (B × C) and (A → B) × (A → C);
B → (C → A) and (B × C) → A;
1 → A and A;
A → 1 and 1;

are identities.

A morphism of factorial closed categories is a morphism of factorial categories which induces on objects a morphism of HO-monoïds such that the following diagram commutes:

[figure: Hom(A × B, C) →^{∼} Hom(A, B → C); Hom(F (A), F (B → C)) =; Hom(F (A) × F (B), F (C)) →^{∼} Hom(F (A), F (B) → F (C))]

Factorial closed categories form a Category FCC with a forgetful functor U : FCC → FCG.

Proposition 4. This functor admits a left adjoint F_{FCC}.

The proof produces for each factorial closed graph a concrete category made of (higher-order) trees. We will meet again these trees later on.

Definition 5. If G is a factorial closed graph, we say that F_{FCC}(G) is the higher-order abstract syntax (HOAS) associated with G, and we call higherorder abstract syntax (HOAS) any factorial closed category isomorphic to F_{FCC}(G) for some factorial closed graph G.

We say that a factorial closed graph G is simple if the target of any of its arrows is atomic.

Proposition 6. Any HOAS is isomorphic to a HOAS associated with a simple factorial closed graph.

In a HOAS, we thus have atomic objects and base arrows: these are the images of arrows of G by the unit of adjunction ([9] p.81). The target of each of them is an atomic object.

We say that an abstract syntax is effective iff it contains an arrow of type 1 → L_{i} for every atomic type L_{i}.

We say that an abstract syntax is extensional iff it contains at least two arrows from the final object 1 to L for every atomic object L. For example, the abstract syntax defined by z : L is not extensional because the two (different) terms λx.x and λx.z are equal when applied to the only element z of the syntax.

For an extensional abstract syntax C, the functor T → Hom(1, T) from C to Sets is faithful, thus in this case, C is a concrete category (see [9] p.26). This statement may be called extensionality principle.

1.3 Vocabulary

In the syntactical terminology, objects are called types. The base arrows are called constructors. Morphisms from A to B, with atomic B are called terms of type A → B . We call terminal any constructor of type 1 → L with L atomic.

We say that terms of type 1 → L (with L is atomic) are ground (or closed), and we also say that they have type L.

1.4 Examples

We consider a factorial closed graph with one single atomic type {Exp} and three constructors:

lambda : (Exp → Exp) → Exp

apply : Exp^{2} → Exp

zero : Exp^{0} → Exp.

For instance, λa:Exp.apply(lambda(λx:Exp.x), a) is a term of type Exp → Exp, and the son of its first son is a function of two arguments: λa,x:Exp.x.

Higher-order abstract syntax has mainly been used to express the semantics of languages based on a λ-calculus. However it can be used also for imperative languages as shown in the following example.

Consider a language with instructions, expressions and (integer) variables. The base of types is {Inst, Exp, V ar}, and let us define the following operators:

decl : (V ar → Inst) → Inst

assign : V ar × Exp → Inst

plus : Exp^{2} → Exp

var : V ar → Exp

zero : Exp^{0} → Exp

The functional tree representation of the program “declare X; X=X+0” will

be decl(λa:Var.assign(var(a),plus(var(a),zero))). Note that in this ex-

ample there is no operator of type V ar. Thus, only an object variable previously declared by means of the decl operator can be used in the instruction. This feature can be used for syntactical editing as explained in the last section.

2 FOAS (First-Order Abstract Syntax)

2.1 Setting

In this section we review what are the main features of first-order abstract syntaxes, with respect to induction, separation (injection), extensionality, unification and recursion. As far as open terms are concerned, induction, separation and recursion involve the functional counterparts of variables, namely projections.

Thus, we consider a FOAS S, with its set T (S) = T of atomic types, and its set C(S) = C of constructors. We also have its set of arities A(S) = A, that is to say the set of applications with finite support from T to N. We denote by N the set of non-negative integers, and for n such an integer, we write \underline{n} for the interval [1, ..., n] (if n = 0 the interval is empty).

For any arity a ∈ A, we denote by T^{a} the corresponding object in S, namely Π_{t∈T} t^{a(t)}, as well as the corresponding set of (closed) terms. For instance if T consists of the two elements nat and bool, and if a(nat) = 2 and a(bool) = 1, then T^{a} is simply nat^{2} × bool. Furthermore we denote by T_{a}^{t} the set of morphisms from T^{a} to t. More generally, for b another arity, we denote by T_{a}^{b} the set of morphisms from T^{a} to T^{b}. Notice that each type is of the form T_{a}^{b}.

The set C is equipped with the two maps dom, from C to A, and codom, from C to T . Finally, we have the set of projections P(S) = P: this one too is equipped with the two maps dom, from P to A, and codom, from P to T , and we denote by C_{a} (resp. P_{a}) (resp. C_{a,t} (resp. P_{a,t})) the subset of C (resp. P) of elements with domain a (resp. with domain a and codomain t).

2.2 Induction Principles

Already for a FOAS, we have two induction principles, one for closed and one for functional terms.

Proposition 7. (closed FO induction principle) Let B a collection indexed by T of sets B_{t}, B_{t} being a subset of t. For a an arity, we set B^{a} := Π_{t}(B_{t})^{a(t)}.

We suppose that B is stable by all the constructors, more precisely if C_{c} is a constructor mapping T^{a} to t, then it sends B^{a} into B_{t};

Then, for every t, B_{t} is the whole t.

The induction principle allows inductive proofs on FOAS: if a property is stable by composition with the operators of the syntax, then it is verified by all the closed terms of the syntax. In particular, it allows inductive proofs concerning a single type (or any set of types) of the syntax: just extend the desired property from the concerned type(s) to all types, by declaring that it is true for non concerned types.

For the open induction principle, we need to introduce the second-order constructors. For each constructor C_{c} mapping with domain d and codomain t and each arity a, we denote by C_{c}^{a} the corresponding map from T_{a}^{d} into T_{a}^{t}, and we call it a second-order constructor of the syntax.

Proposition 8. (open FO induction principle) Let B a collection indexed by A × T of sets B_{a}^{t}, B_{a}^{t} being a subset of T_{a}^{t}.

We suppose that

(i) B contains the projections, more precisely if a projection p ∈ P is in T_{a}^{t}, then it is in B_{a}^{t}.

(ii) B is stable by all second-order constructors, more precisely if C_{c}^{a} is a second-order constructor mapping T_{a}^{d} to T_{a}^{k}, it sends B_{a}^{d} to B_{a}^{k}.

Then, for each arity a and atomic type t B_{a}^{t} is the whole T_{a}^{t}.

The open induction principle is stronger than the closed one in this sense that any property of closed terms which can be proved by the latter can be extended to be true by definition on open terms and proved by the former. For the other way around, there is no such a trivial reduction. One way to connect properties of open terms to the domain of the closed induction principle is to prove that they are extensional: the property P is extensional if for any term x of type ΠA_{i} → A, with atomic A_{i}’s, P (x) holds if and only if, for any collection (x_{i}) of closed terms of types (A_{i}) satisfying the collection of conditions (P (x_{i})), P (x((x_{i})) holds.

2.3 Separation Principles

Proposition 9. (closed separation principle): Let A_{1} and A_{2} be two ground terms of a FOAS such that A_{j} = C_{j} ∏_{i=1}^{n_{j}} x_{i,j}, where C_{1} and C_{2} are constructors and the x_{i,j} are ground terms. Then A_{1} = A_{2} iff C_{1} = C_{2}, n_{1} = n_{2}, and ∀i ∈ [1, n_{1}], x_{i,1} = x_{i,2}.

Together with the closed induction principle, the closed separation principle endows each closed term with a tree structure, through a well defined head constructor and well-defined sons.

In order to state the open separation principle, we need to identify more carefully the projections.Among morphisms in T_{a}^{t}, we have projections: these are labelled by \underline{a}(t). Thus projections are parametrized by the set Θ of triples θ = (a, t, k) where a is an arity, t is an atomic type, and k is an element of \underline{a}(t).

Proposition 10. (open separation principle) Let A_{1} and A_{2} be two terms of a S such that A_{j} = C_{c_{j}}^{a} ∏_{i=1}^{n_{j}} x_{i,j}, where the c_{j} are in C and the x_{i,j} are terms. Then A_{1} = A_{2} iff c_{1} = c_{2}, n_{1} = n_{2}, and ∀i ∈ [1, n_{1}], x_{i,1} = x_{i,2} (this concerns in particular terminal constructors, for which n_{j} is zero). Furthermore, such a term with a head constructor cannot be equal to a projection; and two projections p_{θ} and p_{θ′} are equal if and only if the two triples θ and θ′ are equal.

Together with the open induction principle, the open separation principle endows each term with a first-order tree structure, through a well defined second-order head constructor and well-defined sons.

2.4 Recursion

The closed recursion principle reads as follows.

Proposition 11. (closed FO recursion principle) Given - a collection B of sets B_{t}, indexed by T;

- a collection M of maps M_{c} indexed by C, M_{c} mapping T^{dom(c)} × B^{dom(c)} into B_{codom(c)}, where B^{dom(c)} is defined as Π_{t∈T} B_{t}^{dom(c)(t)};

there exists a unique collection r := rec(B, M) of maps r_{t} indexed by T, r_{t} sending t into B^{t}, satisfying the collection indexed by C of reduction rules:

r_{codom(c)}(C_{c}((x_{t,k})_{k∈\underline{d}om(c)(t)})) = M_{c}((x_{t,k})_{k∈\underline{d}om(c)}, (r_{t}(x_{t,k}))_{k∈\underline{d}om(c)}).

The open recursion principle generates maps from sets of open terms instead of maps from sets of closed terms; and accordingly, it involves projections. It also involves what we call the second-order constructors: these are naturally associated with the constructors in the following way: il C_{c} has domain d and codomain k, and a is an arity, then the second-order constructor C_{c}^{a} is the map from T_{a}^{d} to T_{a}^{k} defined by composition with C_{c}.

Proposition 12. (open FO recursion principle) Given - a collection B, indexed by A × T of sets B_{a,t};

- a collection M, indexed by C × A of maps M_{a,c} sending T_{a}^{dom(c)} × B_{a}^{dom(c)} into B_{a,codom(c)}, where B_{a}^{b} stands for Π_{t∈T} B_{a,t}^{b(t)};

and in addition

- a collection M′, indexed by P of elements M′_{p}, with M′_{p} ∈ B_{dom(p),codom(p)}; there exists a unique collection r := rec(B, M) of maps r_{a,t} indexed by A×T ,

r_{a,t} sending T_{a}^{t} into B_{a,t}, satisfying the two collections of reduction rules: r_{a,codom(c)}(C_{c}^{a}((x_{t,k})_{k∈\underline{d}om(c)(t)})) = M_{a,c}((x_{t,k})_{k∈\underline{d}om(c)(t)}, (r_{a,t}(x_{t,k}))_{k∈\underline{d}om(c)(t)}) and r_{dom(p),codom(p)}(p) = M′_{p}.

Remark This recursion principle builds for each a a collection r_{a} of maps r_{a,t}, and all of these constructions are independent. This will no more hold true in the second-order case, to be considered next.

2.5 Unification

Definition 13. Two terms A and B of the same type unify iff there exists a term C called unifier of A and B such that A ∘ C = B ∘ C. A most general unifier is an equalizer (see [9] p. 70).

Proposition 14. (unification principle) If two terms unify, a most general unifier for these two terms exists.

3 SOAS (Second-Order Abstract Syntax)

3.1 Setting

In this section we review what are the main features of second- order abstract syntaxes. At first we focus on first-order terms of such a syntax.

Thus, we consider a SOAS S, with its set T^{0}(S) = T^{0} of atomic types, and its set C(S) = C of constructors. We also have its set of 0-arities A^{0}(S) = A^{0}, which is as above the set of applications with finite support from T^{0} to N. We also have the set T^{1} of first-order simple types: T^{1} is identified with A^{0} × T^{0}, by the pair of maps: (dom, codom). Note that T^{1} contains T^{0} embedded by t → (0, t). We then have the set A^{1} of 1-arities, which is as above the set of applications with finite support from T^{1} to N. Note that A^{1} contains A^{0} : zeroth-order arities may be extended by zero to become first-order arities.

For a a 0-arity, t an atomic type, and b a 1-arity, we use the notations T^{a} , T_{a}^{t} and T_{a}^{b} in the same way as above. Note that T_{a}^{b} decomposes in a single way as a product of simple first-order types of the form T_{a′}^{t′}.

Now the set C is equipped with the two maps dom, from C to A^{1}, and codom, from C to T^{0}, and the second-order constructors are defined in the following way: il C_{c} has domain d and codomain k, and a is a 0-arity, then the second-order constructor C_{c}^{a} is the map from T_{a}^{d} to T_{a}^{k} defined by composition with C_{c}.

Finally, we have the set of projections P^{1}(S) = P^{1}: this one too is equipped with the two maps dom, from P^{1} to A^{0}, and codom, from P^{1} to T^{0}, and we denote by C_{a} (resp. P_{a}) (resp. C_{a,t} (resp. P_{a,t})) the subset of C (resp. P) of elements with domain a (resp. with domain a and codomain t).

3.2 Induction Principles

For our SOAS S, we have at least two induction principles, one for closed and one for functional terms.

Proposition 15. (closed SO induction principle) Let B a collection indexed by T^{0} of sets B_{t}, B_{t} being a subset of t.

We suppose that for each constructor C_{c} the following holds: writing a for dom(c) and t for codom(c), for any collection f = (f_{θ,k})_{k∈\underline{a}(θ)}, with f_{θ,k}) ∈ T_{θ}, satisfying, for each (θ, k) with k ∈ \underline{a}(θ), writing b for dom(θ) and t′ for codom(θ), for any collection x = (x_{s,m})_{m∈\underline{b}(s)} in Π_{m∈\underline{b}(s)}B_{s}, f_{θ,k}(x) is in B_{t′}. Then, for each t ∈ T^{0}, B_{t} is the whole T_{t}.

Proposition 16. (open SO induction principle) Let B a collection indexed by T^{1} of sets B_{θ}, B_{θ} being a subset of θ.

We suppose that

(i) B contains the projections, more precisely if a projection p ∈ P is in T_{θ}, it is in B_{θ}.

(ii) B is stable by all the second-order constructors, more precisely if C_{t}^{a} is a second-order constructor sending T_{a}^{d} to T_{a}^{k} and if T_{a}^{d} = Π_{i}T_{θ_{i}}, then, for any family f = (f_{i})_{i} with f_{i} ∈ B_{θ_{i}}, C_{c}^{a}(f) is in B_{k}^{a}.

Then, for each θ ∈ T^{1}, B_{θ} is the whole T_{θ}.

The open induction principle is stronger than the closed one in this sense that any property of closed terms which can be proved by the latter can be extended to be true by definition on terms and proved by the former. For the other way around, there is no such a trivial reduction. One way to connect properties of open terms to the domain of the closed induction principle is to prove that they are extensional: the property P is extensional if for any term x of type ΠA_{i} → A, with atomic A_{i}’s, P (x) holds if and only if, for any collection (x_{i}) of closed terms of types (A_{i}) satisfying the collection of conditions (P (x_{i})), P (x((x_{i}))) holds.

3.3 Separation Principle

Proposition 17. (first-order separation principle): Let A_{1} and A_{2} be two (first-order) terms of our SOAS such that A_{j} = C_{j} ∏_{i=1}^{n_{j}} x_{i,j}, where the C_{j} are second-order constructors and the x_{i,j} are (first-order) terms. Then A_{1} = A_{2} iff C_{1} = C_{2}, n_{1} = n_{2}, and ∀i ∈ [1, n_{1}], x_{i,1} = x_{i,2} (This concerns in particular terminal constructors, for which n_{j} is zero). Furthermore, such a term with a head constructor cannot be equal to a projection; and two projections p_{θ} and p_{θ′} are equal if and only if the two triples θ and θ′ are equal.

3.4 Recursion

Proposition 18. (first-order SO recursion principle) Given - a collection B, indexed by A^{0} × T^{0} of sets B_{a}^{t};

- a collection M, indexed by the set A^{0} × C of second-order constructors, of maps M_{c}^{a} such that if C_{c}^{a} sends T_{a}^{d} = Π_{i}T_{a_{i}}^{k_{i}} into T_{a}^{k}, then M_{c}^{a} sends Π_{i}T_{a_{i}}^{k_{i}} × Π_{i}B_{a_{i}}^{k_{i}} into B_{a}^{k};

- a collection M′, indexed by P of elements M′_{p}, with M′_{p} ∈ B_{dom(p)}^{codom(p)};

there exists a unique collection r := rec(B, M, M′) of maps r_{a}^{t} indexed by A^{0} × T^{0}, r_{a}^{t} mapping T_{a}^{t} into B_{a}^{t}, satisfying the two collections of reduction rules:

for each C_{c}^{a} sending T_{a}^{d} = Π_{i}T_{a_{i}}^{k_{i}} into T_{a}^{k},

r_{a}^{k}(C_{c}^{a}((x_{i})_{i})) = M_{c}^{a}((x_{i})_{i}, (r_{a_{i}}^{k_{i}}(x_{i}))_{i}), and

r_{dom(p)}^{codom(p)}(p) = M′_{p}.

Remark This general principle has the weak feature that the arguments of the meta-level construction rec have a quite complicated nature (type). Here are some tricks inspired by [3] for simplifying this nature. First we choose the collection of sets B_{a}^{t} in the following way: we first choose a collection D_{t} indexed by T^{0}, and we set B_{a}^{t} = T^{a} × D^{a} ⇒ D_{t} where D^{a} stands for Π_{t}D_{t}^{a(t)}. The presence of D^{a} in this formula offers a possibility to settle once and for all a (default) value for the images of projections:

r_{dom(p)}^{codom(p)}(p) = p,

where the right hand side refers to the projection corresponding to p from D^{a} to D_{t}. The presence of T^{a} in this formula offers similarly a possibility of giving a (default) formula for M_{c}^{a} in terms of a substitute m_{c}^{a} of type Π_{i}T_{k_{i}}Π_{i}B_{a′_{i}}^{k_{i}} into

B_{k}, where we have written a_{i} = a + a′_{i}, so that the type of C_{c} is Π_{i}T_{a′_{i}}^{k_{i}} → T_{k}.

Accordingly, the type of M_{c}^{a} may be written Π_{i}T_{a_{i}}^{k_{i}} × Π_{i}T^{a_{i}}Π_{i}B^{a} → B_{a′_{i}}^{k_{i}} ⇒ B_{a}^{k} and the default formula for M is

M_{c}^{a}((f_{i})_{i}, (x_{i})_{i}, (g_{i})_{i}) = [λz : B^{a}]m_{c}^{a}((f_{i}(x_{i}))_{i}, (g_{i}(z))_{i}).

Each of these two tricks may be used separately, with

B_{a}^{t} = D^{a} ⇒ D_{t}

or

B_{a}^{t} = T^{a} ⇒ D_{t},

so that all together we have three variants here.

3.5 Unification

Proposition 19. (unification principle) If two terms unify, a most general unifier for these two terms exists.

Remark This is not the usual first-order unification principle but a slight variant. There is a corresponding algorithm.

4 General Case

4.1 Setting

Thus, we consider a general HOAS S, with its set T^{0}(S) = T^{0} of atomic types, and its set C(S) = C of constructors. We also have its set T of simple types, and its set of arities A which is the set of applications with finite support from T to N, and T is identified with A × T^{0}, by the pair of maps: (dom, codom). Note that T contains T^{0}, t being embedded as (0, t). For a an arity, t an atomic type, and b a 1-arity, we use the notations T^{a} , T_{a}^{t} and T_{a}^{b} in the same way as above. Note that T_{a}^{b} decomposes in a single way as a product of simple first-order types of the form T_{a′}^{t′}.

Now the set C is equipped with the two maps dom, from C to A, and codom, from C to T^{0}, and the higher-order constructors are defined in the following way: il C_{c} has domain d and codomain k, and a is an arity, then the higher-order constructor C_{c}^{a} is the (meta-level) map from T_{a}^{d} to T_{a}^{k} defined by composition with C_{c}.

Finally, we have the set of higher-order projections P(S) = P: this one too is equipped with the two maps dom, from P to A, and vcodom, from P to T (in vcodom, v stands for virtual). We denote by C_{a} (resp. P_{a}) (resp. C_{a,θ} (resp. P_{a,θ})) the subset of C (resp. P) of elements with domain a (resp. with domain a and codomain θ). The subset P_{a,θ} is naturally identified with \underline{a}(θ). Thus, for k ∈ \underline{a}(θ), we have a higher-order projection p_{a}^{θ,k} and we now explain what it is:

We first explain what it is not, namely the natural naive projection in T_{a}^{θ}, which we denote by p′_{a}^{θ,k}. Indeed, we prefer the following kind of "long η form". We write θ = T_{b}^{t} and we set

p_{a}^{θ,k} = [Λz : T_{a}^{b}][λx : T^{a}]p′_{a}^{θ,k}(x)(z(x)). Here Λ refers to the meta-level abstraction, while λ refers to the abstraction in our HOAS. So this ho-projection is a meta-level map sending T_{a}^{b} into T_{a}^{t}.

4.2 Induction principle

For a general HOAS S, there is a closed induction principle but its formulation is intricated and we turn directly to the following:

Proposition 20. (open HO induction principle) Let B a collection indexed by T of sets B^{θ}, B^{θ} being a subset of T^{θ}. If a is an arity and θ a simple type, we set B_{a}^{θ} = B^{θ′}, where θ′ = a → θ. If a and b are arities, we define B_{a}^{b} as Π_{θ}(B_{a}^{θ})^{b(θ)}. We suppose that

(i) B is stable by the ho-projections, more precisely if p_{a}^{θ,k} sends T_{a}^{b} into T_{a}^{t}, then it also sends B_{a}^{b} into B_{a}^{t}.

(ii) B is stable by the ho-constructors, more precisely if C_{t}^{a} is a ho-constructor sending T_{d}^{a} to T_{k}^{a},

then it also sends B_{a}^{d} into B_{a}^{k}.

4.3 Separation Principle

Proposition 21. (higher-order separation principle): Let A_{1} and A_{2} be two terms of our HOAS such that A_{j} = C_{j} ∏_{i=1}^{n_{j}} x_{i,j}, where the C_{j} are hoconstructors and the x_{i,j} are terms. Then A_{1} = A_{2} iff C_{1} = C_{2}, n_{1} = n_{2}, and ∀i ∈ [1, n_{1}], x_{i,1} = x_{i,2} (This concerns in particular terminal constructors, for which n_{j} is zero). Furthermore, such a term with a head constructor cannot be equal to an image by a ho-projection; and two such images p_{a}^{θ,k}(x_{1}, …, x_{n}) and p_{a′}^{θ′,k′}(x′_{1}, …, x′_{n′}) are equal if and only if a = a′, θ = θ′ and k = k′ (so that n = n′), and x_{1} = x′_{1} … x_{n} = x′_{n}.

4.4 Recursion.

Proposition 22. (HO recursion principle) Given - a collection B, indexed by T = A × T^{0} of sets B_{a}^{t};

- a collection M, indexed by the set A × C of ho-constructors, of maps M_{c}^{a} such that if C_{c}^{a} maps T_{a}^{d} = Π_{i}T_{a_{i}}^{k_{i}} into T_{a}^{k}, then M_{c}^{a} maps Π_{i}T_{a_{i}}^{k_{i}} × Π_{i}B_{a_{i}}^{k_{i}} into B_{a}^{k};

- a collection M′, indexed by P of maps M′_{p}: if p_{a}^{θ,k} maps T_{a}^{b} = Π_{i}T_{a_{i}}^{k_{i}} into T_{a}^{t}, then M′_{p} maps T_{a}^{b} × B_{a}^{b} into B_{a}^{t}, where B_{a}^{b} stands for Π_{i}B_{a_{i}}^{k_{i}},

there exists a unique collection r := rec(B, M, M′) of maps r_{t}^{a} indexed by A × T^{0}, r_{a}^{t} mapping T_{a}^{t} into B_{a}^{t}, satisfying the two collections of reduction rules:

for each C_{a}^{c}, mapping T_{a}^{d} = Π_{i}T_{a_{i}}^{k_{i}} into T_{a}^{k},

r_{a}^{k}(C_{c}^{a}((x_{i})_{i})) = M_{c}^{a}((x_{i})_{i}, (r_{a_{i}}^{k_{i}}(x_{i}))_{i})

and, for each ho-projection p = p_{a}^{θ,k}, mapping T_{a}^{d} = Π_{i}T_{a_{i}}^{k_{i}} into T_{a}^{k},

r_{a}^{k}(p((x_{i})_{i})) = M′_{p}((x_{i})_{i}, (r_{a_{i}}^{k_{i}}(x_{i}))_{i}).

4.5 Unification

There is no most general unifier in general. However there are some weaker solution for this problem.

5 Editing Higher-Order Terms

Up to now, higher-order abstract syntax has been used only to specify the semantics of programming languages, in particular for functional ones. The goal of this section is to describe how it can be used for very practical applications, as syntactical editing.

The goal of syntactical editing is to guarantee at any time that a program that is edited is syntactically correct. The abstract syntax definition can be used to generate a menu driven mode that will help the user to construct and modify programs. In Centaur [7], a first-order abstract syntax and a notion of metavariable are used to achieve this goal. At any place in an abstract tree the user can be prompted with a list of operators or transformation rules of the correct type. This is completely independent of the context and can be done completely locally. The limit of this technique is reached when one wants to edit a leaf of a program, for example an identifier. One would like, for example to be prompted with the list of objects that are accessible, taking into account the scope rules of the language. But this is not possible since with first-order abstract syntax the notion of scope is part of the semantic specification.

Integrating the notion of binder in the syntax of a programming language can improve this aspect of editing. Our goal in this section is to describe the basic actions of editing in the context of an higher-order abstract syntax. To fix ideas, we will use the previous Exp example, and for simplicity we will forget in the following the type of the arguments (which will be always Exp). In the following example, some pieces of the text are in boldface to enhance our notion of selection.

Selection: Giving a term and a legal path we can select a sub-term of this term. Note that the arity of the selected subterm will be greater than the arity of the source term if we cross some binders along the given path.

select(λa.apply(lambda(λx.x),a), []) = λa.apply(lambda(λx.x),a) select(λa.apply(lambda(λx.x),a), 1) = λa.lambda(λx.x)

   select(λa.apply(lambda(λx.x),a), 1.1) = λa,x.x
   select(λa.apply(lambda(λx.x),a), 2) = λa.a

Arity Modification: Higher-order terms are functional. Type coercion consists in seeing one particular term that is a function of n arguments as a function of one more or one less argument. In the last case, this can be done only for functions that do no depend of one particular argument (i.e. that argument is not referenced (used) in the term). We have to give an index to designate the rank of the new (resp. old) argument.

   new(λa.apply(lambdaλx.x,a),2) = λa,b.apply(lambdaλx.x,a)
   del(λa,b.apply(lambdaλx.x,a),2) = λa.apply(lambdaλx.x,a)
   del(λa,b.apply(lambdaλx.x,a),1) is an error

Cut: The cut operation takes two arguments: the initial term and a path to one of its sub-terms; it returns two results: the first one is the initial term in which the designated subtree has been replaced by a place-holder (or metavariable) that is in fact a new argument, the second one is equal to the designated subtree. In the following, meta-variables (i.e. arguments that are generated by the system, not by the user) are denoted by capitals.

   cut(λa.apply(lambda(λx.x),a), 1.1) =
      (λa,U.apply(lambda(λx.U),a), λa,x.x)

Application: This operation is very natural. One can think of a variant of application in which one give the rank of the variable to which one argument must be applied. The traditional paste operation is an application. The traditional change operation is the composition of a cut and an application as explained in the section on menus.

   app(λa,b.apply(lambda(λx.b),a), 2, λa,b.b) =
      λa,b,c.apply(lambda(λx.c,a))

Menus: As it is traditionally done in first order syntactical editing, it is natural to propose the list of (higher-order) operators that can be put at a certain place (selection). This list is extended by the so called projections. Among these projections one can find the arguments of the term when it is functional, and also those that have been introduced by binders on the path going from the root to the current location, allowing, for exemple the use of declared objects.

menu(λa.apply(lambda(λx.x),a), 1) =

      (a, λU,V.apply(U,V), λU.lambda(λy.U))
   menu(λa.apply(lambda(λx.x),a), 1.1) =
      (a, x, λU,V.apply(U,V), λU.lambda(λy.U))

When a projection proposed by a menu is choosen, the current tree is replaced by the corresponding argument. In this way, it is not possible to use a terminal object that has not been introduced before.

   choose(λa.apply(lambda(λx.x),a), 1, 1) = λa.apply(a,a)
   choose(λa.apply(lambda(λx.x),a), 1.1, 1) = λa.apply(lambda(λx.a),a)

When an operator proposed by a menu is selected, two consecutive operation are performed: first the current tree is cut, generating a temporary meta-variable, second the whole tree is applied to the selected (functional) operator using the rank of this temporary meta-variable. Depending on the arity of the operator, some new meta-variables will appear.

   choose(λa.apply(lambda(λx.x),a), 1.1, 4) =

λa,U.apply(lambda(λx.lambda(λy.U),a)

All the previous operations operate modulo α-conversion. A complete editor should allow to visualize arguments by user-defined names, checking for eventual captures.

6 Conclusion

We have better understood what is a higher-order abstract syntax, and we have formulated its main features in three principles, making clear the need for an implementation of higher-order abstract syntax in a logical framework where these principles could be available at the object-level. Our next goals now will be to implement a prototype of a higher-order syntactical editor and to use functional abstract syntax for semantics.

Thanks are due to Joëlle Despeyroux and Pierre Leleu for discussions and reading of the previous version of this paper.

References

1. P. Borras, D. Clement, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. Centaur: the system. In Proceedings of the 3rd Symp. on Software Development Environments, Boston, USA, November 1988. Rapport de Recherche INRIA 777, Inria-Sophia-Antipolis, France, December 1987.

2. R. D. Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhaüser, ISBN 0-8176-3763-X, 1995.

3. J. Despeyroux, F. Pfenning, and C. Schürmann. Primitive recursion for higherorder abstract syntax. In To appear in the Proceedings of the TLCA 97 Int. Conference on Typed Lambda Calculi and Applications, Nancy, France, April 2– 4. Springer-Verlag LNCS, April 1997. An extended version is available as CMU Technical Report CMU-CS-96-172.

4. J. A. Goguen and J. Meseguer. Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. In Symposium on Logic in Computer Science, IEEE Press, 1987.

5. J. A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance , overloading, exceptions and partial operations. Technical Monograph PRG-80, Programming Research Group, Oxford University Computing Laboratory, December 1989.

6. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In Journal of the ACM, 40(1):143-184, January 1993.

7. I. Jacobs. The centaur 2.0 manual. Technical report, Inria, Sophia-Antipolis, France, 1994.

8. J.-P. J. Joseph A. Goguen and J. Meseguer. Operational semantics of order-sorted algebra. In International Conference on Automata, Languages and Programming, W. Brauer, Ed. Springer Verlag, LNCS 194., 1985.

9. S. M. Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer Verlag, 1971.

10. G. Nadathur and D. Miller. An overview of λProlog. In K. A. Bowen and R. A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810– 827, Seattle, Washington, Aug. 1988. MIT Press.

11. G. Nadathur and F. Pfenning. The type system of a higher-order logic programming language. In F. Pfenning, editor, Types in Logic Programming, pages 245–283. MIT Press, 1992.

12. F. Pfenning. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811–815, Nancy, France, June 1994. Springer-Verlag LNAI 814. System abstract.

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

14. B. C. Pierce. Basic Category Theory for Computer Scientists. Foundations of Computing. MIT Press, 1991.

15. D. Terrasse. Encoding natural semantics in coq. In Fourth International Conference on Algebraic Methodology and Software Technology, (AMAST ’95). Springer-Verlag LNCS, July 1995.