A Technical report by Kazutaka Matsuda, Zhenjiang Hu and Masato Takeichi
An implementation of the version 0.0.1 using Haskell
Currently, the program takes an input forward transformation form the standard input, derives the complement function of the input, calculates the inverse of the tupled function of the input forward transformation and the derived complement function, and returns the derived complement function and the calculated the inverse of the tupled function.
For example, for the following input (assume that this input is in a file named "test1.txt")
data T = <a>(S) | >b<(S) | <c>; data S = <a>(S) | >c<; g ( x :: T ) = f(x); f( <a>(x) ) = <a>(f(x)); f( <b>(x) ) = <a>(f(x)); f( <c> ) = <c>;
with typing
> bidirectionalizer_f < test1.txt
the program without type specialization flag returns the following complement function and the inverse of tupled function.
---------------------
Complement Function
---------------------
46 ==> {;RWithout []}
26 ==> {;RNothing}
25 ==> $
19 ==> <"c">[26,25,25]
19 ==> <"a">[26,f,25]
14 ==> <"c">[26,25,25]
14 ==> <"a">[26,f,25]
9 ==> <"c">[26,25,25]
9 ==> <"a">[26,f,25]
5 ==> <"c">[26,25,25]
5 ==> <"a">[26,5,25]
4 ==> <"c">[26,25,25]
4 ==> <"b">[26,5,25]
4 ==> <"a">[26,5,25]
0 ==> $
0 ==> <_>[46,0,0]
f ==> <"c">[26,25,25]
f ==> <"a">[26,f,25]
1:
g_c(x :: Type4) =
f_c__9
where
f_c__9 :: Type9 = f_c(x)
2:
f_c(<a>(x :: Type0)) =
R_2[f_c__14]
where
f_c__14 :: Type14 = f_c(x)
3:
f_c(<b>(x :: Type0)) =
R_3[f_c__19]
where
f_c__19 :: Type19 = f_c(x)
4:
f_c(<c>) =
R_4[]
-----------------
Inverted Tupled
-----------------
46 ==> {;RWithout []}
26 ==> {;RNothing}
25 ==> $
5 ==> <"c">[26,25,25]
5 ==> <"a">[26,5,25]
4 ==> <"c">[26,25,25]
4 ==> <"b">[26,5,25]
4 ==> <"a">[26,5,25]
0 ==> $
0 ==> <_>[46,0,0]
f ==> <"c">[26,25,25]
f ==> <"a">[26,f,25]
1:
g_Tinv((f__9 :: Typef, f_c__9 :: Type)) =
x
where
x :: Type4 = f_Tinv(f__9,f_c__9)
2:
f_Tinv((<a>(f__14 :: Typef), R_2[#f_c__14])) =
<a>(x)
where
x :: Type0 = f_Tinv(f__14,f_c__14)
3:
f_Tinv((<a>(f__19 :: Typef), R_3[#f_c__19])) =
<b>(x)
where
x :: Type0 = f_Tinv(f__19,f_c__19)
4:
f_Tinv((<c>, R_4[])) =
<c>
The above output is a bit hard to read because types are not represented in data formart.
We will soon provide a new implementation that generates more pretty outputs.
Here, 4 in the transitions corresponds to the type T,
and 5 in the transitions corresponds to the type S.
The type name of the form TypeX in the program corresponds the state X in the transitions above.
If you use the implementation with type specialization flag as
> bidirectionalizer_f < test1.txt
the implementation returns a different result for the input as follows.
---------------------
Complement Function
---------------------
58 ==> {;RNothing}
57 ==> <"c">[58,56,56]
57 ==> <"a">[58,f[0],56]
56 ==> $
34 ==> <"c">[58,56,56]
34 ==> <"a">[58,f[5],56]
29 ==> <"c">[58,56,56]
29 ==> <"a">[58,f[5],56]
13 ==> {;RNothing}
12 ==> $
10 ==> <"c">[13,12,12]
10 ==> <"a">[13,10,12]
9 ==> <"c">[13,12,12]
9 ==> <"b">[13,10,12]
9 ==> <"a">[13,10,12]
7 ==> {;RWithout []}
6 ==> $
6 ==> <_>[7,6,6]
5 ==> $
5 ==> <_>[7,6,6]
3 ==> {;RNothing}
2 ==> $
1 ==> <"c">[3,2,2]
1 ==> <"a">[3,1,2]
0 ==> <"c">[3,2,2]
0 ==> <"a">[3,1,2]
f[5] ==> <"c">[58,56,56]
f[5] ==> <"a">[58,f[5],56]
f[0] ==> <"c">[58,56,56]
f[0] ==> <"a">[58,f[0],56]
1:
f[0]_c(<a>(x :: Type0)) =
$
2:
f[0]_c(<c>) =
$
3:
f[5]_c(<a>(x :: Type5)) =
R_3[f[5]_c__29]
where
f[5]_c__29 :: Type29 = f[5]_c(x)
4:
f[5]_c(<b>(x :: Type5)) =
R_4[f[5]_c__34]
where
f[5]_c__34 :: Type34 = f[5]_c(x)
5:
f[5]_c(<c>) =
R_5[]
6:
f[9]_c(<a>(x :: Type0)) =
R_6[]
7:
f[9]_c(<b>(x :: Type0)) =
R_7[]
8:
f[9]_c(<c>) =
R_8[]
9:
g[]_c(x :: Type9) =
f[9]_c__57
where
f[9]_c__57 :: Type57 = f[9]_c(x)
-----------------
Inverted Tupled
-----------------
58 ==> {;RNothing}
56 ==> $
13 ==> {;RNothing}
12 ==> $
10 ==> <"c">[13,12,12]
10 ==> <"a">[13,10,12]
9 ==> <"c">[13,12,12]
9 ==> <"b">[13,10,12]
9 ==> <"a">[13,10,12]
7 ==> {;RWithout []}
6 ==> $
6 ==> <_>[7,6,6]
5 ==> $
5 ==> <_>[7,6,6]
3 ==> {;RNothing}
2 ==> $
1 ==> <"c">[3,2,2]
1 ==> <"a">[3,1,2]
0 ==> <"c">[3,2,2]
0 ==> <"a">[3,1,2]
f[9] ==> <"c">[58,56,56]
f[9] ==> <"a">[58,f[0],56]
f[5] ==> <"c">[58,56,56]
f[5] ==> <"a">[58,f[5],56]
f[0] ==> <"c">[58,56,56]
f[0] ==> <"a">[58,f[0],56]
1:
f[0]_inv(<a>(f[0]__18 :: Typef[0])) =
<a>(x)
where
x :: Type0 = f[0]_inv(f[0]__18)
2:
f[0]_inv(<c>) =
<c>
3:
f[5]_Tinv((<a>(f[5]__29 :: Typef[5]), R_3[#f[5]_c__29])) =
<a>(x)
where
x :: Type5 = f[5]_Tinv(f[5]__29,f[5]_c__29)
4:
f[5]_Tinv((<a>(f[5]__34 :: Typef[5]), R_4[#f[5]_c__34])) =
<b>(x)
where
x :: Type5 = f[5]_Tinv(f[5]__34,f[5]_c__34)
5:
f[5]_Tinv((<c>, R_5[])) =
<c>
6:
f[9]_Tinv((<a>(f[0]__45 :: Typef[0]), R_6[])) =
<a>(x)
where
x :: Type0 = f[0]_inv(f[0]__45)
7:
f[9]_Tinv((<a>(f[0]__50 :: Typef[0]), R_7[])) =
<b>(x)
where
x :: Type0 = f[0]_inv(f[0]__50)
8:
f[9]_Tinv((<c>, R_8[])) =
<c>
9:
g[]_Tinv((f[9]__57 :: Typef[9], f[9]_c__57 :: Type)) =
x
where
x :: Type9 = f[9]_Tinv(f[9]__57,f[9]_c__57)
Here, f[0] represents the function f specialized to the type S,
f[9] represents the function f specialized to the type T,
and f[5] represents the function f without any assumption on its inputs.
This implementation is a protopype and just for test. The implemetation contains many bugs and inefficient implementations. We would appreciate it if you would tell us the bugs and the inefficient parts of the program.
Any type checking mechanism including view update checker is not implementated yet.
Our testing evironment is as follows:
We think a bit newer or older versions of them also work but I have not tested them.