key: cord-0043258-vwgfffnh
authors: Bhaskar, Siddharth; Chandlee, Jane; Jardine, Adam; Oakden, Christopher
title: Boolean Monadic Recursive Schemes as a Logical Characterization of the Subsequential Functions
date: 2020-01-07
journal: Language and Automata Theory and Applications
DOI: 10.1007/978-3-030-40608-0_10
sha: f3dbd8610321729e75cec0eb60eb5dac967242e0
doc_id: 43258
cord_uid: vwgfffnh

This paper defines boolean monadic recursive schemes (BMRSs), a restriction on recursive programs, and shows that when interpreted as transductions on strings they describe exactly the subsequential functions. We discuss how this new result furthers the study of the connections between logic, formal languages and functions, and automata.

A fundamental result in the connection between automata and logic is that of Elgot [7] , Büchi [1] , and Trakhtenbrot [21] , which states that sentences in monadic second-order (MSO) logic describe exactly the same class of formal languages as finite-state acceptors (FSAs); namely, the regular class of languages. Further work established many connections between restrictions on MSO, restrictions on FSAs, and sub-classes of the regular languages [14, 20] .

More recently, a major result of Engelfriet and Hoogeboom shows the relationship between MSO and regular functions on strings-that is, exactly those functions described by two-way finite state transducers [9] . Essentially, string functions can be described by a MSO interpretation in which the binary successor relation and alphabet labels of the output string are defined by a series of binary and unary predicates in the MSO logic of the input strings, relativized over a copy set which allows the output string to be larger than the input string. Each element in the output string is thus a copy of an index in the input string, and the character it receives and where it is in the order is determined by which predicates are satisfied by the input string at that index. This technique has allowed a rich study of the relationship between sub-MSO logics and restrictions on finite-state transducers [10, 11] parallel to the earlier work on logic and finite-state automata and languages.

However, there remain some interesting classes for which no logical characterization has been previously established. In this paper, we investigate the subsequential functions, a strict sub-class of the rational functions, or those that are describable by one-way finite-state transducers. 1 While a weak class, there are a number of reasons why the subsequential class is a worthy object of study. From a theoretical perspective, the subsequential functions admit an abstract characterization that generalizes the Myhill-Nerode equivalence classes of regular languages [19] . This property makes the subsequential functions learnable from a sample of positive data [18] . In terms of practical applications, the subsequential functions have applications to speech and language processing [16] , and form a hypothesis for the computational upper bound of functions in certain domains of natural language phonology [12, 13] .

In this paper, we define boolean monadic recursive schemes (BMRSs), a restriction on the general notion of a recursive program scheme in the sense of Moschovakis [17] . As indicated by the name, these schemes recursively define a series of unary functions that take as inputs indices from a string and return a boolean value. A system of BMRS functions can be used to express a logical transduction in the sense of Engelfriet and Hoogeboom by assigning these functions to symbols in an output alphabet. An output string then consists of the characters whose functions are true at each index in the input string. We show that string transductions defined by BMRS transductions with predecessor or successor describe exactly the left-and right-subsequential functions, respectively. This is an entirely novel result; the closest result in the literature is that of [6] , who give a fragment of least-fixed point logic that captures strict subsets of the left-and right-subsequential functions. As we discuss at the end of the paper, the current result allows for further study of the connections among subclasses of the subsequential functions and of rational functions in general.

This paper is structured as follows. Sections 2 and 3 establish the notation and definitions for strings, subsequential functions, and subsequential transducers. Section 4 establishes BMRSs and BMRS transductions, and Sect. 5 shows the equivalence between BMRS transductions and subsequential functions. Sections 6 and 7 discuss the implications of this result and conclude the paper.

An alphabet Σ is a finite set of symbols; let Σ * be all strings over Σ, including λ, the empty string. We will frequently make use of special left and right string boundary symbols , ∈ Σ. We denote by

For a string w, |w| indicates the length of w. We write w r for the reversal of w.

A string u is a prefix of w, written u w, iff w = uv for some string v. For a set L ⊆ Σ * of strings let the common prefixes be comprefs(L) = w∈L {u | u w}. The longest common prefix of L is the maximum element in comprefs(L): lcp(L) = w ∈ comprefs(L) s.t. for all v ∈ comprefs(L), |v| ≤ |w|.

We first define the subsequential functions based on the notion of tails [16, 19] . Let f : Σ * → Γ * be an arbitrary function and f p (x) = lcp({f (xu) | u ∈ Σ * }). Then of course, for every u, f p (x) f (xu). Now let the tail function f x (u) be defined as v such that f p (x)v = f (xu). This function represents the tails of x. This allows us to define the subsequential functions as follows.

is left-subsequential. Note that for any x = a n for an even n, f p (x) = (abb) n/2 , and so f x = f . For any y = a n for an odd n, then f p (y) = (abb) (n−1)/2 a, and so f y is the function f y (a m ) = d if m = 0; bb · f (a m−1 ) otherwise. Then f is describable by these two tail functions {f x , f y }.

Conversely, the function g defined as g(a n ) = ca n−1 if n is even; da n−1 if n is odd,

is not left-subsequential. Note that for any x = a n , g p (x) = λ. This is because {g(xu) | u ∈ Σ * } includes both ca i and da j for some i and j. Because g x (u) is defined as v such that g p (x)v = g(xu), and because g p (x) = λ, g x (u) = g(xu).

The consequence of this is that for any x = a n and y = a m for a distinct m = n, for any u, g x (u) = g y (u). Thus the set of tails functions for g is an infinite set

The right-subsequential functions are those that are the mirror image of some left-subsequential function.

A function f is right-subsequential iff there is some left-subsequential function f such that for any string in the domain of f , f (w) = (f (w r )) r .

We leave it to the reader to show that g is right-subsequential. Thus, the subsequential functions are those functions that are either left-or rightsubsequential.

A (left-)subsequential finite-state transducer (SFST) for an input alphabet Σ and an output alphabet Γ is a tuple

and ω : Q f → Γ * is the final function. We define the reflexive, transitive closure of δ and o as δ * : Q × Σ * → Q and o * : Q × Σ * → Γ * in the usual way.

The semantics of a SFST is a transduction t(T ) defined as follows 

For more properties of the subsequential functions and their application to speech and language processing see [16] .

We identify strings in Σ with structures of the form S = D; σ 1 , σ 2 , ..., σ n , p, s where the domain D is the set of indices; for each character σ ∈ Σ , we also write σ i for the unary relation σ i ⊆ D selecting the indices of that character (and we assume that the least and greatest indices contain the characters and , respectively); p is the predecessor function on indices (fixing the least index); and s is the successor function on indices (fixing the greatest index). As an abbreviatory convention we use x − i for i applications of p to x, and likewise x + i for i applications of s. (E.g. x − 2 is the same as p(p(x))).

Boolean monadic recursive schemes are simple programs that operate over such string structures. They are a particular case of the recursive programs of Moschovakis [17] . We briefly review the syntax and semantics of such recursive programs in this particular signature, then impose (Definition 3) the pertinent syntactic restriction to obtain BMRSs.

We have two types of data: boolean values and string indices. We have two countably infinite set of variables: (index) variables X, which range over string indices, and recursive function names F. Each recursive function name f ∈ F comes with an arity n ∈ N and an output type, either "index" or "boolean". Function names f of arity n and type s range over n-ary functions from string indices to s.

Terms. Terms are given by the following grammar

Terms inherit "boolean" or "index" types inductively from their variables and function names, and term formation is subject to the usual typing rules: for

, the type of each T I must be "index"; for T 1 = T 2 , the types of T 1 and T 2 must be the same; for and "if T 1 then T 2 else T 3 ," then the type of T 1 must be "boolean," and the types of T 2 and T 3 must agree.

where T i is a term whose type agrees with the output type of f i , every variable that occurs in T i is some x ij , and every function name that occurs in T i is some f j . Syntactically, we will write

to indicate that the above properties hold.

Semantics. We impose the usual least fixed-point semantics on recursive programs. Briefly; over a given string, terms denote functionals which are monotone relative to extension relation on partial functions. We define the semantics of a program to be the first coordinatef 1 of the least fixed-point ( [17] .

Boolean monadic recursive schemes compute (partial) functions from string indices to booleans, or equivalently (partial) subsets of indices. For example, the following scheme detects exactly those indices with some preceding b.

We can define a string transduction t : Σ * → Γ * via a BMRS interpretation as follows. Fix a copy set C = {1, . . . , m} and for n = |Γ | consider a system T of equations with a set of recursive functions f = (γ 1 1 , . . . , γ m 1 , γ 1 2 , . . . , γ m n , f 1 , . . . , f k ); that is, with a function γ c for each γ ∈ Γ and c ∈ C.

Following the definition of logical string transductions [9, 10] , the semantics of T given an input model S with a universe D as follows. For each d ∈ D, we output a copy d c of d if and only if there is exactly one γ ∈ Γ for c ∈ C such that γ c (x) ∈ T evaluates to when x is mapped to d. We fix the order of these output copies to be derived from C and the order on D induced by the predecessor function p: for any two copies d c and d e of a single index d, d c < d e iff c < e in the order on C, and for any copies d c i and d e j for distinct input indices

the order on the indices in S. We fix the order due to the relation between order-preserving logical transductions and one-tape finite-state transducers [10] .

This semantics of T thus defines a string transduction t = t(T ) where for a string w ∈ Σ * of length , t(w) = u 0 u 1 ...u u +1 , where each u i = γ 1 ...γ r if and only if for each γ j , 1 ≤ j ≤ r, γ j is the unique symbol in Γ for j ∈ C such that γ j j (x) evaluates to when x is assigned to i in the structure of w . An example is given in Example 2.

To describe partial functions we can add to f a special function def(x) and specify the semantics of t to state that t(w) is defined iff def(x) evaluates to for element in w.

The following is a BMRS definition of f from Example 1 using strings models from Σ * . The copy set is C = {1, 2}.

The following shows how this maps aaaaa to abbabbad: We define two important variants of BMRS logic. For BMRS systems of equations over a set of recursive function symbols f, we say a system of equations T ∈ BMRS p iff it contains no terms of the form s(T 1 ) for any term T 1 , and likewise T ∈ BMRS s iff it contains no terms of the form p(T 1 ) for any term T 1 . We define these as they fix the 'direction' of the recursion, which will be important in connecting them to the left-and right-subsequential functions.

We only want to consider BMRS that compute well-defined transductions. Therefore, we require that for each string w ∈ Σ * , each index i of w, and each c ∈ C and γ ∈ Γ , every function γ c (i) converges, and furthermore for each c, there is a unique γ such that γ c (i) = .

This is of course a semantic property, which is not an issue as far as the following proofs of extensional equivalence are concerned. However, there is an effective way of transforming a BMRS T into a BMRS T such that T computes a well-defined transduction, and agrees with T on inputs where T is well-defined. 2 Therefore, considering partially-defined schemata do not increase the computational power in any appreciable way.

For a left-subsequential function f : Σ * → Γ * , we can define an equivalent function in BMRS p over models of strings in Σ * . We do this by giving a construction of its SFST.

For an SFST T = Q, q 0 , Q f , δ, o, ω , where Q is the set of k states, we construct a BMRS p system of equations T over the set of recursive functions f = (γ 1 1 , ..., γ m 1 , γ 1 2 , ..., γ m n , q 0 , . . . , q k−1 ), where n = |Γ | and m is the maximum length of any output of o or ω. The definitions in T are fixed as follows. First, we define q 0 , . . . , q k−1 to parallel the transition function δ. For each state q ∈ Q we define its corresponding recursive function symbol q as

where q 1 , ..., q is the set of states reaching q; that is, the set of states such that for each q i , δ(q i , σ i ) = q. For the start state we instead set the final 'else' statement to x is the minimum element in the string; i.e. that (p(x)).

We then define the set of functions γ 1 1 , ..., γ m 1 , γ 1 2 , ..., γ m n representing the symbols in the output strings to parallel the output and final functions o and ω:

for all states q i whose output on σ i has γ as the cth symbol. That is, for each

If there are no such states we set γ c (x) = ⊥.

Finally, in cases when Q f Q we can, via the definition of the semantics of BMRS transductions for partial functions, we set the equation for the special function def(x) determining when the function is defined as

An example definition modeling the SFST in Fig. 1 , and an example computation for an input string aaaa is given in Table 1 . Table 1 . A BMRS transduction for the SFST in Fig. 1 (left) and an example derivation (right). The rows for a 2 (x), c 2 (x), and d 2 (x) have been omitted.

Proof. It is sufficient to show that the above construction creates from any SFST T a BMRS p system of equations T whose transduction t(T ) = t(T ). Consider any string in w = σ 1 ...σ n ∈ Σ * of length n; we refer to the positions in w as their indices 0, 1, ..., n + 1. From the construction q 0 (x) is always true of position 1; likewise by definition T is in state q 0 at position 1. By definition (2) for T , whenever T is in state q i , reads position i, and δ(q i , σ i ) = q j , then q j (x) in T evaluates to for i+1, because 'if q i (x) then σ i (x)' is in the definition for q j (x). By induction on δ * it is thus the case that whenever T is in state q i at position i, position i satisfies q i (x) in T .

Let o(q i , σ i ) = u = γ 1 ...γ m for any position i in w. By (3), for each γ j there is a function γ j j (x) whose definition includes 'if q i (x) then σ i (x)'. Because i satisfies q i (x) in T , then each jth copy of i will be γ j , and so the output of i under T will also be γ 1 ...γ j = u. This also holds for the output function ω.

Thus for any w, t(T )(w) = w implies that t(T )(w) = w , and it is not hard to show that the reverse holds.

The following lemma shows that the same is true for right-subsequential functions and BMRS s , which follows by the same logic as for Lemma 1.

Any right-subsequential function has some BMRS s definition.

To show the converse, we show that for any well-defined BMRS p transduction T , for f = t(T ), the sets {f x | x ∈ Σ * } are finite. For a copy set C = {1, ..., m} and for n = |Γ | consider a system T of equations with a set of recursive functions

let F be the set of function names appearing in f, and let be the maximum number such that x − appears as a term in T . First, define sats(w, i) = {f ∈ T | f(i) = in w} to identify the functions in T true in w at index i. The following fact will be used throughout this proof.

For any f ∈ F and string w ∈ Σ * , the value of f(i) can be calculated from the sets F , F −1 , ..., F 1 , where for each 1 ≤ j ≤ , F j = sats(w, i−j).

Proof. Let f(x) = T f be the equation for f in T . By the definition of T , is the maximum number of times the p function can be applied to a variable in any term in T . Thus, for any function g ∈ F , T f can only contain g(x−h) for at most some h ≤ . Thus, in terms of the semantics of f(i) for some index i in w, the value of g(i − h) can be determined by whether g is in F h . The remainder of the semantics of f(i) then follows from the definition of the semantics of BMRSs.

The following states that sats(w, i) holds no matter how w is extended. This follows directly from Remark 1.

For any w, v ∈ Σ * , sats(w, i) = sats(wv, i).

Recall that among the functions in F there is a function γ c ∈ F for each γ ∈ Γ and c ∈ C. Recall also that the semantics of BMRS transductions produces an output string u i at each input index i such that γ is the cth position in u i if and only if γ c (i) evaluates to . (The stipulation that there is only one such γ c ensures that only a single output string is produced for each index). To refer to this string we define out(w, i) = γ 1 γ 2 ...γ h where each γ j ∈ sats(w, i).

Then let out T (w) = out(w, 1)·out(w, 2)·...·out(w, last(w)), where last(w) indicates the final index in w.

We can now connect these facts to the string function f = t(T ) described by T . Recall the technicality that the domain of f is Σ * but T is defined over string models of the form Σ * . First, the above allows us to make the following assertion about the relationship between out T and f p .

Proof. This follows directly from Remark 2: the output at each index at w will be constant no matter how w is extended. Thus, f p (w) at least includes out T ( w).

The final piece is to define when two strings w and v are equivalent with respect to T , which we then show that they are equivalent with respect to f ; that is, that f w = f v . Intuitively, w and v are equivalent if their final indices satisfy exactly the same functions in F . Formally,

Proof. For any sequence of indices, there are at most (2 |F | ) possible sequences of subsets of F that they satisfy.

The following states the key implication that equivalence with respect to T implies equivalence with respect to f .

Proof. First, for any σ ∈ Σ , out( wσ, last( wσ)) = out( vσ, last( vσ)). In other words, the string output at any additional σ following w and v is the same. This follows from Remark 1 and the fact that the final indices in w and v satisfy the same sets of functions in F .

For any string u ∈ Σ * , then, by induction on the length of u it is clear that f (wu) = out T ( w)u and f (vu) = out T ( v)u for the same u ∈ Γ * . From this and Remark 3, we know that f p (w) = out T ( w)u 1 and f p (v) = out T ( v)u 1 for the same u 1 ∈ Γ * . Clearly then for any u ∈ Σ * , f (wu) = f p (w)u and f (vu) = f p (v)u and so by the definition of f w and f v , f w = f v .

Proof. The set {f x | x ∈ Σ * } is finite: from Remark 4, ≡ T induces a finite partition on Σ * , and by Lemma 3, for any two strings w, v in the same block in this partition, f w = f v . Thus there can only be finitely many such functions f x .

We omit the proof for the following parallel lemma for BMRS s .

For any BMRS s transduction T , the function f = t(T ) is a rightsubsequential function.

We now can give the central result of the paper. Theorem 3. BMRS p (respectively, BMRS s ) transductions are equivalent to the left-subsequential (resp., right-subsequential) functions.

Proof. From Lemmas 1, 2, 4, and 5.

The above result provides the first logical characterization of the subsequential functions. A consequence of this is we can get a better understanding of subclasses of the subsequential functions. We sketch two here.

First, the input strictly local (ISL) functions are a strict subset of the subsequential class for which the output string is computed by referencing a bounded window in the input string only [2, 3] . Briefly, a function is ISL iff there is some number k such that for any two strings w and v that share a k − 1 suffix, f w = f v . This class has attractive learnability properties [3] and empirically is relevant to processes in natural language phonology [5] . We omit a proof, but it is almost certainly the case that a BMRS system of equations T corresponds to an ISL function iff for each function symbol f ∈ f, the definition of f contains no recursive function calls. This is further interesting in that it suggests that any left-subsequential function f has a ISL counterpart whose input alphabet subsumes the recursive function symbols in the BMRS p definition of f . 3 This is strongly reminiscent of the old result that any regular language is the homomorphism of a strictly 2-local language [15] .

A sister class to the ISL functions is the output strictly local (OSL) functions, which are those subsequential functions which compute the output string by referencing the current input and a bounded window in the output [2, 4] . They are divided into two classes the left-and right-OSL functions depending on whether the string is read from the left or right. We conjecture that a BMRS system of equations T corresponds to an OSL function iff for each function f i ∈ f corresponding to γ c ∈ Γ , for any non recursively-defined σ(t) (σ ∈ Σ), then t = x. BMRS p systems of equations of this type correspond to left-OSL functions, while BMRS s systems of this type correspond to right-OSL functions.

Finally, this paper has limited its discussion to BMRS transductions restricted to either p or s, so an obvious open question is to what functions are described by BMRS transductions without this restriction. As any rational function is the composition of a right-and left-subsequential function [8] , it is clear that BMRS transductions in general are strictly more expressive than either the BMRS p and BMRS s transductions. Based on this, we tentatively conjecture that the BMRS transductions in general are equivalent to the rational functions, but this claim requires more rigorous investigation than can be done here.

This paper has given the first logical characterization of the subsequential functions. As with previous work connecting logical, language-theoretic, and automata-theoretic characterizations of formal languages and functions, we are confident this will further study of the connections between subclasses of the subsequential functions, and subclasses of the rational functions in general.

Weak second-order arithmetic and finite automata

Strictly Local Phonological Processes

Learning strictly local subsequential functions

Output strictly local functions

Strictly locality and phonological maps

Autosegmental input-strictly local functions

Decision problems of finite automata design and related arithmetics

On relations defined by generalized finite automata

MSO definable string transductions and two-way finite-state transducers

Logic-automata connections for transformations

Transducers, logic, and algebra for functions of finite words

The computational nature of phonological generalizations

Vowel harmony and subsequentiality

Counter-Free Automata

On the class of events representable in a finite automaton

Finite-state transducers in language and speech processing

Abstract Recursion and Intrinsic Complexity

Learning subsequential transducers for pattern recognition tasks

Sur une variante des fonctions séquentielles

Classifying regular events in symbolic logic

Finite automata and logic of monadic predicates