Project topics and materials
Get Complete Project Material File(s) Now! »
Functional Two-way Finite-State Transducers
As defined in Section 1.3, the class of functions realised by functional 2FSTs is the class of regular functions [EH01]. [AC10] introduced the copyless DSST model and proved that the class of func-tions it realises is exactly the class of regular functions, by providing construc-tions from sequential 2FSTs to copyless DSSTs and from copyless DSSTs to de-terministic Monadic Second Order Transductions. From these results, we draw the following proposition.
Proposition 2.1. Let A, B be two alphabets. Let f be a function from A∗ to B∗.
The following assertions are equivalent:
1. f is a regular function,
2. f can be realised by a functional 2FST,
3. f can be realised by a copyless DSST.
Remark. Some copyful DSSTs are not within the class of regular functions. In-deed, copyfulness gives the ability to describe transductions whose output grows non-linearly w.r.t. the growth of their input word. For example, Figure 2.1 depicts a copyful DSST that realises the function u ∈ {a}∗ 7→a2|u|, whose output obviously grows exponentially. a X=XX X = a q X
Functional Finite-State Transducers
As defined in Section 1.2, the class of functions realised by functional FSTs is the class of rational functions [Ber13]. The following proposition extends this connection to copyful appending DSSTs, using a construction similar to [Alu+13].
Proposition 2.2. Let A, B be two alphabets. Let f be a function from A∗ to B∗.
The following assertions are equivalent:
1. f is a rational function,
2. f can be realised by a functional FST,
3. f can be realised by a copyful appending DSST.
The equivalence between 1 and 2 comes from the definition of rational func-tions. We will detail the equivalence between 2 and 3 in the next two subsections as it will be useful when considering S2Cs. Remark. In contrast to regular functions, we need copyfulness to fully express the rational functions with appending DSSTs. We will see in Section 2.4 that, if we only use copyless appending DSSTs, we loose some form of non-determinism and obtain the class of multi-sequential rational functions.
From Copyful Appending DSSTs to Functional FSTs
Let S = (Q, X , qinit, ν, δ, µ) be a copyful appending DSST. We build an equiva-lent functional FST T = (Q0, tinit, tfinal, T ). States The states of T are pairs of a state and a register of S, i.e. Q0 = Q × X . Each state of T thus designates a register of S, the content of which has already been outputted.
Initial Function Initial states of T must produce the initial valuation for their designated register. w for all X ∈ X such that ν(X) = w, then −→ (qinit, X) T Transitions We add a transition in T for each assignation Y = X ·w in S. These transitions must produce the word that is appended to the designated register of their source state. for all p, q ∈ Q, a ∈ A, w ∈ B∗ and X, Y ∈ X , a|σ a|w such that p −→ q and σ(Y ) = X · w, then (p, X) −−→ (q, Y ) S T Final Function Final states of T correspond to final states of S. They must also produce the word appended to their designated register, if any. ∗forallp∈Q,w∈B and X ∈ X X· w w such that p −−→, then (p, X) −→ S T.
The following lemma states that S and T are equivalent. As S is functional by definition, so is T , and this also proves the implication from 3 to 2 of Proposi-tion 2.2.
From Functional FSTs to Copyful Appending DSSTs
Let T = (Q, tinit, tfinal, T ) be a functional FST. We now build an equivalent copy-ful appending DSST S = (Q0, X , qinit, ν, δ, µ). Intuitively, this construction extends the classical power set construction used to determinise a non-deterministic finite-state automata. States The states of S are subsets of states of T , i.e. Q0 = 2Q. Registers We use one register per state of T to store the output T would have produced before reaching each of these states.
X = {Xq | q ∈ Q} Initial State The initial state of S is the set of initial states of T . We define the corresponding initial valuation accordingly. w qinit = dom(tinit) and ν = {Xq 7→w | −→ q} T.
Transitions Given a state of S and a letter a ∈ A, we identify the set of tran-sitions of T that are enabled, compute the new state, and update the registers accordingly. We define δ as follows: for all S1 ∈ Q0 and a ∈ A, such that S2 = {q2 | ∃q1 ∈ S1 ∧ q1 a|w }6=∅, −−→ q2 T.
From Copyless Appending DSSTs to Multi-Sequential Functional FSTs
Let S = (Q, X , qinit, ν, δ, µ) be a copyless appending DSST with X = {X1, . . . , Xk} for some k ∈ N. We build an equivalent k-sequential functional FST T = ∪i∈{1,…,k}Ti with Ti = (Q0i, tiinit, tifinal, Ti) for i ∈ {1, . . . , k}. We build each Ti from S with the construction of Section 2.2.1 but keeping only (qinit, Xi) as its unique initial state and trimming it appropriately. The following lemma proves the forward implication of Proposition 2.6. Lemma 2.7. Ti is sequential, for all i ∈ {1, . . . , k}, and [[T ]] = [[S]]. Proof. As S is deterministic, for all p ∈ Q and a ∈ A, there is only one transition a|σ p −→ q, for some σ ∈ Upd (X , B). As S is copyless, for all X ∈ X , there is only one register Y such that σ(Y ) = Xw, for some w ∈ B∗. We obtain that for all a|w a|w0 (q0, Y 0) then w = w0, p ∈ Q, X ∈ X and a ∈ A, if (p, X) −−→i (q, Y ) and (p, X) −−→i T T q = q0 and Y = Y 0. Therefore Ti is sequential.
We now prove the equivalence between T and S. Let T 0 the functional FST equivalent to S, obtained by the construction of Section 2.2.1. This construction is such that the initial states of T 0 are {(qinit, Xi) | i ∈ {1, . . . , k}}, i.e. the initial states of the Ti’s. Therefore, we obtain that [[T ]] = [[T 0]] and thus [[T ]] = [[S]].
From Multi-Sequential Functional FSTs to Copyless Appending DSSTs
Let T = ∪i∈{1,…,k}Ti be a k-sequential functional FST where for all i ∈ {1, . . . , k}, Ti = (Q0i, tiinit, tifinal, Ti). From each of the Ti, we build an equivalent appending DSST with 1 register, using the construction of Section 2.3. We then make the product of these k DSSTs and we obtain an appending DSST S with k registers. It can easily be shown that [[S]] = [[T ]]. As every update of S is of the form Xi = Xiw, for some i ∈ {1, . . . , k} and w ∈ B∗, we obtain that S is copyless, therefore proving the reverse implication of Proposition 2.6.
Table of contents :
Abstract
Résumé
Remerciements
Contents
Introduction
About Transformations
Formal Methods for Safer Systems
Efficient Evaluation of Models
Models of Transformations
General Methodology
Outline of this Thesis
1 Models of Transducers
1.1 Preliminaries
1.2 Finite-State Transducers (FST)
1.3 Two-way Finite-State Transducers (2FST)
1.4 Deterministic Streaming String Transducers (DSST)
1.5 String-to-Context Transducers (S2C)
1.6 Summary
2 Comparison of Expressiveness
2.1 Functional Two-way Finite-State Transducers
2.2 Functional Finite-State Transducers
2.3 Sequential Finite-State Transducers
2.4 Multi-Sequential Functional Finite-State Transducers
2.5 Functional String-to-Context Transducers
2.6 Sequential String-to-Context Transducers
2.7 Summary
3 Sequentiality of Finite-State Transducers
3.1 Characterisation of Sequential Functions
3.2 Construction of a Sequential Equivalent
3.3 Deciding Sequentiality
3.4 Sequentiality in Other Contexts
4 k-Sequentiality of Finite-State Transducers
4.1 Preliminaries
4.2 Characterisation of k-Sequential Functions
4.3 Construction of a k-Sequential Equivalent
4.4 Deciding k-Sequentiality
4.5 Minimisation of the Degree of Sequentiality
5 Sequentiality of String-to-Context Transducers
5.1 Preliminaries
5.2 Characterisation of Sequential S2Cs
5.3 Combinatorial Analysis
5.4 Construction of an Equivalent Sequential S2C
5.5 Deciding Sequentiality of S2Cs
5.6 Related Work
Conclusion
List of Figures
List of Tables
Bibliography
