# Rational functions via recursive schemes

Siddharth Bhaskar, Jane Chandlee, and Adam Jardine

##  1\. Introduction

One of the central notions of formal language theory is that of _regularity_.
The paradigmatic example of a regular language of finite strings over a finite
alphabet has been generalized in several directions. There are now robust
notions of regularity for other types of data (e.g., infinite strings and
trees), as well as for functions as opposed to languages. Each notion of
regularity can typically be characterized three ways: mechanically (via finite
automata), algebraically (via grammars), and logically (via fragments of
monadic second-order logic). Much of the enterprise of formal language theory
has concerned itself with extending the notion of regularity and making it
more robust.

The present paper is no exception. Here we are concerned with _function
classes_ over finite strings. These are perhaps most easily approached through
automata theory: a regular function is anything computable by a _transducer_ ,
a finite automaton whose transitions can print strings to output. However,
life is immediately more complicated: the equivalence between deterministic,
nondeterministic, one-way, and two-way automata are broken into three classes
in the case of transducers:

  1. (1)

One-way deterministic transducers compute the class of _subsequential_
functions.111Sometimes called _sequential_ , cf. [Sak09]. These are further
factored into _left-_ and _right-_ subsequential depending on which way the
transducer reads the string.

  2. (2)

One-way nondeterministic transducers compute the strictly larger class of
_rational_ functions; these are closed under string reversal even though the
transducer is one-way, and we do not have to factor into left and
right.222Note that whenever considering nondeterministic transducers, we
restrict ourselves to those that do compute functions, i.e., the output for a
given input is invariant of the sequence of nondeterministic choices.

  3. (3)

Two-way deterministic and nondeterministic transducers compute the yet
strictly larger class of _regular_ functions. (These are obviously closed
under string reversal.)

Each of these classes admits a logical characterization as well. These are in
the spirit of finite model theory: we interpret each string over a fixed
alphabet $\Sigma$ as a finite structure over a fixed signature, also called
$\Sigma$. The domain of the structure is the set of indices of the string, we
have a predicate for each character in the alphabet that picks out those
indices carrying that character, and we have some way of comparing or
operating on indices, such as a linear order or successor and predecessor
functions.

Under this identification of strings with finite structures, string languages
can be identified with spectra. This is the fundamental bridge between
automata-theoretic and logical characterizations of complexity classes. The
prototypical such characterization is the identification of regular string
languages with spectra of sentences in monadic second-order (MSO) logic
[B6̈0]. This was extended by Engelfriet and Hoogeboom to regular _functions_
and MSO-definable _interpretations_ [EH01].

#### A word on interpretations

Given two signatures $L$ and $K$, an interpretation $L\to K$ is a $K$-formula
for every symbol of $L$. This gives a map from $K$-structures to
$L$-structures: given a $K$-structure, we can interpret any $L$-symbol by its
$K$-definition.333Note the reversal in direction from $K$ to $L$; properly
formalized, we can define a contravariant semantics functor from
interpretations to the maps they define. If $L$ and $K$ are string alphabets
$\Sigma$ and $\Gamma$, then we can identify the set of finite $L$-structures
and $K$-structures with $\Sigma^{\star}$ and $\Gamma^{\star}$ respectively,
and an interpretation $L\to K$ defines a map
$\Gamma^{\star}\to\Sigma^{\star}$.

In formal language theory, we are interested in defining functions which
increase the string by at most a constant multiplicative factor. Following the
work of Engelfriet and Hoogeboom [EH01] (and ultimately Courcelle [Cou94]), we
identify indices of the defined $L$-string with single indices of the original
$K$-string. To increase the constant factor beyond 1, we are allowed to do
this a fixed finite number of times and merge the resulting copies.
Henceforth, when we say _interpretation_ , we mean an interpretation in this
sense.444The term _interpretation_ comes from model theory, where the domain
of the output structure is typically identified with _tuples_ , as opposed to
copies, of the input structure. (For example, complex numbers can be
identified with pairs of real numbers.) An alternate term used in formal
language theory is _transduction_.

#### Order-preservation.

Fix an interpretation $\pi$ from $\Sigma$ to $\Gamma$. Then if $s$ is some
$\Gamma$-string and $|s|$ is its set of indices, $\pi$ defines a
$\Sigma$-string whose set of indices is $m\times|s|$ for some fixed
$m\in\omega$. There is a $\Gamma$-formula in $\pi$ which defines the order of
these indices in the output string. An _order-preserving_ interpretation is
one which says: no, there is no such formula. Rather, you _must_ consider the
indices of the output string in the natural lexicographic order on
$m\times|s|$. Bojanczyk [Boj14] and Filiot [Fil15] found that by refining MSO-
interpretations to order-preserving MSO-interpretations, the resulting class
of computable functions drops from regular to rational.

#### Boolean monadic recursive schemes

The present authors [BCJO20] introduced the notion of a _boolean monadic
recursive scheme_ (BMRS), a weak programming language on strings, and found
that _one-way_ order-preserving BMRS interpretations compute exactly
subsequential functions. BMRS are motivated by considerations in computational
phonology, as they provide a formalism which simultaneously enforces the
“correct” computational upper bound while being flexible enough that
linguistically significant phenomena may be easily legible in the code [CJ21].

#### Our contributions

The _syntactic composition problem_ is: given two interpretations computing
functions $g$ and $f$, find an interpretation computing $g\circ f$. In the
present paper we solve the syntactic composition problem for order-preserving
BMRS interpretations.

Standard interpretations are naturally compositional. Given interpretations
$\pi:L\to K$ and $\rho:K\to J$, we can form an interpretation $L\to J$ by
substituting each occurrence of a $K$-symbol in the formulas of $\pi$ by the
corresponding $J$-formula of $\rho$.

Order-preserving interpretations, however, are _not_ naturally compositional:
they use the index ordering on the input string, but do not define them on the
output string. Compounding this, order-preserving interpretations are allowed
to skip indices of the output on which no character has been defined.555So,
even if the indices of the output are identified with $m\times|s|$, the output
string might have length less than $m|s|$. Naively, it seems like composing
order-preserving interpretations would require some basic arithmetic to count
skipped indices, whereas BMRS lack any mechanism for counting.666We write BMRS
for both the singular and plural of a boolean monadic recursive scheme. This
acronym has come to be pronounced _beamers_ in the plural and _beamer_ in the
singular via back-formation.

Our core technical contribution is a fine analysis of the syntactic
composition problem for order-preserving interpretations. We factor this
syntactic composition problem into four parts, three of which are routine and
go through in practically any logic. The last is difficult in the absence of
counting and requires, it seems, precisely the computational power of a BMRS.

As a consequence of this analysis, we find that _order-preserving BMRS
interpretations compute the class of rational functions_. Any rational
function can be factored as a composition of a left and right subsequential
function [EM65]. By our previous paper, each of these can be computed by a
one-way BMRS; by the current paper, their composition is computed by a BMRS.
In other words, while each BMRS interpretation is easily seen to be an MSO
interpretation, we show that the converse is true as well. This result,
combined with that of our previous paper, shows that there are natural BMRS
characterizations of both the subsequential and rational functions—a
characterization not (currently) available to MSO logic.

#### Related work

The monadic fragments of various programming languages already attracted
attention from the early days of schematology, as they were often found to
combine nontrivial expressive power while being more tractable than general
recursive programs. In formal language theory, monadic logics such as MSO
occupy a place of central importance. The relationship between MSO and various
monadic first-order logics equipped with a mechanism for recursion (such as
monadic least fixed-point logic and monadic datalog) is an important one, and
these are known to be as powerful as MSO over string and tree data, as least
for boolean queries [Sch06].777At least one paper notes that such results are
folklore in the database community, cf. [GK04].

Despite the differences in our approach—our choice of string primitives,
considering interpretations instead of simple queries, etc.—we surmise that
our characterization of rational functions by order-preserving BMRS
interpretations could probably be cobbled together out of known results. What
we believe we have, however, is a genuinely new proof—one that comes out of
solving the syntactic composition problem for order-preserving BMRS
interpretations instead of a direct simulation of a given MSO interpretation.

#### Structure of this paper

Section 2 gives a model-theoretic definition of strings, Section 3 defines
BMRS over these structures, and Section 4 defines order-preserving BMRS
interpretations and shows how they define functions on strings. The technical
work is presented in Sections 5 and 6, which show how to compose order-
preserving BMRS interpretations; Section 7 uses this to establish that such
interpretations capture rational functions. Finally, Section 8 discusses
further directions.

##  2\. Strings as finite structures

We are concerned with finite _strings_ over a finite _alphabet_ , or some
nonempty set of symbols. We typically use capital Greek letters (e.g.,
$\Sigma$, $\Gamma$, $\Delta$) to name alphabets, and lowercase Latin letters
(e.g., $s$, $t$) to name strings.

Strings over an alphabet $\Sigma$ can be associated with a first-order
_signature_ , also written $\Sigma$.

######  Definition 1.

Given an alphabet $\Sigma$, the signature $\Sigma$ consists of:

  * •

a monadic (i.e., unary) relation symbol $\sigma$ for each character
$\sigma\in\Sigma$,

  * •

monadic relation symbols $\max$ and $\min$, and

  * •

monadic function symbols $\mathrm{S}$ and $\mathrm{P}$ (for _successor_ and
_predecessor_).

Where the distinctions are necessary, we will refer to the elements of the
alphabet $\Sigma$ as the _characters_ of $\Sigma$, and the functions and
relations in the signature $\Sigma$ as the _primitives_ of $\Sigma$.

We also identify each string in $\Sigma^{\star}$ with a finite
$\Sigma$-structure as follows.

######  Definition 2.

Given a string $s\in\Sigma^{\star}$, let the $\Sigma$-structure, also called
$s$, have as a domain the set of indices of $s$ (which we represent with an
initial segment of the natural numbers), and for an index $x$ of $s$, let

  * •

$s\models\sigma(x)$ iff character of $s$ at index $x$ is $\sigma$,

  * •

$s\models\min(x)$ iff $x$ is the least index $0$,

  * •

$s\models\max(x)$ iff $x$ is the greatest index $|s|-1$,

  * •

$s\models\mathrm{S}(x)=y$ iff $y=x+1$ or $x=y=|s|-1$, and

  * •

$s\models\mathrm{P}(x)=y$ iff $y=x-1$ or $x=y=0$.

Note that successor and predecessor fix the greatest and least indices
respectively. Note as well that a finite $\Sigma$-structure is a string if and
only if for each $x<|s|$, $s\models\sigma(x)$ for a unique character
$\sigma\in\Sigma$. Without risk of ambiguity we often conflate strings in
$\Sigma^{\star}$ with their first-order structure over the signature $\Sigma$.
Furthermore, we adopt the set-theoretic convention that identifies a natural
number with its set of predecessors, i.e., $n=\\{0,1,\dots,n-1\\}$. This
allows us to identify the domain of a string $s$ with its _length_ $|s|$.

##  3\. Boolean monadic recursive schemes

We now define _boolean monadic recursive schemes_ (BMRS), a programming
language first introduced in [BCJO20]. These are presented in a pure
functional style and equipped with a standard big-step environment-based
semantics.888Our presentation is particularly influenced by McCarthy [McC59]
via Moschovakis [Mos19].

Programs are executed relative to a given finite string. Program variables
range over two types of data: booleans $\mathbf{bool}$ and string indices
$\mathbf{ind}$. Each recursive function symbol in a boolean monadic recursive
scheme is required to have type $\mathbf{ind}\to\mathbf{bool}$; i.e., they are
_boolean_ -valued and _monadic_ (i.e., have a single input variable), hence
the name.

These twin requirements impose quite stringent limitations on the expressive
power of boolean monadic recursive schemes. For example, our inability to
program functions of type $\mathbf{ind}\to\mathbf{ind}$ means that we cannot
do arithmetic on string indices to, e.g., locate the halfway point of a
string. Our inability to program functions of type
$\mathbf{ind}\times\mathbf{ind}\to\mathbf{bool}$ means we cannot cheat by
computing the graph relation of a function $\mathbf{ind}\to\mathbf{ind}$. The
fact that inputs and outputs are of different types prohibits nested recursive
calls.

We first define terms, then programs, and then their semantics. We use
typewriter script for program syntax (i.e., program variables and keywords—the
purely logical elements of our programming language). We fix a countably
infinite set $\mathcal{F}$ of recursive function names, and a single variable
$\mathtt{x}$ of type $\mathbf{ind}$.

######  Definition 3.

Given a signature $\Sigma$, a _$\Sigma$ -term_ is any term that can be derived
from the inference rules in Figure 1.

$\mathtt{x}:\mathbf{ind}$ $T:\mathbf{ind}$ $\mathrm{P}(T):\mathbf{ind}$
$T:\mathbf{ind}$ $\mathrm{S}(T):\mathbf{ind}$ $\mathtt{tt}:\mathbf{bool}$
$\mathtt{ff}:\mathbf{bool}$ $T:\mathbf{ind}$ $\mathtt{f}\in\mathcal{F}$
$\mathtt{f}(T):\mathbf{bool}$ $T:\mathbf{ind}$ $\sigma(T):\mathbf{bool}$
$T:\mathbf{ind}$ $\max(T):\mathbf{bool}$ $T:\mathbf{ind}$
$\min(T):\mathbf{bool}$ $T_{0}:\mathbf{bool}$ $T_{1}:\mathbf{ind}$
$T_{2}:\mathbf{ind}$ $\mathtt{if}\ T_{0}\ \mathtt{then}\ T_{1}\ \mathtt{else}\
T_{2}:\mathbf{ind}$ $T_{0}:\mathbf{bool}$ $T_{1}:\mathbf{bool}$
$T_{2}:\mathbf{bool}$ $\mathtt{if}\ T_{0}\ \mathtt{then}\ T_{1}\
\mathtt{else}\ T_{2}:\mathbf{bool}$

Figure 1. $\Sigma$-terms. Here $\sigma$ ranges over the characters of
$\Sigma$.

######  Definition 4.

A _headless $\Sigma$-boolean monadic recursive scheme_ is a finite set of
lines

$\displaystyle\mathtt{f}_{0}(\mathtt{x})$ $\displaystyle=T_{0}$
$\displaystyle\mathtt{f}_{1}(\mathtt{x})$ $\displaystyle=T_{1}$
$\displaystyle\vdots$ $\displaystyle\mathtt{f}_{k}(\mathtt{x})$
$\displaystyle=T_{k}$

such that for each $0\leq i\leq k$, $T_{i}$ is a $\Sigma$-term which does not
contain any other recursive function names other than
$(\mathtt{f}_{0},\dots,\mathtt{f}_{k})$.999Note that this is a _set_ rather
than a _list_ of lines; the order does not matter. However, overwhelming
programming intuition compels us to present it like a list.

For a headless BMRS $p=\\{\mathtt{f}_{i}(\mathtt{x})=T_{i}\\}_{0\leq i\leq
k}$, by a _$p$ -term_ we mean a term in which no recursive function name
occurs besides $(\mathtt{f}_{0},\dots,\mathtt{f}_{k})$. In particular, each
$T_{i}$ is a $p$-term.

######  Definition 5 (Semantics).

Let $\Sigma$ be a signature, $s$ be a $\Sigma$-string, $x$ be an index of $s$,
$p$ be a headless $\Sigma$-BMRS, $T$ be a $p$-term, and $v$ be a value whose
type agrees with $T$. We define the five-place relation $s,x\vdash_{p}T\to v$
according to the inference rules in Figure 2.

$x\vdash\mathtt{x}\to x$ $x\vdash\mathtt{tt}\to\top$
$x\vdash\mathtt{ff}\to\bot$ $x\vdash T\to v$ (if $v>0$)
$x\vdash\mathrm{P}(T)\to v-1$ $x\vdash T\to v$ (if $v=0$)
$x\vdash\mathrm{P}(T)\to v$ $x\vdash T\to v$ (if $v<|s|-1$)
$x\vdash\mathrm{S}(T)\to v+1$ $x\vdash T\to v$ (if $v=|s|-1$)
$x\vdash\mathrm{S}(T)\to v$ $x\vdash T\to v$ (if $v>0$)
$x\vdash\min(T)\to\bot$ $x\vdash T\to v$ (if $v=0$) $x\vdash\min(T)\to\top$
$x\vdash T\to v$ (if $v<|s|-1$) $x\vdash\max(T)\to\bot$ $x\vdash T\to v$ (if
$v=|s|-1$) $x\vdash\max(T)\to\top$ $x\vdash T\to v$ (if $s_{v}=\sigma$)
$x\vdash\sigma(T)\to\top$ $x\vdash T\to v$ (if $s_{v}\neq\sigma$)
$x\vdash\sigma(T)\to\bot$ $x\vdash T\to v$ $s,v\vdash T^{\mathtt{f}}\to w$
$x\vdash\mathtt{f}(T)\to w$ $x\vdash T_{0}\to\top$ $x\vdash T_{1}\to v$
$x\vdash\mathtt{if}\ T_{0}\ \mathtt{then}\ T_{1}\ \mathtt{else}\ T_{2}\to v$
$x\vdash T_{0}\to\bot$ $x\vdash T_{2}\to v$ $x\vdash\mathtt{if}\ T_{0}\
\mathtt{then}\ T_{1}\ \mathtt{else}\ T_{2}\to v$

Figure 2. Program semantics, $s$ and $p$ omitted for legibility. For a
recursive function name $p$, $T^{\mathtt{f}}$ is its recursive definition in
$p$, and for an index $v$, $s_{v}$ is the character of $s$ at $v$.

Finally, we give our boolean monadic recursive schemes heads. Unlike the
recursive programs of [Mos19], we allow for the possibility of multiheaded
programs.

######  Definition 6.

For a signature $\Sigma$, a $\Sigma$-boolean monadic recursive scheme is
composed of a headless $\Sigma$-boolean monadic recursive scheme $p$ along
with a finite nonempty collection of $p$-terms, called the _heads_.

Following [Mos19], given a $\Sigma$-BMRS, we call the underlying headless part
its _body_. We extend the usage of $s,x\vdash_{p}T\to v$ to include $p$ which
have heads; in this case, remember that the meaning of $\vdash$ does not
depend on them.

Finally, we define two important subclasses of programs.

######  Definition 7.

A $\mathrm{BMRS}^{\mathrm{P}}$, or _predecessor_ BMRS, is one in which the
successor function $\mathrm{S}$ does not occur. Similarly a
$\mathrm{BMRS}^{\mathrm{S}}$, or _successor_ BMRS, is one in which the
predecessor function $\mathrm{P}$ does not occur.

##  4\. Interpretations

######  Definition 8.

Let $\Sigma$ and $\Gamma$ be alphabets. An ($m$-fold) interpretation
$\pi:\Sigma\times m\to\Gamma$ is a multiheaded $\Gamma$-BMRS $\pi$ with a head
$\pi(\sigma,i)$ for each character $\sigma\in\Sigma$ and $i<m$.

######  Definition 9.

An interpretation $\pi:\Sigma\times m\to\Gamma$ is _well-defined_ in case for
each string $s\in\Gamma^{\star}$, $i<m$, and $x<|s|$,
$s,x\vdash\pi(\sigma,i)\to\top$ for at most one $\sigma\in\Sigma$ and
$s,x\vdash\pi(\tau,i)\to\bot$ for every other $\tau\in\Sigma$.

It is additionally _strict_ if $s,x\vdash\pi(\sigma,i)\to\top$ for exactly one
$\sigma$.

######  Definition 10.

If $\pi:\Sigma\times m\to\Gamma$ is a well-defined interpretation, then the
_transduction induced by $\pi$_ is the function
$\mbox{$[[$}\pi\mbox{$]]$}:\Gamma^{\star}\to\Sigma^{\star}$ such that for
every $s\in\Gamma^{\star}$,

  * •

$|\mbox{$[[$}\pi\mbox{$]]$}(s)|=|J|$, where $J=\\{(q,r)\in|s|\times
m:(\exists\sigma\in\Sigma)\,s,q\models\pi(\sigma,r)\to\top\\}$, and

  * •

for each $x<|J|$, $\mbox{$[[$}\pi\mbox{$]]$}(s)\models\sigma(x)\iff
s,q\models\pi(\sigma,r)\to\top$, where $(q,r)$ is the unique element of $J$
with $x$ predecessors, where

  * •

$|s|\times m$ is ordered lexicographically, with $|s|$ being the more
significant and $m$ being the less significant coordinate.

In the important special case that $\pi$ is strict, this specializes to:

  * •

$|\mbox{$[[$}\pi\mbox{$]]$}(s)|=m|s|$, for every $s\in\Gamma^{\star}$, and

  * •

for each $x<m|s|$, $\mbox{$[[$}\pi\mbox{$]]$}(s)\models\sigma(x)\iff
s,q\vdash\pi(\sigma,r)\to\top,$ where $r$ and $q$ are the remainder and
quotient respectively of $x\div m$.

For example, let $\Gamma=\left\\{a\right\\}$, $\Sigma={7,8,9}$, and $m=3$. The
interpretation $\pi$ where $\pi(7,0)=\pi(8,1)=\pi(9,2)=a(\mathtt{x})$ defines
a function that takes a string $s$ of $|s|$ $a$ characters and returns a
string of length $|s|\times 3$ of the form $(789)^{|s|}$. To see how this
obtains, the following table shows how each index in the string $aaaa$ is
interpreted at each $m$-coordinate $i$: a $7$ at $m$-coordinate $0$, an $8$ at
$m$-coordinate $1$, and a $9$ at $m$-coordinate $2$.

$\begin{array}[t]{lllll}&0&1&2&3\\\ i&a&a&a&a\\\ \hline\cr 0&7&7&7&7\\\
1&8&8&8&8\\\ 2&9&9&9&9\\\ \end{array}$

By collating the copies of the indices of $aaaa$ first by order of index and
then by order of $i<3$, we obtain the string $789789789789$. Note that $\pi$
is strict.

The authors have previously shown [BCJO20] that order-preserving
$\mathrm{BMRS}^{\mathrm{P}}$ interpretations and order-preserving
$\mathrm{BRMS}^{\mathrm{S}}$ interpretations describe exactly the left-
subsequential functions and right-subsequential functions, viz.,

######  Theorem 1.

For any well-defined order-preserving $\mathrm{BMRS}^{\mathrm{P}}$ (resp.
$\mathrm{BMRS}^{\mathrm{S}}$) interpretation $\pi$,
$\mbox{$[[$}\pi\mbox{$]]$}$ is a left-subsequential (resp. right-
subsequential) function. Likewise, for any left-subsequential (resp. right-
subsequential) function $f$, $f=\mbox{$[[$}\pi\mbox{$]]$}$ for some order-
preserving $\mathrm{BMRS}^{\mathrm{P}}$ (resp. $\mathrm{BMRS}^{\mathrm{S}}$)
interpretation $\pi$.

This paper solves one of the questions left open in [BCJO20]; that is, to
characterize order-preserving BMRS interpretations in the presence of both
$\mathrm{P}$ and $\mathrm{S}$. It turns out that we get this more or less for
free from the solution of the syntactic composition problem.

Before moving on, we note that there is a natural notion of _substitution_ of
an interpretation into a program.

######  Definition 11.

Suppose $p$ is a headless $\Sigma$-BMRS and $\pi:\Sigma\times m\to\Gamma$ is
an interpretation. For each $i<m$, let $p^{\pi}_{i}$ be the $\Gamma$-BMRS
obtained from $p$ by replacing any occurrence of $\sigma$ with
$\pi(\sigma,i)$.

As stated this definition is a bit imprecise. Since the BMRS language contains
no let- or where- constructs that allow you to directly embed a program into
another program, what we mean is this: take $p$, stick a copy of the body of
$\pi$ underneath, and replace each occurrence of $\sigma$ by the head
corresponding to $\pi(\sigma,i)$. We trust that this is sufficiently
clear.101010A technical note: when we take the union of two headless programs,
we possibly rename recursive function names so there are no accidental
overlaps. Note that every $p$-term is a $p^{\pi}_{i}$-term.

Substitutions enjoy the following property.

######  Lemma 1.

For any well-defined strict interpretation $\pi:\Sigma\times m\to\Gamma$, any
string $s\in\Gamma^{\star}$, any headless $\Sigma$-BMRS $p$, any $p$-term $T$,
any $x<m|s|$, and any boolean $b\in\\{\top,\bot\\}$,

$\mbox{$[[$}\pi\mbox{$]]$}(s),x\vdash_{p}T\to b\iff
s,q\vdash_{p^{\pi}_{r}}T\to b,$

where $q<|s|$ and $r<m$ are the quotient and remainder respectively of $x\div
m$.

##  5\. Syntactic composition

We now turn to the following question: given two “composable” interpretations
$\pi:\Sigma\times m\to\Gamma$ and $\rho:\Delta\times n\to\Sigma$, how do we
define an interpretation $\omega:\Delta\times mn\to\Gamma$ such that
$\mbox{$[[$}\rho\mbox{$]]$}\circ\mbox{$[[$}\pi\mbox{$]]$}=\mbox{$[[$}\omega\mbox{$]]$}$?
This is an instance of a general problem in the theory of programming
languages, namely: how do we pull back a given semantic operation on functions
to a corresponding syntactic operation on the program texts
themselves?111111Cf. [Jon91] where such operations are called _symbolic_
rather than _syntactic_.

In most programming languages, the fact that programs _can_ be composed is not
in and of itself hard to show; the subtlety (if there is one) usually lies in
how efficient the composition can be made. However, this is not the case for
order-preserving BMRS interpretations. For example, suppose we wanted to
compose the interpretations $\rho$ and $\pi$ above. Loosely speaking, $\rho$
defines each function $\delta(x)$ (“index $x$ carries character $\delta$”),
for $\delta\in\Delta$, using $\sigma(x)$ as primitives, for $\sigma\in\Sigma$.
Similarly $\pi$ defines each function $\sigma(x)$, for $\sigma\in\Sigma$,
using $\gamma(x)$ as primitives, for $\gamma\in\Gamma$.

So one is tempted to define $\omega$ by taking $\rho$ and replacing each call
to $\sigma(x)$ by its definition in $\pi$. That is indeed the right idea. The
problem is that order-preserving interpretations are not _quite_
compositional: they use the successor and predecessor functions on the input
strings, but they are not required to define them on their output string.

This is not a huge problem for strict interpretations, in which index
successors and predecessors easily carry over from input to output strings.
(For example, in a strict 1-fold interpretation we can simply identify the
indices in the input and output strings.) Life gets more complicated, however,
for non-strict interpretations, which may _skip_ certain indices in the output
string. Naively, it would seem that to relate indices of the input and output,
a program would have to _count_ skipped indices, an impossibility in languages
with boolean-valued recursive functions. Overcoming this obstacle is the core
technical contributions of this paper.

In this section, we factor the problem of composing functions into several
sub-problems. The syntactic versions of all but one of these sub-problems are
routine, and we dispatch them in the present section. The final sub-problem
cuts to the heart of the matter, so we postpone it to its own section.

###  5.1. Four sub-problems

Say that a _sharply bounded function_ is a string function $f$ such that there
exists a natural number $n$ satisfying $|f(x)|\leq n|x|$, for each $x$ in the
domain of $f$. In this case, we say $f$ is _sharply bounded_ by $n$. Of
course, if $\pi$ is an $n$-fold interpretation, then
$\mbox{$[[$}\pi\mbox{$]]$}$ is sharply bounded by $n$. By analogy to
interpretations, say that a sharply bounded function $f$ is _strict_ if there
exists an $n$ such that $|f(x)|=n|x|$ for each $x$ in the domain of $f$.

The problem we want to consider is: given two sharply bounded functions
$f:\Gamma^{\star}\to\Sigma^{\star}$ and $g:\Sigma^{\star}\to\Delta^{\star}$
bounded by $n$ and $m$ respectively, how can we compose them to obtain $g\circ
f:\Gamma^{\star}\to\Delta^{\star}$ bounded by $nm$? Let’s say we know how to
compose _strict_ sharply bounded functions, and we want to reduce the general
problem to the strict case in the simplest way possible.

Suppose $\square$ is a character that appears neither in $\Sigma$, $\Delta$,
nor $\Gamma$. (We shall think of it as a “blank” character.) Let
$\Sigma_{\square}$, $\Delta_{\square}$, and $\Gamma_{\square}$ be obtained
from $\Sigma$, $\Delta$, and $\Gamma$ respectively by adding this blank
character. Then there is a natural _deletion_ map, e.g.,
$d_{\Sigma}:\Sigma^{\star}_{\square}\to\Sigma^{\star}$ that deletes all blank
characters from a given string. (So, e.g., $d(ab\square a\square\square)=aba$)
We shall abuse notation and just write $d$ for $d_{\Sigma}$, $d_{\Gamma}$,
etc.

Say that $f^{\prime}:\Gamma^{\star}\to\Sigma^{\star}_{\square}$ is a
_strictification_ of $f:\Gamma^{\star}\to\Sigma^{\star}$ in case both
functions are sharply bounded by the same bound, $f^{\prime}$ is strict, and
$d\circ f^{\prime}=f$. Any sharply bounded function admits a (non-unique)
strictification by arbitrarily padding each $f(x)$ with blanks until its
length is equal to $n|x|$. We might hope that we can obtain $g\circ f$ from
sharply bounded functions $f$ and $g$ by

  * •

finding two strictifications $f^{\prime}$ and $g^{\prime}$ of $f$ and $g$, and

  * •

composing them (i.e., $g^{\prime}\circ f^{\prime}$).

This has two problems. Less seriously, the codomain of $g^{\prime}$ is
$\Delta_{\square}^{\star}$ and not $\Delta^{\star}$. We fix this by simply
composing on the outside by $d:\Delta^{\star}_{\square}\to\Delta^{\star}$, an
easy operation on program codes. More seriously, $f^{\prime}$ and $g^{\prime}$
are not composable, as the codomain of $f^{\prime}$ and the domain of
$g^{\prime}$ are not identical
($f^{\prime}:\Gamma^{\star}\to\Sigma^{\star}_{\square}$ while
$g^{\prime}:\Sigma^{\star}\to\Delta^{\star}_{\square}$). Naively we might try
to fix this by replacing $f^{\prime}$ by $d\circ f^{\prime}$, until we
realized that we are now tasked with composing the (non-strict) $d\circ
f^{\prime}$ with $g$, placing us right back where we started.

Instead, we convert $g^{\prime}:\Sigma^{\star}\to\Delta_{\square}^{\star}$
into another strict function
$g_{b}:\Sigma^{\star}_{\square}\to\Delta^{\star}_{\square}$ such that $d\circ
g_{b}=d\circ g^{\prime}\circ d$, i.e., the following diagram commutes:

${{\Sigma^{\star}_{\square}}}$${{\Delta^{\star}_{\square}}}$${{\Delta^{\star}}}$${{\Sigma^{\star}}}$${{\Delta^{\star}_{\square}}}$$\scriptstyle{d}$$\scriptstyle{d}$$\scriptstyle{g^{\prime}}$$\scriptstyle{g_{b}}$$\scriptstyle{d}$

In which case,

$d\circ g_{b}\circ f^{\prime}=d\circ g^{\prime}\circ d\circ f^{\prime}=g\circ
f$

which is what we wanted to compute in the first place. Diagrammatically,

${{\Sigma^{\star}_{\square}}}$${{\Delta^{\star}_{\square}}}$${{\Delta^{\star}_{\square}}}$${{\Delta^{\star}}}$${{\Gamma^{\star}}}$${{\Sigma^{\star}}}$$\scriptstyle{g}$$\scriptstyle{d}$$\scriptstyle{d}$$\scriptstyle{g^{\prime}}$$\scriptstyle{f}$$\scriptstyle{f^{\prime}}$$\scriptstyle{g_{b}}$$\scriptstyle{d}$

Therefore, we have factored the problem of composing $g$ with $f$ into the
following subtasks:

  1. (1)

Strictifying $f$ into $f^{\prime}$ and $g$ into $g^{\prime}$.

  2. (2)

Lifting $g^{\prime}$ to $g_{b}$, which we call _blank-enrichment_.

  3. (3)

Composing strict functions $g_{b}$ and $f^{\prime}$.

  4. (4)

De-strictifying $(g_{b}\circ f^{\prime})$ into $d\circ(g_{b}\circ
f^{\prime})$.

Of these, strictifying and de-strictifying are the simplest to realize as
operations on program codes, and we deal with them first. Composition of
strict interpretations is straightforward, thought it takes some care to state
and verify cleanly. Blank-enrichment is the most complicated, requiring both
new ideas and attention to technical detail, and it is this which we postpone
to the end.

###  5.2. Strictification

This is perhaps the easiest transformation on program codes. Given an
interpretation $\pi:\Sigma\times m\to\Gamma$, we define
$\pi^{\prime}:\Sigma_{\square}\times m\to\Gamma$ by simply saying that an
index of the input string carries the blank character $\square$ in
$\pi^{\prime}$ when that index carries no character in $\pi$. This has the
effect that $\mbox{$[[$}\pi^{\prime}\mbox{$]]$}$ is obtained by stuffing
$\square$ where $\mbox{$[[$}\pi\mbox{$]]$}$ had nothing, effectively
strictifying it. More precisely:

######  Definition 12.

Given $\pi:\Sigma\times m\to\Gamma$, let $\pi^{\prime}:\Sigma_{\square}\times
m\to\Gamma$ have the same body as $\pi$. Define its heads by:

  * •

$\pi^{\prime}(\sigma,i)\equiv\pi(\sigma,i)$ for each $i$ and
$\sigma\neq\square$, and

  * •

$\pi^{\prime}(\square,i)\equiv\bigwedge_{(\sigma\neq\square)}\neg\pi(\sigma,i)$.121212This
should be regarded as syntactic sugar for a list of if-then-else statements.

Then we have:

######  Lemma 2.

If $\pi$ is well-defined, then $\pi^{\prime}$ is well-defined and strict;
moreover,
$d\circ\mbox{$[[$}\pi^{\prime}\mbox{$]]$}=\mbox{$[[$}\pi\mbox{$]]$}$.

###### Proof.

Fix $s\in\Gamma^{\star}$, $i\in m$, and $x<|s|$. If
$s,x\vdash\pi(\sigma,i)\to\top$ for some $\sigma\in\Sigma$ then
$s,x\vdash\pi^{\prime}(\sigma,i)\to\top$ for just that $\sigma$, and
$s,x\vdash\pi^{\prime}(\square,i)\to\bot$. If $s,x\vdash\pi(\sigma,i)\to\top$
for no $\sigma\in\Sigma$, then the same is true of $\pi^{\prime}$; moreover,
$s,x\vdash\pi^{\prime}(\square,i)\to\top$. This shows that $\pi^{\prime}$ is
well-defined and strict.

To show that
$d\circ\mbox{$[[$}\pi^{\prime}\mbox{$]]$}=\mbox{$[[$}\pi\mbox{$]]$}$, it
suffices to show that for every $\Gamma$-string $s$ and index $x$ of
$\mbox{$[[$}\pi\mbox{$]]$}(s)$, if $\mbox{$[[$}\pi\mbox{$]]$}(s)$ carries
$\sigma$ at index $x$, then $\mbox{$[[$}\pi^{\prime}\mbox{$]]$}(s)$ carries
$\sigma$ at index $y$, where $y$ is the index of
$\mbox{$[[$}\pi^{\prime}\mbox{$]]$}(s)$ with $x$ non-blank predecessors.

Fix a string $s\in\Gamma^{\star}$. The indices of
$\mbox{$[[$}\pi\mbox{$]]$}(s)$ can be identified with the set $J$ of pairs
$(q,r)\in|s|\times m$ such that $s,q\models\pi(\sigma,r)\to\top$ for some
$\sigma\in\Sigma$. Since $\pi^{\prime}$ is strict, the indices of
$\mbox{$[[$}\pi\mbox{$]]$}(s)$ can be identified simply with the set
$|s|\times m$. Order this set lexicographically, first on $q$ then on $r$, and
let $J$ inherit the induced order as a subset.

Now fix $x<|\mbox{$[[$}\pi\mbox{$]]$}(s)|$. There is a unique
$\sigma\in\Sigma$ such that $\mbox{$[[$}\pi\mbox{$]]$}(s)\models\sigma(x)$.
Let $(q,r)$ be the unique element of $J$ with $x$ predecessors. Then
$s,q\models\pi(\sigma,r)\to\top$, so
$s,q\models\pi^{\prime}(\sigma,r)\to\top$, which says that
$\mbox{$[[$}\pi^{\prime}\mbox{$]]$}(s)\models\sigma(mq+r)$. But $mq+r$ is
exactly the index of $\mbox{$[[$}\pi^{\prime}\mbox{$]]$}(s)$ with $x$ non-
blank predecessors, which is exactly what we wanted to show. ∎

###  5.3. De-strictification

Suppose we have a well-defined, strict interpretation
$\pi:\Sigma_{\square}\times m\to\Gamma$, and we want to obtain a well-defined,
non-strict interpretation $\pi^{\dagger}:\Sigma\times m\to\Gamma$ such that
$\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}=d\circ\mbox{$[[$}\pi\mbox{$]]$}$. This
transformation is extremely simple: we simply take $\pi$ and “forget” each
$\pi(\square,i)$.

######  Definition 13.

Given $\pi$ as above, let $\pi^{\dagger}$ have the same body. For each $i<m$
and character $\sigma\in\Sigma$, let

$\pi^{\dagger}(\sigma,i)\equiv\pi(\sigma,i).$

Then we have:

######  Lemma 3.

If $\pi$ is a well-defined strict interpretation, then $\pi^{\dagger}$ is
well-defined; moreover,
$\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}=d\circ\mbox{$[[$}\pi\mbox{$]]$}$.

###### Proof.

To show that $\pi^{\dagger}$ is well-defined we don’t even need that $\pi$ is
strict; $\pi^{\dagger}$ trivially inherits well-definedness from $\pi$.

As in the proof of Lemma 2: to show that
$d\circ\mbox{$[[$}\pi\mbox{$]]$}=\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}$, it
suffices to show that for every $\Gamma$-string $s$ and index $x$ of
$\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}(s)$, if
$\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}(s)$ carries $\sigma$ at index $x$, then
$\mbox{$[[$}\pi\mbox{$]]$}(s)$ carries $\sigma$ at index $y$, where $y$ is the
index of $\mbox{$[[$}\pi\mbox{$]]$}(s)$ with $x$ non-blank predecessors. As
before, let $J$ be those pairs $(q,r)$ in $|s|\times m$ such that
$s,q\vdash\pi(\sigma,r)\to\top$ for some $\sigma\in\Sigma$.

Fix $s\in\Gamma^{\star}$ and an index $x$ of
$\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}(s)$. Let $\sigma$ be the character of
$\mbox{$[[$}\pi^{\dagger}\mbox{$]]$}(s)$ at $x$, so that
$s,q\vdash\pi(\sigma,r)\to\top$, where $(q,r)$ is the unique element of $J$
with $x$ predecessors. But then $mq+r$ is the index of
$\mbox{$[[$}\pi\mbox{$]]$}(s)$ with $x$ non-blank predecessors, which is what
we wanted to show. ∎

###  5.4. Strict composition

Suppose that we have two strict interpretations $\pi:\Sigma\times m\to\Gamma$
and $\rho:\Delta\times n\to\Sigma$. How can we construct a strict
interpretation $\mu:\Delta\times mn\to\Gamma$ such that
$\mbox{$[[$}\mu\mbox{$]]$}=\mbox{$[[$}\rho\mbox{$]]$}\circ\mbox{$[[$}\pi\mbox{$]]$}$?

Consider the following example for motivation. Suppose that
$\Gamma=\\{0,1\\}$, $\Sigma=\\{a,b,c\\}$, $m=2$, $\Delta=\\{8,9\\}$, and
$n=3$. Suppose that $\mbox{$[[$}\pi\mbox{$]]$}(010)=abbcaa$, and
$\mbox{$[[$}\rho\mbox{$]]$}(abbcaa)=988989998998998899$ i.e.,

| 0 | 1 | 0
---|---|---|---
$c_{0}$ | $a$ | $b$ | $a$
$c_{1}$ | $b$ | $c$ | $a$

| $a$ | $b$ | $b$ | $c$ | $a$ | $a$
---|---|---|---|---|---|---
$c_{0}$ | 9 | 9 | 9 | 9 | 9 | 8
$c_{1}$ | 8 | 8 | 9 | 9 | 9 | 9
$c_{2}$ | 8 | 9 | 8 | 8 | 8 | 9

Then we want $\mbox{$[[$}\mu\mbox{$]]$}(010)=988989998998998899$, i.e.,

| 0 | 1 | 0
---|---|---|---
$c_{0}$ | 9 | 9 | 9
$c_{1}$ | 8 | 9 | 9
$c_{2}$ | 8 | 8 | 8
$c_{3}$ | 9 | 9 | 8
$c_{4}$ | 8 | 9 | 9
$c_{5}$ | 9 | 8 | 9

We can form this new table from the two old ones like so:

| 0 | 1 | 0
---|---|---|---
$c_{0}$ | 9 | 9 | 9
$c_{1}$ | 8 | 9 | 9
$c_{2}$ | 8 | 8 | 8
$c_{3}$ | 9 | 9 | 8
$c_{4}$ | 8 | 9 | 9
$c_{5}$ | 9 | 8 | 9

Each double-edge box is a “tile.” We take the first table and replace each
$a$, $b$, and $c$ by the appropriate tile obtained by the second table. Out of
the 6 copies $c_{0},\dots,c_{5}$ in the composed table, the quotient upon
division by $3$ tells us which copy ($c_{0}$ or $c_{1}$) to look at in the
first table, and the remainder ($c_{0}$, $c_{1}$, or $c_{2}$) tells us which
copy to look up in the second table. This suggests the following definition of
composition.

######  Definition 14.

Given an interpretation $\pi:\Sigma\times m\to\Gamma$ and $\rho:\Delta\times
n\to\Sigma$, define an interpretation $(\rho\otimes\pi):\Delta\times
mn\to\Gamma$ as follows:

  * •

The body of $\rho\otimes\pi$ is the union of the bodies of $\rho^{\pi}_{q}$,
for each $q\in m$.131313Another technical note: each $\rho^{\pi}_{q}$ contains
a copy of the body of $\pi$. These can be identified in the union. Otherwise,
the recursive function symbols in each component must be renamed so they are
not identified in the union.

  * •

For every $i\in mn$, let $q$ and $r$ be the integer quotient and remainder
respectively of $i\div n$. (Then $r\in n$ and $q\in m$.) For every
$(\delta,i)\in\Delta\times mn$, let the head $(\rho\otimes\delta)(\delta,i)$
be $\rho(\delta,r)^{\pi}_{q}$, i.e., the term obtained from $\rho(\delta,r)$
by replacing each occurrence of any $\sigma$ by $\pi(\sigma,q)$.

First observe that this transformation preserves strictness: if $\pi$ and
$\rho$ are well-defined and strict, then so is $\rho\otimes\pi$. Next, we
prove correctness:

######  Lemma 4.

$\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}=\mbox{$[[$}\rho\mbox{$]]$}\circ\mbox{$[[$}\pi\mbox{$]]$}$.

###### Proof.

We know that the strings $\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}(s)$ and
$\mbox{$[[$}\rho\mbox{$]]$}(\mbox{$[[$}\pi\mbox{$]]$}(s))$ each have length
$mn|s|$. For each $x<mn|s|$ and $\delta\in\Delta$, we must show that

$\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}(s)\models\delta(x)\iff\mbox{$[[$}\rho\mbox{$]]$}(\mbox{$[[$}\pi\mbox{$]]$}(s))\models\delta(x).$

Let $q<|s|$ and $r<mn$ be the quotient and remainder respectively of $x\div
mn$. Then $x=mn\cdot q+r$. Let $q^{\prime}<m$ and $r^{\prime}<n$ be the
quotient and remainder respectively of $r$ upon division by $n$. Then
$r=n\cdot q^{\prime}+r^{\prime}$, and $x=n\cdot(m\cdot
q+q^{\prime})+r^{\prime}$. Hence $r^{\prime}$ is also the remainder of $x\div
n$, and the quotient $q^{\dagger}$ of $x\div n$ is $m\cdot q+q^{\prime}$.
Observe that the quotient and remainder of $q^{\dagger}\div m$ are $q$ and
$q^{\prime}$ respectively.

By definition of $\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}$,

$\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}(s)\models\delta(x)\iff
s,q\vdash(\rho\otimes\pi)(\delta,r)\to\top.$

By definition of $\otimes$, $(\rho\otimes\pi)(\delta,r)$ is
$\rho(\delta,r^{\prime})^{\pi}_{q^{\prime}}$, so

$\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}(s)\models\delta(x)\iff
s,q\vdash\rho(\delta,r^{\prime})^{\pi}_{q^{\prime}}\to\top.$

On the other hand,

$\mbox{$[[$}\rho\mbox{$]]$}(\mbox{$[[$}\pi\mbox{$]]$}(s))\models\delta(x)\iff\mbox{$[[$}\pi\mbox{$]]$}(s),q^{\dagger}\vdash\rho(\delta,r^{\prime})\to\top,$

by definition of $\mbox{$[[$}\rho\mbox{$]]$}$. By Lemma 1,

$\mbox{$[[$}\pi\mbox{$]]$}(s),q^{\dagger}\vdash\rho(\delta,r^{\prime})\to\top\iff
s,q\vdash\rho(\delta,r^{\prime})^{\pi}_{q^{\prime}}\to\top.$

Hence, by composing these equivalences,

$\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}(s)\models\delta(x)\iff\mbox{$[[$}\rho\mbox{$]]$}(\mbox{$[[$}\pi\mbox{$]]$}(s))\models\delta(x),$

which is what we wanted to show. ∎

##  6\. Blank enrichment

We now tackle the following problem: given a strict interpretation
$\pi:\Sigma_{\square}\times m\to\Gamma$, find a strict interpretation
$\pi_{b}:\Sigma_{\square}\times m\to\Gamma_{\square}$ such that
$d\circ\mbox{$[[$}\pi_{b}\mbox{$]]$}=d\circ\mbox{$[[$}\pi\mbox{$]]$}\circ d$.
The following terminology is helpful in understanding how this works. For a
string $s\in\Gamma_{\square}^{\star}$, call $d(s)$ its _underlying_
$\Gamma^{\star}$-string. Conversely, call any member of the $d$-preimage of a
$\Gamma^{\star}$-string $s$ a _padding_ of $s$. Call two strings
$s,t\in\Gamma_{\square}^{\star}$ _siblings_ if $d(s)=d(t)$, i.e., they have
the same underlying string.

Now what we want is to construct $\pi_{b}$ such that for any string
$s\in\Gamma_{\square}^{\star}$, $\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ and
$\mbox{$[[$}\pi\mbox{$]]$}(t)$ are siblings, where $t$ is the underlying
string of $s$. Of course, there are many ways to do this. We do so in the most
straightforward way possible. For example, if $m=1$, we simply reproduce
$\square$ in $\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ wherever $s$ has a blank, then
fill in $\mbox{$[[$}\pi\mbox{$]]$}(t)$ in the remaining spaces. For example,
let $\Gamma=\\{0,1\\}$, $\Sigma_{\square}=\\{a,b,\square\\}$. Then we would
want to define $\pi_{b}$ such that:

  * •

if $\mbox{$[[$}\pi\mbox{$]]$}(00)=ab$,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(00\square)=ab\square$;

  * •

if $\mbox{$[[$}\pi\mbox{$]]$}(00)=ab$, $\mbox{$[[$}\pi_{b}\mbox{$]]$}(0\square
0)=a\square b$;

  * •

if $\mbox{$[[$}\pi\mbox{$]]$}(01)=b\square$,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(0\square 1)=b\square\square$,

  * •

if $\mbox{$[[$}\pi\mbox{$]]$}(01)=b\square$,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(\square 01)=\square b\square$,

  * •

if $\mbox{$[[$}\pi\mbox{$]]$}(010011)=aabbab$,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(01\square 00\square 11)=aa\square bb\square
ab$;

  * •

if $\mbox{$[[$}\pi\mbox{$]]$}(010011)=aabbab$,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(010\square 01\square\square 1)=aab\square
ba\square\square b$.

Notice that in all of these instances $\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ and
$\mbox{$[[$}\pi\mbox{$]]$}(t)$ are siblings, where $t$ is the underlying
string of $s$.

When $m=2$, we do the same thing, but reproduce 2 copies of $\square$ in the
output for each $\square$ in the input. For example, if
$\mbox{$[[$}\pi\mbox{$]]$}(010)=aa\square bab$, we would like
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(\square 01\square 0)=\square\square aa\square
b\square\square ab$. The $\square\square$ pattern in indices $(0,1)$ and
$(6,7)$ in the output come from the $\square$’s at indices $0$ and $3$ in the
input. The rest comes from filling in $\mbox{$[[$}\pi\mbox{$]]$}(010)$ in the
remaining indices.

Why is realizing this transformation on program codes hard? Again, briefly
assume that $m=1$.141414All the technical difficulty is encapsulated in the
case $m=1$, but it is less cumbersome to discuss. The basic idea is that to
figure out which character is carried by index $x$ in
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$, we have to figure out the number
$x^{\star}$ of _non-blank predecessors_ of $x$ (that is, the number of indices
of $\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ preceding $x$ which do not carry
$\square$), and look up index $x^{\star}$ in the string
$\mbox{$[[$}\pi\mbox{$]]$}(s)$.

This sounds easy: given $x$, all we have to do is compute $x^{\star}$ and use
$\pi$ to find the character it carries. But the boolean monadic restriction
prevents us from computing an index from another index as a subroutine! Even
worse, it seems impossible to count the number of blank indices before a
certain point.

What we have to do instead is modify $\pi$ so that it “ignores” $\square$
characters. Whenever $\pi$ tests whether an index is the min or the max,
$\pi_{b}$ tests whether the same index is the min or max _non-blank_ index.
Whenever $\pi$ takes the successor or predecessor of an index, $\pi_{b}$ goes
forward or backward to the next non-blank index. Here, the limited recursive
capabilities of a BMRS are enough: all we have to remember are what state
we’re in and what direction we’re going, and use tail recursion to skip over
any blank indices we see. In so doing, we avoid having to count anything.

So much for the overview, let us see how it works more formally. For the
remainder of this section, let $\pi:\Sigma_{\square}\times m\to\Gamma$ be a
fixed strict interpretation.

###  6.1. A normal form

We can ensure that all calls to $\max$ and $\min$ in $\pi$ have the form
$\max(\mathtt{x})$ and $\min(\mathtt{x})$ respectively. This construction is
rather artificial: simply make two additional recursive functions
$\mathtt{f}_{\max}(\mathtt{x})\equiv\max(\mathtt{x})$ and
$\mathtt{f}_{\min}(\mathtt{x})\equiv\min(\mathtt{x})$, and replace all other
occurrences of $\max(T)$ or $\min(T)$ by $\mathtt{f}_{\max}(T)$ and
$\mathtt{f}_{\min}(T)$ respectively. In precisely the same way, we can ensure
that all calls to any character $\gamma\in\Gamma$ have the form
$\gamma(\mathtt{x})$.

Next, we can ensure that every recursive call has one of three forms:
$\mathtt{f}(\mathtt{x})$, $\mathtt{f}(\mathrm{S}\mathtt{x})$, and
$\mathtt{f}(\mathrm{P}\mathtt{x})$, for some recursive function name
$\mathtt{f}$. Due to the restrictions of BMRS syntax, it’s already the case
that each recursive call is of the form $\mathtt{f}(T)$, for some index-valued
term $T$, and each index-valued term is a string of $\mathrm{S}$’s and
$\mathrm{P}$’s applied to $\mathtt{x}$. We can reduce this to the above three
forms by adding more recursive functions. For example,
$\mathtt{f}(\mathrm{S}\mathrm{S}\mathtt{x})$ can be replaced by
$\mathtt{g}(\mathrm{S}\mathtt{x})$, where
$\mathtt{g}(\mathtt{x})\equiv\mathtt{f}(\mathrm{S}\mathtt{x})$.

So what we have done is shown that we can assume every call to a boolean-
valued primitive ($\max$, $\min$, or some $\gamma$) in $\pi$ is of the form
$\max(\mathtt{x})$, $\min(\mathtt{x})$, and $\gamma(\mathtt{x})$, and every
call to a recursive function $\mathtt{f}$ in $\pi$ is of the form
$\mathtt{f}(\mathtt{x})$, $\mathtt{f}(\mathrm{S}\mathtt{x})$, or
$\mathtt{f}(\mathrm{P}\mathtt{x})$.

###  6.2. A program transformation

We now define a program transformation $p\mapsto p^{\star}$ from headless
$\Gamma$-BMRS’s to headless $\Gamma_{\square}$-BMRS’s; the rough idea being
that for any string $t\in\Gamma^{\star}$, $p^{\star}$ will do on any padding
of $t$ what $p$ does on $t$.

In the definitions below, by a “blank” or “non-blank” index of a given string,
we simply mean an index which does or does not carry the character $\square$
respectively.

######  Definition 15.

For any string $s\in\Gamma_{\square}^{\star}$, let $x\mapsto x^{\star}$ be the
map from non-blank indices of $s$ to indices of $d(s)$ defined by
$x^{\star}=x-\delta$, where $\delta$ is the number of blank predecessors of
$x$ in $s$.

Extend $x\mapsto x^{\star}$ by two partial maps $x\mapsto x^{S}$ and $x\mapsto
x^{P}$ from _all_ indices of $s$ to indices of $d(s)$. Namely,
$x^{S}=y^{\star}$, where $y$ is the least non-blank index $\geq x$, and
$x^{P}=z^{\star}$, where $z$ is the greatest non-blank index $\leq
x$.151515These maps may be partial as $x^{S}$ and $x^{P}$ will not be well-
defined if there is no succeeding or preceding non-blank index respectively.

For example, if $\Gamma=\\{a,b\\}$ and $s=a\square\square b\square a$, then
$d(s)=aba$ and $0^{\star}=0$, $3^{\star}=1$, and $5^{\star}=2$. Moreover
$0^{P}=1^{P}=2^{P}=0$, $3^{P}=1$, and $4^{P}=5^{P}=2$. Finally $0^{S}=0$,
$1^{S}=2^{S}=3^{S}=1$, and $4^{S}=5^{S}=2$. Note that all of these maps are
non-decreasing and that $x\mapsto x^{\star}$ is a bijection between non-blank
indices of $s$ and indices of $d(s)$.

Now consider the function $\mathrm{maxc}$ defined by:

$\displaystyle\mathrm{maxc}(\mathtt{x})$ $\displaystyle\equiv\mathtt{if}\
\square(\mathtt{x})\ \mathtt{then}\ \mathtt{f}(\mathtt{x})\ \mathtt{else}\
\bot$ $\displaystyle\mathtt{f}(\mathtt{x})$ $\displaystyle\equiv\mathtt{if}\
\max(\mathtt{x})\ \mathtt{then}\ \top\ \mathtt{else}\ \mathtt{if}\
\square(\mathrm{S}\mathtt{x})\ \mathtt{then}\ \bot\ \mathtt{else}\
\mathtt{f}(\mathrm{S}\mathtt{x}).$

Then $\mathrm{maxc}$ detects the maximum non-blank index. We can similarly
define $\mathrm{minc}$.

The following remark encapsulates several basic properties of the maps defined
so far:

######  Remark 1.

For any string $s\in\Gamma_{\square}^{\star}$, any non-blank index $x$ of $s$
and any character $\gamma\in\Gamma$, we have:

  1. (1)

$s\models\gamma(x)\iff d(s)\models\gamma(x^{\star}),$

  2. (2)

$s\vdash\mathrm{maxc}(x)\to\top\iff d(s)\models\max(x^{\star}),$

  3. (3)

$s\vdash\mathrm{minc}(x)\to\top\iff d(s)\models\min(x^{\star}),$

  4. (4)

$s\vdash\mathrm{maxc}(x)\to\bot\iff d(s)\models\neg\max(x^{\star}),$

  5. (5)

$s\vdash\mathrm{minc}(x)\to\bot\iff d(s)\models\neg\min(x^{\star}),$

  6. (6)

$x^{S}=x^{P}=x^{\star}$, and

  7. (7)

$\mathrm{P}x^{\star}=(\mathrm{P}x)^{P}$, and
$\mathrm{S}x^{\star}=(\mathrm{S}x)^{S}$.

Finally, for any _blank_ index $x$ of $s$, $x^{S}=(\mathrm{S}x)^{S}$ and
$x^{P}=(\mathrm{P}x)^{P}$.

######  Definition 6.2.

For each recursive function name $\mathtt{f}$, let $\mathtt{f}^{\star}$,
$\mathtt{f}^{S}$, and $\mathtt{f}^{P}$ be three distinct recursive function
symbols. We define a transformation $T\mapsto T^{\star}$ from boolean-valued
$\Gamma$-terms (in the above normal form) to boolean-valued
$\Gamma_{\square}$-terms as follows.

  * •

If $T\equiv\top$ or $T\equiv\bot$, then $T^{\star}\equiv T$.

  * •

If $T\equiv\gamma(\mathtt{x})$ for any character $\gamma\in\Gamma$, then
$T^{\star}\equiv\gamma(\mathtt{x})$.

  * •

If $T\equiv\max(\mathtt{x})$ or $T\equiv\min(\mathtt{x})$, then
$T^{\star}\equiv\mathrm{maxc}(\mathtt{x})$ or
$T\equiv\mathrm{minc}(\mathtt{x})$ respectively.

  * •

If $T\equiv\mathtt{f}(\mathtt{x})$, then
$T^{\star}\equiv\mathtt{f}^{\star}(\mathtt{x})$, for any recursive function
name $\mathtt{f}$.

  * •

If $T\equiv\mathtt{f}(\mathrm{S}\mathtt{x})$, then
$T^{\star}\equiv\mathtt{f}^{S}(\mathrm{S}\mathtt{x})$, for any recursive
function name $\mathtt{f}$.

  * •

If $T\equiv\mathtt{f}(\mathrm{P}\mathtt{x})$, then
$T^{\star}\equiv\mathtt{f}^{P}(\mathrm{P}\mathtt{x})$, for any recursive
function name $\mathtt{f}$.

  * •

If $T\equiv\mathtt{if}\ T_{0}\ \mathtt{then}\ T_{1}\ \mathtt{else}\ T_{2}$
then $T^{\star}\equiv\mathtt{if}\ T_{0}^{\star}\ \mathtt{then}\ T_{1}^{\star}\
\mathtt{else}\ T_{2}^{\star}$.

######  Definition 6.3.

For any headless $\Gamma$-BMRS $p=(\mathtt{f}_{i}(\mathtt{x})=T_{i})_{0\leq
i\leq k}$, define the $\Gamma_{\square}$-BMRS $p^{\star}$ by
$(\mathtt{f}_{i}^{\star}(\mathtt{x})=T_{i}^{\star})_{0\leq i\leq k}$ plus, for
each $0\leq i\leq k$,

$\mathtt{f}_{i}^{S}(\mathtt{x})=\mathtt{if}\ \square(\mathtt{x})\
\mathtt{then}\ \mathtt{f}_{i}^{S}(\mathrm{S}\mathtt{x})\ \mathtt{else}\
T_{i}^{\star},$ $\mathtt{f}_{i}^{P}(\mathtt{x})=\mathtt{if}\
\square(\mathtt{x})\ \mathtt{then}\ \mathtt{f}_{i}^{P}(\mathrm{P}\mathtt{x})\
\mathtt{else}\ T_{i}^{\star}.$

######  Theorem 6.4.

For any string $s\in\Gamma_{\square}^{\star}$, headless $\Gamma$-BMRS $p$,
non-blank index $x$ of $s$, boolean-valued $p$-term $T$, and boolean $b$,

$d(s),x^{\star}\vdash_{p}T\to b\implies s,x\vdash_{p^{\star}}T^{\star}\to b.$

Furthermore, for any index $x$ of $s$, any recursive function symbol
$\mathtt{f}$, and any boolean $b$, if $x^{S}$ exists, then

$d(s),x^{S}\vdash_{p}\mathtt{f}(\mathtt{x})\to b\implies
s,x\vdash_{p^{\star}}\mathtt{f}^{S}(\mathtt{x})\to b,$

and if $x^{P}$ exists, then

$d(s),x^{P}\vdash_{p}\mathtt{f}(\mathtt{x})\to b\implies
s,x\vdash_{p^{\star}}\mathtt{f}^{P}(\mathtt{x})\to b.$

######  Proof 6.5.

Fix $s$, $p$, $x$, $T$ and $b$. Let $t=d(s)$ be the underlying
$\Gamma^{\star}$-string of $s$. For legibility we omit the subscripts under
the turnstiles. We understand $t,\dots\vdash\dots$ to mean
$t,\dots\vdash_{p}\dots$ and $s,\dots\vdash\dots$ to mean
$s,\dots\vdash_{p^{\star}}\dots$. We prove all three statements by
simultaneous induction on the length of the computation in $p$.

First, let us prove $t,x^{\star}\vdash T\to b\implies s,x\vdash T^{\star}\to
b.$ Assume $t,x^{\star}\vdash T\to b$. If $T\equiv\gamma(\mathtt{x})$ for some
character $\gamma\in\Gamma$, then $T^{\star}\equiv\gamma(\mathtt{x})$, and the
conclusion follows from Remark 1. If $T\equiv\max(\mathtt{x})$ or
$\min(\mathtt{x})$ then $T^{\star}\equiv\mathrm{maxc}(\mathtt{x})$ or
$\mathrm{minc}(\mathtt{x})$ and the conclusion again follows from Remark 1.

Suppose that $T\equiv\mathtt{f}_{i}(\mathtt{x})$, and let
$\mathtt{f}_{i}(\mathtt{x})=T_{i}$ be the recursive definition of
$\mathtt{f}_{i}$ in $p$. Then $t,x^{\star}\vdash T_{i}\to b$, and by
induction, $s,x\vdash T_{i}^{\star}\to b$. But
$\mathtt{f}_{i}^{\star}(\mathtt{x})=T_{i}^{\star}$ is the recursive definition
of $\mathtt{f}_{i}^{\star}$ in $p^{\star}$, so
$s,x\vdash\mathtt{f}_{i}^{\star}(\mathtt{x})\to b$, which is what we want to
prove, because $T^{\star}\equiv\mathtt{f}_{i}^{\star}(\mathtt{x})$.

Suppose that $T\equiv\mathtt{f}(\mathrm{P}\mathtt{x})$. (The case that
$T\equiv\mathtt{f}(\mathrm{S}\mathtt{x})$ is similar.) Since
$t,x^{\star}\vdash\mathtt{f}(\mathrm{P}\mathtt{x})\to b$,
$t,\mathrm{P}x^{\star}\vdash\mathtt{f}(\mathtt{x})\to b$. Furthermore suppose
that $\mathrm{P}x$ is a non-blank index of $s$. By Remark 1
$t\models\mathrm{P}x^{\star}=(\mathrm{P}x)^{P}$. Therefore,
$t,(\mathrm{P}x)^{P}\vdash\mathtt{f}(\mathtt{x})\to b$. By induction,
$s,\mathrm{P}x\vdash\mathtt{f}^{P}(\mathtt{x})\to b$, thus
$s,x\vdash\mathtt{f}^{P}(\mathrm{P}\mathtt{x})\to b$, which is what we wanted
to show, since $T^{\star}\equiv\mathtt{f}^{P}(\mathrm{P}\mathtt{x})$.

Now suppose that $y=\mathrm{P}x$ is a blank index of $s$. Then
$t\models\mathrm{P}x^{\star}=y^{P}$ (Remark 1). Then
$t,y^{P}\vdash\mathtt{f}(\mathtt{x})\to b$; by induction,
$s,y\vdash\mathtt{f}^{P}(\mathtt{x})\to b$, so
$s,x\vdash\mathtt{f}^{P}(\mathrm{P}\mathtt{x})\to b$, which is what we wanted
to show.

Finally, suppose that $T\equiv\mathtt{if}\ T_{0}\ \mathtt{then}\ T_{1}\
\mathtt{else}\ T_{2}$ and $t,x^{\star}\vdash T_{0}\to\top$. (The case
$t,x^{\star}\vdash T_{0}\to\bot$ is similar, replacing $T_{1}$ by $T_{2}$.)
Then $t,x^{\star}\vdash T_{1}\to b$, so $s,x\vdash T_{0}^{\star}\to\top$, and
$s,x\vdash T_{1}^{\star}\to b$. Hence, $s,x\vdash T^{\star}\to b$. This
concludes the proof of the first statement.

Next, let us prove that $t,x^{S}\vdash\mathtt{f}(\mathtt{x})\to b\implies
s,x\vdash\mathtt{f}^{S}(\mathtt{x})\to b$. (The proof of
$t,x^{P}\vdash\mathtt{f}(\mathtt{x})\to b\implies
s,x\vdash\mathtt{f}^{P}(\mathtt{x})\to b$ is similar.) Assume
$t,x^{S}\vdash\mathtt{f}(\mathtt{x})\to b$.

Suppose first that $x$ is a non-blank index, so $x^{S}=x^{\star}$. If
$\mathtt{f}(\mathtt{x})\equiv\mathtt{f}_{i}(\mathtt{x})$, then
$t,x^{\star}\vdash T_{i}\to b$. By induction, $s,x\vdash T_{i}^{\star}\to b$.
Therefore

$s,x\vdash\mathtt{if}\ \square(\mathtt{x})\ \mathtt{then}\
\mathtt{f}_{i}^{S}(\mathrm{S}\mathtt{x})\ \mathtt{else}\ T_{i}^{\star}\to b,$

which means that $s,x\vdash\mathtt{f}_{i}^{S}(\mathtt{x})\to b$.

Finally, suppose that $x$ is the index of a blank character. Then
$t\vdash(\mathrm{S}x)^{S}=x^{S}$ by Remark 1 and hence
$t,(\mathrm{S}x)^{S}\vdash\mathtt{f}(\mathtt{x})\to b$. By induction,
$s,\mathrm{S}x\vdash\mathtt{f}^{S}(\mathtt{x})\to b$. Therefore,

$s,x\vdash\mathtt{if}\ \square(\mathtt{x})\ \mathtt{then}\
\mathtt{f}^{S}(\mathrm{S}\mathtt{x})\ \mathtt{else}\ \mathtt{f}(\mathtt{x})\to
b,$

which means $s,x\vdash\mathtt{f}^{S}(\mathtt{x})\to b$. This concludes the
proof.

###  6.3. The definition of $\pi_{b}$

Finally, we are in a position to define $\pi_{b}$ from $\pi$. Recall that
$\pi$ is a strict interpretation of type $\Sigma_{\square}\times m\to\Gamma$.

######  Definition 6.6.

Define the interpretation $\pi_{b}:\Sigma_{\square}\times
m\to\Gamma_{\square}$ as follows:

  * •

The body of $\pi_{b}$ is $p^{\star}$, where $p$ is the body of $\pi$.

  * •

For each character $\sigma\in\Sigma$ and $i<m$, the head $\pi_{b}(\sigma,i)$
is

$\mathtt{if}\ \square(\mathtt{x})\ \mathtt{then}\ \bot\ \mathtt{else}\
\pi(\sigma,i)^{\star}.$

  * •

For each $i<m$, the head $\pi_{b}(\square,i)$ is

$\mathtt{if}\ \square(\mathtt{x})\ \mathtt{then}\ \top\ \mathtt{else}\
\pi(\square,i)^{\star}.$

######  Lemma 6.7.

$\pi_{b}$ is a strict interpretation

######  Proof 6.8.

Fix a string $s\in\Gamma_{\square}^{\star}$, $x<|s|$, and $i<m$. If
$s_{x}=\square$ then $s,x\vdash\pi_{b}(\square,i)\to\top$ and
$s,x\vdash\pi_{b}(\sigma,i)\to\bot$ for every $\sigma\in\Sigma$.

Otherwise $x$ is a non-blank index of $s$. By strictness of $\pi$, there is a
unique $\sigma\in\Sigma_{\square}$ such that
$d(s),x^{\star}\vdash\pi(\sigma,i)\to\top$, and for every other
$\tau\in\Sigma_{\square}$, $d(s),x^{\star}\vdash\pi(\tau,i)\to\bot$. By
Theorem 6.4, $s,x\vdash\pi_{b}(\sigma,i)\to\top$, and
$s,x\vdash\pi_{b}(\tau,i)\to\bot$ for every other $\tau$. This proves
strictness of $\pi_{b}$.

Finally, we prove correctness.

######  Theorem 6.9.

For any string $s\in\Gamma_{\square}^{\star}$,
$d(\mbox{$[[$}\pi_{b}\mbox{$]]$}(s))=d(\mbox{$[[$}\pi\mbox{$]]$}(d(s)))$.

######  Proof 6.10.

Fix a string $s\in\Gamma^{\star}_{\square}$ and let $t=d(s)$ be the underlying
string in $\Gamma^{\star}$. Let $u=\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ and
$v=\mbox{$[[$}\pi\mbox{$]]$}(t)$, so that $|u|=m|s|$ and $|v|=m|t|$; we want
to show that $d(u)=d(v)$. Instead of showing this directly, we show that $u$
can be obtained from $v$ by padding it with more $\square$’s, which comes to
the same thing.

Let $X\subseteq|s|$ be the set of non-blank indices of $s$, so that $|X|=|t|$
and $x\mapsto x^{\star}$ is a bijection $X\to|t|$. Let $Y=\\{y<m|s|:y\div m\in
X\\}$; here $\div$ refers to integer division. Then $Y$ can be identified as a
set of indices of $u$; moreover $|Y|=|v|$. Define the map $f:Y\to|v|$ by
$f(mq+r)=mq^{\star}+r$ for every $q\in X$ and $r<m$. Then $f$ is the unique
monotone bijection between $Y$ and indices of $v$.

Let $y$ be an index of $u$ not in $Y$. Let $q$ and $r$ be the quotient and
remainder of $y\div m$ respectively. Then $q\notin X$, so
$s\models\square(q)$. Therefore $s,q\vdash\pi_{b}(\square,r)\to\top$, so
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)\vdash\square(y)$. In other words,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ carries $\square$ on any index outside $Y$.

Now let $y$ be an index of $u$ in $Y$, and again, let $q$ and $r$ be the
quotient and remainder upon division by $m$. Let $z=f(y)=mq^{\star}+r$ and let
$\sigma$ be the character of $v$ at index $z$, so that
$\mbox{$[[$}\pi\mbox{$]]$}(t)\models\sigma(z)$. Then
$t,q^{\star}\vdash\pi(\sigma,r)\to\top$, and by Theorem 6.9,
$s,q\vdash\pi(\sigma,r)^{\star}\to\top$. By definition of $\pi_{b}$,
$s,q\vdash\pi_{b}(\sigma,r)\to\top$; hence,
$\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)\models\sigma(y)$. In other words, for every
$y\in Y$, the character of $\mbox{$[[$}\pi_{b}\mbox{$]]$}(s)$ at $y$ is the
same as the character of $\mbox{$[[$}\pi\mbox{$]]$}(t)$ at $f(y)$.

What we have done is partitioned the indices of $u$ into $Y$ and $|u|\setminus
Y$. In the former part, $v$ appears as a substring; in the latter part, we
have only blank characters. Therefore, $u$ is obtained from $v$ by padding it
with blanks, and hence $d(u)=d(v)$.

##  7\. BMRS and the rational functions

We can now turn to the main results of the paper. First, we define a general
composition operation for BMRS interpretations that are not necessarily
strict. Note the overloading of $\otimes$ for both strict- and non-strict
interpretations.

######  Definition 7.11.

For two order-preserving BMRS interpretations $\rho:\Delta\times n\to\Sigma$
and $\pi:\Sigma\times m\to\Gamma$, let

$\rho\otimes\pi=(\rho_{b}^{\prime}\otimes\pi^{\prime})^{\dagger},$

where $\rho^{\prime}_{b}$ is taken as $(\rho^{\prime})_{b}$.

Then we have

######  Theorem 7.12.

For any $\rho$ and $\pi$ as above,
$\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}=\mbox{$[[$}\rho\mbox{$]]$}\circ\mbox{$[[$}\pi\mbox{$]]$}$.

######  Proof 7.13.

By Lemma 3,
$\mbox{$[[$}\rho\otimes\sigma\mbox{$]]$}=d\circ\mbox{$[[$}\rho^{\prime}_{b}\otimes\pi^{\prime}\mbox{$]]$}$.
By Lemma 4,
$\mbox{$[[$}\rho^{\prime}_{b}\otimes\pi^{\prime}\mbox{$]]$}=\mbox{$[[$}\rho^{\prime}_{b}\mbox{$]]$}\circ\mbox{$[[$}\pi^{\prime}\mbox{$]]$}$.
By Theorem 6.9,
$d\circ\mbox{$[[$}\rho^{\prime}_{b}\mbox{$]]$}=d\circ\mbox{$[[$}\rho^{\prime}\mbox{$]]$}\circ
d$. Hence

$\mbox{$[[$}\rho\otimes\sigma\mbox{$]]$}=d\circ\mbox{$[[$}\rho^{\prime}\mbox{$]]$}\circ
d\circ\mbox{$[[$}\pi^{\prime}\mbox{$]]$},$

but by Lemma 2,
$d\circ\mbox{$[[$}\rho^{\prime}\mbox{$]]$}=\mbox{$[[$}\rho\mbox{$]]$}$ and
$d\circ\mbox{$[[$}\pi^{\prime}\mbox{$]]$}=\mbox{$[[$}\pi\mbox{$]]$}$. Hence
$\mbox{$[[$}\rho\otimes\sigma\mbox{$]]$}=\mbox{$[[$}\rho\mbox{$]]$}\circ\mbox{$[[$}\sigma\mbox{$]]$}$.

Finally we obtain our main characterization of rational functions by order-
preserving BMRS interpretations. We crucially use a theorem of Elgot and Mezei
that every rational function can be decomposed into a composition of a left-
with a right-subsequential function.

######  Theorem 7.14 ([EM65]).

For every rational function $f$, $f=g\circ h$ for some left-subsequential
function $g$ and some right-subsequential function $h$.

######  Theorem 7.15.

For any well-defined order-preserving $\mathrm{BMRS}$ interpretation $\pi$,
$\mbox{$[[$}\pi\mbox{$]]$}$ is a rational function. Likewise, given a rational
function $f$, $f=\mbox{$[[$}\pi\mbox{$]]$}$ for some order-preserving
$\mathrm{BMRS}$ interpretation $\pi$.

######  Proof 7.16.

The forward direction is immediate from the fact that BMRS are a fragment of
MSO, plus the fact that order-preserving MSO interpretations define rational
functions [Boj14, Fil15]. In the backwards direction, given any rational
function $f$, consider its decomposition as $g\circ h$ guaranteed by Theorem
7.14. By Theorem 1 there are order-preserving BMRS interpretations $\rho$ and
$\pi$ such that $g=\mbox{$[[$}\rho\mbox{$]]$}$ and
$h=\mbox{$[[$}\pi\mbox{$]]$}$. Finally,
$f=\mbox{$[[$}\rho\otimes\pi\mbox{$]]$}$ by Theorem 7.12.

##  8\. Discussion and open questions

We factored composition of order-preserving interpretations into four sub-
problems: strictification, de-strictification, strict composition, and blank
enrichment. The solutions to the first three are very general and can be
replicated in almost any logic. Strictification relies only on closure under
boolean operations, strict composition relies on compositionality
(syntactically, the ability to substitute terms for variables of like type),
and de-strictification relies on nothing at all.

Syntactic blank enrichment, on the other hand, seems to call upon all of the
limited recursive power afforded by BMRS. This suggests to us that it is an
important problem to examine in the context of order-preserving
interpretations over different logics. Moreover, our solution seems to adapt
to the following slightly more general problem:

Let’s say we are given a relation $L$ which selects a subset of indices of any
given string. Now we have two (strict) functions $f$ and $g$, and we want to
“hybridize” them with respect to $L$ so that, on a given string $s$, we apply
$f$ “on” $L$ and $g$ “outside” $L$. For example if $s=ababb$ and $L$ selects
indices 0, 1, and 4 of $s$, then $s$ restricted to $L$ is $abb$ and $s$
restricted to its complement is $ab$. If $f(abb)=101$ and $g(ab)=22$, then the
$L$-hybrid of $f$ and $g$ applied to $s$ is $10221$. (See figure.)

${ababb}$${abb}$${ab}$${101}$${22}$${10221}$$\scriptstyle{L}$$\scriptstyle{\bar{L}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{L}$$\scriptstyle{\bar{L}}$

Blank enrichment is simply the special case of hybridization when $L$ is
$\square(\mathtt{x})$, $f$ is the given function, and $g$ is the
constant-$\square$ function. It seems like the technique for blank enrichment
will readily generalize to the more general problem. Many other natural
functionals can be expressed in terms of hybridization, for example
_concatenation:_ given two functions $f,g:\Sigma^{\star}\to\Gamma^{\star}$,
define the function
$\mathit{Concat}(f,g):\Sigma^{\star}_{\square}\to\Gamma^{\star}_{\square}$ by
$u\square v\mapsto f(u)\square g(v)$, at least on strings with exactly one
$\square$.

Concatenation-like functionals are an important example of functionals (or
_combinators_) used in algebraic characterizations of function classes such as
the regular functions [AFR14]. Realizing combinators syntactically by program
transformations (as we have done here for rational functions) gives us a path
towards capturing results different from—and arguably cleaner than—compiling
logical interpretations into transducers and vice versa.

A clear next step is to see whether there is a BMRS characterization of the
class of regular functions. Since these are captured by MSO interpretations
(not necessarily order-preserving), one might guess that the same holds for
BMRS. However it is not exactly clear what a non-order preserving BMRS
interpretation might be: we would need to define the successor function on the
output string, which means accommodating non-boolean valued recursive
functions in our programs.

Another open direction involves adapting BMRS to other data types, like trees
or graphs, which admit some notion of regularity. Here again we encounter the
foundational problem of how to extend the boolean monadic paradigm to data
types which do not fit neatly into it. The advantage of order-preserving BMRS
interpretations over strings lies in their simplicity combined with their
intensional expressiveness. We would regard these qualities as an acid test of
any proposed extension of BMRS to other domains.

## References

  * [AFR14] Rajeev Alur, Adam Freilich, and Mukund Raghothaman.  Regular combinators for string transformations.  In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, New York, NY, USA, 2014. Association for Computing Machinery.
  * [B6̈0] J. Richard Büchi.  Weak second-order arithmetic and finite automata.  Zeitschrift für Mathematische Logik und Grundlagen der Mathmatik, 6:66–92, 1960.
  * [BCJO20] Siddharth Bhaskar, Jane Chandlee, Adam Jardine, and Christopher Oakden.  Boolean monadic recursive schemes as a logical characterization of the subsequential functions.  In Alberto Leporati, Carlos Martín-Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications - LATA 2020, Lecture Notes in Computer Science, pages 157–169. Springer, 2020.
  * [Boj14] Mikołaj Bojańczyk.  Transducers with origin information.  In 41st International Colloquium on Automata, Languages, and Programming (ICALP), volume 8573 of LNCS, pages 26–37. Springer, 2014\.
  * [CJ21] Jane Chandlee and Adam Jardine.  Language, 97(3):485–519, September 2021.
  * [Cou94] Bruno Courcelle.  Monadic second-order definable graph transductions: a survey.  Theoretical Computer Science, 126:53–75, 1994.
  * [EH01] Joost Engelfriet and Hendrik Jan Hoogeboom.  MSO definable string transductions and two-way finite-state transducers.  ACM Transations on Computational Logic, 2:216–254, April 2001\.
  * [EM65] C. C. Elgot and J. E. Mezei.  On relations defined by generalized finite automata.  IBM Journal of Research and Development, 9(1):47–68, 1965.
  * [Fil15] Emmanual Filiot.  Logic-automata connections for transformations.  In Logic and Its Applications (ICLA), pages 30–57. Springer, 2015\.
  * [GK04] Georg Gottlob and Christoph Koch.  Monadic datalog and the expressive power of languages for web information extraction.  J. ACM, 51(1):74–113, Jan. 2004.
  * [Jon91] Neil D. Jones.  Efficient algebraic operations on programs.  In University of Iowa, pages 393–420, 1991.
  * [McC59] John McCarthy.  A basis for a mathematical theory of computation.  In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, volume 26 of Studies in Logic and the Foundations of Mathematics, pages 33–70. Elsevier, 1959.
  * [Mos19] Yiannis N. Moschovakis.  Abstract recursion and intrinsic complexity, volume 48 of Lecture Notes in Logic.  Cambridge University Press, 2019.
  * [Sak09] Jacques Sakarovitch.  Elements of Automata Theory.  Cambridge University Press, 2009.
  * [Sch06] Nicole Schweikardt.  On the expressive power of monadic least fixed point logic.  Theoretical Computer Science, 350(2):325–344, 2006.  Automata, Languages and Programming: Logic and Semantics (ICALP-B 2004).


# MVD: A Novel Methodology and Dataset for Acoustic Vehicle Type
Classification

Mohd Ashhad  Dept. of Computer Science
Jamia Hamdard
Delhi, India
<EMAIL_ADDRESS>Omar Ahmed  Dept. of Computer science
Jamia Hamdard
Delhi, India
<EMAIL_ADDRESS>Sooraj K. Ambat  Zeeshan Ali Haq  Naval, Physical &
Oceanographic Laboratory
Defence R&D Organization
Kochi, India
<EMAIL_ADDRESS>Dept. of Computer Science
Jamia Hamdard
Delhi, India
<EMAIL_ADDRESS>Mansaf Alam  Dept. of Computer Science
Jamia Millia Islamia
Delhi, India
<EMAIL_ADDRESS>
###### Abstract

Rising urban populations have led to a surge in vehicle use and made traffic
monitoring and management indispensable. Acoustic traffic monitoring (ATM)
offers a cost-effective and efficient alternative to more computationally
expensive methods of monitoring traffic such as those involving computer
vision technologies. In this paper, we present MVD and MVDA: two open datasets
for the development of acoustic traffic monitoring and vehicle-type
classification algorithms, which contain audio recordings of moving vehicles.
The dataset contain four classes— Trucks, Cars, Motorbikes, and a No-vehicle
class. Additionally, we propose a novel and efficient way to accurately
classify these acoustic signals using cepstrum and spectrum based local and
global audio features, and a multi-input neural network. Experimental results
show that our methodology improves upon the established baselines of previous
works and achieves an accuracy of 91.98% and 96.66% on MVD and MVDA Datasets,
respectively. Finally, the proposed model was deployed through an Android
application to make it accessible for testing and demonstrate its efficacy.

##  I Introduction

Increasing urban city populations have made automated traffic management vital
to avoid traffic jams, and road accidents and promote road safety[1][2]. With
an increasing need for smart cities, traffic monitoring has received a lot of
attention from researchers in the past decade[3] Traffic monitoring techniques
can be used for various applications such as vehicle detection, sub-type
classification, speed estimation, traffic density estimation, prediction of
road accidents, traffic signal optimization, etc. Acoustic Traffic Monitoring
(ATM) algorithms have shown to be better alternatives to vision-based
approaches as they are more computationally efficient[4], not sensitive to
lighting conditions[5], easily deployable, and have the added benefit of
preserving the privacy of drivers.

ATM algorithms come with their own set of challenges. Vehicle detection and
type classification using just the sound signature is a challenging task as
the sound is a mixture of engine sounds, sounds of tires (which may vary due
to air pressure), road conditions, and environmental sounds such as wind,
rain, horns, pedestrians, animals, etc. Moreover, the lack of large, high-
quality, balanced datasets has made the development of ATM algorithms a
challenging task which often compels researchers to record their own samples
and makes the validation and comparison of algorithms harder.

To address the challenges associated with the lack of open datasets and to
improve the performance of acoustic vehicle type classification, we introduce
two datasets, namely MVD and MVDA, which comprise audio recordings of four
classes of vehicles and a wide range of ambient noises. We’ve devised a robust
approach for identifying vehicle sounds by leveraging both global and local
audio features combined with a multi-input neural network. This approach
outperforms existing models, all while employing significantly fewer trainable
parameters. Additionally, we’ve developed an Android application to assess our
trained model’s performance seamlessly. The main contributions of our paper
are as follows:

  * •

We present the MVD (Moving Vehicle Detection) and MVDA (Moving Vehicle
Detection Augmented) Datasets. The former contains 4229 recordings of trucks,
cars, motorbikes, and a no-vehicle class, which includes recordings of diverse
background noises. The latter is a larger augmented version containing 16,916
recordings for better development and evaluation of ATM algorithms.

  * •

We propose a robust methodology for acoustic vehicle type classification using
global and local audio features and a multi-input neural network. Our
methodology achieves an accuracy of $91.98\%$ and $96.66\%$ on the MVD and
MVDA datasets respectively and improves upon the baseline performance on the
IDMT-Traffic[6] and IDMT-Traffic†[7] datasets while using $97.87\%$ and
$95.65\%$ fewer trainable parameters respectively.

  * •

Finally, we deploy our trained model through an Android application to assess
the performance of the model and investigate its dependence on the quality of
the microphone. The app is freely available for testing.

The structure of the paper is as follows: Section II of the paper provides a
brief overview of the recent ATM research. Section III describes the MVD,
MVDA, and other datasets utilized for the study. The proposed methodology for
the work is discussed in Section IV. The results of the various experiments
are presented in Section V. Finally, Section VI concludes the paper.

##  II Previous work

Traffic monitoring has a wide range of applications. However, in this paper,
we will limit our discussion to vehicle type classification. Over the past
decade, researchers have used many methods for this task. Broadly, these
methods can be classified into three groups: computer vision-based approaches,
seismic monitoring, which uses sensors to monitor the ground vibrations; and
finally, acoustic methods that utilize the sound of passing vehicles.

Sarikan et al.[8] achieved almost perfect classification on a dataset of 1200
samples of cars and motorbikes using a decision tree and k-nearest neighbor.
They captured information from a light curtain and used circularity, heat map,
and skeleton as features for the classifier. Chen et al.[9] proposed a feature
vector of thirteen measurements, which were subjected to Random Forest and
Support Vector Machine classifiers. The authors utilized 2055 CCTV images and
reported an accuracy of 96.26%. Bhujbal et al.[10] used convolutional neural
network layers as feature extractors to generate labels on 2659 images
obtained from cityscapes. Using the YOLO technique, authors achieved 87%
accuracy. Sang et al.[11] achieved a mean Average Precision (mAP) of 94.78% on
the BIT-Vehicle dataset. A revamped version of YOLOv2 called YOLOv2_Vehicle
and k-means++ clustering algorithm was engaged to obtain better anchor boxes,
feature extraction, and weather adaptability.

Jin et al.[12] extracted log-scaled frequency cepstral coefficients (LFCC)
from seismic recordings of DARPA’s SITEX02 Dataset. They achieved an accuracy
of 91.93%. Kalra et al.[13], recorded seismic signals of vehicles as well as
noise using geophones and used Empirical Wavelet Transform (EWT) based time-
frequency coefficients to extract statistical features such as mean, kurtosis,
Renyi entropy, etc., and used an SVM based classifier to get a F-Score of 78%,
67%, and 86% for bus, tractor, and noise, respectively. Bin et al.[14] used
Compressed Sensing (CS) theory to compress seismic signals and used a CNN to
achieve on-site efficient classification of military vehicles. They managed to
achieve an accuracy of 92.05% on the SITEX02 dataset. Later, Bin et al.[15]
used Fractal Theory to extract nonlinear seismic features and used SVM as a
classifier to achieve an F1 score of 0.901 on the same dataset.

Liu et al.[16] proposed a distributed multi-class Gaussian process (MCGP)
algorithm for vehicle type classification. Their experimentation on the
acoustic-seismic classification identification data set (ACIDS) revealed a
test error between 0.3 and 0.06. Mohine et al.[17] proposed a hybrid
convolutional neural network-bidirectional long short-term memory model (CNN-
BiLSTM) that extracts features from acoustic signals and classifies the
acoustic signal into five classes (two-wheeler, low, medium and heavy weight
vehicles and noise). The authors achieved 92% accuracy on their custom dataset
and 96% on the SITEX02 acoustic dataset. Ashhad et al.[7] attained 98.95%
accuracy on a carefully pre-processed version of the IDMT Traffic[6] dataset
by deploying an efficient CNN with MFCC features. Chen et al.[18] proposed a
hybrid neural network classifier with long short-term memory (LSTM) units
fused into CNN layers. The authors extracted MFCC, pitch class profile (PCP)
and short-term energy (STE) features and reported an accuracy of 97.65% on the
SITEX02 acoustic dataset.

##  III Datasets

###  III-A MVD Dataset

In this paper, we present two novel datasets. The MVD dataset consists of 4229
audio samples of passing vehicles moving at variable speeds, recorded with
four separate high-quality MEMS mono channel microphones at four different
urban locations in the Delhi-NCR region of India. The recording scenarios
consist of wet and dry road conditions as well as a plethora of environmental
noise such as wind, rain, animals, pedestrians and vehicles playing loud
music. The samples were captured at a sampling rate of 22,050 kHz. Each audio
is padded to be the same length of 3 seconds. The dataset includes four
classes: cars (1005 samples), trucks (1077 samples), motorcycles (1122
samples), and a no-vehicle class (1025 samples).

###  III-B MVDA Dataset

Apart from the MVD we also present the MVDA (Moving Vehicle Detection
Augmented) dataset which is an augmented version of the MVD dataset. The
motivation behind building this variation of the dataset lies in the fact that
exposing a machine learning model to a gamut of sound variations, and audio
augmentations improves the model’s ability to generalize. This means that the
model is better able to recognize similar sounds, even if they are not exact
replicas of the sounds in the training dataset. The MVDA dataset contains all
the recordings of the MVD dataset as well as augmented variants of each of
these recordings with the following three augmentations:

  * •

Random gain: This technique involves applying a random gain (i.e.,
amplification or attenuation) to the audio signal. This is done by multiplying
the audio signal by a random gain factor between a specified range as
illustrated in the following equation:

$y(t)=x(t)\times g$ (1)

Here $y(t)$ is the output signal, $x(t)$ is the input signal, $t$ denotes time
and $g$ is the random gain factor. We used minimum and maximum gain factors as
0.1 and 2 respectively. In practice, this augmentation has an effect similar
to that of changing the distance of the vehicle from the microphone.

  * •

Noise injection: In this technique, a random amount of white noise is added to
the original audio signal to simulate various types of environmental or
recording noise as illustrated in the following equation:

$y(t)=x(t)+r\times n$ (2)

Here $y(t)$ is the output signal, $x(t)$ is the input signal, $n$ denotes
Gaussian white noise and $r$ is the noise rate which is used to control the
amount of noise added to the signal. For each sample, we randomly applied a
noise rate between 0.001 and 0.003. This range was carefully fine-tuned so as
to not allow the signal-to-noise ratio (SNR) to get too small. This
augmentation was done to simulate the disturbance caused in recordings due to
environmental noise.

  * •

Time stretching: It is an audio augmentation technique that involves altering
the speed or duration of an audio signal without changing its pitch as
illustrated in the following equation.

$y(t)=x(S\times t)$ (3)

Here $y(t)$ is the output signal, $x(t)$ is the input signal, $t$ denotes time
and $S$ is the time scaling factor. For each sample in our dataset, we
randomly applied a stretching factor between 0.8 and 1.5. In practice, this
augmentation has an effect similar to that of changing the speed of the
vehicle recorded.

###  III-C IDMT-Traffic Dataset

In this work, we make use of the IDMT Traffic dataset[6]. Introduced in 2021,
the IDMT Traffic dataset serves as an open benchmark dataset designed for
acoustic traffic monitoring purposes. It encompasses stereo audio recordings
that are time-synchronized, capturing the sounds of moving vehicles in four
distinct recording locations. These locations include three urban traffic
settings and one rural road location situated in and around Ilmenau, Germany.
The recordings were obtained using two types of microphones: high-quality sE8
microphones and more affordable microelectromechanical systems (MEMS)
microphones. The dataset covers various recording scenarios, encompassing
different speed limits (30, 50, and 70 km/h) and varying road conditions,
including both dry and wet surfaces. Specifically, the dataset comprises the
following vehicle categories: Cars (3903 events), Trucks (511 events), Busses
(53 events), and Motorcycles (251 events). Additionally, background recordings
are available, representing situations when no vehicles are present.

###  III-D IDMT-Traffic† Dataset

Ashhad et al.[7] suggested a possible problem with the truck samples of the
IDMT-Traffic dataset leading to poor accuracy of the model in [6] on the truck
class. They proposed a methodology for sample rejection and data augmentation
for better training and evaluation of models trained on samples belonging to
the IDMT-Traffic dataset. We refer to this version of the dataset as IDMT-
Traffic†.

##  IV Methodology

In this section, we present the details of our method as illustrated in Fig.
1.

Figure 1: Methodology of proposed model.

###  IV-A Feature Extraction and Audio Pre-processing

In our audio pre-processing pipeline, we implemented two crucial techniques:
zero padding and pre-emphasis. These steps play a vital role in enhancing the
quality and effectiveness of our audio data analysis. Our study involved the
extraction of local and global audio features. We consider those features as
local, which give a time localized or frame-wise estimation of the frequency,
intensity, and energy contours of the audio samples, such as mel-spectrograms,
MFCCs, GFCCs, etc., while global features convey information about the entire
signal.

####  IV-A1 Local audio features

  * •

Mel-spectrogram: A mel-spectrogram is a mathematical representation of the
spectrum of a sound signal, where the frequency axis is divided into mel
frequency bands instead of linear frequency bands. To compute the mel-
spectrogram we used a window size of 1024, a hop size of 512, and an FFT size
of 2048. We used 128 mel-bands in the filter bank and applied log magnitude
scaling.

  * •

MFCC: Mel Frequency Cepstrum Coefficients (MFCC) are a set of coefficients
that represent the spectral envelope of the sound signal in the mel frequency
domain. For our experiments, we utilized the first 40 coefficients while the
rest of the parameters were the same as the previous section.

  * •

GFCC: After the success of the mel filterbank, Patterson and Smith[19] created
a more comprehensive model that mimicked the features of the ear based on
psychophysical research of the auditory periphery, called the Gammatone
Filterbank. The human auditory systems are modelled by the Gammatone filter
bank as a set of overlapping band-pass filters. The impulse response of each
filter is given by the following equation:

$g(t)=a{t}^{n-1}{e}^{-2\pi bt}cos(2\pi f_{c}t+\phi)$ (4)

Here $t$ denotes time, $n$ is the order of the filter, $a$ is a constant
(usually equal to 1), $b$ is the bandwidth parameter, $f_{c}$ is the filter
center frequency and $\phi$ is the phase of the fine-structure of the impulse
response. Based on the Gammatone filterbank, Xu et al.[20] developed a feature
extraction method called the Gammatone Frequency Cepstrum Coefficients (GFCC)
which performed better than MFCC in certain tasks.

####  IV-A2 Global audio features

We extract statistical features from the spectrum of the audio signals as a
second set of features since local features alone might be inadequate for
robust acoustic vehicle classification. The motivation behind including these
features in our model is that the pattern of these spectra can be used to
infer specific differences in the frequency distribution and associated
magnitudes among the sound signals of the various classes of vehicles.
Additionally, the magnitude of the pure-tone frequencies in the spectrum may
fluctuate as the distance between the car and the microphone varies, but their
distribution (shape) remains similar, which can be used to increase the
robustness of our model. Fig. 2(a),(b),(c) depicts the spectrums of
motorcycles, cars, and trucks, respectively. It is clear from the figure that
the shape of the spectrum of samples belonging to the same class is
independent of the distance of the recording microphone from the vehicle. We
calculate thirteen statistical features to create our input global feature
vector. The features are as follows: kurtosis, skewness, standard deviation,
variance, mode, iqr, mean, geometric mean, harmonic mean, median absolute
deviation, variation, geometric standard deviation, and entropy.

Figure 2: Spectra of (a) bikes, (b) cars, and (c) trucks recorded at two-meter
(left) and one-meter (right) illustrates similarities in signal envelopes
within each class and the dissimilarities between the classes.

###  IV-B Neural Network Architecture

We developed a multi-input neural network architecture that works well for the
task after extensive testing and review. Local feature matrix of size $m\times
n$ (where $m$ corresponds to the frame index and $n$ to the index of cepstrum
coefficient or frequency bin) is fed into 1D-CNN layers, while the global
feature vector of size $1\times f$ (where $f$ corresponds to the index of
feature) is fed in parallel to a fully connected layer. The outputs of the
parallel layers are then concatenated and passed to another fully connected
layer. The final softmax layer gives the output label. Fig. 1 illustrates our
methodology and the architecture of the model.

Figure 3: Working of the MVD android application. The user can choose between
recording a new sample or loading an existing one. The app then shows the
prediction as well as the confidence score.

###  IV-C Deployment through Android application

We deployed our model through an Android application for mobile devices. The
application is capable of capturing audio samples in real-time as well as
loading existing audio files, extracting the proposed features from the audio,
feeding the features into the trained model, and finally predicting the
vehicle type (refer Fig. 3). The application makes use of Chaquopy to run
Python scripts. For prompt processing, the model is hosted on a cloud
platform, where it receives the input from the app, processes it, and sends
the output back through API calls. The App is developed in Kotlin and uses the
Flask API for the backend.

##  V Experiments and Results

All the experiments were performed on Google Colab Pro with the Tensorflow
framework in Python. All the models were trained for 50 epochs with early
stopping and learning rate reduction with patience of 4 (minimum learning rate
= 1e-3). We use the categorical cross-entropy loss function and Adam
optimizer.

###  V-A Study of local features

We conducted multiple experiments aimed at determining the optimal combination
of global and local features for vehicle type classification. Understanding
the most effective feature set was crucial for improving the accuracy and
efficiency of our model. We experimented with MFCC, GFCC, and mel-spectrograms
(MS) on the MVD dataset with 5-fold validation. As for the classifier, we use
our fine-tuned multi-input neural network (refer Fig. 1). The study’s findings
are summarised in Table I. It is clear that GFCC, combined with global
features produces the most accurate predictions with an accuracy of $91.98\%.$

TABLE I: Classification results on the MVD dataset with varied features Class |  Feature |  Precision |  Recall |  F1-Score |  Accuracy (5-fold)
---|---|---|---|---|---
Car |  Global + MS |  0.81 |  0.76 |  0.79 |  86.80%
Motorcycle |  0.80 |  0.82 |  0.81
Truck |  0.92 |  0.93 |  0.93
No Vehicle |  0.96 |  0.92 |  0.94
Car |  Global + MFCC |  0.83 |  0.83 |  0.83 |  89.83%
Motorcycle |  0.89 |  0.96 |  0.93
Truck |  0.86 |  0.83 |  0.84
No Vehicle |  1.00 |  0.99 |  0.99
Car |  Global + GFCC |  0.88 |  0.85 |  0.86 |  91.98%
Motorcycle |  0.86 |  0.88 |  0.87
Truck |  0.96 |  0.95 |  0.95
No Vehicle |  0.99 |  0.99 |  0.99

###  V-B Performance of the proposed model

We evaluated the performance of our proposed methodology on 4 datasets: MVD,
MVDA, IDMT Traffic[6] and IDMT-Traffic†[7]. We performed 5-fold validation on
the MVD and MVDA datasets (refer Table II). The comparative results of our
proposed model on the IDMT-Traffic and IDMT-Traffic† datasets are shown in
Table III. For a fair comparison, we use the same train-test split as employed
by the authors in the original papers. It is clear from Table III that our
proposed methodology improves upon the established baselines while using
$97.87\%$ and $95.65\%$ fewer trainable parameters respectively (refer Table
IV).

TABLE II: Performance of the proposed model on MVD & MVDA datasets  Class |  Dataset |  Precision |  Recall |  F1-Score |  Accuracy (5-fold)
---|---|---|---|---|---
Car |  MVD |  0.88 |  0.85 |  0.86 |  91.98%
Motorcycle |  0.86 |  0.88 |  0.87
Truck |  0.96 |  0.95 |  0.95
No Vehicle |  0.99 |  0.99 |  0.99
Car |  MVDA |  0.95 |  0.95 |  0.95 |  96.66%
Motorcycle |  0.96 |  0.96 |  0.96
Truck |  0.97 |  0.96 |  0.97
No Vehicle |  0.99 |  0.99 |  0.99
TABLE III: Class-wise F1 score of our model against baselines Model |  Dataset |  Car |  Truck |  Motorcycle |  No Vehicle
---|---|---|---|---|---
Abeßer, J et al.[6] |  IDMT-Traffic |  0.94 |  0.5 |  0.96 |  1.00
Proposed Model |  IDMT-Traffic |  0.96 |  0.57 |  0.98 |  1.00
Ashhad et al.[7] |  IDMT-Traffic† |  0.99 |  0.92 |  0.99 |  1.00
Proposed Model |  IDMT-Traffic† |  0.99 |  0.94 |  0.99 |  1.00
TABLE IV: Comparison of the number of trainable parameters of the proposed model with baselines Model |  Features |  #Parameters
---|---|---
Abeßer, J et al.[6] |  Mel-spectrogram |  1,400,000
Ashhad et al.[7] |  MFCC |  712,436
Proposed Model |  GFCC + Statisical |  30,471
TABLE V: Confusion Matrix of predictions with Android app Class |  Car |  Truck |  Motorcycle |  No Vehicle
---|---|---|---|---
Car |  20 |  2 |  3 |  0
Truck |  3 |  23 |  1 |  0
Motorcycle |  1 |  0 |  21 |  0
No vehicle |  1 |  0 |  0 |  25

###  V-C Testing of the proposed model through Android application

The existing models for acoustic vehicle type classification can be quite
large for efficient training and deployment [6][7] [17]. Through our proposed
model, we managed to reduce the complexity without compromising the
performance. To demonstrate the efficiency of our model and study the
dependence of its performance on the microphone quality, we deployed it as an
application for Android devices. We tested the application on five separate
smartphones. Each smartphone was used to record 5 samples of each class (20
samples per phone) at various urban locations, and then the application was
used to perform predictions using the trained model. The results have been
presented as a confusion matrix (refer to Table V). With an accuracy of $90\%$
our model performs well at the task irrespective of the quality of the
microphone utilized for recording, thus increasing the utility of our approach
for real-world conditions.

##  VI Conclusion

In this paper, we present the MVD and MVDA datasets, two new open datasets for
the development and testing of ATM algorithms. With our proposed multi-input
neural network and carefully extracted audio features, we managed to
outperform baseline models at the task of acoustic vehicle type classification
while using $95.65\%$ to $97.87\%$ fewer trainable parameters. Additionally,
through our Android application, we showed that our methodology is independent
of the quality of the microphone and can be deployed with ease. In further
research, we want to investigate the deployability of ATM algorithms on edge
devices with limited computing capacity.
Reproducible Results: In the spirit of reproducible research, we provide
necessary codes, data and android application publicly[21].

## Acknowledgements

The authors would like to thank Ashad Naushad (Dept. of CSE, Jamia Hamdard)
for his invaluable contribution to the app development process.

## References

  * [1] Abdul Kadar Muhammad Masum, Md Kalim Amzad Chy, Iaamanur Rahman, Mohammad Nazim Uddin, and Khairul Islam Azam,  “An internet of things (iot) based smart traffic management system: a context of bangladesh,”  in 2018 International Conference on Innovations in Science, Engineering and Technology (ICISET). 2018, pp. 418–422, IEEE.
  * [2] Shuja Rafiq and Mohammadi Akheela Khanum,  “A review on minimization of ambulance response time using image processing and critical path mapping based on traffic control,”  Journal of Informatics Electrical and Electronics Engineering (JIEEE), vol. 2, no. 2, pp. 1–7, 2021.
  * [3] Soledad Pellicer, Guadalupe Santa, Andres L. Bleda, Rafael Maestre, Antonio J. Jara, and Antonio Gomez Skarmeta,  “A global perspective of smart cities: A survey,”  in 2013 Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing. 2013, pp. 439–444, IEEE.
  * [4] Nicolas Lefebvre, Xiandong Chen, Pierre Beauseroy, and MengYao Zhu,  “Traffic flow estimation using acoustic signal,”  Engineering Applications of Artificial Intelligence, vol. 64, pp. 164–171, 2017.
  * [5] Vivek Tyagi, Shivkumar Kalyanaraman, and Raghuram Krishnapuram,  “Vehicular traffic density state estimation based on cumulative road acoustics,”  IEEE Transactions on Intelligent Transportation Systems, vol. 13, no. 3, pp. 1156–1166, 2012.
  * [6] Jakob Abeßer, Saichand Gourishetti, András Kátai, Tobias Clauß, Prachi Sharma, and Judith Liebetrau,  “Idmt-traffic: an open benchmark dataset for acoustic traffic monitoring research,”  in 2021 29th European Signal Processing Conference (EUSIPCO). 2021, pp. 551–555, IEEE.
  * [7] Mohd Ashhad, Umang Goenka, Aaryan Jagetia, Parwin Akhtari, Sooraj K. Ambat, and Mary Samuel,  “Improved vehicle sub-type classification for acoustic traffic monitoring,”  in 2023 National Conference on Communications (NCC). 2023, pp. 1–6, IEEE.
  * [8] Selim S. Sarikan, A. Murat Ozbayoglu, and Oguzhan Zilci,  “Automated vehicle classification with image processing and computational intelligence,”  Procedia Computer Science, vol. 114, pp. 515–522, 2017.
  * [9] Zezhi Chen, Tim Ellis, and Sergio A. Velastin,  “Vehicle type categorization: A comparison of classification schemes,”  in 2011 14th International IEEE Conference on Intelligent Transportation Systems (ITSC). 2011, pp. 74–79, IEEE.
  * [10] Avinash Bhujbal and D. T. Mane,  “Vehicle type classification using deep learning,”  in Soft Computing and Signal Processing: Proceedings of 2nd ICSCSP 2019 2. 2020, pp. 279–290, Springer.
  * [11] Jun Sang, Zhongyuan Wu, Pei Guo, Haibo Hu, Hong Xiang, Qian Zhang, and Bin Cai,  “An improved yolov2 for vehicle detection,”  Sensors, vol. 18, no. 12, pp. 4272, 2018.
  * [12] Guozheng Jin, Bin Ye, Yezhou Wu, and Fengzhong Qu,  “Vehicle classification based on seismic signatures using convolutional neural network,”  IEEE Geoscience and Remote Sensing Letters, vol. 16, no. 4, pp. 628–632, 2018.
  * [13] Manish Kalra, Satish Kumar, and Bhargab Das,  “Seismic signal analysis using empirical wavelet transform for moving ground target detection and classification,”  IEEE sensors journal, vol. 20, no. 14, pp. 7886–7895, 2020.
  * [14] Kangcheng Bin, Jun Lin, and Xunqian Tong,  “Edge intelligence-based moving target classification using compressed seismic measurements and convolutional neural networks,”  IEEE geoscience and remote sensing letters, vol. 19, pp. 1–5, 2021\.
  * [15] Kangcheng Bin, Yun Long, Xunqian Tong, and Jun Lin,  “Ground moving target detection with seismic fractal features,”  IEEE Geoscience and Remote Sensing Letters, vol. 19, pp. 1–5, 2021\.
  * [16] Xingchi Liu, Qing Li, Jiaming Liang, Jinzheng Zhao, Peipei Wu, Chenyi Lyu, Shidrokh Goudarzi, Jemin George, Tien Pham, and Wenwu Wang,  “Advanced machine learning methods for autonomous classification of ground vehicles with acoustic data,”  in Artificial Intelligence and Machine Learning for Multi-Domain Operations Applications IV. 2022, vol. 12113, pp. 524–533, SPIE.
  * [17] Shailesh Mohine, Babankumar S. Bansod, Rakesh Bhalla, and Anshul Basra,  “Acoustic modality based hybrid deep 1d cnn-bilstm algorithm for moving vehicle classification,”  IEEE Transactions on Intelligent Transportation Systems, vol. 23, no. 9, pp. 16206–16216, 2022.
  * [18] Haoze Chen and Zhijie Zhang,  “Hybrid neural network based on novel audio feature for vehicle type identification,”  Scientific Reports, vol. 11, no. 1, pp. 7648, 2021.
  * [19] Roy D. Patterson, Ian Nimmo-Smith, John Holdsworth, and Peter Rice,  “An efficient auditory filterbank based on the gammatone function,”  in a meeting of the IOC Speech Group on Auditory Modelling at RSRE, 1987, vol. 2.
  * [20] He Xu, Lin Lin, Xiaoying Sun, and Huanmei Jin,  “A new algorithm for auditory feature extraction,”  in 2012 International Conference on Communication Systems and Network Technologies. 2012, pp. 229–232, IEEE.
  * [21] Ashhad,  “Source code,”  https://github.com/Ashhad785/MVD.git, 2023.