H. Fabender and S. Maneth. A Strict Border for the Decidability of E-Unification for Recursive Functions. In proceedings of the intern. Conf. on Algebraic and Logic Programming. To appear., 1996. 30  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....assume linearity for the goal, right linearity and (nearly) left linearity for the TRS. Unfortunately, their procedure does not represent the set of solutions, and does not terminate for an example 3 like fs(x) y s(x y) 0 x xg because of the superposition of s(x) with s(x y) In [14] H. Fabender and S. Maneth give a decision procedure for unifiability, without representing the set of solutions. But they need very strong restrictions. Only one function can be defined and every constructor and every function is monadic (i.e. admits at most one argument) Concerning the ....

....grammar. Example 8.4 Let R = f 0 x x; x 0 x; s(x) s(y) s(s(x y) s(x) p(y) x y; p(x) s(y) x y; p(x) p(y) p(p(x y) g that defines the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in the previous work [19, 23, 9, 26, 21, 8, 20, 14] but satisfies ours. Therefore we are able to solve linear equations modulo this theory. Example 8.5 Let ( r 1 : f(c(x; x 0 ) c(y; y 0 ) c(f(x; y 0 ) f(x 0 ; y) r 2 : f(0; 0) 0 This system provides an idea of the expressiveness of TTSG s because when solving the equation f(x; ....

H. Fabender and S. Maneth. A Strict Border for the Decidability of E-Unification for Recursive Functions. In proceedings of the intern. Conf. on Algebraic and Logic Programming. To appear., 1996. 30

....shows that the word problem for right ground TRS is undecidable whereas the word problem in left linear and right ground TRS is decidable in polynomial time. In the undecidability proof for right ground systems Oyamaguchi used rewrite rules with non linear variable occurrences at different depth. Fassbender Maneth (1996) investigate decidability of E unification in theories induced by TRS called top down tree transducers. Syntactic restrictions based on separated function and constructor alphabets are assumed. Eunification in top down tree transducers with only one function symbol in the alphabet is shown to be ....

Fassbender, H. & Maneth, S. (1996), A strict border for the decidability of e-unification for recursive functions, in M. Hanus & M. Rodr'iguez-Artalejo, eds, `Algebraic and Logic Programming (ALP-5) : 5th international conference, Aachen, Germany, September 25-27, 1996', Vol. 1139 of Lecture notes in computer science, Springer, Berlin.

....and does not terminate for an example like fs(x) y s(x y) 0 x xg because of the superposition of s(x) with s(x y) Note that our algorithm works (and terminates) for this example when solving linear equations, since our restrictions are satisfied (see Sect. 4) Fabender and Maneth [23] give a decision procedure for unifiability without representing the set of solutions. However, they need very strong restrictions. Only one function can be defined, and every constructor and every function is monadic (i.e. admits at most one argument) 4 Additional Restrictions and their Need ....

....synchronized grammar. Example 8.7 Let R = f 0 x x; x 0 x; s(x) s(y) s(s(x y) s(x) p(y) x y; p(x) s(y) x y; p(x) p(y) p(p(x y) g define the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in previous work [3, 16, 18, 19, 20, 17, 22, 23], but does satisfy ours. Therefore, we are able to solve linear equations modulo this theory. Example 8.8 Let ae r 1 : f(c(x; x 0 ) c(y; y 0 ) c(f(x; y 0 ) f(x 0 ; y) r 2 : f(0; 0) 0 This system provides an idea of the expressiveness of TTSGs, because when solving the equation ....

Fabender, H. and Maneth, S. (1996). A strict border for the decidability of E-unification for recursive functions. Proceedings of the Intern. Conf. on Algebraic and Logic Programming. Volume 1139 of LNCS, pp. 194--208. Springer-Verlag.

....of solutions, and does not terminate for an example like fs#x##y#s#x#y## 0#x#xgbecause of the superposition of s#x# with s#x #y#. Note that our algorithm works (and terminates) for this example when solving linear equations, since our restrictions are satisfied (see Sect. 4) Fabender and Maneth [23] give a decision procedure for unifiability without representing the set of solutions. However, they need very strong restrictions. Only one function can be defined, and every constructor and every function is monadic (i.e. admits at most one argument) 4 Additional Restrictions and their Need ....

....be expressed by a tree tuple synchronized grammar. Example 8.7 Let R # f 0#x#x# x #0#x# s#x##s#y##s#s#x#y###s#x##p#y##x#y# p#x##s#y##x#y# p#x##p#y##p#p#x#y## g define the addition in positive and negative integers. This rewrite system does not satisfy the restrictions given in previous work [3, 16, 18, 19, 20, 17, 22, 23], but does satisfy ours. Therefore, we are able to solve linear equations modulo this theory. Example 8.8 Let # r 1 # f#c#x# x 0 ##c#y# y 0 ## # c#f#x# y 0 ##f#x 0 #y## r 2 # f#0# 0# # 0 This system provides an idea of the expressiveness of TTSGs, because when solving the equationf#x# ....

Fabender, H. and Maneth, S. (1996). A strict border for the decidability of E-unification for recursive functions. Proceedings of the Intern. Conf. on Algebraic and Logic Programming. Volume 1139 of LNCS, pp. 194--208. Springer-Verlag.

No context found.

H. Fabender and S. Maneth. A strict border for the decidability of E- unification for recursive functions. Journal of Functional and Logic Programming, 4, 1998.

No context found.

H. Fabender and S. Maneth. A strict border for the decidability of E- unification for recursive functions. To appear in Journal of Functional and Logic Programming, The MIT Press, 1997.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.