# Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic

Lê Thành Dũng Nguyễn, Cécilia Pradic

► To cite this version:

Lê Thành Dũng Nguyễn, Cécilia Pradic. Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic. 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), Jul 2020, Saarbrücken (virtual conference), Germany. hal-02476219v3

HAL Id: hal-02476219

https://hal.science/hal-02476219v3

Submitted on 13 Feb 2023

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>
# Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic

Lê Thành Dũng (Tito) Nguyễn ID

Laboratoire d'informatique de Paris Nord, Villetaneuse, France
Laboratoire Cogitamus (http://www.cogitamus.fr/indexen.html)
nltd@nguyentito.eu

Cécilia Pradic ID

Department of Computer Science, University of Oxford, United Kingdom

## Abstract

We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages instead. A key ingredient in our approach – that it shares with higher-order model checking – is the use of Church encodings for inputs and outputs. Our result is, to our knowledge, the first use of non-commutativity in implicit computational complexity.

**2012 ACM Subject Classification** Theory of computation → Algebraic language theory; Theory of computation → Linear logic

**Keywords and phrases** Church encodings, ordered linear types, star-free languages

**Related Version** In ICALP'20 proceedings: doi:10.4230/LIPIcs.ICALP.2020.135

**Acknowledgements** The initial trigger for this line of work was twofold: the serendipitous rediscovery of Hillebrand and Kanellakis's theorem by Damiano Mazza, Thomas Seiller and the first author, and Mikołaj Bojańczyk's suggestion to the second author to look into connections between transducers and linear logic. Célia Borlido proposed looking at star-free languages at the Topology, Algebra and Categories in Logic 2019 summer school.

During its long period of gestation, this work benefited from discussions with many other people: Pierre Clairambault, Amina Doumane, Marie Fortin, Jérémy Ledent, Paolo Pistone, Lorenzo Tortora de Falco, Noam Zeilberger and others that we may have forgotten to mention.

We also thank the anonymous reviewers for their constructive feedback, especially for their highly relevant pointers to the literature.

## 1 Introduction

**A type-theoretic implicit automata theory** This paper explores connections between the languages recognized by automata and those definable in certain typed λ-calculi (minimalistic functional programming languages). It is intended to be the first in a series, whose next installments will investigate the functions computable by transducers (automata with output, see e.g. [16, 37]). Insofar as programming language theory is related to proof theory, via the Curry-Howard correspondence, we are therefore trying to *bridge logic and automata*. That said, our work does not fit in the “logics as specification languages” paradigm, exemplified by the equivalence of recognition by finite-state automata and Monadic Second-Order Logic (MSO). One could sum up the difference by analogy with the two main approaches to machine-free complexity: *implicit computational complexity (ICC)* and *descriptive complexity*.
## 2 Aperiodicity in a non-commutative logic

Both aim to characterize complexity classes without reference to a machine model, but the methods of ICC have a more computational flavor.

<table><thead><tr><th>programming paradigm</th><th>declarative</th><th>functional</th></tr></thead><tbody><tr><td>complexity classes</td><td>Descriptive Complexity</td><td>Implicit Computational Complexity</td></tr><tr><td>automata theory</td><td>subsystems of MSO</td><td><b>this paper</b> (and planned sequels)</td></tr></tbody></table>

To our knowledge, very few works have looked at this kind of “type-theoretic” or “proof-theoretic” ICC for automata. Let us mention a few recent papers (that we will discuss further in §7) concerning transducers [13, 10] and multi-head automata [46, 29] and, most importantly, a remarkable result from 1996 that provides our starting point:

**Theorem 1.1** (Hillebrand & Kanellakis [25, Theorem 3.4]). A language $L \subseteq \Sigma^*$ can be defined in the simply typed $\lambda$-calculus by some closed $\lambda$-term of type $\text{Str}_{\Sigma}[A] \to \text{Bool}$ for some type $A$ (that may depend on $L$) if and only if it is a regular language.

Let us explain this statement. We consider a grammar of simple types with a single base type: $A, B ::= o \mid A \to B$, and use the *Church encodings* of booleans and strings:

$$ \text{Bool} = o \to o \to o \qquad \text{Str}_{\Sigma} = (o \to o) \to \dots \to (o \to o) \to o \to o $$

with $|\Sigma|$ arguments of type $(o \to o)$, where $\Sigma$ is a finite alphabet. Moreover, given any other chosen type $A$, one can form the type $\text{Str}_{\Sigma}[A]$ by substituting $A$ for the ground type $o$:

**Notation 1.2.** For types $A$ and $B$, we denote by $B[A]$ the substitution $B\{o := A\}$ of every occurrence of $o$ in $B$ by $A$.

Every closed $\lambda$-term $t$ of type $\text{Str}_{\Sigma}$ can also be seen as a term of type $\text{Str}_{\Sigma}[A]$. (This is a way to simulate a modicum of parametric polymorphism in a monomorphic type system.) It follows that any closed $\lambda$-term of type $\text{Str}_{\Gamma}[A] \to \text{Bool}$ in the simply typed $\lambda$-calculus defines a predicate on strings, i.e. a language $L \subseteq \Sigma^*$.

Although little-known<fnref n="1" />, Hillebrand and Kanellakis’s theorem should not be surprising in retrospect: there are strong connections between Church encodings and automata (see e.g. [45, 48, 35]), that have been exploited in particular in *higher-order model checking* for the past 15 years [2, 38, 26, 22, 24, 49]. This is not a mere contrivance: these encodings have been a canonical data representation for $\lambda$-calculi for much longer<fnref n="2" />.

**Star-free languages** We would like to extend this result by characterizing strict subclasses of regular languages, the most famous being the *star-free languages*. Recall that the canonicity of the class of regular languages is firmly established by its various definitions: regular expressions, finite automata, definability in MSO and the algebraic characterization.

**Theorem 1.3** (cf. [44, §II.2.]) A language $L \subseteq \Sigma^*$ is regular if and only if for some finite monoid $M$, some subset $P \subseteq M$ and some monoid morphism $\varphi \in \text{Hom}(\Sigma^*, M)$, $L = \varphi^{-1}(P)$.

Similarly, the seminal work of Schützenberger, Petrone, McNaughton and Papert in the 1960s (see [47] for a historical discussion) has led to many equivalent definitions for star-free languages, with the algebraic notion of *aperiodicity* playing a key role:

<footnote n="1">¹ See e.g. Damiano Mazza’s answer to this MathOverflow question: https://mathoverflow.net/q/296879</footnote>

<footnote n="2">² They were introduced for booleans and integers by Church in the 1930s, and later generalized by Böhm and Berarducci [12], see also http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html. (Similar ideas appear around the same time in [32].) As for the refined encodings with linear types that we use later, they already appear in Girard’s founding paper on linear logic [18, §5.3.3].</footnote>
**► Definition 1.4.** A monoid $M$ is aperiodic when any sequence of iterated powers is eventually constant, i.e. for any $x \in M$ there exists an exponent $n \in \mathbb{N}$ such that $x^n = x^{n+1}$.

**► Theorem 1.5** (cf. [47]). For a language $L \subseteq \Sigma^*$, the following conditions are equivalent:

- $L$ is defined by some star-free regular expression: $E, E' ::= \emptyset | \{a\} | E \cup E' | E \cdot E' | E^c$ where a can be any letter in $\Sigma$ and $E^c$ denotes the complement of $E$ ($[E^c] = \Sigma^* \setminus [E]$);

- $L = \varphi^{-1}(P)$ for some finite and aperiodic monoid $M$, some subset $P \subseteq M$ and some monoid morphism $\varphi \in \text{Hom}(\Sigma^*, M)$;

- $L$ is recognized by a deterministic finite automaton whose transition monoid is aperiodic;

- $L$ is definable in first-order logic.

Attempting to capture star-free languages in a $\lambda$-calculus presents a serious methodological challenge: they form a strict subclass of uniform $\mathcal{AC}^0$, and, as far as we know, type-theoretic ICC has never managed before to characterize complexity classes as small as this.

**Non-commutative affine types** Monoids appear in typed $\lambda$-calculi when one looks at the functions from a type $A$ to itself, i.e. at the (closed) terms of type $A \to A$. At first glance, it seems difficult indeed to enforce the aperiodicity of such monoids via a type system. For instance, one needs to rule out **not** = $\lambda b. \lambda x. \lambda y. by x : \mathbf{Bool} \to \mathbf{Bool}$ since it “has period two”: its iteration yields the sequence (modulo $\beta\eta$-conversion) **not**, $id$, **not**, $id$, ... (where $id = \lambda b. \ \lambda$) which is not eventually constant. Observe that **not** essentially exchanges the two arguments of $b$; to exclude it, we are therefore led to require functions to use their arguments in the same order that they are given in.

It is well-known that in order to make such a non-commutative $\lambda$-calculus work – in particular to ensure that non-commutative $\lambda$-terms are closed under $\beta$-reduction – one needs to make the type system *affine*, that is, to restrict the duplication of data. This is achieved by considering a type system based on Girard's linear<fnref n="3" /> logic [18], a system whose “resource-sensitive” nature has been previously exploited in ICC [21, 20]. Not coincidentally, the theme of non-commutativity first appeared in a form of linear logic *ante litteram*, namely the Lambek calculus [30], and resurfaced shortly after the official birth of linear logic: it is already mentioned by Girard in a 1987 colloquium [19].

We shall therefore introduce and use a variant of Polakow and Pfenning's Intuitionistic Non-Commutative Linear Logic [39, 40], making a distinction between two kinds of function arrows: $A \to B$ and $A \to B$ are, respectively, the types of affine functions and non-affine functions from $A$ to $B$. Accordingly:

**► Definition 1.6.** A type is said to be purely affine if it does not contain the '$\to$' connective.

In our system that we call the $\lambda\varphi$-calculus, the types of Church encodings become

$$ \mathbf{Bool} = o \to o \to o \qquad \mathbf{Str}_{\Sigma} = (o \to o) \to \dots \to (o \to o) \to (o \to o) $$

where $\mathbf{Str}_{\Sigma}$ has $|\Sigma|$ arguments<fnref n="4" /> of type $(o \to o)$. Setting $\mathbf{true} = \lambda^{\circ}x. \lambda^{\circ}y. x : \mathbf{Bool}$ and $\mathbf{false} = \lambda^{\circ}x. \lambda^{\circ}y. y : \mathbf{Bool}$ for the rest of the paper, we can now state our main result:

**► Theorem 1.7.** A language $L \subseteq \Sigma^*$ is star-free if and only if it can be defined by a closed $\lambda\varphi$-term of type $\mathbf{Str}_{\Sigma}[A] \to \mathbf{Bool}$ for some purely affine type $A$ (that may depend on $L$).

<footnote n="3">³ The main difference between so-called linear and affine type systems is that the latter allow weakening, that is, to not use some argument. Typically, $\lambda x. \lambda y. x$ is affine but not linear while $\lambda x. x x$ is neither linear nor affine. The type system that we use in this paper is affine, not strictly linear.</footnote>

<footnote n="4">⁴ $o \to o$ occurs $|\Sigma| + 1$ times in $\mathbf{Str}_{\Sigma}: |\Sigma|$ arguments plus the output.</footnote>
4 Aperiodicity in a non-commutative logic

However, if we use the commutative variant of the $\lambda\varphi$-calculus instead, then what we get is the class of regular languages (Theorem 5.1), just as in Hillebrand and Kanellakis's theorem.

As far as we know, non-commutative type systems have never been applied to implicit complexity before (but they have been used to control the expressivity of a domain-specific programming language [27]). Previous works indeed tend to see non-commutative $\lambda$-terms (or proof nets) as static objects, and to focus on their topological aspects (e.g. [6, 51, 36]), though there is another tradition relating self-dual non-commutativity to process algebras<fnref n="5" /> [41, 23].

**Proof strategy** As usual in implicit computational complexity, the proof of Theorem 1.7 consists of a soundness part – “every $\lambda\varphi$-definable language is star-free” – and an extensional completeness part – the converse implication. In our case, soundness is a corollary of the following property of the purely affine fragment of the $\lambda\varphi$-calculus – what one might call the planar<fnref n="6" /> affine $\lambda$-calculus (cf. [1, 51]):

**Theorem 1.8** (proved in §3). For any purely affine type A, the set of closed $\lambda\varphi$-terms of type $A \to A$, quotiented by $\beta\eta$-convertibility and endowed with function composition ($f \circ g = \lambda^\circ x. f(gx)$), is a finite and aperiodic monoid.

Extensional completeness turns out here to be somewhat deeper than the “programming exercise of limited theoretical interest” [34, p. 137] that one generally finds in ICC. Indeed, we have only managed to encode star-free languages in the $\lambda\varphi$-calculus by relying on a powerful tool from semigroup theory: the *Krohn–Rhodes decomposition* [28].

**Plan of the paper** After having defined the $\lambda\varphi$-calculus in §2, we prove Theorem 1.7: soundness is treated in §3 and extensional completeness in §4. Then we discuss the analogous results for the commutative variant of the $\lambda\varphi$-calculus and its extension with additives (§5), our plans for the next papers in the series (§6) and finally some related work (§7).

**Prerequisites** We assume that the reader is familiar with the basics of $\lambda$-calculi and type systems, but require no prior knowledge of automata theory. This choice is motivated by the impression that it is more difficult to introduce the former than the latter in a limited number of pages. Nevertheless, we hope that our results will be of interest to both communities.

## 2 Preliminaries: the $\lambda\varphi$-calculus and Church encodings

The terms and types of the $\lambda\varphi$-calculus are defined by the respective grammars

$$A, B ::= o \mid A \to B \mid A \to B \quad t, u ::= x \mid tu \mid \lambda^\to x.t \mid \lambda^\circ x.t$$

As always, the $\lambda\varphi$ terms are identified up to $\alpha$-equivalence (both $\lambda^\to$ and $\lambda^\circ$ are binders). There are two rules for $\beta$-reduction (closed under contexts)

$$(\lambda^\to x.t) u \to_\beta t\{x := u\} \quad (\lambda^\circ x.t) u \to_\beta t\{x := u\}$$

and the remaining conversion rules are the expected $\eta$-reduction/$\eta$-expansion rules.

<footnote n="5">⁵ This connection with the sequential composition of processes can be seen as a sort of embodiment of Girard's slogan "time is the contents of non-commutative linear logic" [19, IV.6]. But generally, these works follow a "proof search as computation" paradigm (logic programming) rather than "normalization as computation" (functional programming).</footnote>

<footnote n="6">⁶ Hence our choice of name: the "Weierstraß P" character '$\varphi$' in '$\lambda\varphi$' stands for "planar".</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 1 The typing rules of the $\lambda\wp$-calculus (see Appendix C for examples of derivations).</figcaption></figure>

The typing judgements make use of dual contexts (a common feature originating in [7]): they are of the form $\Gamma | \Delta \vdash t : A$ where $t$ is a term, $A$ is a type, $\Gamma$ is a set of bindings of the form $x : B$ ($x$ being a variable and $B$ a type), and $\Delta$ is an *ordered list* of bindings – this order is essential for non-commutativity. The typing rules are given in Figure 1, where $\Delta \cdot \Delta'$ denotes the *concatenation of the ordered lists* $\Delta$ and $\Delta'$. For both $\Gamma, \Gamma', \dots$ and $\Delta, \Delta', \dots$ we require each variable to appear at most once on the left of a colon.

► **Remark 2.1.** Unlike Polakow and Pfenning’s system [39, 40], the $\lambda\wp$-calculus:

- contains two function types instead of four<fnref n="7" />, with the top two rows of Figure 1 corresponding almost exactly<fnref n="8" /> to the rules given for those connectives in [39];

- is affine instead of linear, as expressed by the “ordered weakening” rule at the bottom of Figure 1 – this seems important to get enough expressive power for our purposes<fnref n="9" />.

► **Remark 2.2.** Morally, the non-affine variables “commute with everything”. More formally, one could translate the $\lambda\wp$-calculus into a non-commutative version of Intuitionistic Affine Logic whose exponential modality ‘!’ incorporates the customary rules (see e.g. [50])

$$ \frac{\Gamma, !A, B, \Delta \vdash C}{\Gamma, B, !A, \Delta \vdash C} \qquad \frac{\Gamma, B, !A, \Delta \vdash C}{\Gamma, !A, B, \Delta \vdash C} $$

► **Proposition 2.3.** *The $\lambda\wp$-calculus enjoys subject reduction and admits normal forms (that is, every well-typed $\lambda\wp$-term is convertible to a $\beta$-normal $\eta$-long one).*

**Proof sketch.** This is routine: subject reduction follows from a case analysis, while the fact that the simply typed $\lambda$-calculus has normal forms entails that the $\lambda\wp$-calculus also does (the obvious translation preserves the $\beta$-reduction and the $\eta$-expansion relations). ◀

We have already seen the type $\text{Str}_{\Sigma} = (o \to o) \to \dots \to (o \to o) \to (o \to o)$ of Church-encoded strings in the introduction. Let us now introduce the term-level encodings:

► **Definition 2.4.** Let $\Sigma$ be a finite alphabet, $w = w[1] \dots w[n] \in \Sigma^*$ be a string, and for each $c \in \Sigma$, let $t_c$ be a $\lambda\wp$-term (on which the next proposition will add typing assumptions). We abbreviate $(t_c)_{c \in \Sigma}$ as $\vec{t}_{\Sigma}$, and define the $\lambda\wp$-term $w^{\dagger}(\vec{t}_{\Sigma}) = \lambda^{\circ}x.t_{w[1]}(\dots(t_{w[n]}x)\dots)$.

<footnote n="7">⁷ Our ‘$\to$’ and ‘$\to$’ are called “intuitionistic functions” and “right ordered functions” in [39]; we have no counterpart for the “linear [commutative] functions” and “left ordered functions” in the $\lambda\wp$-calculus.</footnote>

<footnote n="8">⁸ The only difference is that we drop the linear commutative context.</footnote>

<footnote n="9">⁹ Usually, the linear/affine distinction does not matter for implicit computational complexity if we allow collecting the garbage produced during the computation in a designated part of the output, as in e.g. [31]. But non-commutativity obstructs the free movement of garbage.</footnote>
6 Aperiodicity in a non-commutative logic

Given a total order $c_1 < \dots < c_{|\Sigma|}$ on the alphabet $\Sigma = \{c_1, \dots, c_{|\Sigma|}\}$, the Church encoding of any string $w \in \Sigma^*$ is $\bar{w} = \lambda^\neg f_{c_1} \dots \lambda^\neg f_{c_{|\Sigma|}} \cdot w^\dagger(\vec{f}_\Sigma)$.

This is simpler than the notation might suggest: as an example, for $\Sigma = \{a, b\}$ with $a < b$, $\overline{baa} = \lambda^\neg f_a$. $\lambda^\neg f_b$. $\lambda^\circ x$. $f_b(f_a(f_a x))$. Our choice of presentation is meant to stress the role of the *open* subterm $(baa)^\dagger(\vec{f}_{\{a,b\}}) = \lambda^\circ x$. $f_b(f_a(f_a x))$, cf. Remark 2.9.

We now summarize the classical properties of the Church encoding of strings.

**Proposition 2.5.** We reuse the notations of the above definition.

- Assume that there is a type $A$ and a typing context $\Gamma \mid \Delta$ such that for all $c \in \Sigma$, $\Gamma \mid \Delta \vdash t_c : A \to A$. Then $\Gamma \mid \Delta \vdash w^\dagger(\vec{t}_\Sigma) : A \to A$.

- In particular, $\{f_c : o \to o \mid c \in \Sigma\} \mid \emptyset \vdash w^\dagger(\vec{f}_\Sigma) : o \to o$ for any variables $(f_c)_{c \in \Sigma}$.

- Furthermore, in the case of variables, $w \in \Sigma^* \mapsto w^\dagger(\vec{f}_\Sigma)$ is in fact a bijection between the strings over $\Sigma$ and the $\lambda\varphi$-terms $u$ such that $\{f_c : o \to o \mid c \in \Sigma\} \mid \emptyset \vdash u : o \to o$ and considered up to $\beta\eta$-conversion$^{10}$.

- It follows from the above that $w \in \Sigma^* \mapsto \bar{w}$ is a bijection from $\Sigma^*$ to the set of closed $\lambda\varphi$-terms of type $\text{Str}_\Sigma$ modulo $\beta\eta$.

- Finally, with the assumptions on $t_c$ of the first item, we have $\bar{w} t_{c_1} \dots t_{c_{|\Sigma|}} \to_{\beta}^* w^\dagger(\vec{t}_\Sigma)$.

**Example 2.6.** Given two closed $\lambda\varphi$-terms $t_a, t_b : \text{Bool} \to \text{Bool}$, one can define the term $g = \lambda^\circ s. s t_a t_b \text{ false} : \text{Str}_{\{a,b\}}[\text{Bool}] \to \text{Bool}$. Then for any $w = w[1] \dots w[n] \in \{a,b\}^*$, we have $g \bar{w} \to_{\beta}^* w^\dagger(\vec{t}_{\{a,b\}}) \text{ false} \to_{\beta}^* t_{w[1]}(\dots (t_{w[n]} \text{ false}))$.

- For $t_a = \lambda^\circ x$. true and $t_b = \lambda^\circ x$. x, $g$ decides the language of words in $\{a,b\}^*$ that contain at least one $a$; this language is indeed star-free as it can be expressed as $\emptyset^c a \emptyset^c$.

- Coming back to a point raised in the introduction, if negation were definable by a $\lambda\varphi$-term $\text{not} : \text{Bool} \to \text{Bool}$, then for $t_a = t_b = \text{not}$, the language decided by $g$ would consist of words of odd length: a standard example of regular language that is not star-free.

**Remark 2.7.** Actually, the $\lambda\varphi$-term $\text{not}' : \lambda^\circ b$. $b \text{ false true} : \text{Bool}[\text{Bool}] \to \text{Bool}$ does "define negation". A point of utmost importance is that because of the heterogeneity of the input and output types, this term does not contradict Theorem 1.8 and *cannot be iterated by a Church-encoded string*. Monomorphism is therefore crucial for us: if our type system had actual polymorphism, one could give $\text{not}'$ the type $(\forall \alpha. \text{Bool}[\alpha]) \to (\forall \alpha. \text{Bool}[\alpha])$, whose input and output types are equal, and then the words of odd length would be $\lambda\varphi$-definable.

An analogous phenomenon in the simply typed $\lambda$-calculus is that one can define $n \mapsto 2^n$ on the type of Church numerals Nat by a term of type $\text{Nat}[o \to o] \to \text{Nat}$, but not by a term of type $\text{Nat} \to \text{Nat}$ (since iterating it would give rise to a tower of exponentials of variable height, which is known to be inexpressible by any $\text{Nat}[A] \to \text{Nat}$).

Yet our ersatz of polymorphism still allows for some form of compositionality that will prove useful in several places in §4 (the proof may be found in Appendix B):

**Lemma 2.8.** If $\vdash t : A[T] \to B$ and $\vdash u : B[U] \to C$, then $\vdash \lambda^\circ x. u (tx) : A[T[U]] \to C$.

**Remark 2.9.** One final observation on Church encodings: when the context $\Gamma$ of non-affine variables contains $f_c : o \to o$ for each $c \in \Sigma$, then any string $w \in \Sigma^*$ can be represented as the open $\lambda\varphi$-term $\Gamma \mid \dots \vdash w^\dagger(\vec{f}_\Sigma) : o \to o$ in that context, and such strings can even be concatenated by function composition. The point is that this gives us a kind of *purely affine type of strings*, which will allow us in §4.2 to encode sequential transducers as $\lambda\varphi$-terms of type $\text{Str}_\Sigma[A] \to \text{Str}_\Pi$ for some purely affine type $A$ (compare Theorem 1.7).

<footnote n="10">10 $\eta$-conversion is necessary to identify $\lambda^\neg f. f : \text{Str}_{\{a\}}$ with $\bar{a} = \lambda^\neg f. \lambda^\circ x. f x : \text{Str}_{\{a\}}$.</footnote>
### 3 Proof of soundness

As stated in the introduction, the soundness part of our main Theorem 1.7 will follow from Theorem 1.8, so we start this section by proving the latter. First, the monoid structure on the closed $\lambda\wp$-terms of any type $A \to A$ can be verified routinely: both $(f \circ g) \circ h$ and $f \circ (g \circ h)$ $\beta$-reduce to $\lambda^\circ x. f(g(hx))$, and $\lambda^\circ x.x$ provides the identity element. The finiteness of this monoid for $A$ purely affine comes from a slightly more general statement:

**Proposition 3.1.** For any purely affine type $B$, there are finitely many $\beta\eta$-equivalence classes of closed $\lambda\wp$-terms of type $B$.

*Proof.* This is a well-known property of affine type systems: here, non-commutativity plays no role. We provide a proof in Appendix B. ◀

The substantial part of Theorem 1.8 is the *aperiodicity* of this monoid. It is here that non-commutativity comes into play. Morally, it is a kind of monotonicity condition that $\lambda\wp$-terms obey. A first idea would therefore be to seek to exploit the fact that the monoid of monotone functions on an ordered set is *aperiodic*. What we end up using is closely related:

**Lemma 3.2.** For any $k \in \mathbb{N}$, the monoid of partial non-decreasing functions from $\{1, \dots, k\}$ to itself (endowed with usual function composition) is *aperiodic*.

*Proof.* Let $f: \{1, \dots, k\} \to \{1, \dots, k\}$ be non-decreasing. For any $i \in \{1, \dots, k\}$, the sequence $(f^n(i))_{n \in \mathbb{N}}$ is either non-increasing or non-decreasing as long as it is defined (depending on whether $i \ge f(i)$ or $i \le f(i)$); so at some $n = N_i$, either it becomes undefined or it reaches a fixed point of $f$. By taking $N = \max_{1 \le i \le k} N_i$, we have $f^N = f^{N+1}$. ◀

This underlies the proof of the key lemma below, that allows one to reduce the aperiodicity of some $t: A \to A$ to the aperiodicity of $\lambda\wp$-terms at smaller types.

**Notation 3.3.** $\Delta \vdash t: A$ is an abbreviation for $\emptyset | \Delta \vdash t: A$ (indeed, the context of non-affine variables will be generally empty in our proof).

**Notation 3.4.** Let $u_1, \dots, u_k$ and $v_1, \dots, v_l$ be $\lambda\wp$-terms. The notation $\vec{v}[\vec{y} := \vec{u}]$ denotes the componentwise parallel substitution $(v_i[y_1 := u_1, \dots, y_k := u_k])_{1 \le i \le l}$.

**Lemma 3.5.** Let $t = \lambda^\circ x. \lambda^\circ y_1. \dots \lambda^\circ y_m. x u_1 \dots u_k$ be a well-typed closed $\lambda\wp$-term of type $A \to A$ in $\eta$-long form, so that $x: A$, $y_1: B_1$, ..., $y_k: B_k \vdash x u_1 \dots u_k: o$ with $A = B_1 \to \dots \to B_k \to o$. Then:

- $t^n = t \circ \dots \circ t$ (n times) is $\beta$-convertible to $\lambda^\circ x. \lambda^\circ y_1. \dots \lambda^\circ y_k. x u_1^{(n)} \dots u_k^{(n)}$ where $\vec{u}^{(0)} = (y_1, \dots, y_k)$, $\vec{u}^{(n+1)} = \vec{u}^{(n)}[\vec{y} := \vec{u}]$;

- For large enough $n \in \mathbb{N}$, each $u_i^{(n+1)}$ depends only on $u_i^{(n)}$ for the same $i \in \{1, \dots, k\}$. More precisely, there exists $N \in \mathbb{N}$ such that for all $i \in \{1, \dots, k\}$ there exists a well-typed closed $\lambda\wp$-term $t'_i: B_i \to B_i$ such that for all $n \ge N$, $u_i^{(n+1)} = t'_i u_i^{(n)}$.

*Proof.* The first item is established by induction: abbreviating $\lambda^\circ y_1. \dots \lambda^\circ y_k$ as $\lambda^\circ \vec{y}_k$,

$$ 
\begin{align*}
t \circ (\lambda^\circ x. \lambda^\circ \vec{y}. x u_1^{(n)} \dots u_k^{(n)}) &= \beta \lambda^\circ x. \lambda^\circ \vec{y}. (\lambda^\circ \vec{y}. x u_1^{(n)} \dots u_k^{(n)}) u_1 \dots u_k \\
&= \beta \lambda^\circ x. \lambda^\circ \vec{y}. x (u_1^{(n)}[\vec{y} := \vec{u}]) \dots u_k^{(n)}([\vec{y} := \vec{u}])
\end{align*}
$$

(We invite to reader to reproduce the full computation to check that no spurious capture of free variables happens.)
8 Aperiodicity in a non-commutative logic

For the second item, let us define the partial function $\mu_{\vec{u}} : \{1, \dots, k\} \to \{1, \dots, k\}$
by $\mu_{\vec{u}}(i) = j \iff y_i \in \text{FV}(u_j)$. (FV($u$) denotes the set of free variables of $u$.) The
relation on the right-hand side of the equivalence is indeed a partial function because of
the affineness of $t = \lambda^\circ x. \lambda^\circ y_1. \dots \lambda^\circ y_k. z \, u_1 \dots u_k$. One can also show that for all $n \in \mathbb{N}$,
$\text{FV}(u_i^{(n)}) = \{y_j \mid (\mu_{\vec{u}})^n(j) = i\}$.

As a consequence of non-commutativity, $\mu_{\vec{u}}$ is non-decreasing. This is because for the
typing judgment on $x u_1 \dots u_k$ to hold, there must exist $\Delta_1, \dots, \Delta_k$ such that:

- for all $j \in \{1, \dots, k\}$, $\Delta_j \vdash u_j$ and $\forall i$, $y_i \in \text{FV}(u_j) \iff (y_i : B_i) \in \Delta_j$;

- $\Delta_1 \cdots \Delta_k$ is an ordered subsequence of $(y_1 : B_1) \cdots (y_k : B_k)$.

Therefore, by Lemma 3.2, there exists $N \in \mathbb{N}$ such that $(\mu_{\vec{u}})^N = (\mu_{\vec{u}})^{N+1}$.

Next, let $i \in \{1, \dots, k\}$. We may reformulate our goal as finding $t_i^i : B_i \to B_i$ such that
$t_i^i u_i^{(N+n)} = \beta \eta u_i^{(N+n+1)}$ for all $n \in \mathbb{N}$. The simple case is when $i \notin (\mu_{\vec{u}})^N(\{1, \dots, k\})$: $u_i^{(N)}$
has no free variables, so $u_i^{(N+1)} = u_i^{(N)}[\vec{y} := \vec{u}] = u_i^{(N)}$: we may then take $t_i^i = \lambda^\circ z. z$. For
the remainder of the proof we assume otherwise, that is, we take $i$ in the range of $(\mu_{\vec{u}})^N$.

First, $\vec{u}^{(n+1)} = \vec{u}[\vec{y} := \vec{u}^{(n)}]$ because parallel substitution is associative$^{11}$. Thus,

$$
\forall n \in \mathbb{N}, u_i^{(N+n+1)} = u_i \left[ y_j := u_j^{(N+n)} \text{ for } j \in \{1, \dots, k\} \text{ such that } \mu_{\vec{u}}(j) = i \right]
$$

Any $j \in \{1, \dots, k\} \setminus \{i\}$ such that $\mu_{\vec{u}}(j) = i$ is not a fixed point of $\mu_{\vec{u}}$, and therefore is not in
the range of $(\mu_{\vec{u}})^N$ since $(\mu_{\vec{u}})^N = (\mu_{\vec{u}})^{N+1} = \mu_{\vec{u}} \circ (\mu_{\vec{u}})^N$. By the simple case already treated,
we then have $u_j^{(N+n)} = u_j^{(N)}$. This allows us to write the above equation as

$$
u_i^{(N+n+1)} = r_i[y_i := u_i^{(N+n)}] \quad \text{where} \quad r_i = u_i \left[ y_j := u_j^{(N)} \text{ for } j \neq i \text{ s.t. } \mu_{\vec{u}}(j) = i \right]
$$

Using $\beta$-conversion, $u_i^{(N+n+1)} =_{\beta} (\lambda^\circ y_i \cdot r_i) u_i^{(N+n)}$. We conclude by setting $t_i^i = (\lambda^\circ y_i \cdot r_i)$.
It is clear that this $\lambda^\circ\varphi$-term is closed, but one should check that it is well-typed; to do so,
one convenient observation is that the $u_j^{(N)}$ are closed (because $j \notin (\mu_{\vec{u}})^N(\{1, \dots, k\})$) and
well-typed (as closed subterms of a reduct of the $N$-fold composition $t^N$). $\quad$

The remainder of the proof of Theorem 1.8 is essentially bureaucratic.

**Proof of the aperiodicity part of Theorem 1.8.** Let $t : A \to A$; our goal is to show that the sequence $t^n = t \circ \dots \circ t$ is eventually constant modulo $\beta\eta$. We shall do so by induction on the size of $A$. The type $A$ is purely affine by assumption, and can therefore be written as $B_1 \to \dots \to B_m \to o$ where the $B_i$ are also purely affine for $i \in \{1, \dots, m\}$. The base case $m=0$ being trivial, we assume $m \ge 1$. In this case, by Proposition 2.3, $t$ has an $\eta$-long $\beta$-normal form $t = \lambda^\circ x. \lambda^\circ y_1. \dots \lambda^\circ y_m. z \, u_1 \dots u_k$ where $z$ is a variable. There are two cases:

- $z = y_i$ for some $i$. Then $(y_i : B_i) \cdot \Delta \vdash z u_1 \dots u_k$ by application rule (we omit the non-affine context $\Gamma$ which will always be empty during this proof). The abstraction rule only allows introducing $\lambda^\circ y_i$ when $(y_i : B_i)$ is on the right, so by then $\Delta$ must have been entirely emptied out by previous abstractions. This means that $\lambda^\circ y_i. \dots \lambda^\circ y_m. z \, u_1 \dots u_k$ is a closed term, so in particular it contains no free occurrence of $x$: $t$ is a constant function from $A$ to $A$. So the sequence of iterations stabilizes from $n=1$.

- $z = x$, which entails $k = m$ since the variable $x$ is of type $A = B_1 \to \dots \to B_m \to o$ and we must have $x : A$, $y_1 : B_1$, \dots, $y_m : B_m \vdash x \, u_1 \dots u_k : o$. Lemma 3.5 gives us closed $\lambda^\circ\varphi$-terms $t_i^i : B_i \to B_i$ ($i \in \{1, \dots, k\}$) whose iterates eventually determine those of $t$. Since the type $B_i$ has size strictly smaller than $A$, the induction hypothesis applies: each $((t_i^i)^n)_{n \in \mathbb{N}}$ is eventually constant modulo $\beta\eta$. Therefore, this is also the case for $t$. $\quad$

<footnote n="11">11 More precisely, $(t_1[\vec{x} := t_2])[\vec{y} := t_3] = t_1[\vec{x} := t_2[\vec{y} := t_3]]$ when $\vec{y} \cap (\text{FV}(t_1) \setminus \vec{x}) = \emptyset$.</footnote>
Let us now apply Theorem 1.8 to the $\lambda\wp$-terms defining languages.

**Lemma 3.6.** Let $\Sigma = \{c_1, \dots, c_{|\Sigma|}\}$ be a finite alphabet, A be a purely affine type and $t: \text{Str}_{\Sigma}[A] \to \text{Bool}$ be a closed $\lambda\wp$-term. Then there exist some closed $\lambda\wp$-terms $g_c: A \to A$ for $c \in \Gamma$ and $h: (A \to A) \to \text{Bool}$ such that $t =_{\beta\eta} \lambda^\circ s.h (s g_{c_1} \dots g_{c_{|\Sigma|}})$.

**Proof.** By inspection of the normal form of $t$, see Appendix B.

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

Reusing the notations of this lemma, let us define $\varphi : \Sigma^* \to \{v \mid v : A \to A\} =_{\beta\eta} A$ to be the monoid morphism such that $\varphi(c) = g_c$ for $c \in \Sigma$. Then for all $w \in \Sigma^*$, $\varphi(w) = w^\dagger(\tilde{g}_\Sigma)$ (in the quotient): by a similar computation than for $f \circ (g \circ h) =_{\beta\eta} (f \circ g) \circ h$, we have $g_{w[1]} \circ \dots \circ g_{w[n]} \to_{\beta} w^\dagger(\tilde{g}_\Sigma)$. Therefore, by Proposition 2.5, $\varphi^{-1}(\{v \mid hv =_{\beta\eta} \text{true}\})$ is none other than the language defined by the $t: \text{Str}_{\Sigma}[A] \to \text{Bool}$ in the lemma. Thus, $L$ fits the second definition of star-free languages given in Theorem 1.5: indeed, the codomain of $\varphi$ is finite and aperiodic by Theorem 1.8. This proves the soundness part of Theorem 1.7.

# 4 Expressiveness of the $\lambda\wp$-calculus

We now turn to the extensional completeness part in Theorem 1.7: our goal is to construct, for any star-free language, a closed $\lambda\wp$-term of type $\text{Str}_{\Sigma}[A] \to \text{Bool}$ (for some purely affine $A$) that defines this language. To do so, the most convenient way that we have found is to take a detour through automata that compute an output string instead of a single bit (acceptance/rejection). We will recall the notion of *aperiodic sequential function* (Definition 4.4), and then establish that:

**Theorem 4.1.** Any aperiodic sequential function $\Sigma^* \to \Pi^*$ can be expressed by a $\lambda\wp$-term of type $\text{Str}_{\Sigma}[A] \to \text{Str}_{\Pi}$ for some purely affine type $A$.

The advantage of working with this class of functions is that they can be assembled from small “building blocks” by function composition, as the *Krohn–Rhodes decomposition* (Theorem 4.8) tells us. Our proof strategy for the above theorem will consist in encoding these blocks (Lemma 4.10) and composing them together (as a special case of Lemma 2.8).

To deduce the desired result, we rely on two lemmas (proved in Appendix B):

**Lemma 4.2.** If a language $L \subseteq \Sigma^*$ is star-free, then its (string-valued) indicator function $\chi_L : \Sigma^* \to \{1\}^*$, defined by $\chi_L(w) = 1$ if $w \in L$ and $\chi_L(w) = \varepsilon$ otherwise, is aperiodic sequential.

**Lemma 4.3.** There exists a $\lambda\wp$-term nonempty : $\text{Str}_{\{1\}}[\text{Bool}] \to \text{Bool}$ that tests whether its input string is non-empty.

Let $L$ be a star-free language. Combining Lemma 4.2 and Theorem 4.1, $\chi_L$ is definable by some $\lambda\wp$-term $\text{indic}_L : \text{Str}_{\Sigma}[A] \to \text{Str}_{\{1\}}$ where $A$ is purely affine. To compose this with the non-emptiness test of Lemma 4.3, we use Lemma 2.8 again: the $\lambda\wp$-term $t_L = \lambda^\circ x. \text{nonempty} (\text{indic}_L x) : \text{Str}_{\Sigma}[A[\text{Bool}]] \to \text{Bool}$ defines $L$. Since $A$ and $\text{Bool}$ are purely affine, so is $A[\text{Bool}]$: we just deduced extensional completeness from Theorem 4.1. Proving the latter is the goal of the rest of this section.

## 4.1 Reminders on automata theory

Sequential transducers are among the simplest models of automata with output. They are deterministic finite automata which can append a word to their output at each transition, and at the end, they can add a suffix to the output depending on the final state. The definition is classical; a possible reference is [44, Chapter V].
<figure><img src="image_4.png" /><figcaption>■ **Figure 2** A schematic representation of a sequential transducer whose formal definition is $Q = \{q_a, q_b\}$, $\delta(q, a) = (q_a, a)$ and $\delta(q, b) = (q_b, bb)$ for $q \in Q$, $q_I = q_a$, $F(q_a) = ab$ and $F(q_b) = bbb$.</figcaption></figure>

**Definition 4.4.** A sequential transducer with input alphabet $\Sigma$ and output alphabet $\Pi$ consists of a set of states $Q$, a transition function $\delta: Q \times \Sigma \to Q \times \Pi^*$, an initial state $q_I \in Q$, and a final output function $F: Q \to \Pi^*$. We abbreviate $\delta_{\text{st}} = \pi_1 \circ \delta$ and $\delta_{\text{out}} = \pi_2 \circ \delta$, where $\pi_i: X_1 \times X_2 \to X_i$ is the $i$-th projection of the product $(i \in \{1, 2\})$.

Given an input string $w = w[1] \dots w[n] \in \Sigma^*$, the run of the transducer over $w$ is the sequence of states $q_0 = q_I$, $q_1 = \delta_{\text{st}}(q_0, w[1])$, \dots, $q_n = \delta_{\text{st}}(q_{n-1}, w[n])$. Its output is obtained as the concatenation $\delta_{\text{out}}(q_0, w[1]) \dots \delta_{\text{out}}(q_{n-1}, w[n]) \cdot F(q_n)$.

A sequential function is a function $\Sigma^* \to \Pi^*$ computed as described above by some sequential transducer.

**Definition 4.5.** The transition monoid of a sequential transducer is the submonoid of $Q \to Q$ (endowed with reverse function composition: $fg = g \circ f$) generated by the maps $\{\delta_{\text{st}}(-, c) | c \in \Sigma\}$ (where $\delta_{\text{st}}(-, c)$ stands for $q \mapsto \delta_{\text{st}}(q, c)$).

A sequential transducer is said to be aperiodic when its transition monoid is aperiodic. A function that can be computed by such a transducer is called an aperiodic sequential function.

**Example 4.6.** The transducer in Figure 2 computes $f: w \in \{a, b\}^* \mapsto a \cdot \psi(w) \cdot b$ where $\psi$ is the monoid morphism that doubles every $b$: $\psi(a) = a$ and $\psi(b) = bb$. Its transition monoid $T$ is generated by $G = \{(\delta_{\text{st}}(-, a): q \mapsto q_a), (\delta_{\text{st}}(-, b): q \mapsto q_b)\}$; one can verify that $T = G \cup \{\text{id}\}$ and therefore $\forall h \in T, h \circ h = h$. Thus, $f$ is an aperiodic sequential function.

**Remark 4.7.** The converse to Lemma 4.2 is also true; more generally, the preimage of a star-free language by an aperiodic sequential function is star-free, and the preimage of a regular language is regular. But we will not need this here.

**Theorem 4.8 (Krohn–Rhodes decomposition, aperiodic case, cf. Appendix A).** Any aperiodic sequential function $f: \Sigma^* \to \Pi^*$ can be realized as a composition $f = f_1 \circ \dots \circ f_n$ (with $f_i: \Xi_i^* \to \Xi_{i-1}^*$, $\Xi_0 = \Pi$ and $\Xi_n = \Sigma$) where each function $f_i$ is computed by some aperiodic sequential transducer with 2 states.

Figure 2 gives an example of aperiodic transducer with two states.

**Remark 4.9.** This is not the standard way to state this theorem, though one may find it in the literature, usually without proof (e.g. [10, §1.1]); see [8] for a tutorial containing a proof sketch of this version. In Appendix A, we show how Theorem 4.8 follows from the more usual statement on wreath products of monoid actions.

## 4.2 Encoding aperiodic sequential transducers

Thanks to the Krohn–Rhodes decomposition and to the fact that the string functions definable in the $\lambda\varphi$-calculus (as specified by Theorem 4.1) are closed under composition (by Lemma 2.8), the following entails Theorem 4.1, thus concluding our completeness proof.
**► Lemma 4.10.** Any function $\Sigma^* \to \Pi^*$ computed by some aperiodic sequential transducer with 2 states can be expressed by some $\lambda\wp$-term of type $\mathrm{Str}_{\Sigma}[A] \dashv \mathrm{Str}_{\Pi}$, for a purely affine type A depending on the function.

Let us start by exposing the rough idea of the encoding's trick using set-theoretic maps. We reuse the notations of Definition 4.4 and assume w.l.o.g. that the set of states is $Q = \{1, 2\}$.

Suppose that at some point, after processing a prefix of the input, the transducer has arrived in state 1 (resp. 2) and in the meantime has outputted $w \in \Pi^*$. We can represent this “history” by the pair $(\kappa_w, \zeta)$ (resp. $(\zeta, \kappa_w)$) where

$$ \zeta, \kappa_w : \Pi^* \to \Pi^* \qquad \zeta : x \mapsto \varepsilon \qquad \kappa_w : x \mapsto w \cdot x $$

For instance, in the case of Example 4.6, after reading a string $s = s'b$, the transducer is in the state $q_b$ and has outputted$^{12}$ $w = a \cdot \psi(s')$, which we represent as $(\zeta, \kappa_{a \cdot \psi(s')})$ (taking $q_a = 1$ and $q_b = 2$; $\psi$ is described in Example 4.6). In general, some key observations are

$$ \zeta \circ \kappa_w = \zeta \qquad \kappa_w \circ \kappa_{w'} = \kappa_{ww'} \qquad \kappa_w(w')\zeta(w'') = \zeta(w'')\kappa_w(w') = ww' $$

Now, consider an input letter $c \in \Sigma$; how to encode the corresponding transition $\delta(-, c)$ as a transformation on the pair encoding the current state and output history? It depends on the state transition $\delta_{\mathrm{st}}(-, c)$; we have thanks to the above identities:

- $(h, g) \mapsto (h \circ \kappa_{\delta_{\mathrm{out}}(1,c)}, g \circ \kappa_{\delta_{\mathrm{out}}(2,c)})$ when $\delta_{\mathrm{st}}(-, c) = \mathrm{id}$;

- $(h, g) \mapsto (\kappa_h(\delta_{\mathrm{out}}(1,c))g(\delta_{\mathrm{out}}(2,c)), \zeta)$ when $\delta_{\mathrm{st}}(-, c) : q' \mapsto 1$ (note that $h = \zeta$ xor $g = \zeta$);

- $(h, g) \mapsto (\zeta, \kappa_h(\delta_{\mathrm{out}}(1,c))g(\delta_{\mathrm{out}}(2,c)))$ when $\delta_{\mathrm{st}}(-, c) : q' \mapsto 2$;

- The remaining case $\delta_{\mathrm{st}}(-, c) : q \mapsto 3-q$ is excluded by aperiodicity. This point is crucial: this case would correspond to $(h, g) \mapsto (g \circ \kappa_{\delta_{\mathrm{out}}(2,c)}, h \circ \kappa_{\delta_{\mathrm{out}}(1,c)})$ which morally “uses its arguments $h, g$ in the wrong order”.

Coming back to Example 4.6, let us say that after the transducer has read a prefix $s = s'b$ of its input string as we previously described, the next letter is $a$. Then the expression $h(\delta_{\mathrm{out}}(1, c))g(\delta_{\mathrm{out}}(2, c))$ above is in this case $\zeta(a)\kappa_{a \cdot \psi(s')}(bb) = \varepsilon \cdot a \cdot \psi(s') \cdot bb = a \cdot \psi(s)$ which is indeed the output that the transducer produces after reading the input prefix $sa = s'ba$.

Next, we must transpose these ideas to the setting of the $\lambda\wp$-calculus.

**Proof of Lemma 4.10.** We define the $\lambda\wp$-term meant to compute our sequential function as

$$ \lambda^{\circ} s. \lambda^{\rightarrow} f_{a_1} \dots \lambda^{\rightarrow} f_{a_{|\Pi|}} . \mathit{out} (s \mathit{trans}_{c_1} \dots \mathit{trans}_{c_{|\Sigma|}}) : \mathit{Str}_{\Sigma}[A] \dashv \mathit{Str}_{\Pi} $$

where $\Sigma = \{c_1, \dots, c_{|\Sigma|}\}$, $\Pi = \{a_1, \dots, a_{|\Pi|}\}$ and, writing $\Gamma = \{f_a : o \to o \mid a \in \Pi\}$,

$$ \Gamma \mid \emptyset \vdash \mathit{trans}_c : A \to A \quad (\text{for all } c \in \Sigma) \qquad \Gamma \mid \emptyset \vdash \mathit{out} : (A \to A) \to (o \to o) $$

In the presence of this non-affine context $\Gamma$, the type $S = o \to o$ morally serves as a purely affine type of strings, as mentioned in Remark 2.9. Moreover this “contextual encoding of strings” supports concatenation (by function composition), leading us to represent the maps $\zeta$ and $\kappa_w$ as open terms of type $T = S \to S$ that use non-affinely the variables $f_a$ for $a \in \Pi$.

We shall take the type $A$, at which the input $\mathrm{Str}_{\Sigma}$ is instantiated, to be $A = T \to T \to S$, which is indeed purely affine as required by the theorem statement. This can be seen morally as a type of continuations [42] taking pairs of type $T \otimes T$ (although our $\lambda\wp$-calculus has no actual $\otimes$ connective). Without further ado, let us program (the typing derivations for some of the following $\lambda\wp$-terms are given in Appendix C):

<footnote n="12">12 This is indeed $a \cdot \psi(s')$ and not $a \cdot \psi(s) = a \cdot \psi(s') \cdot bb$. If the input turns out to end there, the final output function will provide the missing suffix $F(q_b) = bbb$ to obtain $f(s) = a \cdot \psi(s) \cdot b = a \cdot \psi(s') \cdot bbb$.</footnote>
12 Aperiodicity in a non-commutative logic

- `cat = λ∘w. λ∘w'. λ∘x. w (w' x) : S → S → o → o = S → S → S = S → T` plays the roles of both the concatenation operator and of `w ↦ κ<sub>w</sub>` (thanks to currying)

- `zeta = λ∘w'. λ∘x. x : S → o → o = T`

- `u_q = δ_{out}(q, c)†(f_Π) : o → o (by Proposition 2.5) represents the output word δ_{out}(q, c) that corresponds to a given input letter c ∈ Σ and state q ∈ Q = {1, 2}`

- case `δ_st(q, c) = q`: `trans_c = λ∘k. λ∘h. λ∘g. k (λ∘y. h (cat u₁ y)) (λ∘z. g (cat u₂ z))` - if we wanted to handle the excluded case `δ_st(q, c) = 3 - q`, we would write a similar term with the occurrences of `h` and `g` exchanged `(λ∘k. λ∘h. λ∘g. k (λ∘y. g ...)) (λ∘z. h ...))`, violating the non-commutativity requirement (contrast with the proof of Theorem 5.4);

- case `δ_st(q, c) = 1`: `trans_c = λ∘k. λ∘h. λ∘g. k (cat (cat (h u₁) (g u₂))) zeta`

- case `δ_st(q, c) = 2`: `trans_c = λ∘k. λ∘h. λ∘g. k zeta (cat (cat (h u₁) (g u₂)))`

- `out = λ∘j. j (λ∘h. λ∘g. cat (h v₁) (g v₂)) (λ∘x. x) zeta`, where `v_q = F(q)†(f_Π)` represents the output suffix for state `q ∈ {1, 2}`, assuming w.l.o.g. that the initial state is 1 (also, here `λ∘x. x` represents `κ<sub>ε</sub>` since the latter is the identity on Π*)

We leave it to the reader to check that these $\lambda\flat$-terms have the expected computational behavior; again, see Appendix C for typing derivations. Note that in functional programming terms, the use of continuations turns the “right fold” of the Church-encoded input string into a “left fold”, and the latter fits with the left-to-right processing of a sequential transducer. ◀

5 Regular languages in extensions of the $\lambda\flat$-calculus

5.1 The commutative case

The $\lambda\flat$-calculus adds two restrictions to the simply typed $\lambda$-calculus, namely affineness and non-commutativity, with the latter depending on the former as already mentioned. One could wonder whether affineness by itself would be enough to characterize star-free languages. We now show that it is not the case.

The commutative variant of the $\lambda\flat$-calculus – let us call this variant the $\lambda a$-calculus<fnref n="13" /> – has the same grammar of types and terms as the $\lambda\flat$-calculus (cf. §2). The typing rules are also given by Figure 1, but their interpretation differs from the previous one as follows: $\Delta$, $\Delta'$ stand for sets of bindings $x: A$, $\Delta \cdot \Delta'$ denotes the disjoint union of sets, and one must read “subset” instead of “subsequence”. In other words, the main difference is that in the $\lambda a$-calculus, the affine context $\Delta$ does not keep track of the ordering of variables.

By plugging this commutative system in the statement of our main result (Theorem 1.7), we get *regular languages* instead of star-free languages:

**Theorem 5.1.** A language $L \subseteq \Sigma^*$ is regular if and only if it can be defined by a closed $\lambda a$-term of type $\mathrm{Str}_{\Sigma}[A] \dashv \mathrm{Bool}$ for some purely affine type $A$ (that may depend on $L$).

**Proof.** Soundness is a consequence of Hillebrand and Kanellakis's Theorem 1.1, by a simple translation from the $\lambda a$-calculus to the simply typed $\lambda$-calculus which “forgets affineness”.

For extensional completeness, consider a regular language $L = \varphi^{-1}(P)$ where $P$ is a subset of a finite monoid $M$ and $\varphi: \Sigma^* \to M$ is a morphism (cf. Theorem 1.3). If we represent an element $m \in M$ by a $M$-indexed bit vector $v_m$ such that $v_m[i] = 1 \iff i = m$, then a translation $m \mapsto mp$ can be represented by a *purely disjunctive* formula:

$$v_{mp}[i] = v_m[j_1] \lor \dots \lor v_m[j_k] \text{ where } \{j_1, \dots, j_k\} = \{j \in M \mid j_p = i\}$$

<footnote n="13">¹³ a standing for “affine”.</footnote>
Moreover, this is linear in the following sense: given a fixed $p \in M$, each index $j \in M$ is involved in the right-hand side of this formula for exactly one $i \in M$.

Let $ttt = \mathcal{X} \cdot x. true : Bool \to Bool$ and $fff = \mathcal{X} \cdot x : Bool \to Bool$. This makes the type $B = Bool \to Bool$ into a kind of type of booleans that supports a disjunction of type $B \to B \to B$ (by function composition) and a type-cast function of type $B \to Bool$ (by applying to false). (Of course $B$ has other closed inhabitants besides $ttt$ and $fff$, but we only use those two.) Using this type and the “iteration+continuations” recipe of the proof of Lemma 4.10, one can define a $\lambda\alpha$-term of type $Str_\Sigma[A] \to Bool$ that decides the language $L$ with $A = B \to \dots \to B \to Bool$ (with $|M|$ arguments of type $B$). ◀

Let us go further. According to Theorem 4.1, the $\lambda\varphi$-calculus can define all aperiodic sequential functions; we show that as one can expect, the aperiodicity condition is lifted when moving to the commutative $\lambda\alpha$-calculus. However, the trick used in the direct encoding of the above proof does not work, and we have only managed to encode general sequential functions by resorting to the Krohn-Rhodes theorem.

**Theorem 5.2 (Krohn-Rhodes decomposition, non-aperiodic case, cf. Appendix A).** Any sequential function $f : \Sigma^* \to \Pi^*$ can be realized as a composition $f = f_1 \circ \dots \circ f_n$ (with $f_i : \Xi_i^* \to \Xi_{i-1}^*$, $\Xi_0 = \Pi$ and $\Xi_n = \Sigma$) where each function $f_i$ is computed by some sequential transducer whose transition monoid is either aperiodic or a group.

**Remark 5.3.** By Theorem 4.8, the aperiodic transducers among the $f_i$ can be further decomposed into two-state aperiodic transducers.

**Theorem 5.4.** Any sequential function $\Sigma^* \to \Pi^*$ can be expressed by some $\lambda\alpha$-term of type $Str_\Sigma[A] \to Str_\Pi$, for a purely affine type $A$ depending on the function.

**Proof sketch.** First, by Theorem 4.1, we can already encode aperiodic sequential functions, since every well-typed $\lambda\varphi$-term is also a well-typed $\lambda\alpha$-term. One can also show that Lemma 2.8 applies to the $\lambda\alpha$-calculus. By the general Krohn-Rhodes theorem, we just need to handle the case of a sequential transducer whose transition monoid is a group.

The idea, in terms of set-theoretic maps as in our explanation of the proof of Lemma 4.10 (whose notations we borrow here), is as follows. The current state $q \in Q$ and output history $w \in \Pi^*$ is represented by a $Q$-indexed family $(g_q)_{q' \in Q}$ of functions such that $g_q = \kappa_w$ and for $q' \neq q$, $g_{q'} = \zeta$. The transition $\delta(-, c)$ is represented by $(g_q)_{q \in Q} \mapsto (g_{\sigma(q)} \circ \kappa_{\delta_{\text{out}}(\sigma(q),c)})_{q \in Q}$ where $\sigma = (\delta_{\text{st}}(-, c))^{-1}$ – the latter is well-defined because the group assumption means that $\delta_{\text{st}}(-, c)$ is a permutation of $Q$. The final output is obtained at the end as the concatenation $g_{q_1}(F(q_1)) \dots g_{q_n}(F(q_n))$ where $Q = \{q_1, \dots, q_n\}$ (with an arbitrary enumeration of $Q$).

The elaboration of the corresponding $\lambda\alpha$-term is left to the reader. Keep in mind that the reason this term will not be well-typed for the $\lambda\varphi$-calculus is that the inversions in the permutation $\delta_{\text{st}}(-, c)$ correspond to violations of non-commutative typing. ◀

## 5.2 Extension with additive pairs

Let's look at what happens if we add the *additive conjunction* connective of linear logic to the $\lambda\varphi$-calculus. The $\lambda\varphi$&-calculus is obtained by adding $A, B ::= \dots | A \& B$ to the grammar of types and $t, u ::= \dots | \langle t, u \rangle | \pi_1 t | \pi_2 t$ for terms, with the typing rules

$$ \frac{\Gamma \mid \Delta \vdash t : A \quad \Gamma \mid \Delta \vdash u : B}{\Gamma \mid \Delta \vdash \langle t, u \rangle : A \& B} \qquad \frac{\Gamma \mid \Delta \vdash t : A_1 \& A_2}{\Gamma \mid \Delta \vdash \pi_i t : A_i} \quad (\text{see [39, §4]}) $$

the $\beta$-reduction rules $\pi_i \langle t_1, t_2 \rangle \to \beta t_i$, and the corresponding $\eta$-conversion rules.
14 Aperiodicity in a non-commutative logic

Recall that we discussed both in the introduction and in Remark 2.7 the need to prevent
the existence of a $\lambda\phi$-term of type $\mathbf{Bool} \dashv \mathbf{Bool}$ for negation. However, if we use the additive
conjunction to define the type $\mathbf{Bool}^\& = (o \& o) \dashv o$, the following are well-typed $\lambda\phi$-terms:

$$
\mathbf{true}^{\&} = \lambda^{\circ} p. \pi_{1} p \quad \mathbf{false}^{\&} = \lambda^{\circ} p. \pi_{2} p \quad \mathbf{not}^{\&} = \lambda^{\circ} b. \lambda^{\circ} p. b \langle \pi_{2} p, \pi_{1} p \rangle
$$

More generally:

**Proposition 5.5.** Let $\mathbf{Fin}^{\&}(n) = (o \& \dots \& o) \dashv o$. For all $n \in \mathbb{N}$, there is a canonical bijection between $\{1, \dots, n\}$ and the closed $\lambda\phi^{\&}$-terms of type $\mathbf{Fin}^{\&}(n)$. Furthermore, using this encoding, every map $\{1, \dots, n_1\} \times \dots \times \{1, \dots, n_k\} \to \{1, \dots, m\}$ can be defined by a closed $\lambda\phi^{\&}$-term of type $\mathbf{Fin}^{\&}(n_1) \dashv \dots \dashv \mathbf{Fin}^{\&}(n_k) \dashv \mathbf{Fin}^{\&}(m)$.

**Corollary 5.6.** Every regular language can be defined by a closed $\lambda\phi^{\&}$-term of type $\mathbf{Str}_{\Sigma}[A] \dashv \mathbf{Bool}$ for some purely affine type $A$ – we consider `&` as an affine connective and therefore allow it in $A$.

**Proof idea.** Take $A = \mathbf{Fin}^{\&}(|M|)$ where $M$ is any finite monoid that recognizes the language as specified in Theorem 1.3. (We could also prove the converse by relying on an extension of Hillebrand and Kanellakis’s Theorem 1.1 to the simply typed $\lambda$-calculus with products.) ◀

Similarly, one could show that the addition of the *additive disjunction* `⊕` of linear logic
to the $\lambda\phi$-calculus would be sufficient to encode all regular languages.

**5.3 On regular and first-order tree languages: a discussion**

There is a rich theory of tree automata that extends the notion of regular language to trees
over ranked alphabets instead of strings. Such trees admit Church encodings; for instance,
for an alphabet with arities $(a : 2, b : 2, x : 0)$ (i.e. for trees with two kind of binary nodes
and one kind of leaf) one would have $\mathbf{Tree}_{(2,2,0)} = (o \to o \to o) \to (o \to o \to o) \to o \to o$.

**Remark 5.7.** A string over an alphabet $\Sigma = \{c_1, \dots, c_{|\Sigma|}\}$ can be seen as a tree with arities $(c_1 : 1, \dots, c_{|\Sigma|} : 1, \varepsilon : 0)$. This would lead to defining the type of Church-encoded strings as $\mathbf{Str}'_{\Sigma} = (o \to o) \to \dots \to (o \to o) \to o \to o$. Our type $\mathbf{Str}_{\Sigma}$, which is the traditional choice in linear logic (see the discussion on Church numerals in [18, §5.3.2]), is a bit more precise since it expresses that such a “unary tree” can only contain one $\varepsilon$ node. But as there exist conversion functions $\mathbf{Str}_{\Sigma} \dashv \mathbf{Str}'_{\Sigma}$ and $\mathbf{Str}'_{\Sigma}[o \to o] \dashv \mathbf{Str}_{\Sigma}$, this choice does not make much difference (thanks again to Lemma 2.8).

We shall not go into the details of tree automata here, but the knowledgeable reader
may check that Proposition 5.5 can be used to encode all *regular tree languages* over
$(a : 2, b : 2, x : 0)$ as closed $\lambda\phi^{\&}$-terms of type $\mathbf{Tree}_{(2,2,0)}[A] \dashv \mathbf{Bool}$ for purely affine $A$.
Predictably, this fails for the $\lambda\phi$-calculus without additive connectives. More noteworthy
is the failure of the trick used to prove Theorem 5.1 for the commutative $\lambda a$-calculus when
one replaces strings with trees. Thus, it seems (though this remains conjectural) that *the
additives of linear logic might be required to express some regular tree languages*.

We believe that this is no accident and that some fundamental difficulty of automata
theory is being manifested here. Indeed, if we had a characterization of regular tree languages
in the $\lambda a$-calculus, we could expect that moving to the $\lambda\phi$-calculus would yield the *first-order
tree languages*, which are the commonly accepted counterpart of star-free languages for
trees. (Recall from Theorem 1.5 that definability in first-order logic is among the equivalent
definitions of star-free languages.) However, while Theorem 1.5 demonstrates that star-free
languages are well-understood, the situation is quite different for first-order tree languages:
there is no known algebraic characterization, and neither is there any known algorithm to decide whether a tree automaton recognizes a first-order language (see e.g. [9, §3]). Another argument for the necessity of additives, discussed in the next section, comes from transducers.

# 6 Next episode preview: transducers in typed λ-calculi

We started from Hillebrand and Kanellakis's Theorem 1.1 and obtained an analogous statement for star-free languages instead of regular languages. Another direction that we could have pursued is to replace languages by functions, by looking at the type $Str_Σ[A] \to Str_Π$. Indeed, an immediate consequence of this "regular = λ-definable" result is:

**Corollary 6.1.** If $f : Σ^* \to Π^*$ is definable by a closed simply typed λ-term of type $Str_Σ[A] \to Str_Π$, then for any regular language $L \subseteq Π^*$, $f^{-1}(L) \subseteq Σ^*$ is also regular.

**Proof idea.** Let $u : Str_Π[B] \to Bool$ and $t : Str_Σ[A] \to Str_Π$ be simply typed λ-terms defining $L$ and $f$ respectively. Then $f^{-1}(L)$ is defined by $\lambda x. u(tx)$ which is well-typed with type $Str_Σ[A[B]] \to Bool$ (analogously to Lemma 2.8). ◀

This suggests a connection between these λ-definable string functions and automata theory. But while it is not too hard to define functions of hyperexponential growth in the simply typed λ-calculus, most classes of string functions from automata theory (see [37] for a recent survey) grow much more slowly (polynomially or even linearly in the input size). The challenge then becomes to restrict the expressiveness via types to capture such classes. This calls for the recipes that have worked here, namely affine types and non-commutativity.

**Claim 6.2 (to be proved in a sequel).** The functions definable by closed terms of type $Str_Σ[A] \dashv Str_Π$, for purely affine $A$, are the *MSO transductions*<fnref n="14" /> [15] (a.k.a. *regular functions*<fnref n="15" />) in the $\lambda a$-calculus and the *FO transductions* in the $\lambda \wp$-calculus.

This goes beyond the encodings of sequential transducers presented in this paper (Theorem 4.1 and Theorem 5.4). But the latter are an important stepping stone, since we do not know how to prove the above claim without using the Krohn–Rhodes decomposition somewhere. To summarize the results of the present paper together with its planned sequel:

<table><thead><tr><th>calculus</th><th>affine</th><th>commutative</th><th>Str<sub>Σ</sub>[A] &rarr; Bool</th><th>Str<sub>Σ</sub>[A] &rarr; Str<sub>Π</sub></th></tr></thead><tbody><tr><td>&lambda;&wp;</td><td>yes</td><td>no</td><td>star-free (FO-definable) languages</td><td>FO transductions</td></tr><tr><td>&lambda;a</td><td>yes</td><td>yes</td><td>regular (MSO-definable) languages</td><td>MSO transductions</td></tr></tbody></table>

While the connection between non-commutativity and aperiodicity came as a surprise to us, we had more reasons to suspect that affine types should have something to do with transducers. Indeed, the term "linear" itself has been used to describe the *copyless assignment* condition on streaming string transducers (SSTs) [3], a machine model for MSO transductions, e.g. "updates should make a linear use of registers" [16, §5] (in our terminology, the register assignments of SSTs are in fact affine, not strictly linear). Moreover, it seems (informally speaking) that the more sophisticated *single-use-restricted assignments* of streaming tree transducers [4] correspond to a form of linearity that incorporates an *additive conjunction*, whereas copyless assignments are purely *multiplicative*; compare with the discussion of §5.3.

<footnote n="14">¹⁴ MSO stands for Monadic Second-Order Logic while FO stands for First-Order Logic, cf. the introduction.</footnote>

<footnote n="15">¹⁵ This name is somewhat confusing, since there are multiple classes of string functions that collapse to the single class of regular languages when we consider indicator functions. For example, in-between the sequential functions (Definition 4.4) and the regular (MSO-definable) functions, there is a widely studied strictly intermediate class called the *rational functions*. (The adjective "rational" is used to refer to regular languages in a French tradition going back to Nivat and Schützenberger.)</footnote>
## 7 Related work

We have already mentioned in the introduction several lines of tangentially related research, such as higher-order model checking or the topology of non-commutative proofs. In this section, we discuss a few references that we deemed to be more directly relevant.

**Automata as circular proofs** Aside from Hillebrand and Kanellakis's Theorem 1.1, perhaps our most direct precursors in “implicit automata theory” are the works by DeYoung and Pfenning [13] on sequential transducers (their version seems to be equivalent to Definition 4.4) and by Kuperberg, Pinault and Pous [29] characterizing regular languages and deterministic logarithmic space complexity. Both rely on a proofs-as-programs interpretation of circular<sup>16</sup> proof systems for some variants of linear logic with fixed points.

The Church encoding of strings is obtained by a systematic procedure [12] from the inductive definition $s ::= \varepsilon \mid c_1 \cdot s \mid \dots \mid c_{|\Sigma|} \cdot s$ ($\Sigma = \{c_1, \dots, c_{|\Sigma|}\}$). Using fixed points of formulas, one can instead turn it into the recursive type<sup>17</sup> $\mathbf{Str}_{\Sigma}^{\mu} = 1 \oplus \mathbf{Str}_{\Sigma}^{\mu} \oplus \dots \oplus \mathbf{Str}_{\Sigma}^{\mu}$; this is the definition of the type of strings in [13], and it is also implicitly at work in<sup>18</sup> [29].

So both our approach (following Hillebrand and Kanellakis [25]) and those using fixed point logics morally work because the consumption of strings represented as inductive data types is similar to their traversal by automata. However, while the use of the “right fold” provided by a Church-encoded string involves an “inversion of control” (in programming jargon) that, in the case of the simply typed $\lambda$-calculus, has drastic effects on expressive power<sup>19</sup> (contrast Theorem 1.1 with the fact that $\beta\eta$-convertibility of simply typed $\lambda$-terms is not elementary recursive [33]), circular proofs seem to give the programmer more degrees of freedom: Kuperberg et al. do not need to add polymorphism to go beyond regular languages.

**Recognizable languages of $\lambda$-terms** A modern point of view on Hillebrand and Kanellakis's Theorem 1.1 can be implicitly found in a paper by Terui [48] emphasizing the method of *evaluation in a finite denotational semantics* used to prove it. Along these lines, general notions of recognizable languages of closed $\lambda$-terms of a given type (specializing to regular languages for the type of Church-encoded strings) have been proposed, based on finite semantics, in the simply-typed $\lambda$-calculus by Salvati [45] and in an infinitary $\lambda$-calculus by Melliès [35]. It is plausible that Theorem 1.1 can be extended to give an equivalent syntactic definition for Salvati's recognizable languages: for a simple type $B$ they would be the languages definable by $B[A] \to \mathbf{Bool}$. An interesting question would be whether one can give an encoding of *higher-dimensional trees* in the simply typed $\lambda$-calculus so that this notion of recognizability coincides with Rogers's automata for those trees [43, 17].

**Other implicit automata results** In a recent preprint, Bojańczyk [10] introduces a new class of string-to-string functions that admits several equivalent definitions (see also [11]). One of them uses the simply typed $\lambda$-calculus enriched with a ground type of lists and several primitive functions on lists. Strings are represented as lists of characters, which differs from our use of functional encodings in a $\lambda$-calculus without any primitive data type.

<footnote n="16"><sup>16</sup>These are sometimes called “cyclic” proofs, but in our context, this would create a confusion with an unrelated non-commutative logic, *cyclic linear logic* [50].</footnote>

<footnote n="17"><sup>17</sup>Formally, this is expressed as the least fixed point $\mathbf{Str}_{\Sigma}^{\mu} = \mu\alpha$. $1 \oplus \alpha \oplus \dots \oplus \alpha$.</footnote>

<footnote n="18"><sup>18</sup>The left rules given in [29, Figure 1] for $A$ and $A^*$ correspond to $A = 1 \oplus \dots \oplus 1$ and $A^* = 1 \oplus (A \otimes A^*)$.</footnote>

<footnote n="19"><sup>19</sup>To overcome those limits and express any elementary recursive function as a simply typed $\lambda$-term, Hillebrand and Kanellakis use an alternative representation of inputs inspired by database theory [25].</footnote>
Using a computational model inspired by denotational semantics of linear logic, Seiller [46] gives a characterization of each level of the *k*-head two-way non-deterministic automata hierarchy. The lowest level (*k* = 1) corresponds to regular languages, while the union over *k* ∈ N≥1 gives the complexity class NL (non-deterministic logarithmic space). Something in common with our work is that the representation of strings used by [46] is more or less a semantic version of Church encodings (see [46, §3.2]). There is one main difference with what one usually calls implicit complexity: Seiller’s result does not take place inside a syntactically defined programming language (and it is far from obvious how to turn this model into a similarly expressive syntax, because of the previously mentioned inversion of control).

**Controlling expressible functions with non-commutativity** The tree-processing programming language of Kodama, Suenaga and Kobayashi [27] uses non-commutative types to force programs to process their input in a depth-first, left-to-right fashion. This allows them to be compiled into a target language that works on a stream of tokens, suggesting a possible connection with nested word automata [5]. The non-commutativity is restricted to arguments of ground type in [27], whereas it is important for our λφ-calculus that it applies at all orders (indeed, since we encode data as functions, higher-order functions are pervasive).

References

1 Samson Abramsky. Temperley–Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics. In Goong Chen, Louis Kauffman, and Samuel Lomonaco, editors, *Mathematics of Quantum Computation and Quantum Technology*, volume 20074453, pages 515–558. Chapman and Hall/CRC, September 2007. doi:10.1201/9781584889007.ch15.

2 Klaus Aehlig. A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata. *Logical Methods in Computer Science*, 3(3), July 2007. doi:10.2168/LMCS-3(3:1):2007.

3 Rajeev Alur and Pavol Černý. Expressiveness of streaming string transducers. In Kamal Lodaya and Meena Mahajan, editors, *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India*, volume 8 of *LIPIcs*, pages 1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. doi:10.4230/LIPIcs.FSTTCS.2010.1.

4 Rajeev Alur and Loris D'Antoni. Streaming Tree Transducers. *Journal of the ACM*, 64(5):1–55, August 2017. doi:10.1145/3092842.

5 Rajeev Alur and P. Madhusudan. Adding nesting structure to words. *Journal of the ACM*, 56(3):16:1–16:43, 2009. doi:10.1145/1516512.1516518.

6 Jean-Marc Andreoli, Gabriele Pulcini, and Paul Ruet. Permutative logic. In C.-H. Luke Ong, editor, *Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings*, volume 3634 of *Lecture Notes in Computer Science*, pages 184–199. Springer, 2005. doi:10.1007/11538363_14.

7 Andrew Barber. Dual Intuitionistic Linear Logic. Technical report ECS-LFCS-96-347, LFCS, University of Edinburgh, 1996. URL: http://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/.

8 Mikołaj Bojańczyk. The simplest transducer models and their Krohn-Rhodes decompositions. https://www.mimuw.edu.pl/~bojan/slides/transducer-course/krohn-rhodes.html. Slides of a lecture given at FSTTCS '19, accessed on 11-02-2020.

9 Mikołaj Bojańczyk. Automata column: Some Open Problems in Automata and Logic. *ACM SIGLOG News*, 1(2):3–12, October 2014. doi:10.1145/2677161.2677163.

10 Mikołaj Bojańczyk. Polyregular functions, 2018. arXiv:1810.08760.

11 Mikołaj Bojańczyk, Sandra Kiefer, and Nathan Lhote. String-to-String Interpretations With Polynomial-Size Output. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and
18 Aperiodicity in a non-commutative logic

Stefano Leonardi, editors, *46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)*, volume 132 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 106:1–106:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019. doi: 10.4230/LIPIcs.ICALP.2019.106.

12 Corrado Böhm and Alessandro Berarducci. Automatic synthesis of typed λ-programs on term algebras. *Theoretical Computer Science*, 39:135–154, January 1985. doi:10.1016/0304-3975(85)90135-5.

13 Henry DeYoung and Frank Pfenning. Substructural proofs as automata. In Atsushi Igarashi, editor, *Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings*, volume 10017 of *Lecture Notes in Computer Science*, pages 3–22, 2016. doi:10.1007/978-3-319-47958-3_1.

14 Volker Diekert, Manfred Kufleitner, and Benjamin Steinberg. The Krohn-Rhodes Theorem and Local Divisors. *Fundamenta Informaticae*, 116(1-4):65–77, 2012. doi:10.3233/FI-2012-669.

15 Joost Engelfriet and Hendrik Jan Hoogeboom. MSO definable string transductions and two-way finite-state transducers. *ACM Transactions on Computational Logic*, 2(2):216–254, April 2001. doi:10.1145/371316.371512.

16 Emmanuel Filiot and Pierre-Alain Reynier. Transducers, Logic and Algebra for Functions of Finite Words. *ACM SIGLOG News*, 3(3):4–19, August 2016. doi:10.1145/2984450.2984453.

17 Neil Ghani and Alexander Kurz. Higher dimensional trees, algebraically. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, *Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings*, volume 4624 of *Lecture Notes in Computer Science*, pages 226–241. Springer, 2007. doi:10.1007/978-3-540-73859-6_16.

18 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50(1):1–101, January 1987. doi:10.1016/0304-3975(87)90045-4.

19 Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and A. Scedrov, editors, *Categories in Computer Science and Logic*, volume 92 of *Contemporary Mathematics*, pages 69–108. American Mathematical Society, Providence, RI, 1989. Proceedings of a Summer Research Conference held June 14–20, 1987. doi:10.1090/conm/092/1003197.

20 Jean-Yves Girard. Light Linear Logic. *Information and Computation*, 143(2):175–204, June 1998. doi:10.1006/inco.1998.2700.

21 Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. *Theoretical Computer Science*, 97(1):1–66, April 1992. doi:10.1016/0304-3975(92)90386-T.

22 Charles Grellois. *Semantics of linear logic and higher-order model-checking*. PhD thesis, Université Paris 7, April 2016. URL: https://tel.archives-ouvertes.fr/tel-01311150/.

23 Alessio Guglielmi. A system of interaction and structure. *ACM Transactions on Computational Logic*, 8(1), January 2007. doi:10.1145/1182613.1182614.

24 Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible Pushdown Automata and Recursion Schemes. *ACM Transactions on Computational Logic*, 18(3):25:1–25:42, August 2017. doi:10.1145/3091122.

25 Gerd G. Hillebrand and Paris C. Kanellakis. On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. In *Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science*, pages 253–263. IEEE Computer Society, 1996. doi:10.1109/LICS.1996.561337.

26 Naoki Kobayashi. Model Checking Higher-Order Programs. *Journal of the ACM*, 60(3):1–62, June 2013. doi:10.1145/2487241.2487246.

27 Koichi Kodama, Kohei Suenaga, and Naoki Kobayashi. Translation of tree-processing programs into stream-processing programs based on ordered linear type. *Journal of Functional Programming*, 18(3):333–371, 2008. doi:10.1017/S0956796807006570.
28 Kenneth Krohn and John Rhodes. Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines. *Transactions of the American Mathematical Society*, 116:450–464, 1965. doi:10.1090/S0002-9947-1965-0188316-1.

29 Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In Arkadev Chattopadhyay and Paul Gastin, editors, *39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)*, volume 150 of Leibniz International Proceedings in Informatics (LIPIcs), pages 45:1–45:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019. doi:10.4230/LIPIcs.FSTTCS.2019.45.

30 Joachim Lambek. The mathematics of sentence structure. *The American Mathematical Monthly*, 65(3):154–170, 1958. URL: http://www.jstor.org/stable/2310058.

31 Olivier Laurent. Polynomial time in untyped elementary linear logic. *Theoretical Computer Science*, 813:117–142, April 2020. doi:10.1016/j.tcs.2019.10.002.

32 Daniel Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In *24th Annual Symposium on Foundations of Computer Science (FOCS 1983)*, pages 460–469, Tucson, AZ, USA, November 1983. doi:10.1109/SFCS.1983.50.

33 Harry G. Mairson. A simple proof of a theorem of Statman. *Theoretical Computer Science*, 103(2):387–394, September 1992. doi:10.1016/0304-3975(92)90020-G.

34 Damiano Mazza. *Polyadic Approximations in Logic and Computation*. Habilitation à diriger des recherches, Université Paris 13, November 2017. URL: https://lipn.fr/~mazza/papers/Habilitation.pdf.

35 Paul-André Melliès. Higher-order parity automata. In *2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–12, Reykjavik, Iceland, June 2017. IEEE. doi:10.1109/LICS.2017.8005077.

36 Paul-André Melliès. Ribbon Tensorial Logic. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18*, pages 689–698, Oxford, United Kingdom, 2018. ACM Press. doi:10.1145/3209108.3209129.

37 Anca Muscholl and Gabriele Puppis. The Many Facets of String Transducers. In Rolf Niedermeier and Christophe Paul, editors, *36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)*, volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1–2:21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019. doi:10.4230/LIPIcs.STACS.2019.2.

38 C.-H. Luke Ong. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In *21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)*, pages 81–90, Seattle, WA, USA, 2006. IEEE. doi:10.1109/LICS.2006.38.

39 Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-communicative linear logic. In Jean-Yves Girard, editor, *Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings*, volume 1581 of Lecture Notes in Computer Science, pages 295–309. Springer, 1999. doi:10.1007/3-540-48959-2_21.

40 Jeff Polakow and Frank Pfenning. Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. *Electronic Notes in Theoretical Computer Science*, 20:449–466, January 1999. doi:10.1016/S1571-0661(04)80088-4.

41 Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In Philippe de Groote, editor, *Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings*, volume 1210 of Lecture Notes in Computer Science, pages 300–318. Springer, 1997. doi:10.1007/3-540-62688-3_43.

42 John C. Reynolds. The discoveries of continuations. *LISP and Symbolic Computation*, 6(3):233–247, Nov 1993. doi:10.1007/BF01019459.

43 James Rogers. Syntactic Structures as Multi-dimensional Trees. *Research on Language and Computation*, 1(3):265–305, September 2003. doi:10.1023/A:1024695608419.

44 Jacques Sakarovitch. *Elements of Automata Theory*. Cambridge University Press, 2009. Translated by Reuben Thomas. doi:10.1017/CBO9781139195218.
45 Sylvain Salvati. Recognizability in the simply typed lambda-calculus. In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, *Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings*, volume 5514 of *Lecture Notes in Computer Science*, pages 48–60. Springer, 2009.
doi:10.1007/978-3-642-02261-6_5.

46 Thomas Seiller. Interaction Graphs: Non-Deterministic Automata. *ACM Transactions on Computational Logic*, 19(3):21:1–21:24, August 2018. doi:10.1145/3226594.

47 Howard Straubing. First-order logic and aperiodic languages: a revisionist history. *ACM SIGLOG News*, 5(3):4–20, 2018. doi:10.1145/3242953.3242956.

48 Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In *23rd International Conference on Rewriting Techniques and Applications (RTA’12)*, pages 323–338, 2012. doi:10.4230/LIPIcs.RTA.2012.323.

49 Igor Walukiewicz. LambdaY-calculus with priorities. In *34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019*, pages 1–13. IEEE, 2019. doi:10.1109/LICS.2019.8785674.

50 David N. Yetter. Quantales and (noncommutative) linear logic. *The Journal of Symbolic Logic*, 55(1):41–64, March 1990. doi:10.2307/2274953.

51 Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. *Logical Methods in Computer Science*, 11(3), September 2015.
doi:10.2168/LMCS-11(3:22)2015.

**A Reminder: the Krohn–Rhodes decomposition theorems, from transformation monoids to sequential transducers**

While we have not found a source with a proof for the precise versions of the Krohn–Rhodes theorem for sequential functions that we use, all the material covered in this subsection is well-known among practitioners of automata theory. In other words, we make no claim to originality.

**► Definition A.1.** A transformation monoid $(X, M)$ consists of a set $X$, a monoid $M$ and a right action of $M$ on $X$ (kept implicit in the notation $(X, M)$, and denoted by $(x, m) \mapsto x \cdot m$). It is finite when both $X$ and $M$ are finite.

Typical transformation monoids are obtained by considering pairs $(Q, T)$ such that $Q$ is the state space of some transducer $(Q, \delta, q_I, F)$ and $T$ is its transition monoid, acting on $Q$ via function application.

**► Definition A.2.** Let $(X, M)$ and $(Y, N)$ be two transformation monoids. Their wreath product is a transformation monoid $(X, M) \bowtie (Y, N) = (X \times Y, W)$ where:

- the underlying set of the monoid $W$ is $M^Y \times N$;

- the right action of $(f, n) \in W = M^Y \times N$ on $(x, y) \in X \times Y$ is $(x, y) \cdot (f, n) = (x \cdot f(y), y \cdot n)$;

- the multiplication on $W$ is $(f, n)(g, k) = ((y \mapsto f(y)g(y \cdot n)), nk)$ – it is chosen so that the above item is a legitimate monoid action.

**► Proposition A.3.** The wreath product of transformation monoids is associative up to canonical isomorphism.

**Proof sketch.** We give a direct description of $(X, M) \bowtie (Y, N) \bowtie (Z, P) = (X \times Y \times Z, W)$:

- the underlying set of the monoid $W$ is $M^{Y \times Z} \times N^Z \times P$ – note that it is canonically isomorphic to $(M^Y \times N)^Z \times P$;

- the right action is $(x, y, z) \cdot (f, g, p) = (x \cdot f(y, z), y \cdot g(z), z \cdot p)$;
■ the multiplication on W is

$$ (f, g, p)(f', g', p') = (((y, z) \mapsto f(y, z)f'(y \cdot n, z \cdot p)), (z \mapsto g(z)g'(z \cdot p)), pp'). $$

◀

**► Definition A.4.** A transformation monoid $(X, M)$ strongly divides $(Y, N)$ if there exists a submonoid $N' \leq N$, a surjective morphism $\varphi : N' \to M$ and a surjection $s : Y \to X$ such that for all $y \in Y$ and $n' \in N'$, $s(y \cdot n') = s(y) \cdot \varphi(n')$.

A monoid $M$ divides $N$ if $M$ is the homomorphic image of a submonoid of $N$.

**► Proposition A.5.** A finite monoid is aperiodic if and only if it there are no non-trivial groups that divide it.

**Proof.** Let $M$ be a finite monoid. Suppose that for $x \in M$, there is no $n \in \mathbb{N}$ such that $x^n = x^{n+1}$; then by finiteness, $(x^i)_{i \in \mathbb{N}}$ must be ultimately periodic with period $k \geq 2$, and one can define a surjective morphism from the submonoid generated by $x$ to the cyclic group of order $k$ by sending $x$ to the latter's generator. The converse follows a similar reasoning (recall that every non-trivial group contains a non-trivial cyclic subgroup). ◀

**► Theorem A.6 (Krohn–Rhodes with strong divisors [14, Theorem 4.1]).** Every finite transformation monoid $(X, M)$ strongly divides some wreath product $(Y_1, N_1) \wr \dots \wr (Y_n, N_n)$ where each $(Y_k, N_k)$ is either:

■ the flip-flop $(Y_k, N_k) = (\{1, 2\}, \{\mathrm{id}_{\{1,2\}}, (x \mapsto 1), (x \mapsto 2)\})$ (with the action $x \cdot f = f(x)$ and the monoid multiplication $fg = g \circ f$);

■ a finite group dividing $M$ acting on itself by right multiplication.

In particular, if $M$ is aperiodic, $(X, M)$ strongly divides a wreath product of several copies of the flip-flop transformation monoid.

**► Remark A.7.** The flip-flop transformation monoid is precisely the transition monoid of the transducer of Example 4.6 endowed with its action on the set of states.

**► Remark A.8.** We can also require $G$ above to be a simple group. This is the statement given in [14], but group simplicity is not needed for our purposes. (To be more precise, every finite group divides a wreath product of its Jordan–Hölder factors.)

**► Remark A.9.** Let $(Y, N) = (Y_1, N_1) \wr \dots \wr (Y_n, N_n)$. In both the flip-flop and group cases, the action of $N_k$ on $Y_k$ is faithful, i.e. two distinct elements of $N_k$ act differently on at least one element of $Y_k$. Furthermore, the wreath product of faithful transformation monoids is faithful. Therefore, one can safely identify $N$ with a submonoid of $Y \to Y$.

Now let us relate this wreath product operation to sequential functions. This is sufficient to derive Theorem 4.8 and Theorem 5.2 as corollaries of Theorem A.6.

**► Proposition A.10.** Let $(Q, \delta, q_I, F)$ be a sequential transducer with transition monoid $T$ describing a function $f : \Sigma^* \to \Pi^*$. Suppose that $(Q, T)$ strongly divides some faithful transformation monoid $(X, M) \wr (Y, N)$. Then there is an alphabet $\Xi$ and transducers

$$ (X, \delta_X, x_I, F_X) : \Sigma^* \to \Xi^* \quad \text{and} \quad (Y, \delta_Y, y_I, F_Y) : \Xi^* \to \Pi^* $$

such that

■ the sequential functions $f_X : \Sigma^* \to \Xi^*$ and $f_Y : \Xi^* \to \Pi^*$ that they respectively compute verify $f = f_X \circ f_Y$;

■ there are injective homomorphisms $T_X \hookrightarrow M$ and $T_Y \hookrightarrow N$ from their respective transition monoids.
**Proof.** Let $(Q, \delta, q_I, F)$ be the transducer under scrutiny. Let $K \subseteq M^Y \times N$ such that $\varphi: K \to T$, $s: X \times Y \to Q$ be the maps witnessing that $(Q, T)$ strongly divides $(X, M) \upharpoonright (Y, N)$. We choose a pair $(x_I, y_I)$ such that $s(x_I, y_I) = q_I$ and, for each $a \in \Sigma$, we choose an element $(g_a, n_a) \in M^Y \times N$ which is mapped by $\varphi$ to $\delta_{\text{st}}(-, a) \in T$. Set $\Xi = (\Sigma \uplus \{\ast\}) \times Y$, $(x_I, y_I) = s^{-1}(x, y)$ and

$$ 
\begin{align*}
F_Y(y) &= (\ast, y) & F_X(x) &= \epsilon \\
\delta_Y(y, a) &= (y \cdot m_a, y) & \delta_X(x, (a, y)) &= (x \cdot g_a(y), \delta_{\text{out}}(s(x), a)) \\
& & \delta_X(x, (\ast, y)) &= (x, F(s(x, y)))
\end{align*}
$$

We leave checking that this defines transducers with the expected properties to the reader. ◀

This generalizes to $n$-fold wreath products in the expected way.

**► Proposition A.11.** Let $T$ be the transition monoid of a sequential transducer with state space $Q$ computing the function $f: \Sigma^* \to \Pi^*$. Suppose that $(Q, T)$ strongly divides some wreath product $(X, M) = (X_1, M_1) \wr \dots \wr (X_n, M_n)$ of faithful transformation monoids. Then $f$ admits a decomposition $f = f_1 \circ \dots \circ f_n$ (with $f_i: \Xi_i^* \to \Xi_{i-1}^*$, $\Xi_0 = \Pi$ and $\Xi_n = \Sigma$) such that for each $i \in \{1, \dots, n\}$, $f_i$ is computed by a sequential transducer whose transformation monoid embeds in $M_i$ and with state space $X_i$.

**Proof.** By induction starting from $n=1$.

- For $n=1$, let $\varphi: K \to T$ and $s: X \to Q$ be the maps witnessing that $(Q, T)$ strongly divides $(X, M)$. Let $x_I$ be such that $s(x_I) = q_I$, and, for each $a \in \Sigma$, pick an element $m_a \in K$ such that $\varphi(m_a) = \delta_{\text{st}}(-, a)$. Then, letting $(Q, \delta, q_I, F)$ being the transducer under scrutiny, a suitable transducer $(X, \delta', x_I, F')$ is defined by setting $\delta'(x, a) = (x \cdot m_a, \delta_{\text{out}}(s(x), a))$ and $F'(x) = F(s(x))$.

- For $n > 1$, use Proposition A.10 and the induction hypothesis. ◀

**Proof of Theorems 4.8 and 5.2.** Let $(Q, \delta, q_I, F)$ be a transducer computing a certain sequential function $f: \Sigma^* \to \Pi^*$ and let $T$ be its transition monoid. By Theorem A.6, there is a transformation monoid $(Y, N)$ which can be written as a wreath product $(Y, N) = (Y_1, N_1) \wr \dots \wr (Y_k, N_k)$ such that $(Q, T)$ strongly divides $(Y, N)$, and the $(Y_i, N_i)$ are either flips or groups (the latter case being ruled out for Theorem 4.8, thanks to Proposition A.5). By applying Proposition A.11, we may obtain transducers $\mathcal{T}_i$ implementing sequential functions $f_i: \Xi_i^* \to \Xi_{i+1}^*$ such that $\Xi_0 = \Sigma$, $\Xi_k = \Pi$ and $f = f_{k-1} \circ \dots \circ f_0$. Furthermore, we know that the state space of $\mathcal{T}_i$ is $Y_i$ and that the corresponding transition monoid $T_i$ embeds into $N_i$. Recalling that “being aperiodic” and “being a finite subgroup” are properties stable under homomorphic embeddings, we know that either $Y_i$ has cardinality 2 and $T_i$ is aperiodic with two states or $T_i$ is a group (a trivial group if $T$ was aperiodic), thus we may conclude. ◀

## B Omitted proofs

### B.1 Proof of Lemma 2.8

The lemma follows from the more usual stability of typing judgments under type substitution. We write $\Gamma[A]$ and $\Delta[B]$ for the obvious extension of Notation 1.2 to contexts.

**Lemma B.1.** If $\Gamma | \Delta \vdash t: A$, then, for every type $B$, we have $\Gamma[B] | \Delta[B] \vdash t: A[B]$.

**Proof.** Routine induction on the typing derivation. ◀
Picturing Lemma B.1 as an admissible typing rule (dashed inference line), we have

$$ \frac{
  \begin{array}{c}
    \begin{array}{c}
      \emptyset | \emptyset \vdash t : A[T] \to \emptyset \\
      \emptyset | \emptyset \vdash t : A[T[U]] \to \emptyset
    \end{array} \\
    \begin{array}{c}
      \emptyset | x : A[T[U]] \vdash t : A[T[U]] \\
      \emptyset | x : A[T[U]] \vdash t : B[U]
    \end{array}
  \end{array}
}{
  \begin{array}{c}
    \emptyset | x : A[T[U]] \vdash u (t x) : C \\
    \emptyset | \emptyset \vdash \lambda^\circ x. u (t x) : A[T[U]] \to \emptyset
  \end{array}
} $$

## B.2 Proof of Proposition 3.1

We follow Notation 3.3 throughout this subsection, writing $\Delta \vdash \dots$ instead of $\emptyset | \Delta \vdash \dots$.

Let us show something slightly stronger: for any $\Delta$ containing only purely affine types, and any purely affine type $A$, there are finitely many $\lambda\wp$-terms $t$ such that $\Delta \vdash t : A$, up to $\beta\eta$-conversion. Our proof is by strong induction on $|\Delta| + |A|$, where $|A|$ is the size of $A$ (as a syntax tree) and $|\Delta| = |B_1| + \dots + |B_n|$ for $\Delta = x_1 : B_1, \dots, x_n : B_n$.

If $A = C_1 \to \dots \to C_m \to o$, such a term admits an $\eta$-long form $t = \lambda y_1. \dots \lambda y_m. u$ where $\Delta$, $y_1 : C_1, \dots, y_m : C_m \vdash u : o$. Since $t$ is determined by $u$ (modulo $\beta\eta$), and $|\Delta| + |C_1| + \dots + |C_m| + o < |\Delta| + |A|$, we can apply the induction hypothesis to reduce to a case with $m=0$ i.e. $A = o$ and $t = u$. We assume these conditions for the rest of the proof.

Let $t$ be in head normal form: $t = z v_1 \dots v_p$. There are finitely many possible choices for $z$ in $\Delta$. Suppose we make one of these choices: $z : D = E_1 \to \dots \to E_p \to o$. Then for any $i \in \{1, \dots, p\}$, $|\Delta \setminus \{z\}| + |E_i| = |\Delta| - |D| + |E_i| = |\Delta| - (|D| - |E_i|) < |\Delta|$. The induction hypothesis then applies to show that there are finitely many possibilities for $v_i$: the fact that the variable $z$ can only be used once means that a typing judgment of the form $\Delta' \vdash v_i : E_i$ for some subsequence $\Delta' \setminus \{z\}$ must necessarily be proven as part of the typing derivation for $t$. This concludes the proof.

The reader may verify that our arguments can be applied verbatim to the commutative $\lambda a$-calculus of §5.

## B.3 Proof of Lemma 3.6

The $\beta$-normal $\eta$-long form of a closed $\lambda\wp$-term $t$ of type $\text{Str}_\Sigma[A] \to (o \to o \to o)$ (by definition of Bool) is

$$ t =_{\beta\eta} \lambda^\circ s. \lambda^\circ x. \lambda^\circ y. z t_1 \dots t_n \quad \text{where} \quad \emptyset | s : \text{Str}_\Sigma[A], x : o, y : o \vdash z t_1 \dots t_n : o $$

If $z \in \{x, y\}$, then $n=0$ and $t$ is a constant function from strings to booleans: the statement of Lemma 3.6 is true with $g_c = \lambda^\circ a. a$ and $h = \lambda^\circ f. \lambda^\circ x. \lambda^\circ y. z$ (the latter is the constant function equal to either true or false depending on whether $z = x$ or $z = y$) or, said explicitly, $t =_{\beta\eta} \lambda^\circ s. (\lambda^\circ f. \lambda^\circ x. \lambda^\circ y. z) (s (\lambda^\circ a. a) \dots (\lambda^\circ a. a))$.

In the remaining case $z = s$, the $t_i$ must be closed $\lambda\wp$-terms for $i \le |\Sigma|$. That is because if they contained any free variable, it would necessarily be either $x$ or $y$, so it would be an affine variable. But since $s : (A \to A) \to \dots \to (A \to A) \to A \to A$ is non-affine in its $|\Sigma|$ first arguments, the dependency on this non-affine variable would contradict the elimination rule for `→` (cf. Figure 1) which requires the emptiness of the affine context for the argument – this is analogous to the condition for the promotion rule of linear logic. This ensures that one can take $g_{c_i} = t_i$ for $i \in \{1, \dots, |\Sigma|\}$. To conclude, observe that $h = \lambda^\circ f. \lambda^\circ x. \lambda^\circ y. f t_{|\Sigma|+1} \dots t_n$ works ($s t_1 \dots t_n$ already uses the affine variable $s$ once, so the $t_j$ for $j \in \{|\Sigma|+1, \dots, n\}$ can only have $x$ and $y$ as free variables).
## B.4 Proof of Lemma 4.2

Since $L$ is star-free, $L = \varphi^{-1}(P)$ for some $\varphi \in \operatorname{Hom}(\Sigma^*, M)$ and $P \subseteq M$, where $M$ is an aperiodic monoid. Here is a sequential transducer computing $\chi_L: Q = M, q_I = e$ (the identity element of $M$), $\delta(m, c) = (m\varphi(c), \varepsilon)$, $F(m) = 1$ if $m \in P$ and $F(m) = \varepsilon$ otherwise. Its transition monoid is isomorphic to $\varphi(\Sigma^*) \subseteq M$, which is aperiodic.

## B.5 Proof of Lemma 4.3

The $\lambda\delta$-term in question is $\text{nonempty} = \lambda^\circ s. s (\lambda^\circ x. \text{true}) \text{false}$.

### C Typing derivations for the proof of Lemma 4.10

We set $\Gamma = \{f_a : S \mid a \in \Pi\}$. Recall that $S = o \dashv o$, $T = S \dashv S$ and $A = T \dashv T \dashv S$.

### C.1 $\mathit{cat} = \lambda^\circ w. \lambda^\circ w'. \lambda^\circ x. w (w' x)$

$$ \begin{array}{c} \frac{\Gamma \mid w : S \vdash w : S = o \dashv o}{\Gamma \mid w' : S \vdash w' : S = o \dashv o} \qquad \frac{\Gamma \mid w' : S, x : o \vdash w' x : o}{\Gamma \mid w' : S, x : o \vdash x : o} \\ \frac{\Gamma \mid w : S, w' : S, x : o \vdash w (w' x) : o}{\Gamma \mid w : S, w' : S \vdash \lambda^\circ x. w (w' x) : o \dashv o} \\ \frac{\Gamma \mid w : S \vdash \lambda^\circ w'. \lambda^\circ x. w (w' x) : S \dashv o \dashv o}{\Gamma \mid \emptyset \vdash \lambda^\circ w'. \lambda^\circ x. w (w' x) : S \dashv S \dashv o \dashv o} \end{array} $$

### C.2 $\mathit{zeta} = \lambda^\circ w'. \lambda^\circ x. x$

$$ \frac{\frac{\Gamma \mid x : o \vdash x : o}{\Gamma \mid w' : S, x : o \vdash x : o} \qquad \Gamma \mid w' : S \vdash \lambda^\circ x. x : o \dashv o}{\Gamma \mid \emptyset \vdash \lambda^\circ w'. \lambda^\circ x. x : S \dashv o \dashv o} $$

### C.3 $\mathit{trans}_c$ for $c \in \Sigma$

We only treat the case $\delta_{\text{st}}(q, c) = q$ (the other ones involve rather similar computations):

$$ \mathit{trans}_c = \lambda^\circ k. \lambda^\circ h. \lambda^\circ g. k (\lambda^\circ y. h (\mathit{cat} u_1 y)) (\lambda^\circ z. g (\mathit{cat} u_2 z)) $$

First of all, for $q \in Q = \{1, 2\}$, since $u_q = \delta_{\text{out}}(q, c)^{\dagger}(f_{\Pi})$ and $(f_a : o \dashv o) \in \Gamma$ for all $a \in \Pi$, by Proposition 2.5 we have $\Gamma \mid \emptyset \vdash u_q : o \dashv o$.

We start by typing a subterm:

$$ \begin{array}{c} \frac{\frac{\begin{array}{c} \text{[see Appendix C.1]} \\ \Gamma \mid \emptyset \vdash \mathit{cat} : S \dashv S \end{array}}{\Gamma \mid \emptyset \vdash u_1 : S}}{\Gamma \mid y : S \vdash \mathit{cat} u_1 y : S \dashv S} \qquad \frac{\begin{array}{c} \text{[see above]} \\ \Gamma \mid y : S \vdash y : S \end{array}}{\Gamma \mid y : S \vdash \mathit{cat} u_1 y : S} \\ \frac{\Gamma \mid h : T \vdash h : T}{\Gamma \mid h : T = S \dashv S, y : S \vdash h (\mathit{cat} u_1 y) : S} \qquad \frac{\Gamma \mid h : T \vdash \lambda^\circ y. h (\mathit{cat} u_1 y) : S \dashv S = T}{\Gamma \mid h : T \vdash \lambda^\circ y. h (\mathit{cat} u_1 y) : S \dashv S = T} \end{array} $$
Similarly, $\Gamma | g : T \vdash \lambda^\circ z. g (\mathbf{cat} \, u_2 \, z) : T$.

We can now type the full term, using $A = T \dashv S \dashv S$, so that $k : T \dashv S \dashv S$. For the same reason, the conclusion of the following derivation tree is indeed what we want: $\mathbf{trans}_c : A \dashv T \dashv T \dashv S = A \dashv A$.

$$ \frac{\begin{array}{c} \Gamma | k : A \vdash k : A \\ \Gamma | h : T \vdash \lambda^\circ y. h (\mathbf{cat} \, u_1 \, y) : T \\ \Gamma | k : A, h : T \vdash k (\lambda^\circ y. h (\mathbf{cat} \, u_1 \, y)) : T \dashv S \end{array}}{\begin{array}{c} \Gamma | g : T \vdash \lambda^\circ z. g (\mathbf{cat} \, u_2 \, z) : T \\ \Gamma | k : A, h : T, g : T \vdash k (\lambda^\circ y. h (\mathbf{cat} \, u_1 \, y)) (\lambda^\circ z. g (\mathbf{cat} \, u_2 \, z)) : S \\ \Gamma | \emptyset \vdash \lambda^\circ k. \lambda^\circ h. \lambda^\circ g. k (\lambda^\circ y. h (\mathbf{cat} \, u_1 \, y)) (\lambda^\circ z. g (\mathbf{cat} \, u_2 \, z)) : A \dashv T \dashv T \dashv S \end{array}} \text{[see above]} $$

**Aperiodicity vs non-commutativity, concretely** Let us substantiate the claim made in the main text that if the transition monoid on our two states were not aperiodic – that is, if for some $c \in \Sigma$ we had $\delta(q, c) = 3 - q$ – we would encounter a problem with non-commutative typing. The corresponding $\lambda_\phi$-term that we would want to write is very similar to the one we just successfully typed above:

$$ \lambda^\circ k. \lambda^\circ h. \lambda^\circ g. k (\lambda^\circ y. g (\mathbf{cat} \, u_2 \, y)) (\lambda^\circ z. h (\mathbf{cat} \, u_1 \, z)) $$

Its typing derivation must end with

$$ \frac{\begin{array}{c} \vdots \\ \Gamma | k : A, h : T, g : T \vdash k (\lambda^\circ y. g (\mathbf{cat} \, u_1 \, y)) (\lambda^\circ z. h (\mathbf{cat} \, u_2 \, z)) : S \end{array}}{\Gamma | \emptyset \vdash \lambda^\circ k. \lambda^\circ h. \lambda^\circ g. k (\lambda^\circ y. g (\mathbf{cat} \, u_2 \, y)) (\lambda^\circ z. h (\mathbf{cat} \, u_1 \, z)) : A \dashv T \dashv T \dashv S} $$

The next rule cannot be a weakening since $k, h, g$ all occur as affine free variables in the $\lambda_\phi$-term $k (\lambda^\circ y. g (\mathbf{cat} \, u_2 \, y)) (\lambda^\circ z. h (\mathbf{cat} \, u_1 \, z))$. Therefore, we must have, for some type $R$ and some affine contexts $\Delta, \Delta'$ such that $\Delta \cdot \Delta' = (k : A, h : T, g : T)$,

$$ \frac{\begin{array}{c} \vdots \\ \Gamma | \Delta \vdash k (\lambda^\circ y. g (\mathbf{cat} \, u_2 \, y)) : R \dashv S \\ \Gamma | \Delta \cdot \Delta' \vdash k (\lambda^\circ y. g (\mathbf{cat} \, u_2 \, y)) (\lambda^\circ z. h (\mathbf{cat} \, u_1 \, z)) : S \end{array}}{\Gamma | \Delta' \vdash \lambda^\circ z. h (\mathbf{cat} \, u_1 \, z) : R} $$

But this would lead to a contradiction: $g \in (\mathrm{FV}(k(\lambda^\circ y. g(\mathbf{cat} \, u_2 \, y))) \setminus \Gamma) \subseteq \Delta$ and $h \in \Delta'$ so $(g, h)$ would be an ordered subsequence of $(k, h, g)$.