IRP∩LSI is not RE( Introduction of the manuscript:
Tetsuya Ishiu, “IRP is Strictly Larger Than MTT”
http://twitdoc.com/c/xrwhnm )presentation by Kazuhiro Inaba (NII, kinaba@nii.ac.jp)

IPL-Group Seminar
May 25, 2010

The Talk is about a Property on…
String/Tree Transformations
e.g.,
dup(s) = s ++ sreverse([]) = []reverse(x:xs)= reverse(xs)++[x]andRegular Languages
e.g.,

a*|b*a((a|b)*|c)*bThe Property IRP
Inverse Regularity Preserving
A function f is IRP iff
For any regular language L,
the inv. img. f-1(L) = {s | f(s) ∈ L} is regular

Example: “dup” and “reverse”
Example:a*|b*???

dup(s) =s ++ sa*b*

AgendaWhy you should be interested in IRP?
IRP-based typechecking
Always-IRP computation models

Q: “Do the models cover all IRP?”
A: “No, IRP∩LSI is not RE.”
Proof Tech. 1: Clever diagonalization
Proof Tech. 2: Slenderness of languages

Why IRP?
Typechecking

f :: LIN → LOUT ？

Verify that a transformation always
generates valid outputs from valid inputs.

fLIN

LOUT

XSLT Template forformating bookmarks

XBEL Schema

XHTML Schema

PHP Script

Arbitrary String

String not containing“<script>”Why IRP?
Typechecking

f :: LIN → LOUT ？

If f is IRP, we can check this by …

f is type-correct⇔ f(LIN) ⊆ LOUT-1⇔ LIN ⊆ f (LOUT)(for experts: f is assumed to be deterministic)FAQ: WhyIRP?

ForwardRP also enables typechecking
FRP-based checking: f(LIN) ⊆ LOUT
IRP-based checking : LIN ⊆ f-1(LOUT)
Reasons
IRP provides more useful counter examples.
Many functions in practice tend to be IRP,
but not so for FRP. E.g., “dup”.

IRP-Based Typechecking
Not all transformations are IRP

The trend is to define a restrictedlanguage whose programs are always IRP
and present sound & complete
typechecking for themor use them as clearly defined targets forapproximate checking

Famous Computation Models ofIRP Tree Transformations(note: X* := {f1・f2・…・fn | n∈Nat, fi∈X })MTT* = PTT* = ATT* = …
PTT

MTT [Engelfriet&Vogler 1985][Milo&Suciu&Vianu 2000]

ATT [Fülop 1981]

MSOTT[Courcelle 1994]

BTGSM[Thatcher70,Rounds70]

One Example: MTTMTT = The class of functions on trees definedby (mutual) structural recursion +accumulating parameters
MTT* = Finite composition of MTTs

SyntaxExample

MTT ::= FUN … FUN
FUN ::= f(A(x1,…,xn), y1,…,yk) →RHS ::= C( RHS, … , RHS )| f(xi, RHS, …, RHS) | yi

RHSstart( A(x1) )→ double( x1, double(x1, E) )double( A(x1), y1) → double( x1, double(x1, y1) )double( B, y1 )→ C( y1, y1 )Question
Do they cover all IRP transformations?

MTT* = PTT* = ATT* = .. = IRP ?
⊆ is known⊇?
(Attribution: I’ve first heard this question fromSebastian Maneth, who heard it from Keisuke Nakano)Answer: “No”
K. Inaba, PPL 2010 Short Presentationn2^^ntower( “a..a” ) = “aa…aa”
where 2^^0 = 1, 2^^(n+1) = 22^^nis IRP but not in MTT*

But its growth is toooooooooo fast!
Aren’t there any “milder” counterexample?

LSI: Linear Size Increase =∃c. ∀t. len(f(t))＜c・len(t)MTT* = PTT* = ATT* = …
PTTMTTATTMSOTT= MSOTT*= (MTT*=PTT*=…)∩LSI= (MTT∩LSI)* = …

GSM
TBNew Question
MSOTT= (MTT*=PTT*=ATT*=…)∩LSI= IRP ∩ LSI ?

⊆ is known⊇?

Answer: “No”
There exists a IRP∩LSI transformationthat cannot be written in MSOTT
Main Theorem of This Talk
The class of IRP∩LSI transformations
is not recursively enumerable.
(There’s no Turing machine that enumerates all of them)THE PROOF

Overview
The class of IRP∩LSI transformations
is not recursively enumerable.
(There’s no Turing machine that enumerates all of them)

Basic idea isthe Diagonalization (対角線論法)“Give me a enumeration {g1, g2, g3, …} of theclass of functions. Then I will show you afunction f not in the enumeration.”Diagonalization(Assuming a fixed alphabet,) we canenumerate all string/trees: {t1, t2, t3, …}
Given enumeration {g1, g2, g3, …} of the class

We construct f as:f( ti ) := arbitrary tree
except gi(ti)Caution!
f may not be IRP nor LSIt1 t2 t3 t4
g1 ××
g2×
g3×
g4

…

…

…

Diagonalization
The class of IRP∩LSI transformations
is not recursively enumerable.
(There’s no Turing machine that enumerates all of them)

What we really want is this:“Give me a enumeration {g1, g2, g3, …}of the IRP ∩ LSI functions. Then I willshow you a function f not in theenumeration but in IRP∩LSI.”
which derives contradiction.

Diagonalization
We can enumerate all regular languages:{R1, R2, R3, …}
Given enumeration {g1, g2, g3, …} of the class

We construct f so that:g1f( t ) ≠ gi(t) for someg2t ⇜ {R1,R2,…,Ri}
g3-1f ( Ri ) = almost Ri
g4…

R1 R2 R3 R4 …
××××…

Preparation
Known facts on Regular Languages
All finite sets are regular
They are closed under boolean ops.
If R1, R2 ∈ REG thenR1 ∩ R2 ∈ REG
R1 ∪ R2 ∈ REG～R1 ∈ REG

“Slenderness” is decidable[Paun&Salomaa 1993] “Language-Theoretic Problems Arising from
Richelieu Cryptosystems”, TCS(116), pp.339-357

Preparation: Slenderness
A set L of string is slender iff∃c. ∀n. #{s | s∈L, len(s)=n } ≦ c{1, 11, 111, 1111, …} is slender{0, 1, 10, 11, 100, 101, …} is not slender
L1,L2 is slender  L1∪L2 is slender
L1,L2 is co-slender  L1∩L2 is co-slender

Co-slender ⇔ complement is slenderNot co-slender ⇔ a plenty of supply ofnon-members

Main Lemma
Let {g1, g2, … } be an enumeration of total functions.
Let {R1, R2, … } be an enumeration of all regular langs.
Then we can construct {(f0,D0), (f1,D1), …} such that
Φ=f0 ⊆ f1 ⊆ f2 ⊆ …
# increasing list of partial functions
Φ=D0 ⊆ D1 ⊆ D2 ⊆ …
# eventually covers all
Either Ri ⊆ Di or ～Ri ⊆ Di
regular languages∃x∈Di. fi(x) ≠ gi(x)# different from every gi
Di is not co-slender# technical detailfi is bijective on Di# almost identity
For all but finitely many x∈Di, fi(x) = x(hence IRP)
∀x∈Di. len( fi(x) ) = len(x)# linear size increaseRequirements- Dn+1 must cover
either Rn+1 or ～Rn+1

Proof of the Main Lemma- Dn+1 must not be
co-slender

By Induction-f0 = D0 = Φ- Dn+1 must haveelems
distinguishSuppose we already have fn andDn ,toandgn+1 and fn+1
construct fn+1 and Dn+1.
Set ofAll Strings

Dn+1 = dom(fn+1)

Dn = dom(fn)Rn+1

where fn+1 ≠ gn+1

Proof of the Main Lemma
Dn is not co-slender. Take x, y ∈ ～Dn s.t. len(x)=len(y) but x≠yThen Take
Dn+1 := Dn ∪ {x,y} ∪ Rn
if it is not co-slender

Dn+1 := Dn ∪ {x,y} ∪ ～Rnotherwise↑this becomes
not-co-slender!

Requirements- Dn+1 must cover
either Rn+1 or ～Rn+1- Dn+1 must not beco-slender-- Dn+1 must haveelems to distinguishgn+1 and fn+1

Proof of the Main Lemma
We then construct fn+1fn+1( s ) = fn(s)if gn+1(x) = x
fn+1( x ) = yfn+1( y ) = x

otherwisefn+1( x ) = x
fn+1( y ) = yfn+1( s ) = s

if s ∈ Dn
Requirements- fn ⊆ fn+1
- fn+1 is bijection on Dn+1
- fn+1 is length preserving- fn+1 differs from gn+1
- fn+1 is almost identity

for all other s ∈ Dn+1
Q.E.D.

The class of IRP∩LSI transformationsMainTheorem
is not recursively enumerable.

Suppose it is. By previous lemma,let f = ∪i∈Nat fi
f is equal to none of {g1, g2, …}
f is a total function
Because each singleton {si} regular set must becovered by Di=dom(fi) eventually

f is LSI (in fact, length-preserving)
f is IRP
next page

Main Theorem
f is IRP (In fact, f is FRP by almost the same proof, too.)Take any regular set Ri.
If Ri ⊆ Di
Since fi is bijection & identity except fin. points,f-1(Ri) = fi-1(Ri) differs only finitely from Ri
 regular

If ～Ri ⊆ Di
Similarly, f-1(～Ri) is regular
f is also a bijection, so f-1(Ri)=～f-1(～Ri)
 regularContradiction.
Q.E.D.

Notes
If {g1, g2, … } is an enumeration ofcomputable total functions,
Then the f is a computable function.
f-1 (as a mapping on regular languages) iscomputable.

<Summary> There exists f such that- f :: string string is computable & total- f-1 :: REG REG is computable & total- f is length-preserving, IRP, and FRP- f is not in MSOTT = MTT*∩LSI