Regular Transformations

Macro Tree Transducers (MTT) are a very expressive model of tree transducers, but its restriction to tree-to-tree functions of Linear Size Increase (LSI) has been shown to be as expressive as MSO tree transductions. In this talk we study variations of this LSI semantic contraint, namely Linear Height Increase (LHI) and Linear input Size to output Height Increase (LSHI), and provide a new normal form for MTTs called Depth-normal form. This new normal form allows an elegant characterization of the LHI and LSHI constraints, which in turn gives an algorithm for deciding if a MTT respects these constraints.

String constraints arise naturally when analysing string-manipulating programs. For example, during symbolic execution, determining whether an identified program path is feasible means checking if a set of constraints (from program branches, assignments, and loop conditions) has some satisfying assignment. That, there is some input that will lead to the given path being executed. This then requires constraint satisfaction tools to be able to handle complex string operations, as well as basics such as concatenation and containment in a regular language.

One such operation is the “replaceall” operation, where a matched pattern is replaced in one string to obtain another. The replacement may itself use “references” to the matched text. For example, an author list in the format “first-name last-name” may be converted to “last-name first-name”.

Streaming String transducers provide an elegant model for such string operations. Moreover, they have an important property that the pre-image of a regular language under a replaceall remains regular. Since we additionally need to ensure that matches are “left-most longest”, we introduce “prioritised streaming string transducers” along the lines of Berglund and van der Merwe. Using these techniques, we extend the string constraint solver OSTRICH to support this replaceall operation.

In this talk, we discuss the application of streaming string transducers in constraint satsifaction, and briefly summarise some theoretical and experimental results.

Recent work in theoretical computational linguistics highlights the importance of regular transformations over strings and trees in characterizing linguistic generalizations. This talk reviews some of the main results of this research program. Regular transformations provide an upper bound on morpho-phonological processes in natural languages. Particular subclasses appear to be sufficient, and these subclasses are generally (much) less than FO(<). Additionally, these subclasses are learnable with relatively low time and data complexity in ways the full class of regular transformations is not.

The recently introduced notion of delay for streaming string transducers (SST) has various applications, one of which is demonstrated through the DecompositionTheorem: This theorem states that every $k$-valued SST (where each input is mapped to at most $k$ outputs) can be decomposed into a finite union of $k$ single-valued SST. While similar results have been established in other settings such as finite state transducers, tree transducers and weighted automata, the specific case of SST remained open up to this day. We present a solution that relies on the notion of delay to extract, one after the other, $k$ single-valued SST from a given $k$-valued SST, thus creating the desired decomposition. The Decomposition Theorem holds significant interest due to its implications: it reveals that $k$-valued SST recognise a robust class of functions, for instance equivalent to those recognised by finite-valued transducers. Moreover, it shows that this class enjoys good algorithmic properties. For instance, equivalence between finite-valued SST can be decided efficiently.

We present a class of transductions with exponential growth based on logical interpretations, but with monadic second-order parameters instead of first-order ones. We study some of the closure properties of this class as well as potential alternative characterizations.

While one-valued streaming string transducers define a very robust class of transductions, finite-valued ones still enjoy some good properties. Recent results (see talk by Ismaël Jecker) show that they are equivalent to finite-valued two-way transducers. Moreover, jointly with G. Puppis, we have shown their equivalence problem to be decidable (ICALP 2019).

In this talk I presented a conjecture towards deciding whether a streaming string transducer is finitely valued. The characterisation conjectured reminds of the one for one-way transducers obtained by A. Weber, and exploits ideas about state invariants involved in the equivalence decision procedure for finitely-valued streaming string transducers.

This talk was about the connections between transducer theory and functional programming. An important role is played by type systems inspired from linear logic – linearity in programming language theory provides counterparts to various “copyless” or “single-use” restrictions on automata.

1. 1.

   In our “implicit automata in typed $\lambda$-calculi” research programme [1, 2], Cécilia Pradic and I show that natural questions concerning the expressive power of theoretical functional programming languages turn out to have automata-theoretic answers. In particular, the study of a linear $\lambda$-calculus led us to discover a robust subclass of polyregular functions [3].

2. 2.

   Meanwhile, machine models manipulating higher-order data (functions as first-class values, that may themselves take functions as arguments), taking inspiration from the higher-order grammars of the 1970s, arise from the study of composition hierarchies of transducers [4]. In this context, transducers whose memory stores linear $\lambda$-terms have been used to characterize MSO transductions of trees [5] – which is very close to one of the results of [2].

An example of phenomenon (2) is the composition of streaming string transducers (SSTs, the topic of many other talks): their registers store concatenable strings, which should be seen as order-1 functions on appendable strings, so composing $n$ SSTs results in a machine using order-$n$ registers.

With this point of view, the natural counterpart of SSTs on trees is a bottom-up transducer whose registers store tree contexts, as noted in [6, 7]. But in fact, this model is none other than the much older macro tree transducer (MTT) [8]! A recursive equation such as $q_1⟨a(t,u)⟩=b(q_2⟨u⟩,q_3⟨t⟩)$, read as a top-down propagation of states in the old-style presentation of MTTs ($=$ becomes $\to$), can also be understood as a bottom-up computation of registers ($=$ becomes $:=$). This remark was the subject of its own lightning talk.

This talk highlights foundational and recent results on learning regular transformations. Restrictions on the class of grammars, combined with various ingredients in a learning paradigm, show positive results. The talk overviews positive learning results on subsequential string functions, as well as the subclass of input and output strictly local string functions. On the empirical side, using classes of regular string transformations allows us to study the inference capabilities of black box modes such as neural networks. The talk showcases several negative results in this area.

In this talk, we present Annotated automata (AnnA), a non-deterministic transducer model that outputs a subsequence of increasing positions annotated from a finite alphabet. We show that this model is suitable for encoding computational models for complex event recognition (CER) and information extraction. We show that AnnA allows for streaming enumeration algorithms, which implies the evaluation problems in the previously mentioned settings. Further, one can extend the annotation approach to visibly pushdown automata, context-free grammars, or compressed words, with similar efficient algorithmic results. Finally, we present some implementations of AnnA and the algorithms in the context of CER and information extraction.

We give a summary of three definability results that were established recently. First, we discuss how to decide whether a given bottom-up tree translation can be realised by a top-down tree transducer. This is somewhat similar to deciding whether a left-to-right finite state string transducer can be realised by a right-to-left one (simply by checking the “twinning” property), but turns out to be far more complex in our tree case. This result was presented with Helmut Seidl at ICALP’2020. In fact, we cannot yet prove this result in its entirety, but we can decide whether for a given “uniform-copying” top-down tree transducer with look-ahead an equivalent transducer exists that has no look-ahead (but is uniform copying). It is well-known that every bottom-up tree transducer can be realised by a top-down tree transducer with look-ahead. Next, we show that for a given top-down tree transducer with look-ahead it is decidable whether or not an equivalent linear top-down transducer (without look-ahead) exists. This result will appear in IJFCS with Helmut Seidl and Martin Vu. Lastly, we present preliminary results concerning the conjecture (of Joost Engelfriet), that a macro tree translation can be realised by an attributed transducer (with look-around) if and only if the translation has linear increase of the number of distinct output subtrees with respect to the input tree size.

We consider two natural subclasses of deterministic top-down tree-to-tree transducers, namely, linear and uniform-copying transducers. For both classes we show that it is decidable whether the translation of a transducer with look-ahead can be realized by a transducer from the same class without look-ahead.

The transducers constructed in this way, may still make use of inspection, i.e., have an additional top-down deterministic tree automaton restricting the domain. We provide a second procedure which decides whether inspection can be removed and if so, constructs an equivalent transducer without inspection.

The construction relies on a precise abstract interpretation of inspection requirements and a dedicated earliest-normal form for linear as well as uniform-copying transducers which can be constructed in polynomial time. As a consequence, equivalence of these transducers can be decided in polynomial time.

Applying these results to deterministic bottom-up transducers, we obtain that it is decidable whether or not their translations can be realized by deterministic uniform-copying top-down transducers without look-ahead (but with inspection) - or without both look-ahead and inspection.

In a recent paper (ICALP, 2020) Bojańczyk and I have shown that single-use register automata are equivalent to orbit-finite monoids. In this talk I am going to extend this result to transducers. For this purpose, I introduce a new algebraic model called local semigroups transductions, and I show that it is equivalent to single-use register Mealy machines.

Given a nondeterministic tree transducer, it is a natural question to ask whether or not it is functional. i.e., whether its induced tree transformation is a (partial) function? ésik has shown that this problem is decidable even in the presence of look-ahead. We extend this result by showing that even for compositions of tree transducers the question of functionality is decidable. We prove this result by reducing the problem to the functionality of a single top-down tree transducer with look-ahead.

The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. In this talk we present a new notion of delay tailored to measure the similarity between streaming string transducers (SSTs). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SST equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.