FO definable Transformations of Infinite strings

FO definable Transformations of Infinite strings

Vrunda Dave, S. Krishna, Ashutosh Trivedi

Outline

Introduction

Three formalisms for transductions Related work

Aperiodic transformations for Infinite strings Aperiodic two way transducer

Aperiodic streaming string transducer Equivalence results and Proof ideas

SSTsf

⊂

⊂

Conclusion

Introduction

Three formalisms for transformations:

Logic

Introduction

Three formalisms for transformations:

Logic

Introduction

Three formalisms for transformations:

Two way machines

Logic

Introduction

One way machines with finite registers Three formalisms for transformations:

Two way machines

Logic Transducer

Logic Transducer

[Courcelle’94]

Logic Transducer

input

[Courcelle’94]

a1 a2 a3 a4 a5 a6 a7 a8

Logic Transducer

input

[Courcelle’94]

a1 a2 a3 a4 a5 a6 a7 a8

Logic Transducer

input

dom ✔

⌃

[Courcelle’94]

a1 a2 a3 a4 a5 a6 a7 a8

Logic Transducer

input

dom ✔

⌃

[Courcelle’94]

a1 a2 a3 a4 a5 a6 a7 a8

Logic Transducer

input

dom ✔

output

⌃

[Courcelle’94]

a1 a2 a3 a4 a5 a6 a7 a8

Logic Transducer

input

dom ✔

a

b r w

g d b

a r

output

⌃

[Courcelle’94]

a1 a2 a3 a4 a5 a6 a7 a8

Logic Transducer

input

dom ✔

nodes edges

✔

✔

a

b r w

g d b

a r

output

⌃

[Courcelle’94]

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

where u_i 2 {a, b}^⇤ and v 2 {a, b}^! FO/ MSO transducer

a b b ^# b a # (a, b)^! input:

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

where u_i 2 {a, b}^⇤ and v 2 {a, b}^! FO/ MSO transducer

a b b ^# b a # (a, b)^! input:

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

where u_i 2 {a, b}^⇤ and v 2 {a, b}^! FO/ MSO transducer

a b b ^# b a # (a, b)^! input:

copy 3:

copy 2:

copy 1:

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

where u_i 2 {a, b}^⇤ and v 2 {a, b}^! FO/ MSO transducer

a b b ^# b a # (a, b)^! input:

copy 3:

copy 2:

copy 1:

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

1 (x) = ² (x) = L (x) ^ ¬L_#(x) ^ reach_#(x)

FO/ MSO transducer

reach_#(x) = 9y(x y ^ L_#(y))

3 (x) = L_#(x) _ ¬reach_#(x)

a b b ^# b a # (a, b)^! input:

a b b b a

a b b b a

# _# (a, b)^!

copy 3:

copy 2:

copy 1:

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

1 (x) = ² (x) = L (x) ^ ¬L_#(x) ^ reach_#(x)

FO/ MSO transducer

reach_#(x) = 9y(x y ^ L_#(y))

3 (x) = L_#(x) _ ¬reach_#(x)

a b b ^# b a # (a, b)^! input:

a b b b a

a b b b a

# _# (a, b)^!

copy 3:

copy 2:

copy 1:

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

1 (x) = ² (x) = L (x) ^ ¬L_#(x) ^ reach_#(x)

FO/ MSO transducer

reach_#(x) = 9y(x y ^ L_#(y))

2,2(x, y)

1,3(x, y)

3 (x) = L_#(x) _ ¬reach_#(x)

Two way machine

Two way machine [Rabin, Scott’59]

[Ehrich, Yau’71]

Two way machine

input

[Rabin, Scott’59]

[Ehrich, Yau’71]

Two way machine

a1 a2 a3 a4 a5 a6 a7 a8

input

[Rabin, Scott’59]

[Ehrich, Yau’71]

Two way machine

a1 a2 a3 a4 a5 a6 a7 a8

input

output

[Rabin, Scott’59]

[Ehrich, Yau’71]

Two way machine

a1 a2 a3 a4 a5 a6 a7 a8

input

output

[Rabin, Scott’59]

[Ehrich, Yau’71]

Look-around automaton

Look-around automaton

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

Look-around automaton

w

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

#

Look-around automaton

w

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

#

suffix prefix

Look-around automaton

w

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

#

suffix prefix

property: suffix does not contain #

Look-around automaton

w

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v

#

suffix prefix

property: suffix does not contain #

#

a, b

#, a, b

p r

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

b b

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

a

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

b b

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

a

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

b b a b

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

a b

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

b b a b #

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

a b

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

↵ |↵, 1 ↵ |↵, +1

↵ 2 {a, b}

` |✏, +1

q₀ q₁ q₂ q₃

` |✏, +1

# |✏, 1 # |✏, +1

F = {{q₁}}

⊢ a b b # (a + b)^ω

b b a b # (a + b)^ω

# |#, +1

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

a b

↵, p|✏, +1

↵, r|↵, +1

Two way Transducer (2WST)

One way machine with finite registers

One way machine with finite registers

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x a y z

output :

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x a y z

output :

copyless update :

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x a y z

output :

copyless update : x = ax y = bycz z = c

x = ax y = bycz z = cx

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x a y z

output :

copyless update : x = ax y = bycz z = c

x = ax y = bycz z = cx

✔

[Alur, Černý’10]

One way machine with finite registers

a1 a2 a3 a4

input :

registers : x, y, z…

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x = ax y = bycz z = c

x = 𝜀 y = cz z = by

x a y z

output :

copyless update : x = ax y = bycz z = c

x = ax y = bycz z = cx

✔ ❌

[Alur, Černý’10]

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

Streaming String Transducer (SST)

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

a b b # (a + b)^ω x:

y:

z:

𝜀 𝜀 𝜀

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

a b b # (a + b)^ω x:

y:

z:

𝜀 𝜀 𝜀

aa a 𝜀

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

a b b # (a + b)^ω x:

y:

z:

𝜀 𝜀 𝜀

aa a

𝜀 𝜀 𝜀

baab ab

bbaabb abb

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

a b b # (a + b)^ω x:

y:

z:

𝜀 𝜀 𝜀

aa a

𝜀 𝜀 𝜀

baab ab

bbaabb abb

bbaabb#

𝜀 𝜀

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

a b b # (a + b)^ω x:

y:

z:

𝜀 𝜀 𝜀

aa a

𝜀 𝜀 𝜀

baab ab

bbaabb abb

bbaabb#

𝜀 𝜀

bbaabb#

(a + b)^ω

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

# x := x#

y := ✏ z := ✏

↵ x := x

y := ↵y↵

z := z↵ ↵ x := x

y := ↵y↵

z := z↵

# x := xy# y := ✏

z := ✏

q₁ q₂

a b b # (a + b)^ω x:

y:

z:

𝜀 𝜀 𝜀

aa a

𝜀 𝜀 𝜀

baab ab

bbaabb abb

bbaabb#

𝜀 𝜀

bbaabb#

(a + b)^ω

f(u₁#u₂# . . . #u_n#v) = u^R₁ u₁#u^R₂ u₂# . . . #u^R_n u_n#v where u_i 2 {a, b}^⇤ and v 2 {a, b}^!

F ({q₂}) = xz

Streaming String Transducer (SST)

↵ 2 {a, b}

Related Work

Related Work

FO MSO

Related Work

FO MSO

Finite strings Infinite strings Related Work

FO MSO

Finite strings Infinite strings

MSOT = 2WST MSOT = SST

✔

Related Work

[Engelfriet, Hoogeboom’01]

[Alur, Černý’10]

FO MSO

Finite strings Infinite strings

MSOT = 2WST MSOT = SST

✔

MSOT = 2WSTla = SST

[Alur, Filiot, Trivedi’12]

✔

Related Work

[Engelfriet, Hoogeboom’01]

[Alur, Černý’10]

FO MSO

Finite strings Infinite strings

MSOT = 2WST MSOT = SST

✔

FOT = Ap 2WST FOT = Ap SST

✔

MSOT = 2WSTla = SST

[Alur, Filiot, Trivedi’12]

✔

Related Work

[Engelfriet, Hoogeboom’01]

[Alur, Černý’10]

[Carton, Dartois’15]

[Filiot, Krishna, Trivedi’14]

FO MSO

Finite strings Infinite strings

MSOT = 2WST MSOT = SST

✔

FOT = Ap 2WST FOT = Ap SST

✔

MSOT = 2WSTla = SST

[Alur, Filiot, Trivedi’12]

✔

？

Related Work

[Engelfriet, Hoogeboom’01]

[Alur, Černý’10]

[Carton, Dartois’15]

[Filiot, Krishna, Trivedi’14]

FO MSO

Finite strings Infinite strings

FOT = Ap 2WST = Ap SST

✔

MSOT = 2WSTla = SST

✔

？

Related Work

FO MSO

Finite strings Infinite strings

FOT = Ap 2WST = Ap SST

✔

MSOT = 2WSTla = SST

✔

Related Work

FO MSO

Finite strings Infinite strings

FOT = Ap 2WST = Ap SST

✔

MSOT = 2WSTla = SST

✔

Related Work

FOT = Ap 2WSTsf = Ap SST

FO MSO

Finite strings Infinite strings

FOT = Ap 2WST = Ap SST

✔

MSOT = 2WSTla = SST

✔

Related Work

FOT = Ap 2WSTsf = Ap SST Infinite strings

This Talk FO

MSO

Finite strings Infinite strings

FOT = Ap 2WST = Ap SST

✔

MSOT = 2WSTla = SST

✔

Related Work

FOT = Ap 2WSTsf = Ap SST Infinite strings

Aperiodicity

Outline

Introduction

Three formalisms for transductions Related work

Aperiodic transformations for Infinite strings Aperiodic two way transducer

Aperiodic streaming string transducer Equivalence results and Proof ideas

SSTsf

⊂

⊂

Conclusion

Transition monoid of a Finite state automaton

[Schutzenberger’65]

Transition monoid of a Finite state automaton

r t q

a

b b a

b a

[Schutzenberger’65]