A Theory of Second-Order Trees

Neal Glew

                              aglew@acm.org

Abstract. This paper describes a theory of second-order trees, that is, finite and infinite trees where nodes of the tree can bind variables that appear further down in the tree. Such trees can be used to provide a natural and intuitive interpretation for type systems with equirecursive types and binding constructs like universal and existential quantifiers. The paper defines the set of binding trees, and a subset of these called regular binding trees. These are similar to the usual notion of regular trees, but generalised to take into account the binding structure. Then the paper shows how to interpret a second-order type system with recursive quantifiers as binding trees, and gives a sound and complete axiomatisation of when two types map to the same tree. Finally the paper gives a finite representation for trees called tree automata, and gives a construction for deciding when two automata map to the same tree. To tie everything together, the paper defines a mapping from types to automata, thus giving a decision procedure for when two types map to the same tree.

1 Introduction

In the theory of type systems there are two approaches to recursive types, the isorecursive and equirecursive approach. In the isorecursive approach, the types rec α.τ and τ{α := rec α.τ}^{1} are considered different but isomorphic types. The expression language includes type coercions^{2} roll(e) and unroll(e) for converting a value of one type to the other. The isorecursive approach is easier to construct decision procedures for, and is easier to prove sound; but it requires programs to contain type coercions. In the equirecursive approach, the types rec α.τ and τ{α := rec α.τ} are considered equal, and there are no expression-level constructs for dealing with recursive types. The presence of this equality makes it more difficult to develop decision procedures for equality and subtyping, and more difficult to prove the type system sound. However, there are no type coercions in programs, and more types are equivalent. For example, rec α.τ and rec α.(τ{α := τ}) are equal in the equirecursive types approach but are not intercoercible in the isorecursive approach.

A more fundamental problem with the equirecursive approach is that previous work on formalising it has gaps (see below). This paper fills these gaps by providing solid foundations for second-order type systems with equirecursive types.

1 The notation x{y := z} denotes the capture avoiding substitution of z for y in x. 2 A type coercion changes the type of an expression but has no runtime effect.

Amadio and Cardelli [AC93] were the first to investigate the equirecursive approach. They proposed the tree interpretation of recursive types, which is based on the idea that if the equality between rec α.τ and τ{α := rec α.τ} is applied repeatedly then recursive types expand into infinite trees that have no recursive quantifiers. Then, types are equal exactly when their fully-expanded trees are the same. Furthermore, subtyping can first be defined on trees and then lifted to types. Amadio and Cardelli defined a suitable tree model for a first-order type system, and a definition of subtyping between trees. Then they gave a set of type equality and subtyping rules, and proved them sound and complete with respect to the tree interpretation. Finally they gave an algorithm for deciding type equality and subtyping. Their algorithm is exponential time in the worst case, which is much worse than the linear time algorithm in the isorecursive approach.

Kozen et al. [KPS95] reduced this exponential time complexity to polynomial time. First they defined term automata,^{3} which, like types, are a finite representation for trees. Briefly, a term automaton is finite state machine. Each state represents a collection of nodes in a tree, the initial state is the root of the tree, and the transition function gives the children for each node and the labels on the edges to these children. Kozen et al. gave an intersection-like construction on term automata that can be used to decide equality and subtyping in quadratic time. In both Amadio and Cardelli and Kozen et al.’s work, only first-order systems were considered, and their results do not generalise in a straightforward manner to second-order types.

Colazzo and Ghelli [CG99] investigated a second-order type system with equirecursive quantifiers. They gave a coinductively defined set of type rules (type rules are normally defined inductively), and described and proved correct an algorithm for deciding subtyping. They did not show the relation between their rules and Amadio and Cardelli’s rules. Nor did they analyse the complexity of their algorithm, although they conjectured it was exponential. Their algorithm is essentially a search algorithm with the curious feature that it cuts off search when it sees the same subtyping judgement for the third, not second, time. They were able to show that this criterion is necessary and sufficient, but never gave an intuitive explanation.

This paper extends the tree interpretation and idea of tree automata from first-order to second-order trees. The first contribution is a notion of secondorder finite and infinite trees suitable as a semantic model for types. The second contribution is a proof that the usual equality rules for equirecursive types are sound and complete for this model. The third contribution is notion of tree automata suitable for second-order trees. The fourth contribution is a polynomial time decision procedure for type equality. This paper deals only with equality and subtyping is left to future work. Since equality is not something specific to types, I will call them terms in the sequel. The rest of the paper presents each contribution in turn. Full details including proofs are avaiable in a companion technical report [Gle02].

3 This paper will call Kozen et al.’s term automata, tree automata.

2 Preliminaries

The theory is meant to be general and to abstract over everything else in the term system. Therefore, I will assume the term language consists of variables, recursive quantifiers, and terms build from node labels nl ∈ NL. Each node label will take a number of arguments, which will be identified using labels ℓ ∈ L, and for each argument may bind a certain number of variables. The function spec ∈ NL → L ⇀^{fin} ℕ defines which arguments a node label takes and how many variables it binds for each. For example, the system F_{≤μ} of Colazzo and Ghelli has NL = {⊤, →, ∀}, L = {arg, bnd, bdy, res}, and spec = {(→, arg, 0), (→, res, 0), (∀, bnd, 0), (∀, bdy, 1)}. In this system, ∀ is a quantifier for bounded polymorphic types and binds one variable in its body (label bdy), so its specification is 1; the bound (label bnd) does not bind a variable, so its specification is 0. The rest of the paper will not refer to spec, instead it will use functions labels(nl) = dom(spec(nl)) and bind(nl, ℓ) = spec(nl)(ℓ).

Notations and Conventions A ⇀ B is the set of all partial functions from A to B; A ⇀^{fin} B is the set of partial functions from A to B with finite domain. If e_{1} and e_{2} are possibly undefined expressions then e_{1} = e_{2} means that either both are defined and equal or both are undefined. A^{∗} is the set of finite sequences of elements from A; ϵ is the empty sequence; prefix, concatenation, and append are written using juxtaposition; if x, y ∈ A^{∗} then x ≤ y means that x is a prefix of y. | · | is used both as the size of a set and the length of a sequence. A + B is the disjoint union of A and B; tags in this font will be used for injections, which tags correspond to which arms should be clear. If f is a function then f{x ↦ y} is the same function except that it maps x to y. If R is an equivalence relation then [R] is the set of its equivalence classes and [x]_{R} is the equivalence class of x under R.

3 Binding Trees

Binding trees are just finite or infinite trees whose nodes are labeled by node labels or by variables in a De Bruijn representation [Bru72] and whose edges are labeled by L. A node labeled nl has edges labeled by labels(nl) and variables are leafs. This can be formalised as follows.

Definition 1 The set of binding trees is defined as:

Tree = {t : L^{∗} ⇀ NL + ℕ |

ϵ ∈ dom(t) ∧ (pℓ ∈ dom(t) ⇔ ∃nl : t(p) = nl(nl) ∧ ℓ ∈ labels(nl))}

Distance between two trees is defined as d(t_{1}, t_{2}) = 2^{−min{n|t_{1}(p)≠t_{2}(p)∧n=|p|}} where 2^{−min ∅} = 0.

For example, the term ∀α.rec β.(α → ∀γ.β) maps to the tree {(ϵ, nl(∀)), (bdy, nl(→)), (bdyarg, var(0)), (bdyres, nl(∀)), (bdyresbdy, nl(→)), …} (tree t1 in Figure 1). De Bruijn indices are used to get a unique representation for the binding structure. The term above maps to the above tree rather than to an α-equivalence class of trees, as it would if explicit variables were used in trees.

[figure: ∀; →; 0; ∀; →; 1; ∀; →; 2; ⋯; ∀; →; 0; ∀; →; 1; ∀; →; 1; ⋯]

Fig. 1. Examples trees t1, on left, and t2, on right.

Recursive quantifiers will be interpreted as fixed points of maps on Tree, so it is important that such fixed points exist. In fact, (Tree, d) is a complete ultrametric space, which means that contractive maps on it have unique fixed points (c.f. [Kap77]). A map f is contractive on a metric space (X, d) if there exists a c ∈ [0, 1) such that d(f(x_{1}), f(x_{2})) ≤ cd(x_{1}, x_{2}) for all x_{1} and x_{2} in X—that is, f maps all pairs a certain fraction closer together.

The following two tree constructors will be needed latter. The first builds a tree whose root is the free variable n, and the second builds a tree with root nl and the given trees as the children of the root.

Definition 2 Tree var(n) is {(ϵ, var(n))} and tree nl(nl, ℓ = t_{ℓ})_{ℓ∈labels(nl)} is {(ϵ, nl(nl))} ∪ {(ℓp, t_{ℓ}(p)) | ℓ ∈ labels(nl) ∧ p ∈ dom(t_{ℓ})} if t_{ℓ} ∈Tree.

3.1 Regular Trees

Not all trees are expressible using terms or automata, so it is important to define a subset of trees that are. In the theory of first-order trees, these are called regular trees, and are defined as those with a finite number of subtrees. This definition is inadequate for binding trees, as the above example tree (which should be regular) has a subtree of the form var(n) for each n ∈ ℕ. The problem is that the De Bruijn indices represent conceptually the same variable as possibility different tree nodes. The definition of regular trees needs to take into account the binding structure and De Bruijn representation. Before giving the definition, two preliminary concepts are needed.

Definition 3 The number of variables bound along path p in tree t is:

bind(t, ϵ) = 0
bind(t, pℓ) = bind(t, p) + bind(nl, ℓ) where t(p) = nl(nl)

The number of variables bound from path p_{1} to p_{2} where p_{1} ≤ p_{2} in tree t is bind(t, p_{1} → p_{2}) = bind(t, p_{2}) − bind(t, p_{1}).

The key to regular trees is that variable nodes that conceptually refer to the same variable (e.g., the same free variable or are bound by the same node) should be considered equal. The next definition makes precise what a variable node in a tree refers to.

Definition 4 The variable identified by path p of tree t where t(p) = var(n) is:

varof(t, p) = \{ \begin{matrix}free(n − bind(t, p)) & bind(t, p) ≤ n \\ bound(p_{1}, ℓ, i) & p_{1}ℓ ≤ p ∧ i = n − bind(t, p_{1}ℓ → p) ∧ \\ & bind(t, p_{1}ℓ → p) ≤ n < bind(t, p_{1} → p) \end{matrix}

For example, if t is the tree above then varof(t, bdyarg) = bound(ϵ, bdy, 0) and if t′ is the subtree along the bdy edge then varof(t′, resbdyarg) = free(0).

Using this, when two subtrees of a tree might be equal is defined coinductively as follows.

Definition 5 A relation R is an equivalence of t’s subtrees exactly when R is an equivalence relation on dom(t) and p_{1} R p_{2} implies either

– t(p_{1}) = nl(nl), t(p_{2}) = nl(nl), and p_{1}ℓ R p_{2}ℓ for all ℓ ∈ labels(nl),

– varof(t, p_{1}) = free(n) and varof(t, p_{2}) = free(n), or

– varof(t, p_{1}) = bound(p′_{1}, ℓ, n), varof(t, p_{2}) = bound(p′_{2}, ℓ, n), and p′_{1} R p′_{2}.

However, more is needed. Consider this tree t2 in Figure 1. There exists an equivalence of this trees subtrees that relates all the ∀ nodes and has a finite number of equivalence classes. However, no term or term automata generates this tree. The problem is that the variable on path bdyresbdyarg binds not to the nearest ∀ but to the previous one, and terms never have this kind of binding structure. Therefore I define nonoverlapping equivalences to rule out these kinds of binding structures.

Definition 6 An equivalence R of t’s subtrees is nonoverlapping exactly when varof(t, p_{3}) = bound(p_{1}, ℓ, n) and p_{1} < p_{2} < p_{3} implies (p_{1}, p_{2}) ∉ R.

A tree t is regular if there exists a nonoverlapping equivalence of t’s subtrees with a finite number of equivalence classes. RegTree is the set of regular trees.

While the definition of regular binding trees is not nearly as elegant as that for regular trees without binding, it nevertheless does define exactly the set of trees that are expressible by terms or automata, as will be proven later.

It turns out that trees have a greatest nonoverlapping equivalence of their subtrees; later sections will use this to define a canonical term for each tree and to prove completeness of the equality rules.

Definition 7 For t ∈ Tree, eqst(t) is the union of the nonoverlapping equivalences of t’s subtrees.

Theorem 8 If t ∈Tree then eqst(t) is a nonoverlapping equivalence of t’s subtrees. Hence, t ∈ RegTree if and only if eqst(t) has finite number of equivalence classes.

Proof sketch: The proof shows that eqst(t)’s transitive closure is a nonoverlapping equivalence of t’s subtrees. Then it is a subset and thus equal to eqst(t), so the latter is a nonoverlapping equivalence of t’s subtrees. Since eqst(t) is a union of equivalence relations, its transitive closure is an equivalence relation. Since the other conditions for equivalence of subtrees are monotonic in the relation, it is easy to show that eqst(t)’s transitive closure is an equivalence of t’s subtrees. The tricky part is to show that it is nonoverlapping. Space does not permit showing the details, these are in the companion technical report [Gle02].

⊓ ⊔

One final operator on trees is needed latter. It is the shifting operation common to De Bruijn representations, and returns an identical tree except that the tree’s free variables are incremented by a constant.

Definition 9 The shift of a tree t by n is:

shift(t, n) = λp. \{ \begin{matrix}var(n + i) & t(p) = var(i) ∧ i ≥ bind(t, p) \\ t(p) & otherwise \end{matrix}

4 Terms

The second-order term language with recursive quantifiers is:

τ ::= α | nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ})_{ℓ∈labels(nl)} | rec α.τ

where α ranges over term variables and α^{⇀} is a sequence of term variables. Terms are considered equal up to alpha conversion, where for nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ}), α_{ℓ}^{⇀} binds in τ_{ℓ}, and for rec α.τ, α binds in τ.

Not all phrases matching the above grammar are considered terms, but only those that satisfy two further constraints. In terms of the from nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ}) it must be that | α_{ℓ}^{⇀} | = bind(nl, ℓ). In terms of the form rec α.τ it must be that τ ↓ α, where the latter means that τ is syntactically contractive in α and is defined as:

β ↓ α  ⇔ α ≠ β

nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ}) ↓ α

rec β.τ ↓ α  ⇔ α = β ∨ τ ↓ α

Intuitively, τ ↓ α if mapping α to τ is not equivalent to the identity mapping, for which any term is a fixed point. Instead mapping α to τ produces a term whose outer most constructor is independent of α, and can have only one fixed point.

4.1 Terms to Trees

The interpretation of terms as trees depends upon the interpretation of its free variables. An environment η is a mapping from term variables to Tree. Terms under a binder are interpreted in a shifted environment.

Definition 10

shift(η, α_{0} ⋯ α_{n−1}) = λβ. \{ \begin{matrix}var(i) & β = α_{i} \\ shift(η(β), n) & β ∉ \{α_{0}, …, α_{n−1}\} \end{matrix}

With these preliminaries, the interpretation of a term as a tree is straightforward.

Definition 11

[[α]]_{η}  = η(α)
[[nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ})]]_{η} = nl(nl, ℓ = [[τ_{ℓ}]]_{shift(η,α_{ℓ}^{⇀})})
[[rec α.τ]]_{η}  = fix([[α.τ]]_{η})
[[α.τ]]_{η}  = λt.[[τ]]_{η{α↦t}}

where fix(·) maps a contractive function to its unique fixed point

It is easy to show that a term’s interpretation is a uniquely defined tree, and the proof also shows that syntactically contractive term and variable pairs define contractive maps.

Theorem 12 If η maps term variables to Tree then [[τ]]_{η} ∈ Tree. If τ ↓ α then [[α.τ]]_{η} is contractive.

The interpretation of terms as trees produces a regular tree. Also, all regular trees are also expressible as terms; this is proven in the section on completeness.

Theorem 13 If η maps term variables to RegTree then [[τ]]_{η} ∈ RegTree.

4.2 Term-Equality Rules

The term-equality rules derive judgements of the form ⊢ τ_{1} = τ_{2} intended to mean that terms τ_{1} and τ_{2} are equal. The rules are essentially those of Amadio and Cardelli:

(eqsym) {⊢ τ_{2} = τ_{1} \atop ⊢ τ_{1} = τ_{2}}  (eqtrans) \begin{matrix}⊢ τ_{1} = τ_{2} & ⊢ τ_{2} = τ_{3} \\ ⊢ τ_{1} = τ_{3} \end{matrix}  (eqvar) ⊢ α = α

(eqnl) {⊢ τ_{ℓ} = σ_{ℓ} \atop ⊢ nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ}) = nl(ℓ =α_{ℓ}^{⇀} .σ_{ℓ})}  (eqrec) {⊢ τ = σ \atop ⊢ rec α.τ = rec α.σ}
(eqroll) ⊢ rec α.τ = τ{α := rec α.τ}

(equnq) \begin{matrix}⊢ τ_{1} = σ\{α := τ_{1}\} & ⊢ τ_{2} = σ\{α := τ_{2}\} \\ ⊢ τ_{1} = τ_{2} \end{matrix} (σ ↓ α)

The first two rules express that equality is symmetric and transitive. The next three rules express that equality is closed under all the term constructors and that equality is reflexive. Together these five rules make equality a congruence relation. The last two rules are the interesting ones. Rule (eqroll) expresses that rec α.τ is the fixed point of the mapping of α to τ, and is the rule from the introduction that defines the equirecursive approach. Rule (equnq) expresses the fact that contractive mappings have unique fixed points. The hypotheses expresses that τ_{1} and τ_{2} are a fixed points of the mapping α to σ; the side condition expresses that the mapping is contractive; and the conclusion expresses that the two fixed points are equal.

It is straightforward to prove the rules sound, that is, that provably equal terms map to the same tree.

Theorem 14 (Soundness) If ⊢ τ_{1} = τ_{2} then [[τ_{1}]]_{η} = [[τ_{2}]]_{η} for all environments η.

4.3 Completeness

It is more difficult to show the converse, that terms that map to the same tree are provably equal. Amadio and Cardelli showed completeness by defining something called systems of equations. Unfortunately, it seems very difficult to define systems of equations for second-order terms. So I use a different approach to showing completeness, which also works in the first-order setting. The idea is to define a canonical term for every regular tree and show that a term is provably equal to the canonical term for its tree. Completeness then follows by transitivity.

I will define canonical terms for trees with respect to particular kinds of environments called distinguishing environments. These are environments of the form η(α) = var(g(α)) for some g that is a bijection from term variables to ℕ.

Definition 15 If t ∈ RegTree, η is distinguishing, and R is a nonoverlapping equality of t’s subtrees with a finite number of equivalence classes, then T, S, termof_{η}(t, R), and termof_{η}(t) are defined as follows:

– If f maps [R] to term variables, f maps the pair ([p]_{R}, ℓ) to a sequence of term variables of length bind(nl, ℓ) when t(p) = nl(nl) and ℓ ∈ labels(nl), S is a subset of [R], and p ∈ dom(t) then:

T_{S,p}^{t,η,R,f} = \{ \begin{matrix}f([p]_{R}) & [p]_{R} ∈ S \\ rec f([p]_{R}).S_{S∪\{[p]_{R}\},p}^{t,η,R,f} & [p]_{R} ∉ S \end{matrix}

S_{S,p}^{t,η,R,f} = \{ \begin{matrix}β & varof(t, p) = free(n) ∧ \\ & η(β) = var(n) \\ f([p′]_{R}, ℓ)_{n} & varof(t, p) = bound(p′, ℓ, n) \\ nl(ℓ = f([p]_{R}, ℓ).T_{S,pℓ}^{t,η,R,f}) & t(p) = nl(nl) \end{matrix}

– termof_{η}(t, R) = T_{∅,ϵ}^{t,η,R,f} for some appropriate f that maps to fresh variables – termof_{η}(t) = termof_{η}(t, eqst(t))

These terms do map to the tree they are based on, and this shows that every regular tree is expressible using a term.

Theorem 16 If t ∈ RegTree and η is distinguishing then [[termof_{η}(t)]]_{η} = t.

The key technical result used to show completeness is that every term is provably equal to the canonical term for its tree.

Lemma 17 If η is distinguishing then ⊢ termof_{η}([[τ]]_{η}) = τ.

Proof sketch: The proof is ultimately by induction on the structure of τ. If τ has the form nl(ℓ =α_{ℓ}^{⇀} .τ_{ℓ}) then termof_{η}([[τ]]_{η}) has the form rec α.nl(ℓ =α_{ℓ}^{⇀} .σ_{ℓ}). If the induction hypothesis is ⊢ σ_{ℓ}{α := termof_{η}([[τ]]_{η})} = τ_{ℓ} (1), then the result follows by rules (eqnl), (eqroll), and (eqtrans). If τ has the form rec α.σ then the key is to have the induction hypothesis ⊢ termof_{η}([[τ]]_{η}) = σ{α := termof_{η}([[τ]]_{η})} (2). Then by (eqroll), ⊢ τ = σ{α := τ} and the result follows by rule (equnq). The key then, is to get the induction hypothesis to satisfy properties (1) and (2). The proof first defines for each subterm σ of τ a pair of terms (σ_{1}, σ_{2}) satisfying properties (1) and (2). Next it shows that the trees for these two terms and a corresponding subtree of [[τ]]_{η} are all the same. Finally it shows by induction on σ that ⊢ σ_{1} = σ_{2}. Details are in the companion technical report [Gle02]. ⊓ ⊔

Completeness follows easily from this last lemma.

Theorem 18 (Completeness) If η is distinguishing and [[τ_{1}]]_{η} = [[τ_{2}]]_{η} then ⊢ τ_{1} = τ_{2}.

Proof: By Lemma 17, ⊢ termof_{η}([[τ_{1}]]_{η}) = τ_{1} and ⊢ termof_{η}([[τ_{2}]]_{η}) = τ_{2}. Since [[τ_{1}]]_{η} = [[τ_{2}]]_{η}, termof_{η}([[τ_{1}]]_{η}) = termof_{η}([[τ_{2}]]_{η}). The result follows by (eqsym) and (eqtrans). ⊓ ⊔

5 Binding Tree Automata

The final step of my programme is to give a decision algorithm for term equality. The algorithm is in terms of a finite representation for trees, similar to the term automata of Kozen et al. The basic idea is that an automaton is given as input a path and gives as output the node at the end of that path. Automata are state machines, that is, each label in the path causes the automaton to transition from one state to another, starting with an initial state, and the state obtained at the end of the path determines the output. Rather than output the node in the form a tree does, that is, as an element of NL + ℕ, the automaton outputs either a node label, a free variable index, or a bound variable. A bound variable is specified as a state, label, and index; the idea being that the variable is bound by the most recent occurrence of the binder generated by the state, along the edge given by the label.

A few preliminaries are needed for the definition. If δ ∈ Q × L ⇀ Q for some Q then δ^{∗} is its extension to L^{∗}, specifically δ^{∗}(q, ϵ) = q and δ^{∗}(q, pℓ) = δ(δ^{∗}(q, p), ℓ). If δ^{∗}(q_{1}, p) = q_{2} then p is a path from q_{1} to q_{2}; if in addition δ^{∗}(q_{1}, p′) ≠ q for all p′ ≤ p then p is a q-less path from q_{1} to q_{2}.

Definition 19 A binding tree automaton is a quadruple (Q, i, δ, sl) satisfying:

– Q is a finite set called the states of the automaton.

– i ∈ Q is the initial state.

– δ ∈ Q × L ⇀ Q is the transition function.

– sl ∈ Q → NL + ℕ + Q × L × ℕ is the labeling or output function.

– (q, ℓ) ∈ dom(δ) ⇔ sl(q) = nl(nl) ∧ ℓ ∈ labels(nl).

– sl(q) = fvar(q′, ℓ, n) implies that:

• sl(q′) = nl(nl),

• ℓ ∈ labels(nl),

• 0 ≤ n < bind(nl, ℓ), and

• if p is a path from i to q then there are paths p_{1} and p_{2} such that p = p_{1}ℓp_{2}, p_{1} is a path from i to q′, and p_{2} is q′-less (from δ(q′, ℓ) to q).

5.1 Automata to Trees

This section explains how an automaton generates a tree. Letting t represent this tree then intuitively: if sl(δ^{∗}(i, p)) = nl(nl) then t(p) = nl(p); if sl(δ^{∗}(i, p)) = bvar(n) then varof(t, p) = free(n); finally, if sl(δ^{∗}(i, p)) = fvar(q′, ℓ, n) then varof(t, p) = bound(p′, ℓ, n) where p′ is the longest path from i to q′ that is a prefix of p.

The formal definition extends the state space to include enough information to compute the De Bruijn indices for free and bound variables. An extended state is a triple consisting of a state of the automaton, the number of variables bound along the path so far (needed to determine free variables), and a function f ∈ Q → ℕ, which gives the number of variables bound since the last occurrence of each state (need to determine bound variables). The transition function is lifted to extended states in such a way as to track the binding information, and the labeling function is lifted to extended states to use the binding information to generate nodes for trees. Then the tree of an automaton at a path is just the lifted labeling function of the lifted transition function on the path.

Definition 20 The tree associated with an automaton is defined as follows:

shift(f, q := n)  = λq′. \{ \begin{matrix}0 & q′ = q \\ f(q′) + n & q′ ≠ q \end{matrix}
δ̂((q, n, f), ℓ)  = (δ(q, ℓ), n + i, shift(f, q := i))
where sl(q) = nl(nl) ∧ i = bind(nl, ℓ)
ŝl(q, n, f)  = \{ \begin{matrix}nl(nl) & sl(q) = nl(nl) \\ var(n + i) & sl(q) = bvar(i) \\ var(f(q′) + i) & sl(q) = fvar(q′, ℓ, i) \end{matrix}
tree((Q, i, δ, sl), qnf ) = λp.ŝl(δ̂^{∗}(qnf , p))
î  = (i, 0, λq.0)
tree(Q, i, δ, sl)  = tree((Q, i, δ, sl), î)

It is not hard to see that automata generate trees, in fact, they generate regular trees.

Theorem 21 If ta is an automaton then tree(ta) ∈ RegTree.

Proof sketch: Let R = {(p_{1}, p_{2}) | δ^{∗}(i, p_{1}) = δ^{∗}(i, P)} where ta = (Q, i, δ, sl). Then R is a nonoverlapping equivalence of tree(ta)’s subtrees. It is clearly an equivalence relation. The other conditions for being an equivalence essentially follow from the fact that tree(ta)(p) is determined by δ^{∗}(i, p)’s label. It is nonoverlapping because of the last condition in the definition of tree automata.

⊓ ⊔

The converse is also true—regular trees are expressible as tree automata.

Theorem 22 If t is a regular tree then there exists an automaton ta such that tree(ta) = t.

Proof: The proof uses the equivalence classes of eqst(t) as the states Q. The initial state i is [ϵ]. If t(p) = nl(nl) then sl([p]) = nl(nl); if varof(t, p) = free(n) then sl([p]) = bvar(n); if varof(t, p) = bound(p′, ℓ, n) then sl([p]) = fvar([p′], ℓ, n). The transition function δ is λ([p], ℓ).[pℓ]. The conditions for equivalence of subtrees ensure that sl and δ are consistently defined. It is easy to check that this defines an automaton, the last part of the last condition follows from eqst(t) being nonoverlapping. An easy induction shows that δ̂^{∗}(î, p) = ([p], bind(t, p), f) where f is such that if p′ is such that p = p′ℓp′′ and p′ is the largest strict prefix of p in [p′] then f([p′]) = bind(t, p′ℓ → p). Then it is easy to show that ŝl([p], bind(t, p), f) = t(p). ⊓ ⊔

5.2 Equality Algorithm

Two trees are different if they differ at some path, but more specifically if they differ at some minimal path. This minimal path will be in the domain of both trees. Therefore to determine if two automata generate the different trees, it suffices to search for paths in their common domain that have different outputs. If the outputs along some path are the same up to but not including the last state then the number of variables bound up to the last state is the same. Thus, two free variable states will differ exactly when their indices differ, free variable states will differ from bound variable states, and bound variable states will differ if the most recent occurrence of the binding state occurred at different prefixes of the path. Thus determining if the outputs are different requires only keeping track of the states and the correspondence between binding states. As in Kozen et al., this can be expressed as a deterministic finite state automaton. The states of this equality automaton are triples, one state from each automata, and the correspondence between binding states. The transition function updates the states according to the input automata’s transition functions and updates the correspondence. The accepting states are those where the output of the two states differs according to the binding state correspondence. The two trees differ if the language of the equality automaton is nonempty. The correspondence between binding states can be expressed as partial bijections, introduced next.

Definition 23 The partial bijections between A and B are A ⇋ B = {R ∈ P(A × B) | (a_{1}, b_{1}) ∈ R ∧ (a_{2}, b_{2}) ∈ R ⇒ (a_{1} = a_{2} ⇔ b_{1} = b_{2})}. Bijection update of R by a maps to b is R{a ⇋ b} = {(a′, b′) ∈ R | a′ ≠ a ∧ b′ ≠ b} ∪ {(a, b)}.

Definition 24 The equality deterministic finite state automaton (over alphabet L) of two automata ta_{1} = (Q_{1}, i_{1}, δ_{1}, sl_{1}) and ta_{2} = (Q_{2}, i_{2}, δ_{2}, sl_{2}) is:

correspond(sl_{1}, sl_{2}, q_{1}, q_{2}, R) =
∨(sl_{1}(q_{1}) = nl(nl) ∧ sl_{2}(q_{2}) = nl(nl))
∨(sl_{1}(q_{1}) = bvar(n) ∧ sl_{2}(q_{2}) = bvar(n))
∨(sl_{1}(q_{1}) = fvar(q′_{1}, ℓ, n) ∧ sl_{2}(q_{2}) = fvar(q′_{2}, ℓ, n) ∧ q′_{1} R q′_{2})
equal(ta_{1}, ta_{2}) =
(Q_{1} × Q_{2} × (Q_{1} ⇋ Q_{2}),
(i_{1}, i_{2}, ∅),
λ(q_{1}, q_{2}, R, ℓ).(δ_{1}(q_{1}, ℓ), δ_{2}(q_{2}, ℓ), R{q_{1} ⇋ q_{2}}),
{(q_{1}, q_{2}, R) | ¬correspond(sl_{1}, sl_{2}, q_{1}, q_{2}, R)})

The next theorem proves the correctness of this construction.

Theorem 25 tree(ta_{1}) = tree(ta_{2}) ⇔ L(equal(ta_{1}, ta_{2})) = ∅

Proof sketch: The main part of the proof shows that if tree(ta_{1})(p′) = tree(ta_{2})(p′) for p′ < p then: tree(ta_{1})(p) = tree(ta_{2})(p) if and only if p ∈ L(equal(ta_{1}, ta_{2})); from which the result easily follows. This property holds because of the correspondence between an automaton’s tree and its state labels, and because q_{1} R q_{2}, where δ^{∗}(i, p) = ( , , R), if and only if the most recent occurrence of q_{1} and q_{2} are at the same prefix of p. ⊓ ⊔

The previous theorem gives an algorithm for deciding the equality of the trees of two automata. Since emptiness of a deterministic finite state automaton’s language is linear time, and the equality automaton is exponential in the size of the tree automata, it is an exponential algorithm. However, an optimisation yields a polynomial time algorithm. This optimisation is based on the following lemma.

Lemma 26 If ta_{1} = (Q_{1}, i_{1}, δ_{1}, sl_{1}) and ta_{2} = (Q_{2}, i_{2}, δ_{2}, sl_{2}) are automata, p_{2} ≠ ϵ, p_{3} ≠ ϵ, δ_{1}^{∗}(i_{1}, p_{1}) = δ_{1}^{∗}(i_{1}, p_{1}p_{2}) = δ_{1}^{∗}(i_{1}, p_{1}p_{2}p_{3}) = q_{1}, δ_{2}^{∗}(i_{2}, p_{1}) = δ_{2}^{∗}(i_{2}, p_{1}p_{2}) = δ_{2}^{∗}(i_{2}, p_{1}p_{2}p_{3}) = q_{2}, and p ∉ L(equal(ta_{1}, ta_{2})) for p ≱ p_{1}p_{2}p_{3} then L(equal(ta_{1}, ta_{2})) = ∅.

This lemma says that the search for a word in L(equal(ta_{1}, ta_{2})) does not need to search the entire space Q_{1} × Q_{2} × (Q_{1} ⇋ Q_{2}), but only needs to search until it sees the same Q_{1} × Q_{2} pair three times. It is insufficient to stop after seeing the same pair twice, as in Colazzo and Ghelli’s algorithm. For example, consider the following two automata:^{4}

4 The notation for automata depicts states as circles with x = y inside; x is the state’s identifier, and y is the states label, either a node label, a natural number for a free variable, or a bn for a variable bound by state n. An arrow not from another circle points to the initial state. The transition function is depicted with arrows between the circles labeled by L.

[figure: 1=∀; 2=∀; 3=0; 4=b1; bdy; bnd; bnd; 5=∀; 6=∀; 7=∀; 8=0; 9=b5; 10=0; bdy; bdy; bnd; bnd; bnd]

The path bdybdybdy produces the pair (2, 6) for the second time, and while bdybnd is not accepted by the equality automaton, bdybdybdybnd is accepted. The problem is that states 4 and 9 are part of repetitive structures and the path bdybnd checks that the first repetition of 4 matches the first repetition of 9, but not that the other repetitions match. The path bdybdybdybnd checks whether the second repetitions match. Only when both the first and second repetitions match will all repetitions necessarily match.

With an appropriate choice of representation and implemented carefully, the above algorithm is quadratic in the sizes of the input automata.

6 Putting it Together

The previous section gave an algorithm for deciding equality of two automata, so an algorithm to convert terms into automata gives an algorithm for deciding term equality. This section gives that algorithm and its correctness.

First an algorithm to convert terms into automata. The states of this automaton are the parts of the term not involved with recursive quantifiers.

Definition 27 The set proper(τ) is the subterms of τ that are not recursive quantifiers or variables bound by recursive quantifiers of τ. Every subterm of τ can be mapped to proper(τ) as follows: if σ ∈ proper(τ) then proper(τ, σ) = σ; proper(τ, rec α.σ) = proper(τ, σ); if α is a subterm of τ bound by the subterm rec α.σ then proper(τ, α) = proper(τ, rec α.σ).

proper(τ, σ) is uniquely defined for all subterms σ of τ, because recursive quantifiers are required to be syntactically contractive.

Armed with these constructs, the automaton of a term is easily defined.

Definition 28 If η is distinguishing then

automatonof_{η}(τ) = (proper(τ), proper(τ, τ), δ, sl)

where δ and sl are as follows. If σ = nl(ℓ =α_{ℓ}^{⇀} .σ_{ℓ}) then δ(σ, ℓ) = proper(τ, σ_{ℓ}) and sl(σ) = nl(nl). If σ is variable subterm of τ that is free in τ then sl(σ) = bvar(n) where η(σ) = var(n). If σ is a variable subterm of τ that is bound by the nth binder of edge ℓ of σ′ subterm of τ then sl(σ) = fvar(σ′, ℓ, n).

The automaton of a term is defined so that its tree is the same as the term’s tree.

Theorem 29 If η is distinguishing then tree(automatonof_{η}(τ)) = [[τ]]_{η}.

Finally, all the previous results can be combined into a decision procedure for equality of terms. Since the algorithm for equality of automata is quadratic and the conversion from terms to automata produces a linear output in linear time, the decision procedure below is quadratic.

Theorem 30 If η is distinguishing then:

⊢ τ_{1} = τ_{2} ⇔ L(equal(automatonof_{η}(τ_{1}), automatonof_{η}(τ_{2})) = ∅

Proof:

⊢ τ_{1} = τ_{2}
⇔ ⟨Theorem 14 and Theorem 18⟩
[[τ_{1}]]_{η} = [[τ_{2}]]_{η}
⇔ ⟨Theorem 29⟩
tree(automatonof_{η}(τ_{1})) = tree(automatonof_{η}(τ_{2}))
⇔ ⟨Theorem 25⟩
L(equal(automatonof_{η}(τ_{1}), automatonof_{η}(τ_{2}))) = ∅
⊓ ⊔

7 Summary and Future Work

This paper has shown how to give a natural interpretation to a second-order term system with recursive quantifiers. In particular it extends the well known tree interpretation, introduced by Amadio and Cardelli, to second-order constructs by defining a theory of trees with binding. It gives an appropriate generalisation of regularity to binding trees, and shows that regular trees characterise both those generated by terms and by automata. It shows the usual set of equality rules are sound and complete in the second-order case. It generalises Kozen et al.’s term automata to the second-order case, providing a polynomial time decision procedure for equality of terms. The result is a natural and intuitive theory of second-order type systems with equirecursive types.

The obvious next step is to add subtyping to the theory. The main idea is to define subtyping on trees coinductively. Then it should be possible to show that a certain set of rules is sound and complete with respect to this definition. Interestingly, the rules I believe are sound and complete are a nonconservative extension of rules for F_{≤} with the Kernel-Fun rule for bounded quantification (c.f. [Pie94] and [CG99]). Finally, it should be possible to extend the construction for equality of automata’s trees to subtyping in a way that combines my ideas for second-order constructs with Kozen et al.’s ideas for subtyping and a simple idea for dealing with bounded variables. The result should be a polynomial time algorithm for deciding subtyping in a system with Kernel-Fun recursivelybounded quantifiers and equirecursive types.

Another extension of the ideas is to higher-order kinds. Languages like ML and Haskell allow the definition of type constructors, which could be thought of as type variables with second-order kinds. Thus at a minimum, it would be good to include this in the theory if not a larger system with a fuller set of kinds. Full F_{ω} (c.f. [Gir71] and [Gir72]) with equirecursive types is likely to be undecidable since it contains the simply-typed lambda calculus with recursive functions at the type level, for which equality is at least as hard as the halting problem. But, it might be possible to restrict F_{ω} with equirecursive types to a decidable system, perhaps by allowing only syntactically-contractive recursive types.

References

[AC93] Roberto Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Progamming Languages and Systems, 15(4):575–631, September 1993.

[Bru72] N. De Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Mat., 34:381–392, 1972.

[CG99] Dario Colazzo and Giorgio Ghelli. Subtyping recursive types in kernel fun. In 1999 Symposium on Logic in Computer Science, pages 137–146, Trento, Italy, July 1999.

[Gir71] Jean-Yves Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63–92. North-Holland Publishing Co., 1971.

[Gir72] Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[Gle02] Neal Glew. A theory of second-order trees. Technical Report TR2001-1859, Department of Computer Science, Cornell University, 4130 Upson Hall, Ithaca, NY 14853-7501, USA, January 2002.

[Kap77] Irving Kaplansky. Set Theory and Metric Spaces. Chelsea Pub Co, 2nd edition, June 1977.

[KPS95] Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113–125, March 1995.

[Pie94] Benjamin Pierce. Bounded quantification is undecidable. Information and Computation, 112:131–165, 1994.