Subtyping Machines]Study of the Subtyping Machine
of Nominal Subtyping with Variance (full version)

Ori Roth

This is a study of the computing power of the subtyping machine behind
Kennedy and Pierce's nominal subtyping with variance.
We depict the lattice of fragments of Kennedy and Pierce's type system and characterize
their computing power in terms of
regular, context-free, deterministic, and non-deterministic tree languages.
Based on the theory, we present Treetop—a generator of CSharp
implementations of subtyping machines.
The software artifact constitutes the first feasible (yet POC) fluent API generator
to support context-free API protocols in a decidable type system fragment.

<concept_desc>Software and its engineering General programming languages</concept_desc>
<concept_desc>Software and its engineering Inheritance</concept_desc>
<concept_desc>Software and its engineering API languages</concept_desc>
<concept_desc>Software and its engineering Software development techniques</concept_desc>

[500]Software and its engineering General programming languages
[500]Software and its engineering Inheritance
[300]Software and its engineering API languages
[300]Software and its engineering Software development techniques

§ INTRODUCTION

Object-oriented programming is all about inheritance or subtyping, and how
software can and cannot be properly engineered using it. In the eyes of the
theoretical computer scientist or the type theorist, the question is what
(compile-time) computations can and cannot be done with subtyping. The question
becomes challenging when generics, i.e., parametric polymorphism, interact with
subtyping, raising the question of when a certain generic taking type
argument $t_1$ is a subtype of the same generic taking type argument $t_2$. In the
invariant regime of subtyping with generics, the answer is negative (unless $t_1=t_2$);
in the covariant regime, the answer is positive precisely when $t_1$ is a subtype
of $t_2$; in contrast, in the contravariant regime, when $t_2$ is a subtype of $t_1$.

Consider, for example, the code in <ref>
(unless said otherwise, all code examples in this paper are written in ):
[style=csharp,caption=subtyping machine recognizing palindromes over $❴a, b❵$,
interface a<out x>  interface b<out x>  interface E
class v0<x> : a<v0<a<x>>>, a<a<x>>, a<x>, b<v0<b<x>>>, b<b<x>>, b<x>
a<b<b<a<b<b<a<E>>>>>>> w1 = new v0<E>(); // Compiles: @$abbabba$@ is a palindrome
a<b<b<a<b<a<a<E>>>>>>> w2 = new v0<E>(); // Does not compile: @$abbabaa$@ is not a palindrome

The program in <ref> defines four classes (lines 1–2):
generic (polymorphic) classes a and b employing a covariant type parameter x,
as indicated by the keyword out;
non-generic class E;
and generic class v0 that inherits from the six supertypes written after the colon.

Below the classes are two variable declarations (lines 3–4).
The type of variable w1 is a<b<b<a<b<b<a<E>>>>>>>, encoding the word $w₁=abbabba$,
and the type of variable w2 is a<b<b<a<b<a<a<E>>>>>>>, encoding the word $w₂=abbabaa$.
<ref> demonstrate the encoding of $ℓ$, the non-deterministic
context-free formal language of palindromes over alphabet $❴a, b❵$, in the type
system of .
Each variable is assigned an instantiation of type v0<E>, that
type checks if and only if the variable type encodes a palindrome.
Thus, the assignment to variable w1 type checks since $w₁∈ℓ$,
but the assignment to w2 fails since $w₂∉ℓ$.

The mechanics behind this ‟magic”, and why it matters, is
revealed by our study of the computing power of subtyping in the
context of the work of <cit.> on the nominal
subtyping with variance type system.

§.§ Kennedy and Pierce's Type System and Its Decidable Fragments

<ref> places our results in context.
The figure shows a three-dimensional lattice, structured similarly
to the $λ$-cube <cit.>.
The lattice is spanned by three type system features, which are
explained briefly here and in greater detail in <ref>.
The head of the lattice is the abstract type system developed by <cit.>,
which employs all three features. The other lattice points are type system
fragments of that use different feature combinations.
Nodes are adorned with references to previous works (shown as citations) and to our
contributions (shown as forward references).

[row sep=2.5em,column sep=4.5em,execute at begin picture=
reference=[rectangle callout,draw=cyan,dashed,callout absolute pointer=(##1.base east),below right=.5ex and .5ex of ##1]
,execute at end picture=

[text width=13ex,reference=cxm] <cit.>;
[text width=7ex,reference=cx] <cit.>;
[text width=9ex,reference=bot] <ref>;
[text width=9ex,reference=c] <ref>;
[text width=8ex,reference=m] <ref>;
[text width=8ex,reference=cm] <ref>;
[text width=9ex,reference=x] <ref>;
[text width=8ex,reference=xm] <ref>;
|[alias=xm,dec,fill=cffgnf]|         |[alias=cxm,undec]| ⏎
|[alias=x,dec,fill=dcff]|         |[alias=cx,undec]| ⏎
|[alias=m,dec,fill=regf]|         |[alias=cm,dec,fill=regf]| ⏎
|[alias=bot,dec,fill=dregf]|        |[alias=c,dec,fill=dregf]|⏎
[from=bot,to=m,mm]Multiple ⏎ Instantiation
[from=c,to=cm,mm]Multiple ⏎ Instantiation
[from=x,to=xm,mm]Multiple ⏎ Instantiation
[from=cx,to=cxm,mm]Multiple ⏎ Instantiation
[from=c,to=cx,xx,crossing over][fill=white,anchor=south]Expansive
[from=x,to=cx,cc,crossing over][fill=white]Contravariant

2p.9Background color indicates the computing power of the type system:

-1pt     Deterministic regular forests

-1pt     Regular forests

-1pt     Deterministic context-free forests

-1pt     Context-free forests with grammars

in Greibach normal form

-1pt     Recursively-enumerable

Lattice describing the eight subtyping type system fragments employing
contravariance (C), expansive inheritance (X), and multiple
instantiation inheritance (M) (defined in <ref>)

The lattice is spanned by three orthogonal Boolean coordinates or features
denoted by $\text{C}$, $\text X$, and $\text M$, representing the three
core features of : Contravariance, eXpansively-recursive inheritance, and Multiple instantiation
inheritance. The most familiar feature is the kind of variance;
the horizontal direction in the figure
denotes the distinction between covariant type systems (positioned
on the plane on the left-hand side of the lattice) and contravariant
type systems (right-hand).

Precise definitions of the three features follow in <ref>; here we provide a quick
review of the concepts and the intuition behind them:

(C) Contravariance:
Type arguments assigned to contravariant type parameters can be substituted with less derived types.
For example, using the “is a” relationship we can say that if x in a<x> is contravariant and b is a c
then a<c> is an a<b>.
interface a<in x>  // type parameter $\color{comment}\cc{x}$ of class $\color{comment}\cc{a}$ is contravariant
interface b : c    // type $\color{comment}\cc{b}$ is a subtype of $\color{comment}\cc{c}$
a<b> x=(a<c>) null;  // type $\color{comment}\cc{a<c>}$ is a subtype of $\color{comment}\cc{a<b>}$

(X) Expansively-recursive inheritance:
The expansion of types through inheritance (as defined by <cit.>) is unbounded.
Intuitively, this expansion involves the curiously recurring template pattern <cit.>,
where a class appears in one of its supertypes' generic arguments.

interface a<x, y> : b<a<b<x>, y>>  // class $\color{comment}\cc{a}\!$'s inheritance is expansively-recursive

(M) Multiple instantiation inheritance:
Inheritance is non-deterministic <cit.>, i.e., type arguments of supertypes are not unique.

interface a : b<c>, b<d>  // supertype $\color{comment}\cc{b}$ is instantiated twice, with arguments $\color{comment}\cc{c}$ and $\color{comment}\cc{d}$

A point in the lattice is denoted by the set of its features. Type
system $\TKP$ is denoted by the triple $\Tcxm$, and the notation $\Tcx$ designates
a type system that allows contravariance and expansive inheritance, but not
multiple instantiation inheritance. The code examples above also demonstrate
two key features ingrained within and its fragments: ‟polyadic” parametric
polymorphism and multiple inheritance, allowing a class to have multiple type
parameters and supertypes, respectively.

As shown in <ref>, the new results here, together with the proof that is undecidable due to Kennedy and Pierce and the subsequent proof
by <cit.> implying that is undecidable, completely characterize
the computing power of all eight points of the lattice.
This characterization is not in terms of the Chomsky hierarchy of classes of
formal languages, but rather in terms of a similar hierarchy of classes of
forests, also called formal tree languages (see, e.g., <cit.>), as
depicted by <ref>.
The classes appearing in the figure are defined in <ref>.

[node distance=5ex]
[fill=dregf] (drf) DRF;
[above left=of drf,fill=regf] (nrf) NRF;
[above right=of drf,fill=dcff] (dcf) DCF;
[above=10ex of drf,fill=cffgnf] (cffgnf) NCFGNF;
[above=of cffgnf,fill=cff] (cff) NCF;
[above=of cff,fill=ref] (re) REF;

margin=.5ex 1ex -7.5ex 1ex,minipage=.6,bgcolor=black!5
-1pt     DRF     Deterministic Regular Forests

-1pt     NRF     Non-deterministic Regular Forests

-1pt     DCF     Deterministic Context-free Forests

-1pt     [t]2*NCFGNF     Non-deterministic Context-free
Forests with

grammars in Greibach Normal Form

-1pt     NCF     Non-deterministic Context-free Forests

-1pt     REF     Recursively-Enumerable Forests

A Chomsky-like hierarchy of formal forest classes (defined in <ref>)

As shown in <ref>, the hierarchy of tree
languages is a non-linear lattice, spanned by two orthogonal Boolean features
abbreviated by letters in the acronyms in the figure as follows:

* Determinism ($\text D<\text N$) distinguishing between
Deterministic forests and their super-set,
Non-deterministic forests;

* Method of specification ($\text R<\text C$) distinguishing between Regular forests and their super-set, Context-free forests.

In <ref>, we see that forest class DRF is the smallest class in the diagram.
Moving up the lattice, the two next classes, NRF and DCF, cannot be compared. Both are contained
in NCF, which is contained in REF, the class of all recursively enumerable
forests. We also make use of class $\text{NCF\sub{GNF}}⊂\text{NCF}$, which
includes the non-deterministic context-free forests that can be specified by
a tree grammar in Greibach normal formal (GNF). Observe that class NCFGNF also
contains DCF and NRF.

The theoretical contribution of our work is a
characterization of the computing power of the six decidable points in the
lattice of <ref> in terms of the hierarchy
of <ref>.
These results are obtained by examining the subtyping machine behind
subtyping queries—a kind of automata with finite control (dictated by the
nominal inheritance table) whose auxiliary storage is not a tape, stack, or
tree, but rather the contents of a specific subtyping query that changes along the
run of this automaton. These machines stand behind Kennedy and Pierce's study and Grigore's

§.§ Fluent APIs and Treetop

Fluent API (application programming interface) <cit.> is a trendy
practice for the creation of software interfaces <cit.>. In a
statically-typed, object-oriented setting, a fluent API method returns a
type that receives other API methods. In this way, fluent API methods are invoked
in a chain of consecutive calls:

\begin{equation}\label{equation:fluent:api}
\cc{$σ₁$().$σ₂$().$⋯$.$σₙ$()}
\end{equation}

The main advantage of fluent API is its ability to enforce a protocol at
compile time. If an invocation of method $σ_{i+1}$ after a call to $σᵢ$ breaks
the protocol, then the type returned from method $σᵢ$ must not
declare $σ_{i+1}$, which would cause the expression to fail type checking.

A practical application of fluent API is embedding domain specific languages
(DSLs) in a host programming
language <cit.>.
The syntax and semantics of a DSL are optimally designed for its domain; for
instance, is a DSL suited for composing database queries. If the protocol
of the fluent API is a grammar $G$ describing the DSL, then the chain of method
calls of <ref> type checks if and only
if $w=σ₁σ₂⋯σₙ∈L(G)$, i.e., the expression encodes a legal DSL program. For
example, with an fluent API implemented in we can embed database
queries as expressions:

\[
\text{\inline[language=scala]{select("id").from(grades).where(_.grade>90)}.}
\]

The expression

\[
\text{\inline[language=scala]{select("name").where(_.length==4)},}
\]

does not type check, as it represents an illegal query,

\[
\text{\inline[language=sql]{SELECT name WHERE length=4}.}
\]

The academic study of fluent APIs seeks new ways to encode increasingly complex
DSL classes. Results in the field are given in the form of generators:
software artifacts that convert a formal grammar into a fluent API encoding its
language. Fling <cit.> and TypeLevelLR <cit.> are two
prominent fluent API generators that support all deterministic context-free
languages (DCFLs). <cit.> implemented a generator that accepts
context-free grammars describing general context-free DSLs—a proper
super-set of DCFLs. Specifically, his implementation coded a CYK parser
in an intermediate simple, yet high level language, and then translated
the code in this language into a Turing machine, being emulated in a
subtyping query. Unfortunately, the resulting APIs are
unusable in practice, as they lead to extremely long compilation times and
crash the compiler.

Examining <ref> we see that the contravariant regime for
combining genericity with subtyping is essential for the undecidability
result of Kennedy and Pierce and its use by Grigore to encode Turing machines with generics.
Contravariance is also essential to Grigore's implementation of a
fluent API generator for all context-free languages.
Grigore's result is noteworthy since the best previous fluent API generators
<cit.>, relying on invariance,
were only able to encode the deterministic subset of context-free
languages (languages with an LR grammar). As shown in <ref>, our results
prove that the covariant regime, exemplified by the simple phrase ‟a bag
of apples is bag of fruit”, is weaker than its contravariant counterpart.

Establishing that covariance is weaker than contravariance and noticing that it is
stronger than invariance, it is natural to ask whether the entire class of
context-free languages can be encoded in a type system with nominal subtyping
combined with only covariant genericity. Conversely, the question is motivated
by the argument that there is no theoretical difficulty in recognizing context-free
languages in a Turing-complete type system, but it might be a challenge
to recognize these in a decidable type system.

Unfortunately, the code produced by Grigore's fluent API generator collapses
under its own weight (measured in gigabytes) and crashes rugged modern
compilers. Another natural question to ask is: Is the (computationally)
weaker artillery of covariance also lighter in weight (in terms of code size)?

Treetop is a product of our theoretical study that answers both questions
affirmatively. It is a proof of concept (POC) generator of ‟covariant generic
subtyping” machines that are implemented as CSharp code.
Given $G$, a CFG defining a formal language $ℓ$ (such as the language
of palindromes in the example of <ref>),
Treetop generates a library in
that defines a fluent API of $ℓ$.
The library uses expansive inheritance (the X feature in the lattice of
<ref>) and multiple instantiation inheritance (M in this
lattice), but not contravariance (C).
Thus, Treetop not only supports general context-free grammars,
but it also does this in a decidable type system fragment.
We demonstrate in an experiment non-trivial subtyping machines
generated by Treetop that compile relatively fast, yet we
also identify at least one example which induces impractically long
compilation times using the CSC compiler.

<ref> elaborate on
Kennedy and Pierce's work on subtyping, to refresh readers' understanding of concepts such as formal forests and
tree grammars, and set up our notations. Subtyping machines are then defined
in <ref> as computational devices that model nominal
subtyping. <ref> derives the results of
<ref>. Treetop, our API generator for context-free protocols,
is the focus of <ref>. <ref> discusses the
results of our study.

*Note on bold notation.
The bold version of a symbol denotes a (possibly empty) sequence of instances of the
non-bold version of this symbol, e.g., $\vv{x}$ stands for $x₁,x₂,…,xₖ$ for
some $k≥0$.
This notation is abused when the intent is clear from the context, e.g.,
\[
\vv{τ}[\vv{x}←\vv{t}]
\]
\[
τ₁[x₁← t₁,…,xₖ← tₖ],…,τₙ[x₁← t₁,…,xₖ← tₖ],
\]
where $\vv{τ}$, $\vv{x}$, and $\vv{t}$ are the three
sequences $\vv{τ}=τ₁…,τₙ$, $\vv{t}=t₁…,tₙ$, and $\vv{x}=x₁,…,xₙ$.

§ PRELIMINARIES: FORMAL FORESTS AND THEIR GRAMMARS

We assume that the reader is familiar with the classical theory of automata and formal
languages (e.g., <cit.>). Here we provide a quick
review of the standard generalization of the theory to forests, also
called (formal) tree languages. (For a more detailed review, see standard references such as

We use parenthetical notation for terms (trees), e.g.,

\begin{equation}\label{eq:example:term}
\end{equation}

Rank $n∈ℕ$ of symbol $σ$, denoted $\rank(σ)$, is the number of its children.
If $n=0$, then $σ$ is called a leaf, and if $n=1$, then $σ$ is monadic.
In both cases, $σ$'s parentheses may be omitted, e.g., $t$ in
<ref> becomes $σ₁(σ₂σ₃,σ₄)$.
The height of a tree $t$ is denoted $\height(t)$, e.g., for $t$ in
<ref>, $\height(t)=3$. The set of trees over ranked
alphabet $Σ$ (i.e., an alphabet of symbols with ranks) is denoted $Σ^▵$,
generalizing the Kleene closure $K^*$ for forests.

Consider the following definitions, adapted from <cit.>:

\begin{equation}\label{eq:example:regular:grammar}
\begin{aligned}
\text{(a)~}\-Nat-&\produce \+z+& \text{(b)~}\-Nat-&\produce \+s+(\-Nat-) ⏎
\text{(c)~}\-List-&\produce \+nil+& \text{(d)~}\-List-&\produce \+cons+(\-Nat-, \-List-)
\end{aligned}
\end{equation}

These are tree grammar productions deriving Peano numbers (productions (a,b))
and cons-lists of those integers (productions (c,d)).
An integer $n∈ℕ$ is encoded by the monadic term $\+s+ⁿ\+z+$.
Instead of strings, tree grammar productions derive terms:
The left-hand side of a production is a variable, and the right-hand
side is a term with which the variable can be substituted.
As in the string case, terminal (ground) terms are derived from variables by
repeatedly substituting the latter according to the given productions.
For example, we encode the list $⟨{}2,1,0⟩$ using the term

\begin{equation}\label{eq:example:list}
\+cons+(\+ssz+, \+cons+(\+sz+, \+cons+(\+z+, \+nil+)))
\end{equation}

This term can be derived from variable List- from
<ref>, as illustrated in <ref>.
<ref> uses arrows to depict variable substitution; an arrow label
references the production from <ref> used to apply the derivation.

l2=[l,below left=-3pt,yshift=1pt]

(l0) $\-\underline{List}-$;
(l1) [below=1ex of l0] $\+cons+(\-\underline{Nat}-, \-\underline{List}-)$;
[e] ($(l0.south)+(0pt,4pt)$)–($(l1.north)+(0pt,-2pt)$) node[l] $(d)$;
(l2) [below right=1ex and 6ex of l1.south] $\+cons+(\-\underline{Nat}-, \-\underline{List}-)$;
[e] ($(l1.south east)+(-15pt,4.5pt)$)–($(l2.north west)+(13pt,-3pt)$) node[l2] $(d)$;
(l3) [below right=1ex and 6ex of l2.south] $\+cons+(\-\underline{Nat}-, \-\underline{List}-)$;
[e] ($(l2.south east)+(-15pt,4.5pt)$)–($(l3.north west)+(13pt,-3pt)$) node[l2] $(d)$;
(l4) [below right=1.75pt and 6ex of l3.south] $\+nil+$;
[e] ($(l3.south east)+(-15pt,4.5pt)$)–($(l4.north)+(-3pt,-2pt)$) node[l2] $(c)$;

(n00) [below=1ex and 3ex of l1.south] $\+s+(\-\underline{Nat}-)$;
[e] ($(l1.south)+(0pt,4.5pt)$)–($(n00.north)+(0pt,-1pt)$) node[l] $(b)$;
(n01) [below right=1ex and .5ex of n00.south west,anchor=north west] $\+s+(\-\underline{Nat}-)$;
[e] ($(n00.south)+(.5ex,4.5pt)$)–($(n01.north)+(0pt,-1pt)$) node[l] $(b)$;
(n02) [below right=1ex and-3.5pt of n01.south] $\+z+$;
[e] ($(n01.south)+(.5ex,4.5pt)$)–($(n02.north)+(0pt,-1pt)$) node[l] $(a)$;
(n10) [below=1ex and 3ex of l2.south] $\+s+(\-\underline{Nat}-)$;
[e] ($(l2.south)+(0pt,4.5pt)$)–($(n10.north)+(0pt,-1pt)$) node[l] $(b)$;
(n11) [below right=1ex and-3.5pt of n10.south] $\+z+$;
[e] ($(n10.south)+(.5ex,4.5pt)$)–($(n11.north)+(0pt,-1pt)$) node[l] $(a)$;
(n20) [below=1ex and 3ex of l3.south] $\+z+$;
[e] ($(l3.south)+(0pt,4.5pt)$)–($(n20.north)+(0pt,-1pt)$) node[l] $(a)$;

The derivation of the term in <ref>, encoding
the list $⟨2,~1, 0⟩$, from variable  according to the
productions of <ref>

For readers familiar with functional programming languages as
and , it is intuitive to see the grammar in <ref>
as a set of datatype definitions, as shown in <ref>.
The grammar variables Nat- and List- are datatypes whose value
constructors are the grammar terminals z+, s+, nil+, and cons+.
For each grammar production $v \produce \sigma$, we define $\sigma$ as a
value constructor of $v$;
if $\sigma$ has children, they are used as constructor parameters.
Type checking in the resulting program coincides with derivation of
Peano numbers.
In particular, an expression belongs to type List if and only
if it can be derived from variable List-, e.g., the expression in line 3
of <ref> encodes the tree in <ref>
and compiles as expected.

[language=ml,caption=The grammar of <ref> encoded as datatypes,label=lst:sml:regular:grammar]
datatype Nat = z | s of Nat;
datatype List = nil | cons of Nat * List;
cons(s(s(z)), cons(s(z), cons(z, nil))) : List;

Formally, a forest grammar $G=⟨Σ, V, v₀, R⟩$ employs a finite ranked alphabet $Σ$, a
finite ranked set of variables $V$, a designated initial leaf $v₀∈V$, and a
finite set of productions $R$. To generate a terminal tree, grammar $G$ repeatedly
applies $R$ productions to the initial leaf $v₀$, as explained below.
Intermediate trees, members of $(Σ∪V)^▵$, are called tree forms, similar to
sentential forms of string grammars.

Let $X$ be a finite set of parameter leaf symbols, disjoint to sets $Σ$
and $V$. Terms over $Σ∪V$, denoted $t$, are ground, while terms over $Σ∪V∪X$, denoted $τ$, are unground. Unground terms are used as tree
patterns, where the $X$ parameters can be substituted with terms (usually
ground). The application of substitution $s=❴\vv{x}←\vv{t} ❵=❴x₁← t₁,…,xₖ←
tₖ ❵$ to unground term $τ$, denoted $τ[s]$, yields a term where every
occurrence of parameter $xᵢ$ is substituted with term $tᵢ$.
(A substitution's curly brackets may be omitted if written inside square brackets.)
A term $τ$ matches term $τ'$ if and only if there exists a substitution $s$ such
that $τ'[s]=τ$, denoted $τ⊑ₛτ'$.
Let $\params(τ)⊆X$ denote the set of parameters appearing in term $τ$.

A production $ρ=τ \produce τ'∈R$ describes a tree transformation.
If tree $t$ matches $τ$ with substitution $s$, $t⊑ₛτ$, the
application of $ρ$ to $t$, denoted $t[ρ]$, yields $τ'$ substituted by $s$,
\[
\]
We require that every parameter $x∈X$ on the right-hand side of production $ρ∈R$
be found on the left-hand side, so that all the applications of $ρ$ to ground trees are ground.

Note the distinction between variables and parameters.
Variables are found in tree forms and constitute the nodes remaining to be derived.
Parameters, on the other hand, appear only in productions and are used as
templates in tree patterns.

We say that tree form $t$ derives tree form $t'$, denoted $t \rightarrow t'$ (or $t \rightarrow_G t'$),
if $t$ can be transformed into $t'$ by a single application of an $R$ production:
\[
t \rightarrow t' ~\Leftrightarrow~ \exists \rho \in R, ~ t[\rho] = t'.
\]

The tree language (forest) of grammar $G$, $L(G)$, is the set of terminal trees that can be
derived from the initial variable $v_0$ in any number of steps:
\[
L(G) = \{ t \in \Sigma^\triangle ~|~ v_0 \rightarrow^*_G t \}.
\]

Each class (family) of tree grammars is defined by a set of restrictions imposed on the
shape of productions.
In regular tree grammars that define regular forests (NRF), productions are
of the form $v \produceσ(\vv{v})$, where $σ∈Σ$ and $v,\vv{v}∈V$; a more relaxed definition simply restricts
variables to be leaves.
Observe that the productions of <ref> belong to
a regular grammar.

Productions of context-free tree grammars (CFTG), yielding context-free forests (NCF),
are of the form $v(\vv{x}) \produceτ$ (the parameters in $\vv{x}$ are unique).
For example, the following productions belong to a CFTG:

\begin{equation}\label{eq:example:derivation:cf}
\text{(a)~}v₀\produce v₁(\+leaf+) \quad \text{(b)~}v₁(x)\produce v₁(\+node+(x, x)) \quad \text{(c)~}v₁(x)\produce x
\end{equation}

These productions derive complete binary trees over $❴\+leaf+, \+node+❵$.
The binary trees are derived recursively.
The child of variable $v₁$, captured by parameter $x$, describes a tree
of height $n≥1$; production (b) is then used to replace $x$ with $\+node+(x, x)$,
the complete binary tree of height $n+1$.
The recursion terminates by production (c), which simply returns the constructed tree.

To encode context-free tree grammars in , we use polymorphic datatypes,
i.e., datatypes that employ type parameters.
Consider, for example, the following grammar:

\begin{equation}\label{eq:context:free:grammar:ml}
\begin{aligned}
v_0(x) &\produce b(x) & v_1 &\produce E \\
v_2(x) &\produce m(x) & v_2(x) &\produce a(v_2(v_0(x)))
\end{aligned}
\end{equation}

This grammar defines the context-free language (forest) $a^n m b^n E$ ($n \ge 0$).
The program encoding the grammar is shown in <ref>.
Variables $v_0$ and $v_2$, which use parameters, are encoded by
polymorphic datatypes that define the parameterized type constructors
v0 and v2.
Following the datatype definitions are three expressions:
While the expression $a^3 m b^3 E$ (line 4) compiles,
the expressions $a^1 m b^2 E$ and $a^2 m b^1 E$ (lines 5–6)
do not, as expected.

[float=ht,language=ml,caption=The grammar of <ref> encoded as polymorphic datatypes,label=lst:sml:context:free:grammar]
datatype 'x v0 = b of 'x;
datatype v1 = E;
datatype 'x v2 = m of 'x | a of 'x v0 v2;
a(a(a(m(b(b(b(E))))))) : v1 v2;
a(m(b(b(E)))) : v1 v2; (* Does not compile *)
a(a(m(b(E)))) : v1 v2; (* Does not compile *)

Not all context-free grammars, however, can be encoded in using this method.
A production deriving a grammar variable to one of its parameters, e.g.,
production (c) in <ref>, results in a nonsensical
declaration [language=ml]datatype 'x v='x.
In addition, a grammar terminal that appears in more than one production
introduces overloaded value constructors, that not supported by .

In CFTG in Greibach normal form (GNF), the roots of the right-hand side of productions are
terminal, $v(\vv{x}) \produceσ(\vv{τ})$ <cit.>.
Observe that none of the productions in <ref> are in GNF:
The roots of the right-hand sides are variables in productions (a,b) and a parameter
in production (c), both forbidden in GNF.
In contrast, the following productions do belong to a CFTG in GNF:

\begin{equation}\label{eq:example:cff:grammar}
\begin{array}{ccc}
\text{(a)~}v₀x \produce av₀ax & \text{(b)~}v₀x \produce aax & \text{(c)~}v₀x \produce ax ⏎
\text{(d)~}v₀x \produce bv₀bx & \text{(e)~}v₀x \produce bbx & \text{(f)~}v₀x \produce bx
\end{array}
\end{equation}

Variable $v_0$ derives palindromes over $\{a,b\}$. For instance, the palindrome
$abbabba$ is derived from the tree form $v_0 E$ ($E$ is a dummy leaf) as follows:
\[
v_0E \xrightarrow{\text{(a)}} av_0aE \xrightarrow{\text{(d)}} abv_0baE \xrightarrow{\text{(d)}} abbv_0bbaE \xrightarrow{\text{(c)}} abbabbaE
\]
(The production from <ref> used in each derivation is written above the arrow.)
The productions in <ref> are context-free, as $v_0$ employs a parameter,
and they are in GNF, as the root of the right-hand side of each
production is a terminal (either $a$ or $b$).

Notice that all regular grammars are context-free and in GNF.

In deterministic context-free tree grammars in GNF,
including deterministic regular tree grammars, if both $ρ₁=v \produceσ(\vv{τ})$
and $ρ₂=v \produceσ(\vv{τ}')$ are productions in $R$, then $\vv{τ}=\vv{τ}'$.
Deterministic regular grammars define deterministic regular forests (DRF), a proper
subset of regular forests, also called path-closed forests <cit.>.
Likewise, deterministic context-free tree grammars define deterministic
context-free forests (DCF).
In contrast to context-free string grammars, not every context-free tree grammar
has a GNF—but every deterministic tree grammar does <cit.>.
The class of context-free forests that can be described by a grammar in GNF
is denoted as NCFGNF.

In this paper, we use an extended version of context-free tree grammars where
the initial variable $v₀$ is replaced by an initial tree.

Extended context-free tree grammars (ECFTGs) generalize standard CFTGs
by allowing initialization by any tree $t₀$. Otherwise, the semantics are the same.

A standard CFTG is extended by definition, with $t₀=v₀$.
We show that extended grammars are as expressive as standard grammars:

For every ECFTG (in GNF), there exists a CFTG (in GNF) that defines the same forest.

Let $G=⟨Σ, V, t₀, R⟩$ be an ECFTG.
If the initial tree $t₀$ is a variable, $t₀=v∈V$ and we are done.
Otherwise, let CFTG $G'=⟨Σ, V', v₀, R'⟩$,
introducing the initial variable $v₀∉V$, $V'=V∪❴v₀ ❵$, and
employing the original productions, $R⊆R'$.
If the initial tree is terminal, $t₀=σ₀∈Σ$, simply add the rule $v₀ \produce σ₀$ to $R'$.
Else $t₀$ is not a leaf: Let $t₀=ξ₀(\vv{t₀})$, where the root $ξ₀∈Σ∪V$
is of rank one or above.
For every production $ξ₀(\vv{x}) \produceτ∈R$ if $ξ₀$ is a variable, or production $ξ₀(\vv{x}) \produceτ$, $τ=ξ₀(\vv{x})$ if $ξ₀$ is terminal,
add production $v₀ \produceτ[\vv{x}←\vv{t₀}]$ to $R'$.

Derivations of the initial variable $v₀$ expand it into the initial tree $t₀$ and
apply an original $R$ derivation in a single step.
After $v₀$ is derived, the resulting tree form is identical to the one derived from $t₀$,
\[
v₀[v₀ \produceτ[\vv{x}←\vv{t₀}]]=t₀[ξ₀(\vv{x}) \produceτ],
\]
thus they derive the same forest.

This construction preserves GNF.
Newly introduced rules derive tree $τ[\vv{x}←\vv{t₀}]$,
whose root is terminal given that either  the root of $t₀$ is terminal,
or otherwise  $τ$ is the right-hand side of a rule in $R$, starting with a terminal
given that the original grammar is in GNF.

§ PRELIMINARIES: NOMINAL SUBTYPING WITH VARIANCE

This work focuses on Kennedy:Pierce:07 abstract type system of nominal subtyping with variance.
This type system supports nominal subtyping with declaration-site variance
as found in, e.g., and .
<ref> describes the abstract syntax (sub-figures (a,b))
and semantics (sub-figures (c,d,e)) of the type system, both adopted from
Note that we reuse notations introduced in <ref>
in the context of formal forests, foreshadowing the connection
between the two formalisms.

$P \produceΔ~q$     ⏎
$Δ\produceδ₁~…~δₙ$     $n≥0$ ⏎
$δ\produce γ(\vv{◇ x}):\vv{τ}$
$\begin{cases}\params(\vv{τ})⊆\vv{x} ⏎\vv{τ}∩\vv{x}=∅\end{cases}$ ⏎
$\vv{x} \produce◇ x₁,…,◇ xₖ$
$k≥0$ ⏎
$◇\produce∘~|~+~|~-$ ⏎
$k≥0$ ⏎
$τ\produce γ(\vv{τ})~|~x$ ⏎
$q \produce t_⊥\subtype t_⊤$ ⏎
$t\produceγ(\vv{t})$ ⏎
$\vv{t} \produce t₁,…,tₖ$
$k≥0$ ⏎

$P$     program ⏎
$δ$     class declaration ⏎
$Δ$     class table; a set of class declarations ⏎
$γ$     class name drawn from finite set $Γ$ ⏎
$τ$     unground type ⏎
$\vv{τ}$     sequence of unground types ⏎
$x$     type parameter drawn from finite set $X$ disjoint from $Γ$ ⏎
$◇x$     type parameter with variance ⏎
$\vv{◇x}$     sequence of type parameters with variances ⏎
$∘$     invariance ⏎
$+$     covariance ⏎
$-$     contravariance ⏎
$q$     subtyping query ⏎
$t$     ground type ⏎
$\vv{t}$     sequence of ground types ⏎
(a) Syntax     (b) Nomenclature ⏎

$\infer{t \inheritsτ[s]}{t⊑ₛ γ(\vv{x}) & γ(\vv{x}):τ}$ ⏎

$\rulename{Var}\infer{γ(\vv{t}) \subtype γ(\vv{t}')}{∀ i, tᵢ \subtype_{\vof[i]{γ}} t'ᵢ}$   $\infer{t \subtype₊ t'}{t \subtype t'}$   $\infer{t \subtype_∘ t}{}$   $\infer{t \subtype₋ t'}{t \suptype t'}$ ⏎
$\rulename{Super}\infer{t \subtype t”}{t \inherits t' & t' \subtype t”}$

(c) Inheritance     (d) Subtyping ⏎

Acyclic ⏎ Inheritance
$γ(\vv{τ}) \inherits⁺ γ'(\vv{τ}')~⇒~γ≠γ'$ ⏎
Valid ⏎ Variance
- &◇=+⏎
∘ &◇=∘ ⏎
\end{cases}$   $\infer{\vv{◇ x}⊢xᵢ}{◇ᵢ∈❴∘,+❵}$   $\infer{\vv{◇ x}⊢γ(\vv{t})}{∀ i, \begin{cases}
\vof[i]{γ}∈❴∘,+❵⇒\vv{◇ x}⊢τᵢ ⏎
\vof[i]{γ}∈❴∘,- ❵⇒¬\vv{◇ x}⊢τᵢ
\end{cases}}$   $\infer{γ(\vv{◇ x}):τ~\checkmark}{\vv{◇ x}⊢τ}$

2|c|(e) Well-Formedness ⏎

Kennedy and Pierce's type system (without mixin inheritance)

The full syntax of the type system is given in
[(a)]figure:type:system and a nomenclature is available in
A program consists of a class table $Δ$ and a subtyping query $q$.
A class table over a finite set of class names $Γ$ is a finite set of
inheritance rules $\boldsymbol\delta$. An inheritance rule $\delta=γ(\vv{◇ x}):\vv{τ}$ declares a
parameterized class (polytype) named $γ$ and its inheritance from (super-)
types $\vv{τ}$; to highlight that a sequence of supertypes $\vv{τ}$ is empty,
we write $∅$ after the colon. We require supertypes to reference only class
parameters, $\params(\vv{τ})⊆\vv{x}$. Although Kennedy and Pierce included
mixin inheritance in their type system, allowing a class to inherit one of
its parameters, we chose to exclude it; accordingly, $\vv{τ}∩\vv{x}=∅$ (nevertheless, the implications of
mixin inheritance are discussed in <ref>). Variance is denoted by
a diamond $◇$, which can be covariant, $◇=+$, contravariant, $◇=-$, or
invariant, $◇=∘$. The variance of the i parameter of class $γ$ is
denoted $\vof[i]{γ}$, and the vector describing all $γ$ parameter variances is
denoted $\vof{γ}$. A subtyping query $t_⊥\subtype t_⊤$ (also
written $t_⊥\subtype_Δ t_⊤$), for subtype $t_⊥$ and supertype $t_⊤$, both
ground, type checks if and only if $t_⊥$ is a subtype of $t_⊤$ (considering
class table $Δ$).

For example, we can write the program of <ref>
using abstract syntax as follows (recall that we use an abbreviated notation of monadic terms):

\begin{equation}\label{eq:example:program}
\begin{aligned}
\Delta&\begin{cases}
&a(+x): \emptyset \\
&b(+x): \emptyset \\
&E: \emptyset \\
&v_0(\circ x): a v_0 a x, a a x, a x, b v_0 b x, b b x, b x \\
\end{cases} \\
&\:v_0 E \subtype a b b a b b a E
\end{cases}
\end{aligned}
\end{equation}

Class table $\Delta$ has four classes, $a$, $b$, $E$, and $v_0$.
In , type parameters are invariant by default, covariance is denoted by
the keyword out, and contravariance by the keyword in.
Therefore, the type parameters of $a$ and $b$ are covariant ($\vof[1]{a}=\vof[1]{b}=+$),
and the type parameter of $v_0$ is invariant ($\vof[1]{v_0}=\circ$).
Query $q$ is the subtyping query invoked by the variable assignment in line 3 of <ref>.

According to the type inheritance relation $t \inherits t'$, defined in [(c)]figure:type:system,
type $t$ inherits type $t'$ if $t'$ matches one of the supertypes of $t$'s root.
Unlike Kennedy and Pierce, we distinguish between the type inheritance relation and
class inheritance, $γ:γ'$, found in class declarations.
We also use the transitive closures of these:

\begin{equation}\label{eq:transitive:inheritance}
\begin{aligned}
\infer{γ(\vv{x}):^* γ(\vv{x})}{} \qquad
\infer{γ(\vv{x}):^*τ[\vv{x}'←\vv{τ}]}
{γ(\vv{x}): γ'(\vv{τ}) & γ'(\vv{x}'):^*τ}
\end{aligned}
\end{equation}

The same rules apply for transitive type inheritance. The asterisk is replaced
with a plus $+$ in the non-reflexive variants $:⁺$ and $\inherits⁺$.

The rules of subtyping are detailed in [(d)]figure:type:system.
The Super rule establishes that a class is a subtype of its supertypes.

The Var rule handles the type parameters, depending on their variance:
Statement $γ(t) \subtypeγ(t')$ implies $t \subtype t'$ if $γ$'s type parameter
is covariant, $t=t'$ if invariant, and $t' \subtype t$ if contravariant.
If $γ$ accepts multiple type parameters, then each may have its own variance.
We also define transitive subtyping:

\begin{equation}
\begin{aligned}
\infer{t \subtype^* t}{\relax} \qquad
\infer{t \subtype^* t”}{t \subtype t' & t' \subtype^* t”}
\end{aligned}
\end{equation}

For example, we can use the Super and Var rules to prove the
subtyping query of <ref>:

\begin{equation*}
\newcommand{\alert}[1]{#1}
\begin{tabular}{rll}
& $\alert{v_0} E \subtype a b b a b b a E$ & \\
$\Leftarrow$\quad & $\alert{a} v_0 a E \subtype \alert{a} b b a b b a E$ & $(\textsc{Super},~v_0(\circ x) : a v_0 a x)$ \\
$\Leftarrow$\quad & $\alert{v_0} a E \subtype b b a b b a E$ & $(\textsc{Var},~\vof[1]{a}=+)$ \\
$\Leftarrow$\quad & $\alert{b} v_0 b a E \subtype \alert{b} b a b b a E$ & $(\textsc{Super},~v_0(\circ x) : b v_0 b x)$ \\
$\Leftarrow$\quad & $\alert{v_0} b a E \subtype b a b b a E$ & $(\textsc{Var},~\vof[1]{b}=+)$ \\
$\Leftarrow$\quad & $\alert v_0 b b a E \subtype \alert{b} a b b a E$ & $(\textsc{Super},~v_0(\circ x) : b v_0 b x)$ \\
$\Leftarrow$\quad & $\alert{v_0} b b a E \subtype a b b a E$ & $(\textsc{Var},~\vof[1]{b}=+)$ \\
$\Leftarrow$\quad & $a b b a E \subtype a b b a E$ \checkmark & $(\textsc{Super},~v_0(\circ x) : a x)$
\end{tabular}
\end{equation*}

Note that this subtyping query is recursive because the type parameters of classes $a$ and $b$
are covariant. If the parameters were contravariant, then the query would reverse ($\suptype$)
after applying the Var rule.

A class table is well-formed if it complies with the rules in
[(e)]figure:type:system. First, inheritance must be acyclic, i.e., a
class may not (transitively) inherit itself. Thus, the class inheritance closure $:^*$ is
finite. Kennedy and Pierce also explain that transitive subtyping and semantic
soundness rely on certain restrictions to class inheritance, $γ(\vv{◇ x}):τ$.

To demonstrate the problem, consider the following invalid class declarations:

\begin{equation*}
\begin{aligned}
& a(-x) : \emptyset \\
& b(+y) : a(y)
\end{aligned}
\end{equation*}

Type parameter $y$ of class $b$ is covariant, but it also substitutes for $a$'s
contravariant parameter $x$.
This means that $y$ can be used both covariantly and contravariantly.
For instance, if $c \inherits d$, then

\begin{equation*}
b(c) \subtype b(d)
\end{equation*}

but also

\begin{equation*}
b(d) \subtype a(c)
\end{equation*}

One way to solve this issue is by changing $b$'s supertype to $a(a(y))$:

\begin{equation*}
b(+y) : a(a(y))
\end{equation*}

Once done, $y$ behaves covariantly, as expected:

\begin{equation*}
\begin{tabular}{rll}
& $bc \subtype aad$ & \\
$\Leftarrow$\quad & $aac \subtype aad$ & $(\textsc{Super},~b(+y) : aay)$ \\
$\Leftarrow$\quad & $ac \suptype ad$ & $(\textsc{Var},~\vof[1]{a}=-)$ \\
$\Leftarrow$\quad & $c \subtype d$ \checkmark & $(\textsc{Var},~\vof[1]{a}=-)$ \\
\end{tabular}
\end{equation*}

Intuitively, one may think of a covariant type parameter as defining a
‟positive position”, and a contravariant one a ‟negative position”. A covariant
type parameter $x∈\vv{x}$ can be placed in supertype $τ$ only in positive
positions, and if it is contravariant, only in negative positions. A
sub-tree $τ'$ of $τ$ in a negative position reverses its polarity: Positive
positions become negative, and negative positions become positive. The initial
position of $τ$ is positive. In this context, an invariant position is both
positive and negative, and so are invariant type parameters. Thus, invariant
type parameters can appear in any position, while a type in an invariant
position contains only invariant type parameters, because its positions are both
positive and negative.

For example, consider the following class table:

\begin{equation}\label{eq:example:class:table}
\begin{aligned}
a(+x):∅&\qquad\qquad d(+x₁): adax₁ ⏎
b(-x):∅&\qquad\qquad e(-x₂): bbabx₂ ⏎
c(∘ x):∅&\qquad\qquad f(-x₃,∘x₄,+x₅): af(x₄, ax₄, x₄)
\end{aligned}
\end{equation}

This class table, ranging over classes $a,b,c,d,e,$ and $f$, is well-formed.
The table has no inheritance cycles, e.g., although type $d$ appears in the
type it inherits, we consider only the roots of supertypes in checks of
circularity.  Restrictions on the use of type parameters are also respected.
Covariant type parameter $x₁$ in type $adax₁$ is in a positive position, as both $a$ and $d$ are covariant.
Contravariant type parameter $x₂$ in type $bbabx₂$ is in a negative position: Type $b$ reverses the
polarity an odd number of times and type $a$ does not change it, so the final position is negative.
Invariant type parameter $x₄$ can be placed in all the positions of $f$ in type $af(x₄, ax₄, x₄)$,
and it is the only parameter suitable for the invariant (second) position.
The programming language enforces the rules of [(e)]figure:type:system;
in <ref>, we encode the class table of <ref> as
interface declarations that compile as expected.
[float=ht,style=csharp,caption=The class table of <ref> encoded in ,label=lst:example:class:table]
interface a<out x>         interface d<out x1> : a<d<a<x1>>>
interface b<in x>          interface e<in x2> : b<b<a<b<x2>>>>
interface c<x>             interface f<in x3, x4, out x5> : a<f<x4,a<x4>,x4>>

Let the type system featured in <ref> be denoted as .
<cit.> proved that is undecidable.
Nevertheless, they introduced three restrictions on , each defining a
decidable type system fragment of .
Each restriction removes a certain feature of the type system:
contravariance (C), expansive inheritance (X), or multiple instantiation inheritance (M).
We denote a type system by the set of features used by its programs, e.g.,
is an alias of , and its subset containing only programs without
contravariance is denoted by .
Each element of the power set of $❴\text{C}, \text{X}, \text{M}❵$ defines
a type system. We organize the eight type systems in a lattice, depicted in
<ref>, ordered with respect to inclusion (of features
and programs). The bottom of the lattice is , bare of any special features.
All these type systems employ polyadic parametric polymorphism, i.e.,
where a class can have multiple type parameters.

The first restriction of Kennedy and Pierce forbids contravariant type
parameters, $-x$, yielding type system .  The second restriction disallows
multiple instantiation inheritance, making inheritance deterministic:
If $γ(\vv{x}):⁺ γ'(\vv{τ})$ and $γ(\vv{x}):⁺ γ'(\vv{τ}')$,
then necessarily $\vv{τ}=\vv{τ}'$.
For instance, the class table of <ref> does not conform
to this restriction, as class $v_0$ extends both $a(x)$ and $a(a x)$.
Kennedy and Pierce suspected that single instantiation inheritance, featured in , is not enough
to achieve decidability.
<cit.> verified the suspicion by simulating Turing machines
with subtyping queries in , which employs deterministic inheritance.
To make single inheritance decidable, it had to be further restricted; the resulting type
system will not be discussed in this paper.

The third restriction, due to <cit.>, limits the growth of types during subtyping.
Consider, for example, the class table depicted in <ref>.
Given type $d t$, for some type argument $t$, on either side of a subtyping query,
it can change to $adat$ by applying the Super rule and then to $dat$ by Var,
yielding the type $dt'$ for $t'=at$.
Type $d t$ can, therefore, expand indefinitely during subtyping.
Kennedy and Pierce named this kind of inheritance recursively expansive and showed its
connection to infinite subtyping proofs.

Originally, Viroli illustrated this growth of types by a graph, depicting the dependencies between
the different type variables employed by the class table.
In this paper, however, we use a more approachable definition, following an equivalence result of
Kennedy and Pierce.
Consider the following definition:

Set $T$ of types is closed under inheritance and decomposition if for every type $γ(\vv{t})$ in $T$,
its sub-trees are in $T$, $\vv{t}⊂T$, and so are its supertypes, $γ(\vv{t}) \inherits t⇒ t∈T$.
The minimal super-set of set $S$ closed under inheritance and decomposition is denoted $\cl(S)$.
(The curly braces of set $S$ may be omitted inside $\cl(·)$, e.g., $\cl(t₁, t₂)$.)

With the class table of <ref>, for instance, $\cl(dt)⊃❴daⁿt~|~n≥0❵$,
as explained above.
<cit.> noted that the set of types involved in a subtyping query $t_⊥\subtype t_⊤$ is
contained in their inheritance and decomposition closure, $\cl(t_⊥, t_⊤)$, following the
Super (inheritance) and Var (decomposition) rules.
If a closure $\cl(t_⊥, t_⊤)$ is finite, then the subtyping query $t_⊥\subtype t_⊤$ is decidable,
as we can trace infinite subtyping cycles.
Therefore, if the closure $\cl(t, t')$ of any two types $t$ and $t'$ is finite,
subtyping is decidable, and the class table is called finitary.
Kennedy and Pierce proved that subtyping with non-expansive inheritance is decidable,
by showing that a class table is non-expansive if and only if it is finitary.
Thus, we can use <ref> to define
non-expansive inheritance directly:

Class table $\Delta$ is non-expansive if and only if the inheritance and
decomposition closure of any set of types $T$ is finite, $|\cl(T)|<\infty$.

We denote the type system fragment where all the class tables are non-expansive as .

If a class table $Δ$ conforms to type system $𝓢$, we write $𝓢⊢Δ$.  For example,
class table $Δ$ of <ref> conforms to , written $\TKP⊢Δ$, as
it is well-formed, but not to , written $\Tcm \nvdashΔ$, as its inheritance is
expansively recursive.

§ SUBTYPING MACHINES AS FOREST RECOGNIZERS

A subtyping machine is a set of type system definitions that utilize subtyping and
its rules to perform a computation. <cit.>, who coined the term,
used subtyping machines to simulate Turing machines in , thus proving its
type system is undecidable.

This section formalizes subtyping machines as
general computation devices, following a standard approach in fluent API
research <cit.>.
Subtyping machines recognize formal forests, i.e., sets of trees
or terms. In <ref>, we use this formalism to classify
the computational power of decidable subtyping in its various forms.

This section's running example is the program shown in <ref>.
We focus on the type declaration in the first two lines of the code:

interface a<out x>  interface b<out x>  interface E
class v0<x> : a<v0<a<x>>>, a<a<x>>, a<x>, b<v0<b<x>>>, b<b<x>>, b<x>

Let us name this program .
In <ref>, we introduced  as an example of a subtyping
machine that recognizes palindromes, but did not explain what “recognize” means.
Our goal is, therefore, to formalize an interpretation of  as
a formal forest of palindromes.

In our type system, presented in <ref>, a program $P=Δ~q$
comprises a set of declarations $Δ$ constituting a class table and a query (or
assertion) $q=t_⊥\subtype t_⊤$. The query succeeds (compiles) if and only if
type $t_⊥$ is a subtype of type $t_⊤$ considering class table $Δ$ and the
subtyping semantics of the type system, $t_⊥\subtype_Δ t_⊤$. Therefore, a
given class table defines the set of queries that compile against it; we call
this set the extent of the class table.

The extent of 's class table $\Delta$ (written using abstract
syntax in <ref>) contains, for instance, the queries

\begin{equation*}
\text{$v_0 E \subtype aE$, \qquad $v_0 E \subtype abaE$, \qquad and\ \ \ $v_0 E \subtype abbabbaE$,}
\end{equation*}

because they type check against $\Delta$.
In general, the extent of $\Delta$ contains all the queries of the form

\begin{equation*}
v_0 E \subtype p E
\end{equation*}

where $p$ is a palindrome over $\{a, b\}$ (we prove this in <ref>).
$\Delta$'s extent, however, also contains queries that do not include palindromes at all,
such as

\begin{equation*}
\text{$E \subtype E$, \qquad $v_0 a E \subtype baE$, \qquad and\ \ \ $a v_0 E \subtype abE$.}
\end{equation*}

To correlate 's extent with a forest of palindromes,
we first need to restrict the contents of its queries.

Recall that formal grammars distinguish between
terminal and non-terminal (variable) symbols, drawn from sets $Σ$ and $V$,
respectively. This dichotomy allows grammars to use variables as auxiliary
symbols, which cannot appear as part of derived words. To make our definition of
subtyping machines effective, we introduce an analogous separation in $Γ$, the
set of class names in $Δ$. Let sub-alphabet $Σ_⊥⊆Γ$ and
super-alphabet $Σ_⊤⊆Γ$ be the domains of subtypes $t_⊥$ and
supertypes $t_⊤$ in subtyping queries, i.e., types $t_⊥$
and $t_⊤$ consist of type names drawn from designated $Γ$ subsets $Σ_⊥$
and $Σ_⊤$.
We amend Kennedy and Pierce's type system, defined in <ref>,
to include the sub- and super-alphabets:

\begin{equation}\label{eq:amendment}
q \produce t_⊥\subtype t_⊤ \quad {\scriptstyle\constraint{t_⊥∈Σ_⊥^▵,~t_⊤∈Σ_⊤^▵}} \qquad (Σ_⊥^▵,Σ_⊤^▵\subseteq\Gamma)
\end{equation}

From this point on, we discuss programs that include the amendment presented in <ref>.
We define the extent of class table $Δ$ as the subset of $Σ_⊥^▵⨉Σ_⊤^▵$:

Let $Δ$ be a class table, as described in <ref>.
The extent of $Δ$, denoted $L(Δ)$, contains all the pairs of types $⟨t_⊥, t_⊤⟩$ such
that the subtyping query $t_⊥\subtype t_⊤$ type checks against $Δ$:
\[
L(Δ)=❴⟨t_⊥,t_⊤⟩~|~t_⊥∈Σ_⊥^▵,~t_⊤∈Σ_⊤^▵,~t_⊥\subtype_Δ t_⊤❵
\qquadΣ_⊥,Σ_⊤⊆Γ
\]

<ref> gives us more control over the expressiveness
of programs.
The extent of a class table, however, does not yet describe a formal forest.
Although types are homomorphic to trees, an extent is a set of type pairs
$⟨t_⊥,t_⊤⟩$, rather than a set of lone types.
To solve this issue, we fix the subtype $t_⊥$ to some constant type that is
no longer a variable part of the subtyping query.
Then, a class table $Δ$ defines a (tree) language of $t_⊥$ supertypes;
this set is the projection of type $t_⊥$ onto extent $L(Δ)$:

Let $Δ$ be a class table and $t_⊥$ be a type, as described in <ref>.
The language of $Δ$ over $t_⊥$, denoted $L_{t_⊥}(Δ)$, contains all the supertypes of $t_⊥$ against $Δ$,
\[
L_{t_⊥}(Δ)=❴t_⊤~|~⟨t_⊥, t_⊤⟩∈L(Δ) ❵=❴t_⊤~|~t_⊤∈{Σ_⊤}^▵,~t_⊥\subtype_Δ t_⊤❵
\qquadΣ_⊤⊆Γ
\]

We can now use <ref> to describe 's
language over subtype $t_\bot = v_0 E$ as a forest of palindromes:

\begin{equation}\label{eq:language:pali}
L(\textsf{Pali})_{v_0E} = \{ p E ~|~ \text{$p$ is a palindrome} \} \qquad (\Sigma_\top = \{a, b, E\})
\end{equation}

In other words,  is a subtyping machine that recognizes palindromes
as supertypes of type $t_\bot = v_0 E$.
We prove <ref> in <ref>.

Considering <ref>, we see that class tables describe formal
languages (forests), as grammars do, and their
compilers serve as language (forest) recognizers, similarly to grammar parsers.
Correspondingly, a type system is a family of programs that recognizes a class of languages:

The computational class (expressiveness) of subtyping-based type system $𝓢$, denoted $𝓛(𝓢)$,
is the set of languages described by its programs:
\[
𝓛(𝓢)=❴L_{t_⊥}(Δ)~|~t_⊥∈Σ_⊥^▵,~𝓢⊢Δ❵ \qquad Σ_⊥⊆Γ
\]

(Recall that $𝓢⊢Δ$ means class table $Δ$ is well-formed
and conforms to the restrictions of type system $𝓢$.)

§ EXPRESSIVENESS OF DECIDABLE SUBTYPING

Recall that the type system of Kennedy and Pierce features contravariance (C),
expansive inheritance (X), and multiple instantiation inheritance (M).
Subset $S$ of $❴C,X,M❵$ describes the type system fragment of
endorsing only the features included in $S$.
Subtyping in and is known to be undecidable, but it is decidable in
the other six fragments <cit.>.
In <ref>, we described class tables as subtyping machines that recognize formal forests
(<ref>) and defined the expressiveness
of a type system as the class of forests that its tables recognize (<ref>).
Now we use these formalizations to describe the computational power of Kennedy and Pierce's
decidable type system fragments.

Given type system $𝓢$, we show $𝓢$ is at least as
complex as class of languages $𝓛$ by proving that any language $ℓ$
in $𝓛$ is described by some class table $Δ$ and subtype $t_⊥$ of $𝓢$:
\[
\big(∀ℓ∈𝓛,~∃Δ, t_⊥,~𝓢⊢Δ,~ℓ=L_{t_⊥}(Δ)\big)~⇒~𝓛⊆𝓛(𝓢)
\]
To show that type system $𝓢$ is not more complex than class of
languages $𝓛$, we prove that any class table $Δ$ and subtype $t_⊥$ describe an $𝓛$
\[
\big(∀Δ, t_⊥,~𝓢⊢Δ,~∃ℓ∈𝓛,~ℓ=L_{t_⊥}(Δ)\big)~⇒~𝓛(𝓢)⊆𝓛
\]
If the expressiveness of $𝓢$ is bounded by $𝓛$ from both directions,
then it is exactly $𝓛$:
\[
\]
In all the following proofs, formal languages are specified by their corresponding grammars.

§.§ Non-Expansive Subtyping Is Regular

<cit.> raised a concern about non-expansive inheritance restricting
some conventional class table use-cases.
We go one step further by showing that the expressiveness of non-expansive class tables is regular,
i.e., of the lowest tier.

Any regular forest can be encoded in a class table using only multiple instantiation inheritance:
\[
\|NRF|⊆𝓛(\Tm)
\]

We want to simulate the derivation of a regular tree grammar with subtyping.
In the first step, we encode every terminal node $\sigma$ of rank $k$ by
class $\sigma$ that has $k$ type parameters.
Thus, terminal trees (derived from the grammar) and types (in subtyping queries)
coincide, as both use the same term notation and base alphabet, e.g.,
$\sigma_1(\sigma_2, \sigma_3 \sigma_4)$ is both a tree and a type.
Next, every regular derivation rule $
v \produce \sigma(\vv{v})
$ is directly encoded by a corresponding inheritance rule $
v : \sigma(\vv{v}).
With these definitions, the subtyping query $v \subtype t$ simulates the grammar
derivation $v \rightarrow^* t$:
Let $t=\sigma(\vv{t})$.
Grammar variable $v$ derives $t$ if $v$ derives $\sigma$, $v \produce \sigma(\vv{v})$
and then, recursively, variables $\vv{v}$ derive $\sigma$'s children, $\vv{v} \rightarrow^* \vv{t}$.

Correspondingly, the subtyping query $v \subtype t$ type checks if class $v$
inherits type $\sigma$, $v : \sigma(\vv{v})$ and then, recursively, types $\vv{v}$ are subtypes
of $\vv{t}$, $\vv{v} \subtype \vv{t}$.

The recursion of subtyping originates from the Var rule, under the condition that
the type parameters of $\sigma$ are covariant.

Consider the regular tree grammar in <ref> in <ref>,
describing lists of Peano numbers.
This grammar can be encoded in a program with neither contravariance nor expansive recursive inheritance, as
demonstrated in <ref>.
[style=csharp,caption=program encoding the grammar of <ref>,label=lst:example:regular:program]
interface z                     // Terminal leaf $\color{comment}\+z+$
interface s<out x>              // Terminal node $\color{comment}\+s+(x)$
interface nil                   // Terminal leaf $\color{comment}\+nil+$
interface cons<out x1, out x2>  // Terminal node $\color{comment}\+cons+(x1, x2)$
interface Nat: // Variable $\color{comment}\-Nat-$
z,         // Production $\color{comment}\-Nat-\produce\+z+$
s<Nat>   // Production $\color{comment}\-Nat-\produce\+s+(\-Nat-)$
interface List:        // Variable $\color{comment}\-List-$
nil,               // Production $\color{comment}\-List-\produce\+nil+$
cons<Nat, List>  // Production $\color{comment}\-List-\produce\+cons+(\-Nat-, \-List-)$
// Subtyping query $\color{comment}\-List-\subtype\+cons+(\+ssz+, \+cons+(\+sz+, \+cons+(\+z+, \+nil+)))$
cons<s<s<z>>, cons<s<z>, cons<z, nil>>> t=(List) null;

The grammar terminals s+, z+, cons+, and nil+ are encoded
by interfaces with covariant type parameters, and the grammar variables
Nat- and List- are encoded by interfaces whose supertypes are the possible productions
of each variable.
The last line of the listing contains a variable assignment that
ensures type $v₀=\-List-$ is a subtype of
the type encoding the list $⟨{}2,1,0⟩$ (described in <ref>).
This assignment compiles, as expected.

A given regular forest is described by a regular tree grammar
$G=⟨Σ, V, v₀, R⟩$.
We encode $G$ as class table $Δ$, $\Tm⊢Δ$, such that
the language of $Δ$ (over $t_⊥=v₀$) is exactly the language described
by $G$, $L(G)$.

The class table $Δ$ employs type names drawn from $Γ=Σ∪V$.
The number of type parameters of each type $σ∈Σ$ is identical to its rank in $G$,
and all type parameters are covariant (nodes $v∈V$ are leaves).
For each regular production rule $v \produceσ(\vv v)∈R$, set
type $σ(\vv v)$ as a super-type of type $v$, $v:σ(\vv v)$.
We set the subtype to $t_⊥=v₀$, and the super-alphabet to $Σ_⊤=Σ$.

Correctness of the construction
Subtyping against $Δ$ directly emulates derivations of grammar $G$,
where the left-hand side is the current variable (tree form),
starting with the initial variable $v₀$, and the right-hand side is the
derived tree.
We show that a tree $t$ is produced by variable $v$ if and only if type $t$ is a supertype
of type $v$,

\begin{equation}\label{eq:statement:1}
v→^*_G t~⇔~v \subtype t
\end{equation}

by induction on the height of $t$, $n=\height(t)$.

If $n=0$, then tree $t$ is a leaf, $t=σ$, $σ∈Σ$.
Variable $v$ derives $σ$ only if production $v \produceσ$ is in $R$.
In that case, type $σ$ is a supertype of $v$, $v:σ∈Δ$,
so $v$ is a subtype of $t$ by inheritance:
\[
v→^*_Gσ~⇔~v \produceσ∈R~⇔~
v:σ∈Δ~⇔~v \subtype \sigma
\]
Suppose <ref> holds for $n≥0$,
and let $t$ be a tree of height $n+1$, $t=σ(\vv t)$, $σ∈Σ$, $\vv t∈Σ^▵$,
where the heights of sub-trees $\vv t$ are $n$ at most.
If variable $v$ derives $t$, then there is a production $v \produceσ(\vv v)$ in $R$, for
which every child variable $vᵢ∈\vv v$ derives the corresponding child tree $tᵢ$, $\vv v→^*_G \vv t$.
This production ensures type $v$ inherits type $σ(\vv v)$.
As the heights of $\vv t$ are no higher than $n$, we can use the inductive assumption to deduce $\vv v \subtype \vv t$.
Because the type parameters of $σ$ are covariant, we can show that $v$ is a subtype of $t$ by
applying inheritance, decomposition, and the inductive assumption:
\[
\begin{aligned}
v \subtypeσ(\vv t)~&⇐~v:σ(\vv v)~∧~σ(\vv v) \subtypeσ(\vv t) ⏎
σ(\vv v) \subtypeσ(\vv t)~&⇐~\vv v \subtype \vv t~∧~\vof{σ}=\vv+
\end{aligned}
\]
Overall, we have now proved <ref>:
\[
v→^*_G t~⇔~v \produceσ(\vv v)∧\vv v→^*_G \vv t~⇔~
v:σ(\vv v)∧\vv v \subtype \vv t~⇔~v \subtype t
\]
By applying <ref> to type $t_⊥=v₀$, we get
\[
v₀→_G^* t~⇔~t_⊥\subtype t,
\]
i.e., $L(G)=L_{t_⊥}(Δ)$ by definition.

Class table $Δ$ conforms to the restrictions of the type system, $\Tm⊢Δ$.
First, the class table is well-formed. Only types $v∈V$ inherit types of the form $σ(\vv v)$
for $σ∈Σ$, so there are no inheritance cycles and no type parameters in the wrong position.
Second, $Δ$ does not employ contravariance and is non-expansive:
The structure of inheritance rules guarantees that any type in $\cl(t)$ is
higher than $t$ by one level at the most.

Non-expansive class tables describe regular forests:
\[
\]

A grammar variable $v \in V$ encodes a set of queries $Q$, $v=Q$.
These queries restrict the set of types (trees) that $v$ can derive.
Each query $q \in Q$ is of the form $t \sim x$, where
$t$ is a type,
relation $\sim$ is subtyping ($\sim=\subtype$), suptyping (the opposite
of subtyping, $\sim=\suptype$), or equivalence ($\sim$ is $=$), and
symbol $x$ is a placeholder for the type to be derived.
If query $q=t \sim x$ is included in variable $v$, then
our construction ensures that the type derived by $v$ satisfies $q$:
\[
t \sim x\in v,~v \rightarrow^* t' ~\Rightarrow~ t \sim t'
\]

For example, the initial variable $v_0$ includes a single query $t_\bot \subtype x$,
so each type $t'$ derived by $v_0$ satisfies $t_\bot \subtype t'$—the set of
these types is, by <ref>, exactly the language of
the class table over $t_\bot$.

As the class table is non-expansive, both sets of variables $V$ and productions
$R$ are finite and computable.
If the initial query $t_\bot \subtype x$ is reduced to some
other query $t \sim x$, then, as observed by <cit.>,
type $t$ is included in $t_\bot$'s inheritance and decomposition closure
$\cl(t_\bot)$ (see <ref>).
Because the class table is non-expansive, this set must be finite
(see <ref>).
Thus, for a general query $t \sim x$, there are $|\cl(t_\bot)|$ choices
for $t$, three choices for $\sim$, and, consequently, $3|\cl(t_\bot)|$ possible
queries overall.
As variables are sets of queries, we get that the
set of variables $V$ is finite, $|V|\le 2^{3|\cl(t_\bot)|}$.

A variable $v$ can derive terminal $\gamma$, $v \produce \gamma(\vv{v})$,
if and only if the queries in $v$ can be reduced to the queries in variables
$\vv{v}$; variables $\vv{v}$ then recursively simulate the subtyping algorithm with $\gamma$'s children.
In the proof below we show that as the class table is non-expansive,
it is possible to compute the derived queries $\vv{v}$ in finite time.

Consider the following non-expansive class table $Δ$, first presented in <cit.>:
\[
\begin{aligned}
N(-x) &:∅⏎
C &: NNC
\end{aligned}
\]

Let subtype $t_⊥=C$ and super-alphabet $Σ_⊤=❴N, C ❵$;
then, class table $\Delta$ is encoded by the following grammar $G$:

\begin{equation*}
\begin{array}{ll}
v₀=❴C \subtype x ❵ &\quad v₀→C ⏎
v₁=❴NC \suptype x ❵ &\quad v₀→Nv₁ ⏎
&\quad v₁→Nv₀
\end{array}
\end{equation*}

(Definitions not reachable from the initial variable are omitted.)
The resulting language is indeed regular: $L(G)=❴N^{2k}C~|~k≥0 ❵$.
The grammar productions simulate subtyping against $\Delta$ during

* Variable $v_0=C \subtype x$ derives $C$ because if $x=C$, $C \subtype C$ holds.

* Variable $v_0=C \subtype x$ derives $N v_1$ because if $x=N x'$ for some type $x'$,
the query in $v_0$ holds if $x'$ satisfies the query in $v_1$:
\[
C \subtype N x' ~\Leftarrow~ NNC \subtype Nx' ~\Leftarrow~ NC \suptype x' = v_1.
\]

* Similarly, variable $v_1=NC \suptype x$ derives $N v_0$ because if $x=N x'$ for some type $x'$,
the query in $v_1$ holds if $x'$ satisfies the query in $v_0$:
\[
NC \suptype Nx' ~\Leftarrow~ C \subtype x' = v_0.
\]

* Nevertheless, $v_1=NC \suptype x$ cannot derive $C$, because the query $NC \suptype C$
leads to an infinite proof:

\begin{equation}\label{eq:non:terminating}
NC \suptype C~⇐~NC \suptype NNC~⇐~C \subtype NC~⇐~…
\end{equation}

As the infinite proof in the latter case is cyclic, it can be identified during
the grammar construction.

*Additional notations
A query of the form $t \sim x$, where $t$ is a type, $x$ is a type parameter, and $\sim{}\!∈❴\subtype,=, \suptype❵$,
is denoted by $q$.
A set of queries is denoted by $Q$.
The set of $Q$ queries where parameter $x$ is substituted with term $τ$ is denoted by $Q[τ]$:
\[
Q[τ]=❴t \sim τ~|~t \sim x∈Q ❵
\]

The conjunction of the queries in $Q$ is denoted by $\bigwedge\!Q$.
We write $\bigwedge\!Q \vdash \bigwedge\!Q'$ to say that the queries in $Q$ imply the
queries in $Q'$, i.e., $\bigwedge\!Q\Rightarrow\bigwedge\!Q'$.
If the queries in $Q$ are true, we write $\vdash\bigwedge\!Q$.
A set of queries is minimal if it does not contain redundant queries, e.g.,
including $t \subtype x$ in addition to $t = x$ although the latter implies
the former.

Let $Δ$ be a class table of type system ,
and consider subtyping-queries between type $t_⊥$ and types over
super-alphabet $Σ_⊤$.
We show that the set of $t_⊥$ supertypes is a regular forest,
described by a regular tree grammar $G=⟨Σ, V, v₀, R⟩$.

Let $Σ=Σ_⊤$.
The set of variables $V$ contains all sets of queries over $\cl(t_⊥)$:
\[
V=❰Q~\left|~∀(t \sim{} x)∈Q,~t∈\cl(t_⊥),~
\sim{}\!∈❴\subtype,=, \suptype❵\right.❱
\]
Let $v₀=❴t_⊥\subtype x ❵$.
For every variable $v=Q∈V$ and terminal $σ∈Σ$, $\rank(σ)=n$,
add derivation rule $v \produceσ(\vv v)$ to $R$ if and only if there exists a sequence
of variables $\vv v=~\vv{Q}$, such that the sets in $\vv Q$ are minimal and $\bigwedge\!{\vvp{Q}}⊢\bigwedge\!{Q'}$,
for set $Q'$ and sets $\vvp{Q}$,

*  $Q'=Q[σ(\vv x)]=❴t \simσ(x_⊥,…,xₙ)~|~(t \sim x)∈Q ❵$

*  $∀ i=1,…,n,~Qᵢ'=Qᵢ[xᵢ]=❴t \sim xᵢ~|~(t \sim x)∈Qᵢ ❵$

Expressed in words,
parameter $x$ in $v$ is replaced with the term $σ(x₁,…,xₙ)$, $n=\rank(σ)$;
the type parameters $x$ in $\vv v$ are enumerated according to their position in the sequence;
then we require that the queries of $\vv v$ prove all the queries in $v$.
As the inheritance and decomposition closure of $t_⊥$ is always finite,
variables $\vv v$ can be found by traversing every possible proof of $t \simσ(\vv x)$.

Correctness of the construction
Observe that the grammar is well-defined.
As $Δ$ is non-expansive, $\cl(t_⊥)$ is finite, thus $V$ is finite.
For every $R$ production $v \produceσ(\vv v)$, types $t$ on the left-hand side of
$v$ queries are drawn from $\cl(t_⊥)$, so their sub-queries contain types also drawn from
$\cl(t_⊥)$ by definition of the closure. Therefore, $\vv v⊆V$, and thus $R$ is finite.

We show that variable $v=Q$ derives tree $t$, $v→_G^* t$ if and only if substituting
parameter $x$ in $Q$'s queries with type $t$ satisfies them:

\begin{equation}\label{eq:statement:2}
v→_G^* t~⇔~⊢\bigwedge\!{v[t]}
\end{equation}

<ref> is proved by induction on the height of $t$, $n=\height(t)$.

If $n=0$, then $t$ is a leaf, $t=σ$. Variable $v$, describing a set of
queries $Q$, produces $σ$ if and only if $v \produceσ∈R$.
For nodes of rank $0$, the construction introduces transition $v \produceσ$
if and only if the queries in set $Q'=❴t \simσ~|~(t \sim x)∈Q ❵$
are satisfied (by empty $\vvp{Q}$), i.e., if replacing parameter $x$ in $Q$ with
$t=σ$ satisfies its queries:
\[
v→_G^*σ~⇔~v \produceσ∈R~⇔~
\]
Suppose <ref> holds for $n≥0$,
and let $t$ be a tree of height $n+1$, $t=σ(\vv t)$, $σ∈Σ$, $\vv t∈Σ^▵$,
where the heights of $\vv t$ are, at most, $n$.
Variable $v$ derives $t$, $v→_G^* t$ if and only if $v$ derives $σ$ with production $v \produceσ(\vv v)∈R$,
where variables $\vv v$ derive $σ$'s children, $\vv v→_G^* \vv t$.
According to the construction, $v \produceσ(\vv v)∈R$ if and only if $\bigwedge\!{\vv{v}[\vv x]}⊢\bigwedge\!{v[σ(\vv x)]}$.
By the inductive assumption, $⊢\bigwedge\!{\vv v[\vv t]}$ if and only if $\vv v→_G^* \vv t$,
as the heights of types in $\vv t$ are not higher than $n$.
Thus, by assigning $\vv t$ to $\vv x$ we get that $⊢\bigwedge\!{\vv{v}[\vv t]}⊢\bigwedge\!{v[σ(\vv t)]}$,
or $⊢\bigwedge\!{v[σ(\vv t)]}$ in short:
\[
v→_G^*σ(\vv t)~⇔~v \produceσ(\vv v)∈R~∧~
\vv v→_G^* \vv t~⇔~
⊢\bigwedge\!{v[σ(\vv t)]}
\]
By applying <ref> to $v₀=❴t_⊥\subtype x ❵$, we get that
\[
v₀→_G^* t~⇔~⊢\bigwedge\!{❴t_⊥\subtype t ❵}~⇔~t_⊥\subtype t,
\]
and, therefore, $L(G)=L_{t_⊥}(Δ)$ by definition.

From <ref>, it follows that type systems and are precisely as complex as regular forests.

Class tables of non-expansive type systems describe regular forests:
\[
\]

Consider that
$\|NRF|⊆𝓛(\Tm)$ by <ref>,
$L(\Tm)⊆𝓛(\Tcm)$ as any class table conforms to , $\Tm⊂\Tcm$, and that
$𝓛(\Tcm)⊆\|NRF|$ by <ref>;
\[
\|NRF|⊆𝓛(\Tm)⊆𝓛(\Tcm)⊆\|NRF|~⇒~
𝓛(\Tm)=𝓛(\Tcm)=\|NRF| \qedhere
\]

When both expansive inheritance and multiple instantiation inheritance are taken away,
the complexity of the type system is trimmed down to deterministic forests.

Class tables of non-expansive type systems with single instantiation inheritance
describe deterministic regular forests:
\[
\]

By repeating the constructions in the proofs of <ref> and <ref>
without multiple instantiation inheritance, we get the corresponding results with deterministic
regular forests (and grammars).

In the proof of <ref>, a production $v \produceσ(\vv v)$ is directly
encoded as the inheritance rule $v:σ(\vv v)$.
Thus, the determinism of the grammar coincides with the class table's single instantiation inheritance:
\[
\infer{
\begin{array}{l}
v \produceσ(\vv{v₁})~∧~v \produceσ(\vv{v₂})~⇔~v:σ(\vv{v₁}),σ(\vv{v₂}) ⏎
v \produceσ(\vv{v₁})~∧~v \produceσ(\vv{v₂})~⇒~\vv{v₁}=\vv{v₂}
\end{array}
\]
If a class table employs single instantiation inheritance, then the subtyping algorithm,
consisting of the Var and Super rules, becomes deterministic.
In the proof of <ref>, a production $v \produceσ(\vv v)$ is
introduced if and only if the queries encoded by $\vv v$ prove the queries of $v$
when node $σ$ is encountered.
As subtyping is deterministic, at most one minimal such sequence of queries $\vv v$ exists.

§.§ Non-Contravariant Subtyping Is Context-Free

Yet another way to make subtyping decidable is by prohibiting contravariant type
Computationally, this restriction is less severe than non-expansive inheritance.
We show that non-contravariant class tables are as expressive as context-free forests
with grammars in GNF.
Recall that Greibach productions are of the form $v(\vv x) \produce σ(\vv{τ})$,
i.e., where the root of the derived tree form is terminal, $σ∈Σ$.

In this section, we use the extended variant of context-free grammars, defined in <ref>,
where the initial tree form can be any tree—not just a variable.
Recall that in <ref> we proved that extended context-free tree grammars are
equivalent in expressiveness to standard context-free grammars.

Any context-free tree grammar in GNF
can be encoded in a non-contravariant class table:
\[
\|NCF\sub{GNF}|⊆𝓛(\Txm)
\]

As in the regular case (<ref>), we want to use subtyping
to simulate grammar derivation.
Also, as before, we directly encode productions as inheritance rules and use
covariance to enable recursive subtyping.
In this case, however, we harness expansively-recursive inheritance to encode
the slightly more complex structure of context-free productions.

Consider our palindrome running example.
The context-free grammar productions in <ref> (shown in <ref>),
together with the initial tree $t_0=v_0E$, derive palindromes over $\{a,b\}$ terminated
by end-marker $E$.
We already encoded this grammar as a program in abstract syntax in
<ref> (shown in <ref>)
and in in <ref> (shown in <ref>).
Notice that the parameterized variable $v_0(x)$ is encoded by the polymorphic
[style=csharp]interface v0<x>.

Let $G=⟨Σ, V, t₀, R⟩$ be an extended context-free tree grammar in GNF.
We encode grammar $G$ as class table $Δ$, $\Txm⊢Δ$, such that the language of
$Δ$ (over $t_⊥=t₀$) is exactly the extent of the grammar, $L(G)$.

Class names are drawn from $Γ=Σ∪V$. The rank of each type $γ∈Σ∪V$
is the same as its rank in the grammar. The parameters of class $γ$ are covariant if $γ∈Σ$,
or invariant if $γ∈V$.
The subtype in queries is $t_⊥=t₀$, and supertype names are drawn from $Σ_⊤=Σ$.
For every production $v(\vv x) \produce σ(\vv{τ})∈R$, introduce inheritance rule
$v(\vv{∘ x}):σ(\vv{τ})$ to $Δ$.

Correctness of the construction
We show that tree form $t$ derives terminal tree $t'∈Σ^▵$ if and only if type $t$ is a subtype of type $t'$:

\begin{equation}\label{eq:statement:3}
t→_G^* t'~⇔~t \subtype t',~t'∈Σ^\triangle
\end{equation}

Proof is by induction on the height of $t'$, $n=\height(t')$.

If $n=0$, then $t'$ is a leaf, $t'=σ$.
Tree form $t$ derives $σ$ only if $t=σ$ (in which case, $t \subtypeσ$ is immediate),
or if the root of $t$ is a variable $v$, and there is a production $v(\vv x) \produceσ∈R$.
In the latter case, class $v$ inherits class $σ$, so type $t$ is still a subtype of $σ$:
\[
v(\vv t)→_G^*σ~⇔~v(\vv x) \produceσ∈R~⇔~
v(\vv{∘ x}):σ∈Δ~⇔~v(\vv t) \subtype \sigma
\]
Assume <ref> holds for all trees of height $n$,
and let us prove this for tree $t'=σ(\vvp{t})$ of height $n+1$.
Let $t=ξ(\vv t)$.
If the root of $t$ is a terminal node $ξ∈Σ$, then it must to be $σ$ to derive $t'$.
To complete the derivation, we require the children of $t$ to derive the children of $t'$,
$\vv t→_G^* \vvp{t}$. In this case, type $σ(\vv t)$ is a subtype of type
$σ(\vvp{t})$, by applying the Var rule and $σ$'s covariance to
get $\vv t \subtype \vvp{t}$, which is true by the inductive assumption, given that $\height(\vvp{t})\le n$:
\[
σ(\vv t)→_G^*σ(\vvp{t})~⇔~\vv t→_G^* \vvp{t}~⇔~
\vv t \subtype \vvp{t}~⇔~σ(\vv t) \subtypeσ(\vvp{t})
\]
Otherwise the root of $t$ is a variable, $ξ=v∈V$.
To derive $t'$, there must be a production $ρ=v(\vv x) \produceσ(\vv{τ})∈R$,
and its application to $t$ has to produce $\vvp{t}$,
\[
\vv{τ}[\vv x←\vv t]→_G^* \vvp{t}.
\]
Given production $ρ$, the construction introduces the corresponding
inheritance rule $v(\vv{∘ x}):σ(\vv{τ})∈Δ$, so type $t$ is a subtype of type $t'$:
By applying the Super rule, replacing $v(\vv t)$ with $σ(\vv{τ}[\vv x←\vv t])$,
and then the Var rule, to reduce the query to $\vv{τ}[\vv x←\vv t] \subtype \vvp{t}$,
which is true by the inductive assumption since $\height(\vvp{t})\le n$:
\[
\begin{aligned}
v(\vv t)→_G^*σ(\vvp{t})~&⇔~
v(\vv x) \produceσ(\vv{τ})~∧~\vv{τ}[\vv x←\vv t]→_G^* \vvp{t} ⏎
&⇔~v(\vv x):σ(\vv{τ})~∧~τ[\vv x←\vv t] \subtype \vvp{t} ⏎
&⇔~v(\vv t) \subtypeσ(\vvp{t})
\end{aligned}
\]
By applying <ref> to $t_⊥=t₀$, we get that $t₀→_G^* t~⇔~t_⊥\subtype t$;
thus, $L(G)=L_{t_⊥}(Δ)$ by definition.

Non-contravariant class tables describe context-free grammars in GNF:
\[
\]

For starters, assume that all the type parameters in the class table are covariant
(no invariance).
Consider the subtyping query $t \subtype t'$ where $t=\gamma(\vv{t})$ and $t'=\gamma'(\vv{t'})$.
To prove this query, we first use the Super rule to replace $t$ with $\gamma'(\vv{\tau}[\vv{x}\leftarrow\vv{t}])$,
assuming that class $\gamma(\vv{x})$ transitively inherits ($:^*$) the type $\gamma'(\vv{\tau})$.
In the next step, we use the Var rule to recursively validate the children of $\gamma'$,
$\vv{\tau}[\vv{x}\leftarrow\vv{t}] \subtype \vv{t'}$.
To simulate subtyping with grammar derivation, we simply encode transitive
inheritance as productions, i.e., if $\gamma(\vv{x}) :^* \gamma'(\vv{\tau})$,
$\gamma(\vv{x}) \produce \gamma'(\vv{\tau})$.
Then, the query $t \subtype t'$ is true if and only if $t \rightarrow^* t'$
because, as in the subtyping case, $t=\gamma(\vv{t})$ derives $\gamma'(\vv{\tau}[\vv{x}\leftarrow\vv{t}])$
and then $\vv{\tau}[\vv{x}\leftarrow\vv{t}]$ recursively derive $\vv{t'}$:
\[
\begin{tabular}{l@{}l@{}l}
$\gamma(\vv{t}) \subtype \gamma'(\vv{t'})$ &$~\Leftrightarrow~ \gamma(\vv{x}) :^* \gamma'(\vv{\tau})$ &
$~\wedge~ \vv{\tau}[\vv{x}\leftarrow\vv{t}] \subtype \vv{t'}$ \\
$\gamma(\vv{t}) \rightarrow^* \gamma'(\vv{t'})$ &$~\Leftrightarrow~ \gamma(\vv{x}) \produce \gamma'(\vv{\tau})$ &
$~\wedge~ \vv{\tau}[\vv{x}\leftarrow\vv{t}] \rightarrow^* \vv{t'}$
\end{tabular}
\]

Nonetheless, this clean correspondence between subtyping and context-free grammars
collapses when invariance is re-introduced to the class table.
For instance, consider the following inheritance rules:

\begin{equation}\label{eq:example:class:table:2}
\begin{aligned}
a(+x,∘ y) &:∅⏎
b(∘ z) &: a(z, z)
\end{aligned}
\end{equation}

In the query $b(t) \subtype a(t₁, t₂)$, we use inheritance and decomposition to
deduce both $t \subtype t₁$ and $t=t₂$.
If type $t$ were to be encoded directly as a tree form, as before, then it should be able to derive
the two trees $t₁$ and $t₂$, while simulating both covariance and invariance simultaneously.

To reproduce this behavior in a context-free tree grammar, we encode the kind of position
of type $t$ in the tree form that represents it.
Let $\gamma$ be the root of $t$.
If $t$ appears in a covariant position, then $\gamma$ is encoded by variable $\gamma_+$,
or otherwise by variable $\gamma_\circ$ in an invariant position.
If $t$ is in a covariant position, $t \subtype t_1$, variable $\gamma_+$ derives
the tree $t'$ if and only if $t' \subtype t_1$;
otherwise, if $t$ is in an invariant position, $t = t_2$, variable $\gamma_\circ$ derives
the tree $t'$ if and only if $t' = t_2$.

Variable $\gamma_\circ$ simply derives the node $\gamma$.
If type $t$ is in an invariant position, $t=t_2$, we encode $t$
by annotating each of its nodes with $\circ$, yielding the tree form $t_\circ$.
This tree form derives, recursively, the tree $t$ exactly, so
\[
t_\circ \rightarrow^* t' ~\Leftrightarrow~ t'=t \quad\Rightarrow\quad t_\circ \rightarrow^* t_2 ~\Leftrightarrow~ t=t_2
\]
as required.
On the other hand, if $t$ appears in a covariant position, $t \subtype t_1$,
then its children may appear in either subtyping or equivalence queries (or even both simultaneously).
Let $t=\gamma(\vv{t})$ and $t_i$ be some child of $\gamma$.
We encode $t_i$ as two tree forms, ${t_i}_+$ and ${t_i}_\circ$.
Then, we can use ${t_i}_+$ whenever $t_i$ is covariant, or otherwise ${t_i}_\circ$ when $t_i$
is invariant.
Thus, type $t=\gamma(\vv{t})$ is encoded as the tree form $t_+=\gamma_+(\vv{t_+},\vv{t_\circ})$,
where children $\vv{t_+}$ are, recursively, encoded in a similar way, and $\vv{t_\circ}$ are
encoded as mentioned above.

Continuing our example, we get that class $b$ in <ref> is
encoded by the following productions:
\[
b₊(z₊, z_∘) \produce a(z₊, z_∘) \qquad b_∘(z_∘) \produce a(z_∘, z_∘)
\]
Variable $b₊$ encodes class $b$ in covariant positions, so the first argument to type $a$
is in a covariant position, and $z₊$ is used, while the second position is invariant, and $z_∘$ is
picked instead.
Parameter $z_∘$ in variable $b_∘$ fits both positions, as the initial position (of root $a$)
is invariant.

*Additional notations
To encode unground type $τ$ as invariant tree form $τ_∘$, add
annotation $∘$ to all its nodes:

\begin{equation}\label{eq:invariant:encoding}
x_∘ &τ=x ⏎
γ_∘(\vv{τ_∘}) &τ=γ(\vv{τ})
\end{cases}
\end{equation}

We get the covariant tree form $τ₊$ by encoding both the covariant and invariant
versions of its sub-trees:

\begin{equation}\label{eq:covariant:encoding}
x₊ &τ=x ⏎
γ₊(\vv{τ₊}, \vv{τ_∘}) &τ=γ(\vv{τ})
\end{cases}
\end{equation}

To decode an invariant tree form $τ_∘$ into the tree it represents $τ$,
simply remove all the $∘$ annotations from its nodes.
If the tree form is covariant $τ₊$, also remove any $+$ annotations,
and trim-out half of the sub-trees:

\begin{equation}\label{eq:invariant:covariant:decoding}
x &τ_∘=x_∘~∨~τ₊=x₊ ⏎
γ(\vv{τ}) &τ_∘=γ_∘(\vv{τ_∘})~∨~τ₊=γ₊(\vv{τ₊}, \vv{τ_∘})
\end{cases}
\end{equation}

Observe that if variables $\vv{x₊}$ in covariant tree form $τ₊$ are substituted with covariant trees $\vv{t₊}$,
and the invariant variables $\vv{x_∘}$ are substituted with the corresponding invariant trees $\vv{t_∘}$,
then the resulting tree $τ₊[ \vv{x₊}←\vv{t₊},\vv{x_∘}←\vv{t_∘} ]$
covariantly encodes type $τ[ \vv x←\vv t ]$. The same holds for invariant tree forms:

\begin{equation}\label{eq:auxiliary:lemma}
τ_◇[ \vv{x₊}←\vv{t₊},\vv{x_∘}←\vv{t_∘} ]=(τ[ \vv x←\vv t ])_◇,
~◇∈❴+,∘ ❵
\end{equation}

(The proof is technical, by induction on the height of $τ_◇$.)

Given class table $Δ$, $\Txm⊢Δ$, fixed subtype $t_⊥$, and
super-alphabet $Σ_⊤$, we construct extended context-free tree
grammar $G=⟨Σ, V, t₀, R⟩$ that describes the same language
as $Δ$, $L(G)=L_{t_⊥}(Δ)$.

In this proof we use covariant and invariant tree encoding of types,
defined in <ref>.

Let $Σ=Σ_⊤$.
For every class name $γ∈Γ$, add variables $γ₊$ and $γ_∘$ to $V$, where $\rank(γ_∘)=\rank(γ)$
but $\rank(γ₊)=2·\rank(γ)$.
Let $t₀=(t_⊥)₊$.
For each terminal type $σ∈Σ_⊤$, add rule $σ_∘(\vv{x_∘}) \produceσ(\vv{x_∘})$
to $R$.
For each class name $γ∈Γ$ and terminal type $σ∈Σ_⊤$ of rank $n$, if
class $γ$ inherits (or, is) $σ$, $γ(\vv x):^*σ(\vv{τ})$,
introduce the following production to $R$:
\[
γ₊(\vv{x₊}, \vv{x_∘}) \produceσ(\vv{τ_{\vof[\relax]{σ}}})=σ({(τ₁)}_{\vof[1]{σ}},…,{(τₙ)}_{\vof[n]{σ}})
\]
(Recall that $\vof{σ}$ denotes the sequence of parameter variances of class $σ$,
and $\vof[i]{σ}$ denotes the variance of the i parameter.)
As inheritance is acyclic, transitive inheritance $:^*$ is finite, so the construction of $R$ must terminate.

Correctness of the construction
Each variable $σ_∘$, for terminal node $σ∈Σ$, directly derives $σ$.
Therefore, any invariant tree form $t_∘$ over $Σ$, $t∈Σ^▵$ derives the
terminal tree $t$, and only it:

\begin{equation}\label{eq:fact:1}
t_∘→_G^* t',~t∈Σ^▵~⇔~t=t'
\end{equation}

Conversely, let $t₊=γ₊(\vv{t₊},\vv{t_∘})$ be a covariant tree form.
We show that $t₊$ derives tree $t'$ if and only if type $t$ is a subtype of type $t'$:

\begin{equation}\label{eq:statement:4}
t₊→_G^* t'~⇔~t \subtype t'
\end{equation}

<ref> is proved by induction on the height of $t'$, $n=\height(t')$.

If $n=0$, then $t'$ is a leaf, $t'=σ$.
The root of $t₊$, variable $γ₊$, derives $σ$ if and only if $γ=σ$,
or if class $γ$ inherits class $σ$, $γ(\vv x):^*σ$; in both cases
the construction introduces production $γ₊(\vv{x₊},\vv{x_∘}) \produceσ$ to $R$:
\[
γ₊(\vv{t₊},\vv{t_∘})→_G^*σ~⇔~γ₊(\vv{x₊},\vv{x_∘}) \produceσ∈R~⇔~
γ(\vv{◇ x}):^*σ~⇔~γ(\vv t) \subtype \sigma
\]
Assume <ref> holds for $n≥0$, and let us prove it for tree
$t'$ of height $n+1$, $t'=σ(\vvp{t})$.
As grammar $G$ is in GNF, tree form $t₊$ can
derive terminal tree $t'$ if and only if
there is an $R$ production that derives $γ₊$, the root of $t₊$, to $σ$, the root of $t'$, $
γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{τ_{\vof[\relax]{σ}}})∈R,
$ such that  the resulting sub-tree forms
$\vv{τ_◇}$, substituted with $\vv{t₊}$ and $\vv{t_∘}$, derive $σ$'s children, $\vvp{t}$:

\begin{equation}\label{eq:part:1}
\begin{aligned}
&\qquadγ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{τ_{\vof[\relax]{σ}}})∈R~∧~
\vv{τ_{\vof[\relax]{σ}}}[\vv{x₊}←\vv{t₊},\vv{x_∘}←\vv{t_∘}]→_G^* \vvp{t}
\end{aligned}
\end{equation}

Now focus on tree forms $\vv{τ_{\vof[\relax]{σ}}}[\vv{x₊}←\vv{t₊},\vv{x_∘}←\vv{t_∘}]$
in <ref>.
Following the observation of <ref>, these forms encode the unground types $\vv{τ}$
assigned with types $\vv t$, while respecting the original variances of $σ$, $\vof{σ}$:
\[
\vv{τ_{\vof[\relax]{σ}}}[\vv{x₊}←\vv{t₊},\vv{x_∘}←\vv{t_∘}]=
(\vv{τ}[\vv x←\vv t])_{\vof{σ}}
\]
Let us then simplify <ref> by writing:

\begin{equation}\label{eq:part:2}
γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{τ_{\vof[\relax]{σ}}})∈R~∧~
(\vv{τ}[\vv x←\vv t])_{\vof{σ}}→_G^* \vvp{t}
\end{equation}

Focus on tree forms $(\vv{τ}[\vv x←\vv t])_{\vof{σ}}$ in <ref>.
If tree form $(τᵢ[\vv x←\vv t])_{\vof[i]{σ}}$ is invariant,
$\vof[i]{σ}=∘$, then by <ref>,

\begin{equation}\label{eq:part:3}
(τᵢ[\vv x←\vv t])_∘→_G^* {t'}ᵢ~⇔~
τᵢ[\vv x←\vv t]={t'}ᵢ
\end{equation}

Otherwise the tree form is covariant, $\vof[i]{σ}=+$.
As ${t'}ᵢ$ is a sub-tree of $t'$, its height is $n$ at most, so we can apply the inductive assumption
to get

\begin{equation}\label{eq:part:4}
(τᵢ[\vv x←\vv t])₊→_G^* {t'}ᵢ~⇔~τᵢ[\vv x←\vv t] \subtype {t'}ᵢ
\end{equation}

Production $γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{τ_{\vof[\relax]{σ}}})$ is induced by
the construction following the inheritance rule $γ(\vv{◇ x}):^*σ(\vv{τ})$.
Thus, type $γ(\vv t)$ is a subtype of $σ(\vv{τ}[\vv x←\vv t])$ by inheritance,
which is a subtype of $t'=σ(\vvp{t})$ by decomposition.
In <ref>, we showed that child types $\vv{τ}[\vv x←\vv t]$ and $\vvp{t}$
respect $σ$'s variances, so decomposition can be applied.
Let us extend <ref>:

\begin{equation}\label{eq:part:5}
\begin{aligned}
(\ref{eq:part:2})~&⇔~γ(\vv{◇ x}):^*σ(\vv{τ})~∧~∀ i,~\begin{cases}
τᵢ[ \vv x←\vv t ]={t'}ᵢ & \vof[i]{σ}=∘ ⏎
τᵢ[ \vv x←\vv t ] \subtype {t'}ᵢ & \vof[i]{σ}=+
\end{cases} ⏎
&⇔~γ(\vv t) \subtypeσ(\vvp{t})
\end{aligned}
\end{equation}

Overall, from <ref>, we have
\[
γ₊(\vv{t₊},\vv{t_∘})→_G^*σ(\vvp{t})~⇔~γ(\vv t) \subtypeσ(\vvp{t}),
\]
concluding the induction.

Finally, we can apply <ref> to $t₀={(t_⊥)}₊$ to get
$t₀→_G^* t~⇔~t_⊥\subtype t$; thus, $L(G)=L_{t_⊥}(Δ)$
by definition.

From <ref>, it follows that the computational class
of type system is described by context-free tree grammars in GNF.

Non-contravariant class tables describe context-free forests
that have grammars in GNF:
\[
\]

$\|NCF\sub{GNF}|⊆𝓛(\Txm)$ by <ref>;
$𝓛(\Txm)⊆\|NCF\sub{GNF}|$ by <ref>;

Type system is the subset of employing single-instantiation inheritance.
As before (<ref>), single instantiation inheritance reduces the complexity of
the type system to its deterministic variant.

Class tables of non-contravariant type systems with single instantiation inheritance
describe deterministic context-free forests:
\[
\]

Every deterministic context-free forest has a deterministic tree
grammar in GNF <cit.>.
Again, by repeating the proof of <ref>
with single instantiation inheritance, we get the corresponding results regarding

In the proof of <ref>, we encode each production $v(\vv x) \produceτ$
directly as the inheritance rule $v(\vv{∘ x}) \produceτ$.
Therefore, the grammar's determinism ensures the resulting class table does not use
multiple instantiation inheritance:
\[
\infer{
v(\vv{∘ x}):σ(\vv{τ₁}),σ(\vv{τ₂})~⇒~\vv{τ₁}=\vv{τ₂}
\begin{array}{l}
v(\vv x) \produceσ(\vv{τ₁})~∧~v(\vv x) \produceσ(\vv{τ₂})~⇔~
v(\vv{∘ x}):σ(\vv{τ₁}),σ(\vv{τ₂}) ⏎
v(\vv x) \produceσ(\vv{τ₁})~∧~v(\vv x) \produceσ(\vv{τ₂})~⇒~\vv{τ₁}=\vv{τ₂}
\end{array}
\]
In the proof of <ref>, we derive  $γ_∘$ to $σ$, which is
always deterministic, and  $γ₊$ to $σ(\vv{τ_{\vof[\relax]{σ}}})$ if and
only if $γ$ inherits $σ(\vv{τ})$, which is also deterministic when the class table employs
single instantiation inheritance:
\[
\infer{
γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{(τ₁)_{\vof[\relax]{σ}}})~∧~
γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{(τ₂)_{\vof[\relax]{σ}}})~⇔~
\vv{(τ₁)_{\vof[\relax]{σ}}}=\vv{(τ₂)_{\vof[\relax]{σ}}}
\begin{array}{l}
γ(\vv{◇ x}):^*σ(\vv{τ₁}),σ(\vv{τ₂})~⇔~
γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{(τ₁)_{\vof[\relax]{σ}}})~∧~
γ₊(\vv{x₊},\vv{x_∘}) \produceσ(\vv{(τ₂)_{\vof[\relax]{σ}}}) ⏎
γ(\vv{◇ x}):^*σ(\vv{τ₁}),σ(\vv{τ₂})~⇒~\vv{τ₁}=\vv{τ₂}
\end{array}
\]

§ TREETOP—A CONTEXT-FREE API GENERATOR

Upon its introduction <cit.>, fluent API was recognized as a promising method for
embedding domain-specific languages.
As fluent API methods are called in a chain, and not imperatively, they can
enforce a DSL syntax, or an API protocol in general, at compile time.
(See a brief introduction of the concept in <ref> and more detailed
discussions by <cit.> and <cit.>.)
The subject attracted academic interest, as
researchers introduced new fluent API techniques supporting increasingly
complex DSLs <cit.>.
Because the study of fluent API is motivated by its practical applications,
results in the field are given in the form of actual tools: fluent API
A generator accepts a DSL grammar as input, and encodes it as a
fluent API in the target programming language.
The quality of a generator is determined by its domain, i.e.,
the class of languages (and grammars) for which it can generate fluent APIs.
Generated fluent APIs also need to be practical, in terms of code size and compilation time.
The last two significant works on fluent APIs, published by <cit.> and <cit.>,
presented the generators Fling and TypeLevelLR
that support all deterministic context-free languages (DCFLs). (<cit.> later proved that
the methods implemented in these generators cannot support languages beyond DCFL.)
Programs generated by Fling and TypeLevelLR were shown to compile in linear time,
making both tools practical solutions for embedding DSLs.

The idea of integrating subtyping into fluent APIs was first proposed by <cit.>.
In his design, the role of the fluent API becomes merely to encode the input DSL program in a type,
so it can be accepted by a subtyping machine.
Grigore's subtyping machine implementation of the CYK parser
was introduced as a part of a fluent API generator that supports all context-free languages.
Moving up from DCFL to CFL is a welcome improvement:
CFLs are described by general context-free grammars, which are more expressive than
their deterministic variants (LR, LL, LALR, etc.) and are easier to compose, as they
produce no conflicts.
Unfortunately, it turned out that Grigore's generator is not practical.
The APIs it generates take a lot of time to compile, and cause the compiler to
crash with stack overflow even for basic examples.

<ref> presented in <ref> states that any tree grammar in
GNF can be recognized by a subtyping machine with expansive inheritance and
multiple instantiation inheritance.
As all context-free languages have grammars in GNF <cit.>, this
means we just found a new method for encoding CFLs using subtyping that, in contrast to Grigore's
construction, does not employ contravariance.
Nevertheless, can this method be used in a real programming language, such as ?
Unlike , endorses multiple instantiation inheritance
(required by our construction)—but its version of this feature is weaker than the one
used in this paper.
In , if class $γ$ has (transitive) supertypes $τ$ and $τ'$, then there must
not be a substitution $s$ that unifies $τ$ and $τ'$:

\begin{equation}\label{eq:unification}
\begin{aligned}
\infer{γ:⁺τ'~\checkmark}{τ \not= τ' \wedge γ:⁺τ ~\Rightarrow~ ∄ s,~τ[s]=τ'[s]}
\end{aligned}
\end{equation}

(This trait of was also discussed by <cit.>.)
It is possible that <ref> cannot be utilized to its full
potential in , as the construction described in its proof does not
conform to the restriction of <ref> in the general case.
Nevertheless, the construction does work for all CFLs. If we encode a context-free
production $vx::=αx$ as the inheritance rule $v(x):αx$, then unification with another rule $v(x):α'x$ can
only occur for $α'=α$. To prevent this, we simply ignore duplicated productions.

Thus, <ref> paved the way for the development of our new API generator,
Treetop, used to embed CFLs in †The Treetop project is available at <https://github.com/OriRoth/treetop>..
Treetop is a source generator, a project preprocessor that creates source
files, similarly to 's annotations processors.
Source generation is an experimental Visual Studio feature for introduced in 2020†For more details, see <https://devblogs.microsoft.com/dotnet/introducing-c-source-generators/>..
After an initial deployment, Treetop automatically transforms DSL grammars
into DSL APIs during the standard compilation cycle.

Given a context-free grammar $G$ in file  describing a DSL, Treetop
converts it into an equivalent grammar in GNF,
constructs class table $Δ∈\Txm$ that recognizes the DSL, $L(Δ)=L(G)$, and
encodes the result as interfaces in a new source file .
On request, Treetop also generates a subtyping-based fluent API for the DSL, following Grigore's design.

In theory, the APIs generated by Treetop should be efficient in both space (code size)
and time (compilation time of API invocations).
The class table construction described in the proof of <ref>
is straightforward, so the crucial step of the encoding is the
conversion of the input grammar to GNF.
This transformation is known to introduce a polynomial increase in the size of
the grammar <cit.>, which is translated to a similar increase in code size.
An API generated by Treetop is invoked in subtyping queries, whose compilation
time depends on the compiler implementation.
A specialized compiler can reduce Treetop's interfaces and queries
back to CFGs and strings, whose membership problem is solved in
polynomial time <cit.>.

§.§ Treetop Use Case: The Canvas API

§.§ Treetop Benchmark

§ DISCUSSION

A program that uses the subtyping algorithm to conduct a computation is called
a subtyping machine. By formalizing subtyping machines as
forest recognizers, we tie the decidable subtyping type systems of Kennedy and Pierce with familiar
families of tree grammars. We proved that non-expansively-recursive subtyping
machines recognize regular forests (<ref>) and non-contravariant
machines recognize context-free forests with GNF
(<ref>).  It was  also shown that multiple instantiation
inheritance corresponds to grammar non-determinism
(<ref>). The results are depicted in
<ref> in <ref>.

In non-expansive subtyping, all infinite proofs are cyclic, so they can be
detected by recording all visited sub-queries. The construction in the
proof of <ref> encodes cyclic proofs as
recursive productions $v \produce v$—which are immediately removed from the
grammar. This means that infinite proofs can be intercepted in
pre-computation, i.e., even before the subtyping query is inspected.
Our construction, however, assumes that one of the types
in the query is known and fixed, following our definition of the language
of a class table (<ref>). In the
future, our method may be developed into a better algorithm for non-expansive
subtyping that does not record sub-queries.

Context-free tree grammars (CFTGs) are recognized by pushdown tree automata
(PDTA), that use an auxiliary tree store and accept a tree
input <cit.>.  The proof of <ref>
describes a reduction of non-contravariant subtyping machines to CFTGs. In
contrast to the regular case, here the left-hand side of the subtyping query $t_\bot$ is encoded into the
grammar initial tree form $t₀$ and is not involved with grammar productions.
Therefore, we can resolve non-contravariant subtyping using modified PDTAs,
which accept a second input tree and use this as their initial store. Given
query $t_\bot \subtype t_\top$, we assign $t_\bot$ to the tree store (possibly after the
transformation of <ref>) and run the PDTA on
input $t_\top$. As our construction yields grammars in GNF, their
corresponding PDTAs run in real time <cit.>.
If multiple instantiation inheritance is also restricted, then the grammars
become deterministic and so does the PDTA run time. Thus, subtyping in can be resolved by a PDTA in non-deterministic real time, and in in
deterministic real time.

The theoretical results are accompanied by a POC software artifact, Treetop.
Through Treetop, we demonstrate that subtyping can be used to implement
useful and powerful metaprogramming applications even in a decidable type system.
Treetop converts context-free grammars into subtyping machines
and can be used to embed context-free DSLs as fluent APIs;
its practical relevance can be argued based on the work of
<cit.>, who found cases of context-free API protocols in the wild.
Comparing Treetop to the fluent API generator of <cit.>, we see that
both support all CFGs, but Treetop does so in a decidable type system
While Grigore's generator constructs very large subtyping machines that take
a very long time to compile, Treetop generates small machines that compile
relatively fast (in some cases).
In theory, Treetop's subtyping machines run in polynomial time.
In practice, our experiment found an example that leads to possibly
exponential compilation time using the CSC compiler.
In addition, Treetop's fluent API generation does not yet match the qualities
of previous practical generators (e.g., <cit.>).
More research work (but also implementation) is required to support features
such as auto-completion, early failure, and, run-time parsing to create an AST.

*A note on mixin inheritance
Kennedy and Pierce included mixin inheritance in their abstract type system, allowing classes
to inherit their type variables, $γ(x):x$.
Mixin inheritance was not discussed in this paper, given that not many
programming languages actually support it.
As it turns out, most of our theorems hold when this feature
is re-introduced to the type system.
The construction in the proof of <ref> is left unchanged,
since it relies on the non-expansive guarantee of inheritance in and does
not depend on the structure of inheritance declarations.
In contrast, the proof of <ref> breaks when confronted with mixin
inheritance. The construction encodes (transitive) inheritance
relations $γ(\vv{x}):^*σ(\vv{τ})$ as context-free productions in GNF, $γ(\vv{x}) \produceσ(\vv{τ})$.
The production corresponding to mixin
inheritance is an $𝜀$-production, $γ(\vv{x}) \produce xᵢ$, which does not conform
to GNF.
In this case the resulting grammar describes a general context-free forest,
so the expressiveness of is now bounded from above by class NCF instead
of NCFGNF (which is the lower bound).
The computational power of type system , however, is already
bounded from below by general deterministic NCF, so it too stays the same.
Therefore, the introduction of mixin inheritance to the subtyping-based type
systems in <ref> only adds a loose bound to ,
\[
\|NCF\sub{GNF}|⊆𝓛(\Txm)⊆\|NCF|.
\]