# On the Expressivity of Linear Recursion Schemes

Pierre Clairambault, Andrzej Murawski

► To cite this version:

Pierre Clairambault, Andrzej Murawski. On the Expressivity of Linear Recursion Schemes. 44th International Symposium on Mathematical Foundations of Computer Science, Aug 2019, Aachen, Germany. 10.4230/LIPIcs.MFCS.2019.50 . hal-02313542

HAL Id: hal-02313542

https://hal.science/hal-02313542v1

Submitted on 3 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On the expressivity of linear recursion schemes

Pierre Clairambault

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France

Andrzej S. Murawski

Department of Computer Science, University of Oxford, UK

**Abstract**

We investigate the expressive power of higher-order recursion schemes (HORS) restricted to linear types. Two formalisms are considered: multiplicative additive HORS (MAHORS), which feature both linear function types and products, and multiplicative HORS (MHORS), based on linear function types only.

For MAHORS, we establish an equi-expressivity result with a variant of tree-stack automata. Consequently, we can show that MAHORS are strictly more expressive than first-order HORS, that they are incomparable with second-order HORS, and that the associated branch languages lie at the third level of the collapsible pushdown hierarchy.

In the multiplicative case, we show that MHORS are equivalent to a special kind of pushdown automata. It follows that any MHORS can be translated to an equivalent first-order MHORS in polynomial time. Further, we show that MHORS generate regular trees and can be translated to equivalent order-0 HORS in exponential time. Consequently, MHORS turn out to have the same expressive power as 0-HORS but they can be exponentially more concise.

Our results are obtained through a combination of techniques from game semantics, the geometry of interaction and automata theory.

**2012 ACM Subject Classification** Theory of computation → Program semantics

**Keywords and phrases** higher-order recursion schemes, linear logic, game semantics, geometry of interaction

**Digital Object Identifier** 10.4230/LIPIcs.MFCS.2019.43

**Funding** Pierre Clairambault: Supported by ANR RAPIDO (ANR-14-CE25-0007) and Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), operated by the French National Research Agency (ANR).

Andrzej S. Murawski: Supported by a Royal Society Leverhulme Trust Senior Research Fellowship (LT170023).

**Acknowledgements** We would like to thank Sylvain Salvati for consultations on formal languages.

## 1 Introduction

Higher-order recursion schemes (HORS) have recently emerged as a promising technique for model-checking higher-order programs [17]. Linear higher-order recursion schemes (LHORS) were introduced in [5] to facilitate a finer analysis of HORS by mixing intuitionistic and linear types. In this paper, we investigate the expressivity of their purely linear fragment.

First, we consider *multiplicative additive* HORS (MAHORS), which in addition to the linear function types ($\to^\circ$) feature product types ($\&$), and thus allow for sharing but not re-use. We show that MAHORS are equivalent to a tree-generating variant of tree-stack automata (TSA), originally introduced to capture multiple context-free languages in the word language setting [7]. The translation from MAHORS to TSA amounts to representing the game semantics of MAHORS in the spirit of abstract machines derived from Girard's Geometry of Interaction (GoI) [11, 6]. The GoI view of computation makes it possible to interpret computation as a token machine that traverses a graph strongly related to the syntactic structure of the term. Somewhat suprisingly, so far this nearly automata-theoretic

<figure><img src="image_2.png" /></figure>
43:2 On the expressivity of linear recursion schemes

<figure><img src="image_3.png" /><figcaption>Figure 1 Typing rules for the additive linear λ-calculus</figcaption></figure>

flavour of GoI has not been exploited to establish connections with automata models, and we believe we are the first to do so explicitly. As a consequence, we can conclude that the branch languages of trees generated by MAHORS are multiple context-free and, thus, that they belong to the third level of the collapsible pushdown hierarchy [12]. In addition, we show that MAHORS are strictly more expressive than first-order HORS<fnref n="1" />, and that they are not comparable with second-order HORS.

Secondly, we consider *multiplicative HORS (MHORS)*, featuring linear function types only. In this case, our earlier MAHORS-to-TSA translation specialises to a translation into a special kind of tree-generating pushdown automata (LPDA) in which reachable configurations must be reached in a unique run. We show that MHORS and LPDA are equi-expressive and, moreover, that any MHORS can be translated to an equivalent MHORS of order 1. Further, using reachability techniques for pushdown automata, we show that LPDA are equivalent to bounded pushdown automata that forget elements stored at the bottom of the stack after the stack height exceeds a certain depth. It follows that MHORS generate regular trees, though the MHORS representation may be exponentially more succinct than order-0 HORS.

2 Linear Recursion Schemes

In this section we introduce the object of study of this paper, MAHORS and MHORS.

The main ingredient of MAHORS is the *linear λ-calculus with products* – also called the *additive linear λ-calculus*, as the product is an additive connective in the sense of Linear Logic [10]. The following definitions follow [5], restricting type formers to linear connectives (note that [5] imposes some syntactic restrictions on the shape of types and terms that we can drop here to simplify presentation, as they play no role in the technical development).

Types are formed with the ground type *o* and the connectives $\to$ and $\&$. We define the *typed terms* directly by the typing rules of Figure 1. Typing judgments have the form $\Gamma | \Delta \vdash t : \varphi$, where $\Gamma$ and $\Delta$ are two lists of variable declarations. Intuitively, $\Delta$ is the main context containing variables that can be used at most once (such terms are often called *affine* but we opt for the name *linear* nonetheless). In contrast, $\Gamma$ comprises *duplicable* variables that may be reused at will, as witnessed by the application rule. In M(A)HORS, $\Gamma$ will be used only for terminal and non-terminal symbols. Linear λ-terms are equipped with standard reduction rules; we write $\vdash_\beta$ for β-reduction for functions and products, whose definition can be found e.g. in [5]. Any term $t$ has a normal form, written BT($t$).

Trees arise as ground-type terms typable in replicable contexts representing a ranked alphabet. Recall that in HORS, a symbol *b* of arity *n* is represented as a constant *b* : *o* →

<footnote n="1">¹ Type order is defined by ord(*o*) = 0 and ord(*θ* → *θ*') = max(ord(*θ*) + 1, ord(*θ*')). The order of a HORS is the highest order of (the types of) its non-terminals.</footnote>
o with n arguments. Here, a ranked alphabet Σ may be represented in two distinct ways: multiplicatively, with b : o —o ... —o —o o, or additively, with b : &_no —o o, where &_no stands for o & ... & o (n copies)<fnref n="2" />. The choice does not impact how finite trees are represented: in both cases a ▷_β-normal Σ | — ⊢ t : o (if not —) must start with a variable from Σ with some arity n, followed by n ▷_β-normal sub-trees; i.e. it represents a tree (with certain branches possibly leading to —). The multiplicative vs additive distinction matters in the definition of schemes, though: with additive typing, resources (variables) may be shared when calculating two sub-branches of an infinite tree, which is disallowed with multiplicative typing.

Linear recursion schemes consist of a system of recursive equations, where each clause is
given by a λ-term with a restricted shape. A term Γ | — ⊢ t : ϕ is called **applicative** if it is
▷_β-normal, and has the form λx_1^{φ_1} ... λx_n^{φ_n} . t' where t' has no abstraction.

**► Definition 1.** *A Multiplicative Additive Recursion Scheme (MAHORS) is a 4-tuple* $\mathcal{G} = (\Sigma, \mathcal{N}, \mathcal{R}, S)$ *where:*
(1) $\Sigma$ *is a ranked alphabet*; (2) $\mathcal{N}$ *is a finite set of typed non-terminals; we use upper-case letters F, G, H, ... to range over them. We denote the type of F by $\mathcal{N}(F)$ and write $F : \mathcal{N}(F)$; (3) $S \in \mathcal{N}$ is a distinguished start symbol of type o; and*
(4) $\mathcal{R}$ *is a function associating to each F in *$\mathcal{N}$* an applicative term $\Sigma, \mathcal{N} | \vdash \Gamma(F) : \mathcal{N}(F)$, with $\Sigma$ represented additively. *A MHORS is defined as a MAHORS where $\Sigma$ is represented multiplicatively and the typing of *$\mathcal{N}$* does not involve products.*

If $\mathcal{G} = (\Sigma, \mathcal{N}, \mathcal{R}, S)$ is a MAHORS, then for each $F \in \mathcal{N}$ and $n \in \mathbb{N}$ there is $\Sigma | \vdash_0$ unf$_n(F) : \mathcal{N}(F)$ defined by unf$_0(F) = \perp$ and unf$_{n+1}(F) = \mathcal{R}(F)[\text{unf}_n(G)/G \mid G \in \mathcal{N}]$. The family $(\text{unf}_i(F))_{i \in \mathbb{N}}$ forms a chain for $\le$ defined as usual by $\perp \le t$, closed by congruence. As evaluation is monotone, $(\text{BT}(\text{unf}_i(F))_{i \in \mathbb{N}}$ also forms a chain, hence it has a lub which may be defined as the ideal completion of finite normal terms $\Sigma | \vdash_0 t : o$ ordered by $\le$. We may then define $\text{BT}(\mathcal{G}) = \bigsqcup_{i \in \mathbb{N}} \text{BT}(\text{unf}_i(S))$, the **infinite tree generated by** $\mathcal{G}$.

Our schemes comprise an explicit divergence symbol $\perp$. This is unusual, but does not affect expressivity as it could always be defined with a new non-terminal with rule $\mathcal{R}(\Omega) = \Omega$. Finally, we identify silently trees and terms $\Sigma | \vdash t : o$.

**3 Finite Memory Game Semantics and Geometry of Interaction**

Game semantics is a semantic technique to give a compositional interpretation of higher-order
programs [14]. By presenting higher-order computation as a *game* between two players
embodying the program and its execution environment (Player for the program, Opponent
for the environment), it effectively reduces higher-order computation to an exchange of
tokens between terms. At first forgetting recursion, we briefly review the interpretation of
the linear λ-calculus with products in *simple games*, then introduce its refined interpretation
as finite-memory strategies, which will inform the translation of M(A)HORS to TSA.

**3.1 Games and strategies**

A **game** is a tuple $A = (M_A, \lambda_A, P_A)$ where $M_A$ is a set of **moves**, $\lambda_A : M_A \to \{O, P\}$ is a **polarity function** (we write $M_A^O = \lambda_A^{-1}(\{O\})$ and $M_A^P = \lambda_A^{-1}(\{P\})$), and $P_A \subseteq M_A^*$ is a non-empty prefix-closed set of **valid plays**, whose elements are O-starting and alternating: if $s = s_1 \dots s_n \in P_A$, then $\lambda_A(s_1) = O$ and $\lambda_A(s_i) \neq \lambda_A(s_{i+1})$. We write $\epsilon \in P_A$ for the empty play and $s \subseteq s'$ for the prefix ordering.

<footnote n="2">² [5] considers also intermediate typings, but this does not contribute extra expressivity.</footnote>
43:4 On the expressivity of linear recursion schemes

<figure><img src="image_4.png" /><figcaption>Figure 2 A play on $\llbracket (o \to o) \to o \to o \rrbracket$</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 3 Composition of history-free skeletons</figcaption></figure>

Games represent *types*. Plays in a game for a type $\varphi$ represent executions on $\varphi$ following (for this paper) a call-by-name evaluation strategy. For instance, Figure 2 shows a play in the game for $(o \to o) \to o \to o$, read from top to bottom. We use indices on atom occurrences and moves for disambiguation, but the usual convention in game semantics is to signify the identity of moves simply by their position under the corresponding type component. After Opponent ($\circ$, the environment) starts computation by the initial move on the right, Player ($\bullet$, the program) responds by interrogating its function argument. Opponent, playing for this argument, calls its argument. Player terminates by calling its second argument. This play is, in fact, the maximal play of the interpretation of $\lambda f^{o\to o} \cdot \lambda x^o \cdot f x : (o \to o) \to o \to o$.

Each type $\varphi$ may be interpreted as a game $\llbracket \varphi \rrbracket$. The game $\llbracket o \rrbracket$ has $M_{\llbracket o \rrbracket} = \{\circ\}$ with $\lambda(o) = O$, and $P_{\llbracket o \rrbracket} = \{\epsilon, \circ\}$. To match the type constructor $\to$, the **linear arrow game** $A \to B$ has as moves the tagged disjoint union $M_{A \to B} = M_A + M_B = \{1\} \times M_A \cup \{2\} \times M_B$ with polarity $\lambda_{A \to B}(1, a) = \lambda_A(a)$ and $\lambda_{A \to B}(2, b) = \lambda_B(b)$, where $\overline{O} = P$ and $\overline{P} = O$. The plays $P_{A \to B}$ include all O-starting, alternating sequences $s \in M_{A \to B}^*$ such that the *restrictions* $s \upharpoonright A \in M_A^*$ and $s \upharpoonright B \in M_B^*$, defined in the obvious way, are in $P_A$ and $P_B$ respectively. Hence, $A \to B$ can be viewed as playing the two games $A$ and $B$ in parallel, with the polarity reversed in $A$, in such a way that any play must start in $B$ and Player is able to switch between the components. With these definitions the reader can check that $\llbracket (o \to o) \to o \to o \rrbracket = (\llbracket o \rrbracket \to \llbracket o \rrbracket) \to (\llbracket o \rrbracket \to \llbracket o \rrbracket)$ includes four moves corresponding to the four atom occurrences, and has only two maximal plays: the one in Figure 2, and $\circ_4 \bullet_3$.

The **tensor game** $A \otimes B$ has moves $M_{A \otimes B} = M_A + M_B$, polarity $\lambda_{A \otimes B}(1, a) = \lambda_A(a)$ and $\lambda_{A \otimes B}(2, b) = \lambda_B(b)$, and plays are those $s \in M_{A \otimes B}^*$ that are alternating, O-starting and such that $s \upharpoonright A \in P_A$ and $s \upharpoonright B \in P_B$. Dually to $\to$, it follows from the definition that here only $O$ can change between components. The **product game** $A \& B$ has the same moves and polarity as $A \otimes B$, but only the plays where either $s \upharpoonright A$ or $s \upharpoonright B$ is empty. Hence, with their first move, Opponent fixes the component in which the rest of the game will be played.

A **strategy** $\sigma$ on $A$, written $\sigma : A$, is $\sigma \subseteq P_A^{ev}$ (writing $P_A^{ev}$ for the set of even-length plays) which is non-empty, closed under even-length prefix, and *deterministic*, in the sense that if $sab, sab' \in \sigma$, then $b = b'$. The interpretation of terms yields strategies; for instance

$$ \llbracket \lambda f^{o\to o} \cdot \lambda x^o \cdot f x : (o \to o) \to o \to o \rrbracket = \{\epsilon, \circ_4 \bullet_2, \circ_4 \bullet_2 \circ_1 \bullet_3\} $$

is a strategy on $\llbracket (o \to o) \to o \to o \rrbracket$ with moves following the naming convention of Figure 2.

The interpretation of terms exploits a number of constructions on strategies. In particular, to compute the **composition** of $\sigma : A \to B$ and $\tau : B \to C$ we first let $\sigma, \tau$ interact by considering all sequences in $(M_A + M_B + M_C)^*$ whose restrictions to $A, B$ and $B, C$ are respectively in $\sigma$ and $\tau$; and then project those to $P_{A \to C}$ to obtain $\tau \circ \sigma : A \to C$. We omit the details [14]. Overall, the structure needed to interpret the linear $\lambda$-calculus with products is succinctly summarized by stating that games and strategies form a *symmetric monoidal closed category with products* [14] – to any $\_\cdot\_$ $|x_1 : \varphi_1, \dots, x_n : \varphi_n \vdash t : \varphi$ this lets us associate $\llbracket t \rrbracket : \otimes_{1 \le i \le n} \llbracket \varphi_i \rrbracket \to \llbracket \varphi \rrbracket$ in such a way that this is invariant under reduction – note however
<figure><img src="image_6.png" /><figcaption>Figure 4 The two maximal plays of contraction on $[[o \to o]]$.</figcaption></figure>

that in this paper, we avoid the categorical language as much as possible.

## 3.2 History-free and finite memory strategies

A strategy $\sigma: A$ is **history-free** if its behaviour only depends on the last move, i.e. there is a partial function $f: M_A^O \to M_A^P$ such that for all $s \in \sigma$, for all $sa \in P_A$, we have $sab \in \sigma$ iff $f(a)$ is defined and $b = f(a)$. It is key in *AJM games* [1] that, without products, terms yield history-free strategies. If $\sigma: A$ is history-free, it is characterized by the corresponding partial function $f: M_A^O \to M_A^P$, known as its *history-free skeleton*. For instance, the strategy $[[\lambda f^{o \to o} . \lambda x^o . f x]]$ with a unique maximal play in Figure 2, has history-free skeleton $\{o_4 \mapsto \bullet_2, o_1 \mapsto \bullet_3\}$.

One can also directly interpret terms as history-free skeletons: this is usually referred to as *Geometry of Interaction* [11], which has close ties with game semantics [3]. In particular, composition of history-free strategies can be performed directly on skeletons. If $\sigma: A \to B$ and $\tau: B \to C$ are history-free, their history-free skeletons, which have the types

$$f_{\sigma}: M_A^P + M_B^O \to M_A^O + M_B^P \qquad f_{\tau}: M_B^P + M_C^O \to M_B^O + M_B^P,$$

may be composed via *feedback* on $B$, pictured in Figure 3. For any Opponent move in $A \to C$, we apply the corresponding function $f_{\sigma}$ or $f_{\tau}$. As long as the response is in $B$, we keep applying $f_{\sigma}$ and $f_{\tau}$ alternately. This process may stay in $B$ forever (a *livelock*, in which case the composition $f_{\tau \circ \sigma}$ is undefined), but otherwise we eventually get a Player move in $A \to C$ as required; defining a partial function $f_{\tau \circ \sigma}: M_{A \to C}^O \to M_{A \to C}^P$. One may visualize a token entering on the left carrying an Opponent move, then bouncing in $B$ until it eventually exits on the right. Other constructions used in the interpretation may be presented similarly, altogether giving (for the linear $\lambda$-calculus) a presentation of evaluation through a finite automaton called a *token machine*, where a token enters through an Opponent move, and bounces through the term until it eventually exits, giving the result of computation [18].

This is our starting point to represent evaluation of M(A)HORS via an automaton. However, there is an issue: strategies for linear $\lambda$-terms with products are not in general history-free. For instance, Figure 4 displays the two maximal plays of a *contraction/duplication* strategy $[[\lambda f^{o \to o} . f, f] : (o \to o) \to ((o \to o) \& (o \to o))]$. It reacts to $o_1$ differently depending on the history. To account for this, one may replace partial functions $f: M_A^O \to M_A^P$ with $f: M_A^O \times M_A \to M_A^P \times M_A$, i.e. *transducers*, where $M_A$ is the *memory*, is a finite set (see the *memoryful geometry of interaction* of [13] – however, we are not aware of this being used to define finite memory strategies). We give below a definition in this spirit, adapted to ease the translation to TSA and to deal with the branching in M(A)HORS due to *terminal symbols*.

We fix a ranked alphabet $\Sigma$ (the multiplicative/additive distinction plays no role here).

**Definition 2.** A transducer $T$ on a game $A$, written $T: A$, is $T = (M_- \uplus M_+, m_0, \delta_-, \delta_+)$ where $M_-$ is a finite set of passive memory states with a distinguished initial memory state $m_0 \in M_-$, $M_+$ is a finite set of active memory states, and transition functions:

$$\delta_- : M_- \times M_A^O \to M_+$$

$$\delta_+ : M_+ \to M_+ + M_- \times M_A^P + \{\mathfrak{b}(m_1, \dots, m_{|b|}) \mid m_i \in M_+, \mathfrak{b} \in \Sigma\}.$$
43:6 On the expressivity of linear recursion schemes

<figure><img src="image_7.png" /><figcaption>Figure 5 Positive transitions of the composition of strategic transducers</figcaption></figure>

Any transducer $\mathcal{T}$ on $\llbracket o \rrbracket$ will be called **closed**. Apart from the forced initial $\delta_-(m_0, \circ)$, it is a finite tree-generating automaton, producing a tree $\text{Tree}(\mathcal{T})$. But in general transducers may play on arbitrary games. In passive states, a transducer is waiting for an Opponent move, while in active states, it is performing internal computation that may result in a terminal symbol or in a Player move and the transition to a passive state. If $\delta_+(m) = \mathbf{b}(m_1, \dots, m_{|b|})$, it produces the terminal symbol $\mathbf{b}$; exploring the $i$th child results in continuing with $m_i$.

Like strategies, transducers can be composed.

**Definition 3.** Let $S = (\mathcal{M}_-^S \uplus \mathcal{M}_+, m_0^S, \delta_S^S, \delta_+^S) : A \to B$ and $\mathcal{T} = (\mathcal{M}_-^\mathcal{T} \uplus \mathcal{M}_+, m_0^\mathcal{T}, \delta_-^\mathcal{T}, \delta_+^\mathcal{T}) : B \to C$ be transducers. The transducer $\mathcal{T} \circledast S$ on game $A \to C$ has $\mathcal{M}_-^\mathcal{T} \circledast S = \mathcal{M}_+^S \times \mathcal{M}_+^\mathcal{T}$ and $\mathcal{M}_+^\mathcal{T} \circledast S = \mathcal{M}_+^S \times \mathcal{M}_+^\mathcal{T} \uplus \mathcal{M}_-^S \times \mathcal{M}_+^\mathcal{T}$, with initial state $(m_0^S, m_0^\mathcal{T})$. The transition function is defined via $\delta_-^\mathcal{T} \circledast S((m_S^-, m_T^-), (2, c)) = (m_S^-, \delta_-^\mathcal{T}(m_T^-, (2, c)))$, $\delta_-^\mathcal{T} \circledast S((m_S^-, m_T^-), (1, a)) = (\delta_S^S(m_S^-, (1, a)), m_T^-)$, and positive transitions given in Figure 5.

Besides composition, all operations on strategies used in the interpretation of the linear $\lambda$-calculus with products have a counterpart on transducers. Altogether, for any $\Sigma \mid x_1 : \varphi_1, \dots, x_n : \varphi_n \vdash t : \varphi$, this yields a transducer $\langle t \rangle : \bigotimes_{1 \le i \le n} \llbracket \varphi_i \rrbracket \to \llbracket \varphi \rrbracket$. In particular, if $\Sigma \mid \vdash t : o$, this yields a closed transducer $\langle t \rangle : \llbracket o \rrbracket$. It is obtained directly by induction on syntax following denotational semantics, and in particular in polynomial time. We can prove:

**Proposition 4.** For any $\Sigma \mid \vdash t : o$, $\text{Tree}(\langle t \rangle) = \text{BT}(t)$.

The proof works by linking transducers with game semantics. The simple game semantics presented above cannot directly deal with the presence of non-terminals replicable at will and the associated branching, so we must first extend it to “tree-generating game semantics”. The details, though rather direct, are too lengthy for the paper, so we instead present the connection ignoring the terminal symbols.

Ignoring branching transitions, transducers generate strategies. Writing $m^- \xrightarrow{a} m^+$ when $\delta_-(m^-, a) = m^+, m_1^+ \to m_2^+$ when $\delta_+(m_1^+) = m_2^+$ and $m^+ \xrightarrow{b} m^-$ when $\delta_+(m^+) = (m^-, b)$; the set Traces($\mathcal{T}$) comprises all sequences $s_1 \dots s_{2n} \in \mathcal{M}_A^*$ such that (with $m_0, \dots, m_n \in \mathcal{M}_-$)

$$m_0 \xrightarrow{s_1} \dots \xrightarrow{s_2} m_1 \xrightarrow{s_3} \dots \xrightarrow{s_4} m_2 \dots m_{n-1} \xrightarrow{s_{2n-1}} \dots \xrightarrow{s_{2n}} m_n.$$

We say that $\mathcal{T}$ is a **strategic transducer** if for all $s \in \text{Traces}(\mathcal{T}) \cap P_A$, if $sa \in P_A$ and $sab \in \text{Traces}(\mathcal{T})$, then $sab \in P_A$. Then, $\text{Traces}(\mathcal{T}) \cap P_A$ is a strategy written $\text{Strat}(\mathcal{T})$. We say that $\sigma : A$ has **finite memory** if $\sigma = \text{Strat}(\mathcal{T})$ for a strategic transducer $\mathcal{T}$. We also recover history-free strategies as those for which $\mathcal{M}_-$ is a singleton. For instance, the strategy in Figure 4 is generated using $\mathcal{M}_- = \{m_0, m_1\}$ and $\mathcal{M}_+ = \mathcal{M}_- \times \mathcal{M}_{\llbracket o \to o \rrbracket}^O$, $\delta_-(m, a) = (m, a)$, $\delta_+(\_, \circ_4) = (m_0, \bullet_2)$, $\delta_+(\_, \circ_6) = (m_1, \bullet_2)$, $\delta_+(m_0, \circ_1) = (m_0, \bullet_3)$ and $\delta_+(m_1, \circ_1) = (m_1, \bullet_5)$.

Proposition 4 boils down to the fact that all constructions on transducers in the interpretation preserve strategic transducers, and match operations on strategies – for instance, $\text{Strat}(\mathcal{T} \circledast S) = \text{Strat}(\mathcal{T}) \circ \text{Strat}(S)$. This entails that for all $t$, $\text{Strat}(\langle t \rangle) = \llbracket t \rrbracket$. But for closed transducers $\langle t \rangle$ and tree-generating game semantics, $\text{Tree}(\langle t \rangle) = \text{Strat}(\langle t \rangle)$. Since game semantics is invariant under reduction, $\llbracket t \rrbracket = \llbracket \text{BT}(t) \rrbracket = \text{BT}(t)$, and Proposition 4 follows.
<figure><img src="image_8.png" /><figcaption>Figure 6 Illustration of a state of the n-th unfolding</figcaption></figure>

# 4 Game Semantics to TSA

The previous section lets us associate, to any $Σ | \_ ⊢ t : o$, a finite tree-generating automaton. We extend this with recursion in two steps: first we evaluate finite unfoldings using finite automata, and then we build a single automaton with additional memory (a *Tree Stack Automaton*) whose runs amount to dynamically exploring these finite unfoldings.

## 4.1 Unfolding recursive calls

Let us fix a M(A)HORS $G = ⟨Σ, N, R, S⟩$. By definition, for each $F ∈ N$ we have $Σ, N | \_ ⊢ R(F) : N(F)$. Let $N ∈ N$ be such that for all $F, G ∈ N$, $G$ appears at most $N$ times in $R(F)$. For all $F ∈ N$, we choose a term $Σ | N_1, ..., N_N ⊢ R'(F) : N(F)$ obtained by giving different names $G_1, ..., G_p (p ≤ N)$ to all occurrences of $G ∈ N$ in $R(F)$. How these names are assigned does not matter. Although $R'$ differs from $R$, it can be equivalently used to define the finite approximations of BT($G$). For each $F ∈ N$ and $n ∈ N$, we redefine $Σ | \_ ⊢ \text{unf}_n(F) : N(F)$ by setting $\text{unf}_0(F) = \perp$, and $\text{unf}_{n+1}(F) = R'(F)[\text{unf}_n(G)/G_i | G ∈ N_i, 1 ≤ i ≤ N]$. Although defined differently, this gives the same result as in Section 2.

But, unlike the original unfolding, this one can be replicated with strategic transducers. For each $F ∈ N$, the interpretation of the previous section yields a strategic transducer:

$$⟨R'(F)⟩ : \bigotimes_{1≤i≤N} \bigotimes_{G∈N} [[N(G)]] \to [[N(F)]]$$

The unfolding above can then be replicated as follows.

**Proposition 5.** *Setting $T_F^0 = \perp$ with all positive transitions undefined, and $T_F^{n+1} = ⟨R'(F)⟩ \odot (\otimes_{1≤i≤N} \otimes_{G∈N} T_G^n) : [[N(F)]]$, for all $n ∈ N$, we have $\text{Tree}(T_S^n) = \text{BT}(\text{unf}_n(S))$.*

**Proof.** By the substitution lemma for symmetric monoidal closed categories with products, syntactic substitution matches composition in the denotational model. It follows by induction that for all $F ∈ N$, for all $n ∈ N$, $⟨\text{unf}_n(F)⟩$ and $T_F^n$ are transducers generating the same finite memory strategy. By Proposition 4, $\text{Tree}(T_S^n) = \text{Tree}(⟨\text{unf}_n(S)⟩) = \text{BT}(\text{unf}_n(S))$. ◀

Figure 6 displays the structure of transducer compositions arriving at the finite tree automaton $T_S^n$, for a M(A)HORS $G$ where $R(S)$ has two occurrences of $F$ and two occurrences
43:8 On the expressivity of linear recursion schemes

of G, R(F) has two occurrences of G, and R(G) has two occurrences of F. Each node stands for the matching strategic transducer (corresponding to a non-terminal), edges represent compositions. Running T_S^n passes control between the composed transducers, with always exactly one active after the initial transition. Figure 6 shows a possible state during a run: the grey area marks nodes that have already been explored. Outside of the grey area, the (local) transducer memory must be m_0. The green node is active, and all others passive. Following the transition function of (R(G)), we may next update the local memory m_4, produce a terminal and branch, or update to a passive state and send control up or down.

4.2 Tree Stack Automata

Now we give a single automaton with infinite memory whose bounded restrictions match the approximations above. It has a stack to deal with recursion, such that each state of the stack corresponds to a node in Figure 6. As these nodes stand for strategic transducers, they all have a finite memory. Accordingly, the automaton maintains a store associating, to each previously visited stack state/node, its local memory, accessed or updated only when visiting that node. We think of the store as a tree: the stack alphabet denotes directions, and stack values denote positions in the tree, i.e. nodes in (the infinite version of) Figure 6. Pushes and pops correspond to moving up and down the tree. Such an automata model is known as a Tree Stack Automaton (TSA) [7] – here, we introduce tree-generating TSA.

► **Definition 6.** A tree-generating TSA A is a tuple $\langle \Sigma, Q, \Gamma, \mathcal{M}, \delta, q_0, \gamma_0, m_0 \rangle$ where $\Sigma$ is a ranked alphabet of terminals, $Q$ is a set of states, $\Gamma$ is a finite stack alphabet, $\mathcal{M}$ is a finite memory alphabet, $q_0 \in Q$ is the starting state, $\gamma_0 \notin \Gamma$ is the bottom-of-stack marker and $m_0 \in \mathcal{M}$ is the initial local memory. Letting $\Gamma^\bullet = \Gamma \uplus \{\gamma_0\}$, the transition function $\delta$ has type:

$$ \delta: Q \times \mathcal{M} \times \Gamma^\bullet \rightarrow Q + \{b(q_1, \dots, q_{|b|}) \mid q_i \in Q, b \in \Sigma\} + Q \times \mathcal{M} \times (\{up_\gamma \mid \gamma \in \Gamma\} + \{down\}). $$

Informally, the transitions operate as follows. Initially, only $\gamma_0$ is on the stack. Subsequently, given state $q$, local memory $m$, and top of the stack $\gamma \in \Gamma^\bullet$:

1. if $\delta(q, m, \gamma) = q'$, the automaton changes state to $q'$, leaving the stack and local memory unchanged;

2. if $\delta(q, m, \gamma) = b(q_1, \dots, q_{|b|})$, it outputs $b \in \Sigma$ and branches – to explore the ith child ($1 \le i \le |b|$) it proceeds to state $q_i$ leaving other components unchanged;

3. if $\delta(q, m, \gamma) = (q', m', up_{\gamma'})$, it updates the local memory to $m'$, changes state to $q'$ and pushes $\gamma'$ onto the stack / moves up in direction $\gamma'$ (if this is the first visit to that node, its local memory is set to $m_0$);

4. if $\delta(q, m, \gamma) = (q', m', down)$, it updates the local memory to $m'$ and the state to $q'$, and then pops / moves down (we adopt the convention that $\gamma_0$ cannot be popped so, if $\gamma = \gamma_0$ in this case, the automaton blocks).

Running a TSA A produces a possibly infinite tree $\text{Tree}(A)$.

In the degenerate case where $\mathcal{M} = \{m_0\}$, tree-generating TSAs turn out to be precisely tree-generating deterministic pushdown automata (PDA): the local memory cannot store information, so only the stack remains. In general, however, it is not hard to see that TSAs are Turing-complete; fortunately we will only need TSAs satisfying a further condition called restriction [7]. A tree-generating TSA is k-restricted if every node can be accessed from below at most k times. It is restricted if it is k-restricted for some $k \in \mathbb{N}$.

We implement the evaluation of a MAHORS G with a restricted TSA A(G) with states

$$ Q = \left( \sum_{F \in \mathcal{N}} M_{\otimes_{1 \le i \le N} \otimes_{G \in \mathcal{N}}} [\mathcal{N}(G)] \to [\mathcal{N}(F)] \right) + \left( \sum_{F \in \mathcal{N}} M_{+}^{(\mathcal{R}'(F))} \right). $$
<figure><img src="image_9.png" /><figcaption>Figure 7 Transition function for the GoI TSA.</figcaption></figure>

We use constructors Move and State to refer to elements from the left and right components of $\mathcal{Q}$ respectively. The memory alphabet is $\mathcal{M} = \sum_{F \in \mathcal{N}} \mathcal{M}_{-}^{(\mathcal{R}'(F))} / \equiv$, where $\equiv$ is the smallest equivalence relation with $(F, m_0) \equiv (G, m_0)$ for all $F, G \in \mathcal{N}$. We write $m_0$ for this equivalence class, providing the initial memory state. The stack alphabet is $\Gamma = N \times \mathcal{N}$ where $N$ is the smallest integer such that all non-terminals have fewer than $N$ occurrences in $\mathcal{R}(F)$, for all $F \in \mathcal{N}$. The start state is $q_0 = \text{Move}(S, \circ)$ and the transition function is given in Figure 7.

The TSA $\mathcal{A}(\mathcal{G})$ is designed so that a run of stack size bounded by $n$ simulates a run of $\mathcal{T}_S^n$. When in state $\text{State}(F, m)$, the automaton is currently operating in a $F$ node of $\mathcal{T}_S^n$ (as in Figure 6), performing internal computation following $\delta_+^F$. If this internal computation produces a move, this move will be addressed either up or down the stack, depending of whether it is a Player move in $\mathcal{N}(F)$ (in which case we must move down), or an Opponent move in $\otimes_{1 \le i \le N} \otimes_{G \in \mathcal{N}} [\mathcal{N}(G)]$ (in which case we must move up, passing the control to a recursive call). If the state is $\text{State}(G, m)$ and the top of the stack is $(F, i)$, that means that we are currently running non-terminal $G$, which was called as the $i$-th occurrence of $G$ in $F$. So the stack, together with the non-terminal symbol in the state, indicate the address of a node in Figure 6. When moving up or down the stack, we first change to a transient state $\text{Move}(F, a)$ in which the automaton reads the input move using $\delta_-^F$ and resumes as above.

**Theorem 7.** For any MAHORS $\mathcal{G}$, there exists a restricted TSA $\mathcal{A}(\mathcal{G})$ (constructed in polynomial time) such that $\text{Tree}(\mathcal{A}(\mathcal{G})) = \text{BT}(\mathcal{G})$.

**Proof.** For $n \ge 1$, write $\text{Tree}_n(\mathcal{A}(\mathcal{G}))$ for the tree obtained from the truncated run-tree where the stack size is bounded by $n-1$ (where $\gamma_0$ has size 0). By construction, this truncated run-tree is weakly bisimilar to that of $\mathcal{T}_S^n$. In particular, $\text{Tree}_n(\mathcal{A}(\mathcal{G})) = \text{Tree}(\mathcal{T}_S^n) = \text{BT}(\text{unf}_n(S))$ by Proposition 5, so $\text{Tree}(\mathcal{A}(\mathcal{G})) = \text{BT}(\mathcal{G})$ by continuity.

This TSA is restricted: for any type $\varphi$, there is a bound on the length of plays in $P_{\llbracket \varphi \rrbracket}^-$ in fact $M_{\llbracket \varphi \rrbracket}$ is finite, and plays in $P_{\llbracket \varphi \rrbracket}$ cannot use the same move twice. Let $k$ be an upper bound to the maximal length of a play in $P_{\otimes_{G \in \mathcal{N}} [\mathcal{N}(G)]}$. Then, $\mathcal{A}(\mathcal{G})$ is $k$-restricted. Indeed, fix a stack value $\gamma_{n+1}\gamma_n\dots\gamma_0$ with $\gamma_{n+1} = (F, i)$. Then, all transitions moving between $\gamma_{n+1}\dots\gamma_0$ and $\gamma_n\dots\gamma_0$ carry a move from $M_{\otimes_{G \in \mathcal{N}} [\mathcal{N}(G)]}$. By construction, the sequence of such moves forms a play in $P_{\otimes_{G \in \mathcal{N}} [\mathcal{N}(G)]}$. Hence, it is bounded by $k$. ◀

If the input scheme is an MHORS then each $\mathcal{R}'(F)$ is interpreted by a history-free strategy: $\mathcal{M}_{-}^{(\mathcal{R}'(F))}$ is a singleton. Consequently, $\mathcal{A}(\mathcal{G})$ has trivial memory and is in fact simply a PDA. This PDA is still $k$-restricted but also satisfies a stronger linearity property:

**Lemma 8.** Let $\mathcal{G}$ be an MHORS. Then the tree-generating PDA $\mathcal{A}(\mathcal{G})$ is *linear*, in the sense that the associated graph of reachable configurations is a tree.

**Proof.** A strategic transducer on $\mathcal{A}$ is **reversible** if for each $a \in M_A^P$ there is at most one $m \in M_+$ such that $\delta_+(m) = (\_, a)$ and for each $m \in M_+$ there is at most one $(m', a) \in M_- \times M_A^O$ such that $\delta_-(m', a) = m$ or at most one $m' \in M_+$ such that $\delta(m') = m$, and the two possibilities are mutually exclusive. Reversible strategic transducers are closed under
all operations used in the interpretation, hence if $\Sigma | \Delta \vdash t : A$ involves no product, $\langle t \rangle$ is *reversible* (this phenomenon is well-known in GoI [6]). This entails that $\mathcal{A}(\mathcal{G})$ is linear. ◀

## 5 TSA to MAHORS

In this section we show how to simulate a $k$-restricted TSA $\mathcal{A} = \langle \Sigma, Q, \Gamma, \mathcal{M}, \delta, q_0, \gamma_0, m_0 \rangle$ in MAHORS, i.e. we establish the converse of Theorem 7.

Let $B = |\Gamma|$ and $\Gamma = \{\gamma_1, \dots, \gamma_B\}$. Nodes of the tree store will be represented using non- terminals $F_{q,m,\gamma}^{u_1, \dots, u_B;d}$, where $(q, m, \gamma) \in Q \times \mathcal{M} \times \Gamma^\bullet$ represent the current state, node label and top of the stack respectively, $d$ ($1 \le d \le k+1$) is the number of times the node has already been visited from below and each $u_j$ ($0 \le u_j \le k$, $1 \le j \le B$) is the number of times that the $j$th child has been visited from below. For brevity, we will write $\bar{u}$ instead of $u_1, \dots, u_B$.

For $1 \le d \le k$, $F_{q,m,\gamma}^{\bar{u};d}$ has $B+1$ arguments: the first $B$ arguments are used to simulate $up_{\gamma_j}$ ($1 \le j \le B$) and the last one corresponds to *down*. Each of the arguments is a $Q$-indexed tuple of continuations, so that projection can be used to select the right component to model the associated state change. When moving up the tree ($up_{\gamma_j}$), we call the $j$th argument passing as an argument another continuation that makes it possible to return (move down) later. Dually, when moving down the tree, we call the last argument passing as an argument a continuation that represents a further visit up. Using these ideas, one could code unrestricted TSA in an untyped setting, but we shall rely on carefully crafted types that allow, for each node, for up to $k$ visits from below. In particular, if the automaton is moving down having visited a node $k$ times from below, the corresponding upwards continuation for the $k+1$ visit is of type $o$, i.e. it is not usable for any future calls. The rules for $1 \le d \le k$ are summarised in the table below, using $\lambda$ notation for brevity (for $F_{q,m,\gamma}^{\bar{u};k+1}$ we set $F_{q,m,\gamma}^{\bar{u};k+1} x_1 \cdots x_B = \perp$).

<table><thead><tr><th>δ(q, m, γ)</th><th>rule</th></tr></thead><tbody><tr><td>q'</td><td>F<sub>q,m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub> = F<sub>q',m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub></td></tr><tr><td>b(q<sub>1</sub>, ..., q<sub>b|l</sub>)</td><td>F<sub>q,m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub> = b{F<sub>q<sub>1</sub>,m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub>, ..., F<sub>q<sub>b|l</sub>,m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub>}</td></tr><tr><td>(q', m', down)</td><td>F<sub>q,m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub> = (π<sub>q'</sub>y) {F<sub>q'',m',γ</sub><sup>ū;d+1</sup> x<sub>1</sub>...x<sub>B</sub> | q'' ∈ Q}</td></tr><tr><td>(q', m', up<sub>γ<sub>j</sub></sub>)</td><td>F<sub>q,m,γ</sub><sup>ū;d</sup> x<sub>1</sub>...x<sub>By</sub> = (π<sub>q'</sub>x<sub>j</sub>) {λz<sup>T<sub>j</sub></sup>.F<sub>q'',m',γ</sub><sup>ū+e<sub>j</sub>;d</sup> x<sub>1</sub>...x<sub>j-1</sub>zx<sub>j+1</sub>...x<sub>By</sub> | q'' ∈ Q}</td></tr></tbody></table>

In the *down* case, note that the $q'$th component of $y$ is used to model state change and that the continuation features $m'$ instead of $m$ to reflect the local memory update. Note also the change from $d$ to $d+1$, which updates the count of visits from below.

In the *up* case, the $q'$th component of $x_j$ is used to model state change and the direction of the upward move $(\gamma_j)$. The use of the same $\gamma$ on both sides captures the same position on the stack and $m'$ is used on the rhs to simulate the local memory update. $d$ does not change, because the continuation represents revisiting the node from above (rather than from below). However, once the node is revisited from above in the future, its $j$th child will have been visited $u_j + 1$ times from below: hence the change to $u_j$ (we write $\bar{u} + e_j$ for $\bar{u}$ with the $j$th component incremented by 1). In the *up* case, we use a $\lambda$-term inside a rule to highlight the intention more clearly, this can be avoided by using an auxiliary non-terminal.

The start symbol $S: o$ has rule $S = (F_{q_0,m_0,\gamma_0}^{0,\dots,0;1}) N_1 \cdots N_B \langle \perp | q \in Q \rangle$. The divergent terms correspond to our convention that the automaton blocks when *down* is called at the root node. $N_j$ ($1 \le j \le B$) stands for $\langle N_{q,j} | q \in Q \rangle$, where $N_{q,j}$ are auxiliary non- terminals that represent nodes visited for the first time. They are subject to the rule $N_{q,j}y = F_{q,m_0,\gamma_j}^{0,\dots,0;1} N_1 \cdots N_B y$.

The scheme depends on types of the form $T_i$ ($0 \le i \le k$) defined by $T_k = o$ and $T_i = (\overline{T_{i+1}} \to o) \to o$, where $\overline{T}$ stands for $\&_{q \in Q} T$, i.e. $|Q|$ copies of $T$. In particular, we have $F_{q,m,\gamma}^{\bar{u};d} : \overline{T_{u_1}} \to \dots \to \overline{T_{u_B}} \to T_{d-1}$ and $N_{q,j} : T_0$.
**► Theorem 9.** For any restricted TSA, there exists an equivalent MAHORS (constructible in exponential time).

In conjunction with Theorem 7, this shows that MAHORS and restricted TSA are equivalent.

# 6 Expressivity of MAHORS

It is easy to see that any (classic) first-order recursion scheme (1-HORS) can be viewed as a MAHORS, simply by giving the terminals types of the form $o \& \dots \& o \to o$. Hence, MAHORS are at least as expressive as first-order HORS. Next, informed by results from the preceding sections, we can discuss their relationship with schemes of higher orders. Because our TSA model is a tree-generating variant of the automata from [7], which capture multiple context-free languages [21], we can immediately conclude the following.

**► Lemma 10.** The branch language of a tree generated by a MAHORS is multiple context-free.

Thanks to the Lemma, we can show that MAHORS and second-order HORS are incomparable.

**► Example 11.** There exists a second-order HORS, which is not equivalent to any MAHORS. For example, consider the 2-HORS given by: $S = Fb, Ff = a(f\$)(F(Gf)), Gfx = f(fx)$, where $a: o \to o \to o, b: o \to o$ and $\$ : o$ are terminals and $F: (o \to o) \to o$ and $G: (o \to o) \to o \to o$ are non-terminals. The scheme generates an infinite tree whose finite branches correspond to the language $L = \{a^n b^{2^{n-1}} \$$ | $n \ge 1$\}$. Because it is known that $L$ is not multiple context-free [21, Lemma 3.5], it cannot be the branch language of a MAHORS by Lemma 10.

**► Example 12.** We give a MAHORS that is not equivalent to any second-order HORS, exploiting the fact that the language $L = \{w\#w\#w | w \in D\}$, where $D$ is the Dyck language ($D = \epsilon | [D]D$), is not indexed [8] (see also page 2 of [16]). The MAHORS given below (using $\lambda$-syntax for brevity) has been obtained by lifting the grammar rules for $D$ to triples of words, encoded with the type $T_3 = ((o \to o) \to (o \to o) \to (o \to o) \to o) \to o$. Consequently, it generates a tree whose finite branches are the words of $L$ prefixed by a segment of b's and followed by $\$$. The terminal $b: (o \& o) \to o$ represents rule choice and the other terminals $([], \# : o \to o, \$ : o)$ are used to build the word. The scheme relies on the following non-terminals: $S: o, D: T_3, K: (o \to o) \to (o \to o) \to (o \to o)$ and $I: o \to o$, which are subject to the following rules:

$$ \begin{array}{l} S = D(\lambda xyz.x(\#(y(\#(z\$))))), \quad Kxyv = [(x())(yv))), \quad Iv = v, \\ Df = b(fIII, D(\lambda x_1 y_1 z_1.D(\lambda x_2 y_2 z_2.f(Kx_1x_2)(Ky_1y_2)(Kz_1z_2)))) \end{array} $$

If the scheme were equivalent to a 2-HORS, the language of its branches would be accepted by a 2-CPDA [12], i.e. it would be indexed [2]. However, indexed languages are closed under homomorphism, so $L$ would be indexed too, because erasing b's and $\$$ is a homomorphism.

Lemma 10 identifies a strong restriction on branch languages of trees generated by MAHORS. Since multiple context-free languages form a subset of third-order collapsible pushdown languages [20], it is natural to ask whether every MAHORS might be equivalent to a third-order HORS. One could try to establish this, for example, by showing that, for every restricted TSA, there is an equivalent MAHORS that uses third-order types. Unfortunately, our proof of Theorem 7 uses types whose order grows linearly in the restriction parameter $k$. At the time of writing, we believe this necessary to capture the complexity of run-trees generated by our (infinite-)tree-generating TSA, though we are aware that similar hierarchies for (finite-)word languages and (finite-)tree languages do collapse, e.g. second-order abstract
categorial grammars [19, 15]. The main difficulty that prevents us from translating TSA
into MAHORS of order 3 is that there may be infinitely many (sub)runs that start from a
given node, visit only nodes above it and return to the same node, and all such runs have to
be captured in a single MAHORS. In contrast, for word languages, when TSA are seen as
acceptors of finite words, it suffices to focus on the representation of a single run [7].

7 Multiplicative HORS (MHORS)

In this section we consider MHORS, i.e. &-free MAHORS. Recall from Lemma 8 that, for any MHORS, there exists an equivalent linear PDA (LPDA) $\langle \Sigma, Q, \Gamma, \delta, q_0, \gamma_0 \rangle$ with transition function $\delta : Q \times \Gamma^* \to Q + \{b(q_1, \dots, q_{|Q|}) \mid q_i \in Q, b \in \Sigma\} + Q \times (\{up_\gamma \mid \gamma \in \Gamma\} + \{down\})$ such that any reachable configuration must be reachable through a unique path. Next we prove the converse using first-order MHORS only. In combination with Lemma 8, this amounts to a polynomial-time translation from arbitrary MHORS to first-order MHORS.

In what follows, we view an LPDA as a pushdown system with a successor relation $\Rightarrow$, in order to exploit standard reachability techniques [4, 9]. We work with configurations of the form $(q, t) \in Q \times (\Gamma^*)^*$. As we do not have the space to review all the necessary definitions, let us just recall that the techniques employ *multi-automata* over $\Gamma^*$ to recognise sets of configurations. Multi-automata are finite-state machines with multiple initial states, one for each state of the analysed pushdown system. Let $i_q$ be the initial state of a multi-automaton corresponding to $q \in Q$. Then a multi-automaton is said to recognise $(q, t)$ if it accepts $t$ once started from $i_q$ (this corresponds to processing stack content top-down). In particular, we take advantage of the following facts.

- For any LPDA $\mathcal{A}$, there exists a multi-automaton $\mathcal{A}_{era}$, constructible in polynomial time, which captures erasable stack content, i.e. $\{(q,t) \in Q \times \Gamma^* \mid \exists q' \in Q. (q,t) \Rightarrow^* (q', \epsilon)\}$. Using terminology from [4], this corresponds to $\text{pre}^*(Q \times \{\epsilon\})$. Hence, given $\mathcal{A}$, one can calculate the relation $R_{\mathcal{A}} = \{(q, \gamma, q') \in Q \times \Gamma \times Q \mid (q, \gamma) \Rightarrow^* (q', \epsilon)\}$ in polynomial time.

- For any LPDA $\mathcal{A}$, there exists a multi-automaton $\mathcal{A}_{rea}$, constructible in polynomial time, which represents all configurations reachable from $(q_0, \gamma_0)$, i.e. all $(q, t\gamma_0)$ such that $(q_0, \gamma_0) \Rightarrow^* (q, t\gamma_0)$. This corresponds to representing $\text{post}^*((\{q_0, \gamma_0\})$ [9].

**Lemma 13.** For any LPDA $\mathcal{A}$, there exists an equivalent MHORS (of order 1) and its construction can be carried out in polynomial time.

**Proof.** The translation is similar to the PDA-to-1-HORS translation in [12] except that reachability analysis ($R_A$) is used to identify places where variables actually get used. This is needed to produce a term that is linearly typable. $\quad$

Consequently, LPDA and MHORS are equivalent. We end this section by showing they
generate regular trees. Our first lemma states that, if the stack of an LPDA grows sufficiently,
there is a point after which elements lying below a certain level will no longer be accessible.

**Lemma 14.** Let $s \in \Gamma^*$. There exists a bound $H_s \ge 0$ such that, for any $t \in \Gamma^*$, if $(q, ts\gamma_0)$ is reachable and $|t| > H_s$ then there is no $q'$ such that $(q, t) \Rightarrow^* (q', \epsilon)$.

**Proof.** Consider $X = \{(q, s\gamma_0) \mid (q_0, \gamma_0) \Rightarrow^* (q, s\gamma_0)\}$. Observe that $0 \le |X| \le |Q|$. Because we work with an LPDA, there can be at most $|Q|$ runs from $(q_0, \gamma_0)$ to $X$. Let $H_s$ be the maximum stack height occurring in these runs (take 0 if $X = \emptyset$). Suppose $(q, ts\gamma_0)$ is reachable and $|t| > H_s$. If we had $(q, t) \Rightarrow^* (q', \epsilon)$ for some $q'$ then there would be a run $(q_0, \gamma_0) \Rightarrow^* (q, ts\gamma_0) \Rightarrow^* (q', s\gamma_0)$ in which the stack height exceeds $H_s$ (because it visits $(q, ts\gamma_0)$). This contradicts the choice of $H_s$. $\quad$
The above bound depends on $s$. We show that there is a uniform bound, polynomial with respect to the size of $\mathcal{A}$. First, given $s \in \Gamma^*$, the multi-automaton $\mathcal{A}_{rea}$ discussed earlier can be modified to represent $\{(q,t) | (q_0, \gamma_0) \Rightarrow^* (q, ts\gamma_0)\}$ simply by changing the accepting states of $\mathcal{A}_{rea}$ (to those from which an original accepting state is reachable via an $s\gamma_0$-labelled path). Let $\mathcal{A}_{rea}^s$ be the resultant automaton. Note that the size of $\mathcal{A}_{rea}^s$ is bounded by a polynomial in $|\mathcal{A}|$ that is independent of $s$, because the only difference between $\mathcal{A}_{rea}^s$ and $\mathcal{A}_{rea}$ is the set of accepting states, and its size bounded by $|Q|$.

Observe that $\{(q,t) | (q_0, \gamma_0) \Rightarrow^* (q, ts\gamma_0), (q,t) \Rightarrow^* (q', \epsilon)\}$ for some $q'$ is exactly the set of configurations that are represented by both $\mathcal{A}_{rea}^s$ and $\mathcal{A}_{era}$. Consider the product $\mathcal{A}'$ of the two multi-automata. By Lemma 14, $\mathcal{A}'$ cannot have reachable loops. Consequently, the longest word that it accepts from any initial state is bounded by the number of states of the automaton, which is polynomial in $|\mathcal{A}|$. As this reasoning is independent of $s$, we obtain:

**Lemma 15.** For any LPDA $\mathcal{A}$, there exists a bound $H$, polynomial in $|\mathcal{A}|$, such that, for any $s, t \in \Gamma^*$, if $(q, ts\gamma_0)$ is reachable and $|t| > H$ then there is no $q'$ such that $(q, t) \Rightarrow^* (q', \epsilon)$.

This implies that an LPDA can only use $H$ top elements from its stack, i.e. its stack can be simulated by a finite state automaton, which is exponentially bigger. Because any 0-HORS is also an MHORS, MHORS and 0-HORS are equivalent, i.e. they generate exactly the regular trees. However, it is worth noting that MHORS may be more succinct.

**Example 16.** The MHORS built from terminals $a, b: o \to o$, non-terminals $S: o, F_i: o \to o$ ($1 \le i \le n$) with $S = F_n(bS), F_0(x) = ax$ and $F_i(x) = F_{i-1}(F_{i-1}x)$ for $1 \le i \le n$ generates an infinite branch $(a^{2^n}b)^\omega$, which could only be generated by a 0-HORS of exponential size in $n$.

References

1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. *Inf. Comput.*, 163(2):409–470, 2000. URL: https://doi.org/10.1006/inco.2000.2930, doi: 10.1006/inco.2000.2930.

2. Klaus Aehlig, Jolie G. de Miranda, and C.-H. Luke Ong. Safety is not a restriction at level 2 for string languages. In *Proceedings of FOSSACS*, volume 3441 of *Lecture Notes in Computer Science*, pages 490–504. Springer, 2005.

3. Patrick Baillot. *Approches dynamiques en sémantique de la logique linéaire: jeux et géométrie de l'interaction*. PhD thesis, Aix-Marseille 2, 1999.

4. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In *Proceedings of CONCUR*, volume 1243 of *Lecture Notes in Computer Science*, pages 135–150. Springer, 1997.

5. Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski. Linearity in higher-order recursion schemes. *PACMPL*, 2(POPL):39:1–39:29, 2018.

6. Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal lambda-machines. *Theor. Comput. Sci.*, 227(1-2):79–97, 1999.

7. Tobias Denkinger. An automata characterisation for multiple context-free languages. In *Proceedings of DLT*, volume 9840 of *Lecture Notes in Computer Science*, pages 138–150. Springer, 2016.

8. Joost Engelfriet and Sven Skyum. Copying theorems. *Inf. Process. Lett.*, 4(6):157–161, 1976.

9. Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In *Proceedings of CAV*, volume 1855 of *Lecture Notes in Computer Science*, pages 232–247. Springer, 2000.

10. Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987.

11. Jean-Yves Girard. Geometry of Interaction 1: Interpretation of System F. *Studies in Logic and the Foundations of Mathematics*, 127:221–260, 1989.
43:14 On the expressivity of linear recursion schemes

12 Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. *ACM Trans. Comput. Log.*, 18(3):25:1–25:42, 2017.

13 Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 52:1–52:10, 2014. URL: https://doi.org/10.1145/2603088.2603124, doi:10.1145/2603088.2603124.

14 Martin Hyland. Game semantics. *Semantics and logics of computation*, 14:131, 1997.

15 Makoto Kanazawa. Second-order abstract categorial grammars as hyperedge replacement grammars. *Journal of Logic, Language and Information*, 19(2):137–161, 2010.

16 Makoto Kanazawa and Sylvain Salvati. The copying power of well-nested multiple context-free grammars. In *Proceedings of LATA*, volume 6031 of *Lecture Notes in Computer Science*, pages 344–355. Springer, 2010.

17 Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In *Proceedings of POPL*, pages 416–428, 2009.

18 Olivier Laurent. A token machine for full Geometry of Interaction. In *Proceedings of TLCA*, pages 283–297, 2001. URL: https://doi.org/10.1007/3-540-45413-6_23, doi:10.1007/3-540-45413-6_23.

19 Sylvain Salvati. Encoding second order string acg with deterministic tree walking transducers. In *Proceedings of FG*, pages 143–156. CSLI Publications, 2006.

20 Sylvain Salvati. MIX is a 2-MCFL and the word problem in $Z^2$ is captured by the IO and the OI hierarchies. *J. Comput. Syst. Sci.*, 81(7):1252–1277, 2015.

21 Hiroyuki Seki, Takashi Matsumura, Mamoru Fujii, and Tadao Kasami. On multiple context-free grammars. *Theor. Comput. Sci.*, 88(2):191–229, 1991.

A Additional material (Section 2)

[5] considers intermediate (between multiplicative and additive) typings for terminals, which have the form $b: \&_{n_1} o \dots \&_{n_k} o \to o$. This does not contribute any extra expressivity with respect to the additive typing $b: \&_{\sum_{i=1}^k n_i} o \to o$.

This is because $b: \&_{n_1} o \dots \&_{n_k} o \to o$ can be replaced with a new non-terminal $N_b: \&_{n_1} o \dots \&_{n_k} o \to o$ and the rule

$$N_b x_1 \cdots x_k = b(\pi_1 x_1, \cdots, \pi_{n_1} x_1, \cdots, \pi_1 x_k, \cdots \pi_{n_k} x_k)$$

where $b: \&_{\sum_{i=1}^k n_i} o \to o$.

B Additional material (Section 3)

In this section we give the details for the TSA evaluation of MAHORS given in Section 3. In this appendix, we assume some basic familiarity with game semantics and categorical logic.

B.1 Tree-generating game semantics

We build on the well-known symmetric monoidal closed category *Gam* of *simple games*. We do not give a detailed construction for this category, but it can be found for instance in [14]. We shall first generalize it to deal with strategies that may produce, and branch, on non-terminals. Let us fix a tree signature $\Sigma$. The construction does not depend on whether terminals are typed additively or multiplicatively (but we will come back to that later).
**► Definition 17.** We define a game $(M, P, \lambda)$ with $M = \Sigma \uplus \mathbb{N}$, $\lambda(b) = -$ for $b \in \Sigma$, $\lambda(n) = +$ for $n \in \mathbb{N}$, and non-empty plays (prefixes of) those sequences

$$b_1 n_1 \dots b_p n_p$$

such that for all $1 \le i \le p$, $n_i \le |b_i|$.

Overloading notations we still write $\Sigma$ for this game – this should cause no confusion.

In games coming from the interpretation of types, no move may be played several times. In contrast in $\Sigma$, there is no limitation as to how many times a certain move may be played. Because of that we get:

**► Lemma 18.** There are strategies $e_\Sigma : \Sigma \to 1$ and $d_\Sigma : \Sigma \to \Sigma \otimes \Sigma$ making $(\Sigma, e, d)$ a comonoid in Gam.

**Proof.** First, we define $e_\Sigma$ simply as the empty strategy.

If $s_1, s_2 \in P_\Sigma$, write $s_1 \bowtie s_2$ for the set of plays resulting from interleavings of $s_1$ and $s_2$. We then define

$$d_\Sigma = \{s \in P_{\Sigma_1 \to \Sigma_2 \bowtie \Sigma_3} \mid \forall t \sqsubseteq^+ s, t \upharpoonright \Sigma_1 \in (t \upharpoonright \Sigma_2 \bowtie t \upharpoonright \Sigma_3)\}$$

where the different copies of $\Sigma$ are marked for disambiguation. It is routine to check that this is a strategy and that it satisfies the comonoid laws. ◀

Because $\Sigma$ is a comonoid, it follows that $\Sigma \otimes -$ is a comonad on Gam. We write $\text{Gam}_\Sigma$ for its Kleisli category. $\text{Gam}_\Sigma$ inherits all the categorical structure from Gam, that is to say, it is symmetric monoidal closed category with products, and as such supports the interpretation of the affine $\lambda$-calculus with products and free variables in $\Sigma$ duplicable at will.

In particular, the interpretation of a terminal $b : \&_{p_1} o \to \dots \to \&_{p_n} o \to o$ is the strategy:

$$[[b]] : \Sigma \otimes (\&_{\Sigma p_i} [[o]]) \to [[o]]$$

playing $b$ on the left, and if Opponent calls the argument $(i, j)$, so does Player. Furthermore:

$$[[b]((t_{1,j} | 1 \le j \le p_1), \dots, (t_{n,j} | 1 \le j \le p_n))] = [[b]] \circ_\Sigma \langle t_{i,j} | 1 \le i \le n, 1 \le j \le p_i \rangle$$

In other words, the games model treats all terminal symbols as purely additively typed. This reflects the fact that syntactically, every MAHORS can be re-typed with all terminals typed purely additively. This however comes with a loss of information, because multiplicative branching implies that no sharing is allowed between the branches. This will become particularly relevant for the part of our development that concerns MHORS. Hence we will later add further information on strategies for MHORS to recover a posteriori the linearity information coming from multiplicative branching.

Now, strategies on $\Sigma \to o$ can be regarded as trees – apart from the initial move $o$, we have only player playing terminal symbols and Opponent playing directions allowing us to explore the tree. We keep silent the implicit conversion between distinct representations of trees as normal terms $\Sigma \mid \_ \to t : o$ and as strategies on $\Sigma \to o$; in particular the interpretation of a normal term yields directly the representation of the same tree as a strategy.

Leveraging the categorical structure we just established, we have:

**► Theorem 19.** For any $\Sigma \mid \_ \to t : o$, we have

$$[[t]] = \text{BT}(t)$$

leaving implicit the syntactic correspondence between trees and strategies on $\Sigma \to o$.

**Proof.** From the categorical laws the interpretation preserves the reduction, and then it is an immediate verifications for the normal forms. ◀
## B.2 Finite memory and history-free strategies

To generate finite memory and history-free strategies, we use the strategic transducers of Definition 2. In the main text, the definition of the strategy generated by a strategic transducer ignores the terminal symbols – here, we must extend it to deal with those.

Let $\mathcal{T} = (\mathcal{M}_- \uplus \mathcal{M}_+, m_0, \delta_-, \delta_+)$ be a strategic transducer on $A$. Then, we define a labeled transition system whose nodes are $\mathcal{M}_- \uplus \mathcal{M}_+ \uplus \{m^b | m \in \mathcal{M}_+, b \in \Sigma\}$.

$$m_{-} \xrightarrow{a} m_{+} \quad \text{if } a \in M_{-}^{\tau} \text{ and } \delta_{-}(m_{-}, a) = m_{+}$$

$$m_{+} \xrightarrow{\epsilon} m'_{+} \quad \text{if } \delta_{+}(m_{+}) = m'_{+}$$

$$m_{+} \xrightarrow{b} m_{-} \quad \text{if } b \in M_{+}^{\tau} \text{ and } \delta_{+}(m_{+}) = (m_{-}, b)$$

$$m_{+} \xrightarrow{b} m_{+}^{b} \quad \text{if } \delta_{+}(m_{+}) = b(\dots)$$

$$m_{+}^{b} \xrightarrow{i} m'_{i} \quad \text{if } \delta_{+}(m_{+}) = b(m'_{1}, \dots, m'_{|b|})$$

We refine the definition of Traces($\mathcal{T}$) given in the main text to take account of the terminal symbols. If $s \in M_{\Sigma \to A}^*$, for $m, m' \in \mathcal{M}_- \uplus \mathcal{M}_+$, $\{m^b | m \in \mathcal{M}_+, b \in \Sigma\}$, we define $m \stackrel{s}{\Rightarrow} m'$ as the smallest relation such that $m \stackrel{\epsilon}{\Rightarrow} m$, and if $m \stackrel{s}{\Rightarrow} m'$ and $m' \stackrel{s'}{\Rightarrow} m''$, then $m \stackrel{ss'}{\Rightarrow} m''$. The traces of $\mathcal{T}$ are those $s \in M_{\Sigma \to A}^*$ such that $m_0 \stackrel{s}{\Rightarrow} m$ for some $m$.

**Proposition 20.** If $\mathcal{T}$ is a strategic transducer on $A$, then if $s \in \text{Strat}(\mathcal{T})$, if $sa \in P_{\Sigma \to A}$ and $sab \in \text{Traces}(\mathcal{T})$, then $sab \in P_{\Sigma \to A}$ as well.

**Proof.** Ignoring the part of the play on $\Sigma$, this is by definition of strategic transducers. To this the present definition adds subsequences $bi$ in $\Sigma$, preserving correctness in $\Sigma \to A$. $\quad$ ◀

If $\mathcal{T}$ is a strategic transducer on $A$, then $\text{Plays}(\mathcal{T})$ is a strategy on $\Sigma \to A$. By construction it is non-empty set of even-length plays closed by even-length prefixes. It is deterministic as a strategic transducer is deterministic (its transitions are given by functions). We say that a strategy $\sigma: \Sigma \to A$ has **finite memory** if it is generated by a strategic transducer.

Furthermore, we say that a strategy $\sigma: \Sigma \to A$ is **history-free** if it is generated by a strategic transducer with $\mathcal{M}_-$ a singleton set. At first sight, this seems different from the traditional notion of history-free strategy. Indeed, the traditional notion is too strict to deal correctly with the presence of $\Sigma$ here. For instance, all symbols in $\Sigma$ share the same moves for the subsequent directions, so the strategy for e.g. $b(b(\perp))$ would not be history-free in the traditional sense as the same move (the direction 0) yields the move b the first time and no response the second time. Our revised notion of history-free treats $\Sigma$ in a distinct way as it should. An history-free strategy in the present sense that does not play on $\Sigma$ is exactly a history-free strategy in the traditional sense; so we regard the present notion as a generalization of history-freeness in the context of tree-generating strategies.

In particular, all plain copycat strategies are history-free. This includes all the structural isomorphism from the symmetric monoidal closed structure of $\mathbf{Gam}$. However, there are of course more finite-memory strategies than history-free. In particular, we have the following.

**Lemma 21.** Let $A$ be a game. Then, the duplication strategy:

$$\delta_A: \Sigma \otimes A \to A \& A$$

has finite memory.

**Proof.** Note that the strategy does not play in $\Sigma$, but we include it anyway as it is a structural morphism in the Kleisli category $\mathbf{Gam}_{\Sigma}$.
We have to provide a strategic transducer for $\delta_A$. For clarity, let us label the copies of $A$ in $A \to A \& A$ as $A_1 \to A_2 \& A_3$. In the rest of the argument, the subscripts on moves indicate in which components they rest, while their polarity annotation is that taken for the full game.

Our strategic transducer has $M_-$ = {$m_0, m_l, m_r$} and $M_+$ = $M_- \times M_{\Sigma \otimes A_1 \to A_2 \& A_3}$. Its negative transition function is $\delta_-(m, a) = (m, a)$. Its positive transition function is

$$ \delta_+ : \begin{array}{rcl} \mathcal{M}_+ & \to & \mathcal{M}_- \times M_{\Sigma \otimes A_1 \to A_2 \& A_3}^+ \\ (\_, a_2^-) & \mapsto & (m_l, a_1^+) \\ (\_, a_3^-) & \mapsto & (m_r, a_1^+) \\ (m_l, a_1^-) & \mapsto & (m_l, a_2^+) \\ (m_r, a_1^-) & \mapsto & (m_r, a_3^+) \end{array} $$

and undefined otherwise – note that its codomain does not use all the output possibilities for a positive transition function of a strategic transducer. It is straightforward to check that this is a strategic transducer, and that it generates $\delta_A$. ◀

In general, the symmetric monoidal closed category with products $\mathbf{Gam}_\Sigma$ admits a sub-smcc with products of history-free strategies. To establish that, we must show that all usual operations on strategies can be replicated on strategic transducers in a compatible way.

**Proposition 22.** Let $S: A \to B$ and $T: B \to C$ be strategic transducers. Then, $T \otimes S$ is a strategic transducer and

$$ \mathrm{Strat}(T \otimes S) = \mathrm{Strat}(T) \circ_S \mathrm{Strat}(S) $$

In particular, the composition of finite memory strategies is a finite memory strategy, and the composition of history-free strategies is history-free.

**Proof.** $\subseteq$. If $s \in \mathrm{Strat}(T \otimes S)$, then there is $(m_0, m_0) \stackrel{s}{\Rightarrow} (m_1, m_2)$ in $T \otimes S$. Projecting these transitions on $S$ and $T$, we get two sequences $m_0 \stackrel{s_S}{\Rightarrow} m_1$ and $m_0 \stackrel{s_T}{\Rightarrow} m_2$ where $s_S \in P_{\Sigma \otimes A \to B}$ and $s_T \in P_{\Sigma \otimes B \to C}$. Note that the fact that these are indeed correct plays follows from Proposition 20. By construction, these plays are such that $s_S \upharpoonright B = s_T \upharpoonright B$. By induction on the transitions in $T \otimes S$ for $s$, exploiting that the definition of $T \otimes S$ follows the usual state diagram of interactions in simple games, this lets us build $u \in \tau \otimes (\Sigma \otimes \sigma)$ whose projections yields $s_S$ and $s_T$ and where moves in $\Sigma, A, C$ appear in the same order in $u$ as in $s$. This yields $s' \in \tau \circ (\Sigma \otimes \sigma) : \Sigma \otimes \Sigma \otimes A \to C$ differing only from $s$ in that the calls to $\Sigma$ from $S$ and $T$ appear in different components. Composing with duplication on $\Sigma$, we get $s \in \mathrm{Strat}(T) \circ_S \mathrm{Strat}(S)$ as required.

$\supseteq$. If $s \in \mathrm{Strat}(T) \circ_S \mathrm{Strat}(S)$, then there is a witness $u \in \mathrm{Strat}(T) \otimes (\Sigma \otimes \mathrm{Strat}(S))$, with projections $t_S = u \upharpoonright \Sigma_1, A, B \in \mathrm{Strat}(S)$ and $t_T = u \upharpoonright \Sigma_2, B, C \in \mathrm{Strat}(T)$ are respectively obtained by sequences of transitions from $m_0$ in $S$ and $T$. Following the state diagram of interactions, it is direct to synchronise these two sequences of transitions and obtain a sequence of transitions on $T \otimes S$ generating $s$. ◀

The conclusion on history-free strategies follows from $M_-^{T \otimes S} = M_-^S \times M_-^T$.

Other constructions on strategies are straightforward as there is no interaction between them. In particular, if $S_1: A_1 \to B_1$ and $S_2: A_2 \to B_2$, the tensor strategic transducer $S_1 \otimes S_2$ has $M_-^{S_1 \otimes S_2} = M_-^{S_1} \times M_-^{S_2}$ and $M_+^{S_1 \otimes S_2} = M_+^{S_1} \times M_+^{S_2}$ and transition functions defined componentwise in the obvious sense. It is direct to prove that $S_1 \otimes S_2$ is a strategic transducer and that $\mathrm{Strat}(S_1 \otimes S_2) = \mathrm{Strat}(S_1) \otimes_S \mathrm{Strat}(S_2)$. Overall, we have:
**► Theorem 23.** There are two sub symmetric monoidal closed categories of $\mathbf{Gam}_\Sigma$, written $\mathbf{Gam}_\Sigma^{\text{hf}}$ and $\mathbf{Gam}_\Sigma^{\text{fm}}$, where strategies are respectively history-free and finite memory strategies. Moreover, the latter also has products.

In particular, this means that besides the interpretation $\llbracket - \rrbracket$ of the linear $\lambda$-calculus with products in $\mathbf{Gam}_\Sigma$, there is also a function interpreting each linear $\lambda$-term with products $\Sigma | \Gamma \vdash t : A$ as a strategic transducer $\langle t \rangle : \llbracket \Gamma \rrbracket \to \llbracket A \rrbracket$ such that $\text{Strat}(\langle t \rangle) = \llbracket t \rrbracket$. In particular, if $\Sigma | \Gamma \vdash t : o$, it follows that $\text{Tree}(\langle t \rangle) = \text{Strat}(\langle t \rangle) = \llbracket t \rrbracket = \text{BT}(t)$.

C Auxiliary material (Section 4.2)

Our automata are a variant of tree stack automata proposed in [7], adapted to generate deterministically a potentially infinite tree. The automata feature finite-state control and a tree-shaped memory. In tree nodes one can store and update elements of a finite memory alphabet $\mathcal{M}$. To keep track of the current position in the tree, [7] introduces an implicit stack pointer. In our definition the stack is integrated into the machine and the automaton has access to the top stack symbol. This allows us to conclude immediately that the model reduces to a pushdown automaton for $\mathcal{M} = \{\star\}$. Otherwise, the difference is immaterial for expressivity, because one could maintain the information about the top stack symbol using state and tree memory<fnref n="3" />.

**► Definition 24.** A tree-generating TSA $\mathcal{A}$ is a tuple $\langle \Sigma, Q, \Gamma, \mathcal{M}, \delta, q_0, m_0, \gamma_0 \rangle$ where $\Sigma$ is a ranked alphabet of non-terminals, $Q$ is a set of states, $\Gamma$ is a finite stack alphabet, $\mathcal{M}$ is a finite memory alphabet, $\delta$ is the transition function, $q_0 \in Q$ is the starting state, $m_0 \in \mathcal{M}$ is the starting memory, and $\gamma_0$ is the bottom-of-stack symbol (corresponding to the root of the tree memory). The transition function has the following type

$$ \delta : Q \times \mathcal{M} \times \Gamma^* \to Q + \{b(q_1, \dots, q_{|\Gamma|}) \mid q_i \in Q, b \in \Sigma\} + Q \times \mathcal{M} \times (\{\text{up}_\gamma \mid \gamma \in \Gamma\} + \{\text{down}\}), $$
where $\Gamma^* = \Gamma \uplus \{\gamma_0\}$, writing $\gamma_0$ for the bottom-of-stack marker.

**► Definition 25.** A TSA configuration $\xi$ is a tuple $(q, p, \rho)$, where $q \in Q$, $p \in \Gamma^*\gamma_0$ and $\rho : \Gamma^*\gamma_0 \to \mathcal{M} \times \mathbb{N}_{>0}$ is such that $\text{dom}(\rho)$ is non-empty, finite and suffix-closed, and $p \in \text{dom}(\rho)$.

$\rho$ gives information about node labels and the number of times a particular node has been visited. $p$ corresponds to the current stack, which indicates the current position in the tree. Because $\text{dom}(\rho)$ is non-empty and suffix-closed, we must have $\gamma_0 \in \text{dom}(\rho)$. The initial configuration is $\xi_0 = (q_0, \gamma_0, \{\gamma_0 \mapsto (m_0, 1)\})$. The run-tree of $\mathcal{A}$ is the tree rooted at $\xi_0$ obtained by following the rules given below, where $\xi \to b(\xi_1, \dots, \xi_{|\mathcal{B}|})$ denotes branching and $\xi \to \xi'$ a silent transition. Each rule is predicated on $\pi_1(\rho(p)) = m$.

$$ \delta(q, m, \gamma) = q' $$

$$ (q, \gamma p, \rho) \to (q', \gamma p, \rho) $$

$$ \delta(q, m, \gamma) = b(q_1, \dots, q_{|\mathcal{B}|}) $$

$$ (q, \gamma p, \rho) \to b((q_1, \gamma p, \rho), \dots, (q_{|\mathcal{B}|}, \gamma p, \rho)) $$

<footnote n="3">³ Because our model features a stack, we use $\gamma$ to refer to the stack alphabet and $\mathcal{M}$ to refer to the memory alphabet. [7] uses $\Gamma$ for the latter.</footnote>
■ $\delta(q, m, \gamma) = (q', m', up_{\gamma'})$
$(q, \gamma p, \rho) \rightarrow (q', \gamma' \gamma p, \rho')$

where

$$ \rho'(s) = \begin{cases} \rho(s) & s \in \text{dom}(\rho), s \neq \gamma p, \gamma' \gamma p \\ (m', i) & s = \gamma p, \rho(s) = (m, i) \\ (m_0, 1) & s = \gamma' \gamma p, s \notin \text{dom}(\rho) \\ (m'', i+1) & s = \gamma' \gamma p, \rho(s) = (m'', i) \end{cases} $$

■ $\delta(q, m, \gamma) = (q', m', \text{down})$
$(q, \gamma p, \rho) \rightarrow (q', p, \rho')$

where

$$ \rho'(s) = \begin{cases} \rho(s) & s \in \text{dom}(\rho), s \neq \gamma p \\ (m', i) & s = \gamma p, \rho(s) = (m, i) \end{cases} $$

This transition fires only if $\gamma \neq \gamma_0$, i.e. the automaton gets stuck if down is executed when the bottom-of-stack symbol is at the top of the stack.

A run is a prefix of any branch of the run-tree.

**► Definition 26.** A TSA is k-restricted if no node is entered from below more than k times in any run. Formally, for any configuration $(q, p, \rho)$ reachable from $\xi_0$, we have $\text{img } \rho \subseteq \mathcal{M} \times \{1, \dots, k\}$.

## D Additional material (Section 5)

This is a formal account of the translation. Consider a k-restricted TSA $\mathcal{A} = (\Sigma, Q, \Gamma, \mathcal{M}, \delta, q_0, \gamma_0, m_0)$ with

$$ \delta: Q \times \mathcal{M} \times \Gamma^{\bullet} \rightarrow Q + \{\mathfrak{b}(q_1, \dots, q_{|\mathfrak{b}|}) \mid q_i \in Q, \mathfrak{b} \in \Sigma\} + Q \times \mathcal{M} \times (\{\text{up}_{\gamma} \mid \gamma \in \Gamma\} + \{\text{down}\}). $$

Let $B = |\Gamma|$ and $\Gamma = \{\gamma_1, \dots, \gamma_B\}$. Given a type $T$, let us write $\overline{T}$ for $\&_{q \in Q} T$, i.e. $|Q|$ copies of $T$. The construction of a MAHORS that is equivalent to the given TSA depends on types $T_i$ ($0 \le i \le k$) defined by

$$ T_i = \begin{cases} \frac{o}{(\overline{T_{i+1}} \to o)} & \to o & i=k \\ 0 & \le i < k \end{cases} $$

The corresponding MAHORS $\mathcal{G}_{\mathcal{A}} = (\Sigma, \mathcal{N}, \mathcal{R}, S)$ is defined as follows.

■ Terminals: $\Sigma$

■ Nonterminals $\mathcal{N}$:

$$ \begin{array}{lcl} S & : & o \\ N_{q,j} & : & T_0 \\ F_{q,m,\gamma}^{\bar{u};d} & : & \overline{T_{u_1}} \to \dots \to \overline{T_{u_B}} \to T_{d-1} \\ G_{q,m,\gamma}^{\bar{u};d;j} & : & \overline{T_{u_1}} \to \dots \overline{T_{u_{j-1}}} \to \overline{T_{u_{j+1}}} \to \dots \overline{T_{u_B}} \to (\overline{T_d} \to o) \to \overline{T_{u_j}} \to o \\ \Omega_o & : & o \\ \Omega_{\overline{T_1} \to o} & : & \overline{T_1} \to o \end{array} $$

where $q \in Q$, $1 \le j \le B$, $m \in \mathcal{M}$, $\gamma \in \Gamma^{\bullet}$, $\bar{u} = (u_1, \dots, u_B) \in \{0, \dots, k\}^B$ and $d \in \{1, \dots, k+1\}$.
Rules $\mathcal{R}$:

- Start

$$ 
\begin{aligned}
S &= F_{q_0, m_0, \gamma_0}^{0, \dots, 0; 1} N_1 \cdots N_B D \\
N_{q,j} y &= F_{q, m_0, \gamma_j}^{0, \dots, 0; 1} N_1 \cdots N_B y
\end{aligned}
 $$

for any $q \in Q$, $1 \le j \le B$, where

$$ 
\begin{aligned}
N_j &\equiv \langle N_{q,j} | q \in Q \rangle : \overline{T_0} \\
D &\equiv \langle \Omega_{\overline{T_1 \to o}} | q \in Q \rangle
\end{aligned}
 $$

and $\equiv$ stands for syntactic equality.

- $\delta(q, m, \gamma) = q'$ (state change)

$$ F_{q,m,\gamma}^{\overline{u};d} x_1 \cdots x_B y = F_{q',m,\gamma}^{\overline{u};d} x_1 \cdots x_B y $$

where $\overline{u} \in \{0, \dots, k\}^B$, $1 \le d \le k$ and $(q, m, \gamma) \in Q \times \mathcal{M} \times \Gamma^\bullet$.

- $\delta(q, m, \gamma) = b(q_1, \dots, q_{|b|})$ (branching)

$$ F_{q,m,\gamma}^{\overline{u};d} x_1 \cdots x_B y = b \langle F_{q_1,m,\gamma}^{\overline{u};d} x_1 \cdots x_B y, \dots, F_{q_{|b|},m,\gamma}^{\overline{u};d} x_1 \cdots x_B y \rangle. $$

where $\overline{u} \in \{0, \dots, k\}^B$, $1 \le d \le k$ and $(q, m, \gamma) \in Q \times \mathcal{M} \times \Gamma^\bullet$.

- $\delta(q, m, \gamma) = (q', m', \text{down})$

$$ F_{q,m,\gamma}^{\overline{u};d} x_1 \cdots x_B y = (\pi_{q'} y) \langle F_{q'',m',\gamma}^{\overline{u};d+1} x_1 \cdots x_B | q'' \in Q \rangle. $$

where $\overline{u} \in \{0, \dots, k\}^B$, $1 \le d \le k$ and $(q, m, \gamma) \in Q \times \mathcal{M} \times \Gamma^\bullet$.

- $\delta(q, m, \gamma) = (q', m', up_{\gamma_j})$

$$ 
\begin{aligned}
F_{q,m,\gamma}^{\overline{u};d} x_1 \cdots x_B y &= (\pi_{q'} x_j) \langle F_{q'',m',\gamma}^{\overline{u}+e_j;d;j} x_1 \cdots x_{j-1} x_{j+1} \cdots x_B y | q'' \in Q \rangle, \\
G_{q,m,\gamma}^{\overline{u};d;j} x_1 \cdots x_{j-1} x_{j+1} \cdots x_B y z &= F_{q,m,\gamma}^{\overline{u};d} x_1 \cdots x_{j-1} z x_{j+1} \cdots x_B y.
\end{aligned}
 $$

where $\overline{u} \in \{0, \dots, k\}^B$, $1 \le d \le k$ and $(q, m, \gamma) \in Q \times \mathcal{M} \times \Gamma^\bullet$.

- Auxiliary rules to induce divergences:

$$ 
\begin{aligned}
\Omega_o &= \Omega_o \\
\Omega_{\overline{T_1 \to o}} x &= \Omega_{\overline{T_1 \to o}} x \\
F_{q,m,\gamma}^{\overline{u};k+1} x_1 \cdots x_B &= \Omega_o
\end{aligned}
 $$

for $\overline{u} \in \{0, \dots, k\}^B$ and $(q, m, \gamma) \in Q \times \mathcal{M} \times \Gamma^\bullet$.

In order to prove that the TSA-to-MAHORS translation is correct, it is necessary to understand how a TSA configuration $\xi = (q, p, \rho)$ can be represented using an applicative term $\mathcal{T}_\xi$. We start with an auxiliary definition.

► **Definition 27.** Given $r \in \text{dom}(\rho)$ such that $\rho(r) = (m_r, d_r)$, let $\overline{u}_r$ be the vector $(u_{r,1}, \dots, u_{r,B})$ defined by

$$ u_{r,i} = \begin{cases} 0 & \gamma_i r \notin \text{dom}(\rho) \\ \pi_2(\rho(\gamma_i r)) & \gamma_i r \in \text{dom}(\rho) \end{cases} $$
Suppose $\rho(p) = (m, d)$. The term $\mathcal{T}_\xi$ will use the non-terminal

$$F_{q,m,\gamma_p}^{\tilde{u}_p;d} : \overline{T_{u_{p,1}}} \to \dots \to \overline{T_{u_{p,B}}} \to T_{d-1}$$

as its head variable, where $\gamma_p$ is the topmost (leftmost) element of $p$.

The first $B$ arguments of $F_{q,m,\gamma}^{\tilde{u}_p;d}$ will correspond to visiting nodes above $p$. We call them *upwards continuations*. Note that, because these future visits are from below, the non-terminals involved carry a superscript $(d_r + 1)$ equal to the number of times the node has already been visited plus 1.

**Definition 28.** Let $r = \gamma_{j_r} r' \in \Gamma^* \gamma_0$. The term $\mathcal{U}_r$ is then defined as follows

$$\mathcal{U}_r \equiv \begin{cases} \langle N_{q,j_r} | q \in Q \rangle & r \notin \text{dom}(\rho) \\ \langle F_{q,m_r,\gamma_{j_r}}^{\tilde{u}_r;d_r+1} \mathcal{U}_{\gamma_1 r} \cdots \mathcal{U}_{\gamma_B r} | q \in Q \rangle & r \in \text{dom}(\rho), \rho(r) = (m_r, d_r) \end{cases}$$

Note that this definition refers to $\mathcal{U}_{\gamma_i r}$ when defining $\mathcal{U}_r$. This is well-founded, because $\text{dom}(\rho)$ is finite. Observe that we have $\mathcal{U}_r : \overline{T_{d_r}}$ if $r \in \text{dom}(\rho)$ (and $\rho(r) = (m_r, d_r)$) and $\mathcal{U}_r : \overline{T_0}$ otherwise.

Because $d \le k$, the non-terminal $F_{q,m,\gamma}^{\tilde{u}_p;d}$ has a $(B+1)$th argument. It will correspond to visiting the node below $p$ and we call it a *downwards continuation*. Note that, because the visit will be from above, the non-terminals involved will carry a superscript $(d_{r'})$ that coincides with the number of times the node has been visited so far.

**Definition 29.** Given $r \in \text{dom}(\rho)$ such that $\rho(r) = (m_r, d_r)$, define the term $\mathcal{D}_r : \overline{T_{d_r}} \to o$ as follows.

$$\mathcal{D}_r = \begin{cases} \langle \Omega_{\overline{T_1} \to o} | q \in Q \rangle & r = \gamma_0 \\ \langle G_{q,m_{r'},\gamma_{j_{r'}}}^{\tilde{u}_{r'}} d_{r'}; j_r \mathcal{U}_{\gamma_1 r'} \cdots \mathcal{U}_{\gamma_{j_{r-1} r'}} \mathcal{U}_{\gamma_{j_{r+1} r'}} \cdots \mathcal{U}_{\gamma_B r'} \mathcal{D}_{r'} | q \in Q \rangle & r = \gamma_{j_r} r', r' = \gamma_{j_{r'}} r'' \\ \rho(r') = (m_{r'}, d_{r'}) & \end{cases}$$

This definition is inductive and relies on the fact that $\gamma_0 \in \text{dom}(\rho)$ and $\text{dom}(\rho)$ is suffix-closed. Note that $u_{r',j_r} = d_r$, so in the second case the term indeed has type $\overline{T_{d_r}} \to o$.

**Definition 30.** Given a configuration $\xi = (q,p,\rho)$ such that $\rho(p) = (m,d)$ and $p = \gamma_p r'$, the corresponding term $\mathcal{T}_p : o$ is defined to be

$$\mathcal{T}_p \equiv F_{q,m,\gamma_p}^{\tilde{u}_p;d} \mathcal{U}_{\gamma_1 p} \cdots \mathcal{U}_{\gamma_B p} \mathcal{D}_p.$$

The correctness of the translation can now be established by showing that the MAHORS rules simulate the configuration graph of the TSA faithfully. Let $\xi_0$ be the initial TSA configuration and observe that

$$\mathcal{T}_{\xi_0} \equiv F_{q_0,m_0,\gamma_0}^{0,\dots,0;1} \mathcal{U}_{\gamma_1 \gamma_0} \cdots \mathcal{U}_{\gamma_B \gamma_0} \mathcal{D}_{\gamma_0} \equiv F_{q_0,m_0,\gamma_0}^{0,\dots,0;1} N_1 \cdots N_B D$$

and that $S = F_{q_0,m_0,\gamma_0}^{0,\dots,0;1} N_1 \cdots N_B D$ is a rule in the corresponding MAHORS, i.e. $S = \mathcal{T}_{\xi_0}$. This means that the "starting points" of both formalisms coincide. Next we perform a case analysis of MAHORS rules, showing that every step based on rules from $\mathcal{G}_A$ corresponds to a transition in $A$, and vice versa.

**Definition 31.** An applicative term $M$ built from terminals and non-terminals of $\mathcal{G}_A$ is called a $F$-term if $M$ is of the form $F_{q,m,\gamma}^{\tilde{u}_p;d} \cdots$. Similarly, we define $G$- and $N$-terms.

Suppose $M \equiv \mathcal{T}_\xi$ for some $\xi$ and $M = M'$ (one-step) according to $\mathcal{R}$. Then $M$ is a $F$-term and the following cases arise for $M'$.
43:22 On the expressivity of linear recursion schemes

- $M'$ is an F-term.

This is the case if the rule for (state change) was used to derive $M = M'$. Because $M \equiv \mathcal{T}_\xi$, we have $M' \equiv \mathcal{T}_{\xi'}$, where $\xi \to \xi'$ (via $\delta(q, m, \gamma) = q'$).

- $M' \equiv \mathbf{b}(M_1, \dots, M_B)$

In this case the (branching) rule must have been used. Because $M \equiv \mathcal{T}_\xi$, we have $M_i \equiv \mathcal{T}_{\xi_i}$ for $\xi_1, \dots, \xi_B$ such that $\xi \to \mathbf{b}(\xi_1, \dots, \xi_B)$.

- $M' \equiv (\pi_q \dots)^{\dots}$. In this case, the *up* or *down* rule must have been used.

- If *up* then, because $M \equiv \mathcal{T}_\xi$, after applying the projection rule, one obtains an F- or an N-term. In the former case, it will represent the configuration $\xi'$ such that $\xi \to \xi'$ (via $\delta(q, m, \gamma) = (q', m', up_{\gamma'})$). In the latter case, after a single application of the rule for N, we can conclude the same.

- If *down* then, because $M \equiv \mathcal{T}_\xi$, after applying the projection rule, one obtains a G- or $\perp$-term. In the former case, after a single application of the rule for G, we arrive at a term that represents $\xi'$ such that $\xi \to \xi'$ (via $\delta(q, m, \gamma) = (q', m', \mathit{down})$). The $\perp$-case can arise only for $M \equiv F_{q,m,\gamma_0}^{\vec{u};d} \dots$. Because $M \equiv \mathcal{T}_\xi$, we can conclude that $\xi$ has only $\gamma_0$ on the stack, i.e. the TSA cannot move.

This shows that $\mathcal{A}$ can simulate $\mathcal{R}_\mathcal{A}$. For the converse, since we already established $S = \mathcal{T}_{\xi_0}$, it suffices to observe that

- if $M \equiv \mathcal{T}_\xi$ and $\xi \to \xi'$ then:

- if $\xi \to \xi'$ by (state change) we have $M = \mathcal{T}_{\xi'}$ (by a single F-rule);

- if $\xi \to \xi'$ by (up) then we have $M = M' = \mathcal{T}_{\xi'}$ (by F-rule+projection) or $M = M' = M'' = \mathcal{T}_{\xi'}$ (by F-rule+projection+N-rule);

- if $\xi \to \xi'$ by (down) then we have $M = M' = M'' = \mathcal{T}_{\xi'}$ (by F-rule+projection+G-rule);

- if $M \equiv \mathcal{T}_\xi$ and $\xi \to \mathbf{b}(\xi_1, \dots, \xi_B)$ then $M = \mathbf{b}(\mathcal{T}_{\xi_1}, \dots, \mathcal{T}_{\xi_B})$ (by F-rule).

Altogether we can conclude $\mathcal{A}$ and $\mathcal{R}_\mathcal{A}$ generate the same infinite tree.

E Auxiliary material (Section 6)

Recall the grammar for the Dyck language:

$$D ::= \epsilon \mid [D]D.$$

We are going to recast it in terms of triples of identical words. To represent words over $\{[], \}\}$, we use the type $W = o \to o$ and terminals $[., ]: W$. The empty word then corresponds to the identity function $I: W$. To represent triples of words of type $W$, we use the type $\mathcal{T}_3 = (W \to W \to W \to o) \to o$ on the understanding that a triple $(M_1, M_2, M_3)$ is represented by $\lambda f.f M_1 M_2 M_3: \mathcal{T}_3$.

Then the Dyck grammar can be lifted to type $\mathcal{T}_3$ as follows, where the terminal $\mathbf{b}: o \to o \to o$ represents choice between the two rules.

$$Df = \mathbf{b}(fIII, Concat\,(Bracket\,D)\,Df)$$

where

- **Bracket**: $\mathcal{T}_3 \to \mathcal{T}_3$ represents a function that adds outermost brackets to each component of the given triple $((x, y, z) \mapsto ([x], [y], [z]))$,

- **Concat**: $\mathcal{T}_3 \to \mathcal{T}_3 \to \mathcal{T}_3$ concatenates components of two triples $((x_1, y_1, z_1), (x_2, y_2, z_2) \mapsto (x_1 x_2, y_1 y_2, z_1 z_2))$.
The two terms are defined below.

$$ \text{Bracket } X f = X(\lambda xyz.f(Bx)(By)(Bz)) $$

$$ Bwv = [(w()v)) $$

$$ \text{Concat } X_1 X_2 f = X_1(\lambda x_1 y_1 z_1 . X_2(\lambda x_2 y_2 z_2 . f(Cx_1x_2)(Cy_1y_2)(Cz_1z_2))) $$

$$ Cw_1w_2v = w_1(w_2v) $$

It follows that

$$ \text{Concat} (\text{Bracket } D) D f = D(\lambda x_1 y_1 z_1 . D(\lambda x_2 y_2 z_2 . f(Kx_1x_2)(Ky_1y_2)(Kz_1z_2))), $$

where $Kw_1w_2v = [(w_1()()w_2v))$. This yields the equation used in the main body of the paper:

$$ Df = b(fIII, D(\lambda x_1 y_1 z_1 . D(\lambda x_2 y_2 z_2 . f(Kx_1x_2)(Ky_1y_2)(Kz_1z_2))))). $$

By unfolding the right-hand side one can obtain an infinite tree whose leaves are labelled with terms of the form $fMMM$, where $M$ ranges over (representations of) words from the Dyck language. In order to generate branches that end in words from $L = \{w\#w\#w | w \in D\}$, it now suffices to merge the components of the triples into single words by passing a concatenating function:

$$ S = D(\lambda xyz.x(\#(y(\#(z$))))). $$

Note the use of two new terminals: $\# : W$ to separate the words and $\$ : o$ to end the branch.

Above we have used $\lambda$-syntax for brevity. Below we give an equivalent definition based on applicative terms, obtained by introducing auxiliary non-terminals for various subterms of the $\lambda$-terms.

$$ S = D(\text{Init}) $$

$$ \text{Init } x y z = x(\#(y(\#(z$))) $$

$$ S f = b(fIII, D(Ef)) $$

$$ I v = v $$

$$ E f x_1 y_1 z_1 = D(F f x_1 y_1 z_1) $$

$$ F f x_1 y_1 z_1 x_2 y_2 z_2 = f(K x_1 x_2)(K y_1 y_2)(K z_1 z_2) $$

$$ K w_1 w_2 v = [(w_1()()w_2v)) $$

## F Auxiliary material (Section 7)

First we explain how to define a pushdown system $\mathcal{P}_A = \langle Q, \Gamma^\bullet, \Delta \rangle$ [4], where $\Delta \subseteq Q \times \Gamma^\bullet \times Q \times (\Gamma^\bullet)^*$, from a PDA $\langle \Sigma, Q, \Gamma, \delta, q_0, \gamma_0 \rangle$ whose transition function has the form

$$ \delta : Q \times \Gamma^\bullet \rightarrow Q + \{b(q_1, \dots, q_{|b|}) \mid q_i \in Q, b \in \Sigma\} + Q \times (\{up_\gamma \mid \gamma \in \Gamma\} + \{down\}). $$

We define $\Delta$ as the smallest set satisfying the rules below.

- If $\delta(q, \gamma) = q'$ then $(q, \gamma, q', \gamma) \in \Delta$.

- If $\delta(q, \gamma) = b(q_1, \dots, q_{|b|})$ then $(q, \gamma, q_i, \gamma) \in \Delta$ for any $1 \le i \le |b|$.

- If $\delta(q, \gamma) = (q', up_\gamma)$ then $(q, \gamma, q', \gamma'\gamma) \in \Delta$.

- If $\delta(q, \gamma) = (q', down)$ and $\gamma \neq \gamma_0$ then $(q, \gamma, q', e) \in \Delta$.

The condition $\gamma \neq \gamma_0$ corresponds to our convention that TSA block if down is executed on a stack containing $\gamma_0$ at the top. The corresponding configuration graph has $Q \times (\Gamma^\bullet)^*$ as nodes and edges $\Rightarrow$ are defined by

$$ (q_1, \gamma w) \Rightarrow (q_2, w'w), $$
where $(q_1, \gamma, q_2, w') \in \Delta$ and $w \in (\Gamma^\bullet)^*$. Note that this graph is more general than the TSA configuration graph defined earlier, e.g. it contains configurations with empty stack or without $\gamma_0$. However, the two coincide on configurations reachable from $(q_0, \gamma_0)$.

In the paper we take advantage of reachability analysis for pushdown systems [4, 9]. In particular, the relation $R_A = \{(q, \gamma, q') \in Q \times \Gamma \times Q \mid (q, \gamma) \Rightarrow^* (q', \epsilon)\}$ can be calculated in polynomial time. Recall that an LPDA is PDA with a linearity property: any configuration reachable from $(q_0, \gamma_0)$ can be reached via a unique path.

**Lemma 32.** For any LPDA $\mathcal{A}$, there exists an equivalent MHORS (of order 1) and its construction can be carried out in polynomial time.

**Proof.** W.l.o.g. assume $Q = \{1, \dots, N\}$ and use the following non-terminals $S: o, F_{(q,\gamma)}: o \to \dots \to o \to o$. The translation uses the same term representation of stacks as the 1-CPDA $\underbrace{N}_{N}$ to 1-HORS translation in [12] except that reachability analysis ($R_A$) is used to identify places where the variables actually get used. Intuitively, $F_{(q,\gamma)}x_1 \cdots x_N$ represents a configuration where $\gamma$ is at the top of the stack, and each $x_i$ corresponds to a configuration that would be reached if $\gamma$ was popped and the automaton transitioned to state $i$.

For rules, we take $S = F_{(q_0, \gamma_0)} \perp \cdots \perp \bot$ and

$$ F_{(q, \gamma)} x_1 \cdots x_N = \left\{ \begin{array}{ll} F_{(q', \gamma)} x_1 \cdots x_N & \delta(q, \gamma) = q' \quad \text{(state change)} \\ \mathfrak{b} B_1 \cdots B_{|\mathfrak{b}|} & \delta(q, \gamma) = \mathfrak{b}(q_1, \dots, q_{|\mathfrak{b}|}) \quad \text{(branching)} \\ x_{q'} & \delta(q, \gamma) = (q', \text{down}) \quad \text{(pop)} \\ F_{(q', \gamma')} D_1 \cdots D_N & \delta(q, \gamma) = (q', \text{up}_{\gamma'}) \quad \text{(push)} \end{array} \right. $$

where $B_i \equiv F_{(q_i, \gamma)} y_{i1} \cdots y_{iN}$, $D_i \equiv F_{(i, \gamma)} z_{i1} \cdots z_{iN}$ and

$$ y_{ij} \equiv \begin{cases} x_j & (q_i, \gamma, j) \in R_A \\ \bot & \text{otherwise} \end{cases} \qquad z_{ij} \equiv \begin{cases} x_j & (q', \gamma', i), (i, \gamma, j) \in R_A \\ \bot & \text{otherwise} \end{cases} $$

Because the intended target of the translation is the setting of MHORS, we need to show that, in each of the rules above, every $x_j$ occurs at most once on the right-hand side. This is easy to see for the (pop) and (state change) cases, so it remains to check (branching) and (pushing). We are going to argue that, if linearity were violated, we can actually replace the rhs with $\bot$, because the corresponding configurations would never be reached.

Consider the branching case first and suppose that $x_j$ occurs twice in $\mathfrak{b}B_1 \cdots B_{|\mathfrak{b}|}$. Then we must have $(q_{i_1}, \gamma, j) \in R_A$ and $(q_{i_2}, \gamma, j) \in R_A$ for $i_1 \neq i_2$. Observe that then no configuration of the form $(q, \gamma \Box)$, where $\Box \in (\Gamma^\bullet)^*$, can be reachable from $(q_0, \gamma_0)$, because a run from $(q_0, \gamma_0)$ to $(q, \gamma \Box)$ can be extended (via $(q_{i_1}, \gamma \Box)$ and $(q_{i_2}, \gamma \Box)$ respectively) to two different runs to $(j, \Box)$, which would contradict linearity. Consequently, we can set $F_{(q, \gamma)} x_1 \cdots x_N = \bot$.

Finally, consider the push case and suppose $x_j$ occurs twice in $F_{(q', \gamma')} D_1 \cdots D_N$, i.e. there exist $i_1 \neq i_2$ such that $(q', \gamma', i_1), (i_1, \gamma, j) \in R_A$ and $(q', \gamma', i_2), (i_2, \gamma, j) \in R_A$. We argue that then no configuration of the shape $(q, \gamma \Box)$ is reachable from $(q_0, \gamma_0)$. Indeed, if this were the case, we could extend the run (from $(q_0, \gamma_0)$ to $(q, \gamma \Box)$) with $(q, \gamma \Box) \Rightarrow (q', \gamma' \gamma \Box) \Rightarrow^* (i_k, \gamma \Box) \Rightarrow^* (j, \Box)$ for $k = 1, 2$, i.e. $(j, \Box)$ would be reachable via two runs, contradicting linearity. Consequently, if $x_j$ happens to occur twice, we can replace the rule with $F_{(q, \gamma)} x_1 \cdots x_N = \bot$.

◀