Canonical forms and unification
作者： Jean-Marie Hullot
关键词: Canonical form 、 Computer programming 、 Discrete mathematics 、 Set (abstract data type) 、 Equational theory 、 Set theory 、 Term (logic) 、 Unification 、 Mathematics 、 Rewriting
摘要: Fay has described in [2,3] a complete T-unification for equational theories T which possess set of reductions as defined by Knuth & Bendix [12]. This algorithm relies essentially on using the narrowing process Lankford [13]. In this paper, we first study relations between and unification give new version Fay's algorithm. We then show how to eliminate many redundancies sufficient condition termination last part, extend previous results various kinds canonical term rewriting systems.
springer.com
sci-hub.se 参考文章(16)
J. M. Hvllot, Associative commutative pattern matching international joint conference on artificial intelligence. pp. 406- 412 ,(1979)
Mark E. Stickel, A complete unification algorithm for associative-commutative functions international joint conference on artificial intelligence. pp. 71- 76 ,(1975) , 10.21236/ADA015846
Jean-Marie Hullot, A Catalogue of Canonical Term Rewriting Systems. Defense Technical Information Center. ,(1980) , 10.21236/ADA087641
J. Siekmain, Ch. Mathis, S. Kuhner, P. Raulefs, Unification of idempotent functions international joint conference on artificial intelligence. pp. 528- 528 ,(1977)
Gérard Huet, Derek C. Oppen, Equations and rewrite rules: a survey Formal Language Theory#R##N#Perspectives and Open Problems. pp. 349- 405 ,(1980) , 10.1016/B978-0-12-115350-2.50017-8
D. E. Knuth, P. B. Bendix, Simple Word Problems in Universal Algebras Computational Problems in Abstract Algebra#R##N#Proceedings of a Conference Held at Oxford Under the Auspices of the Science Research Council Atlas Computer Laboratory, 29th August to 2nd September 1967. pp. 342- 376 ,(1983) , 10.1007/978-3-642-81955-1_23
Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems Journal of the ACM. ,vol. 27, pp. 797- 821 ,(1980) , 10.1145/322217.322230
G S Makanin, The Problem of Solvability of Equations in a Free Semigroup Mathematics of The Ussr-sbornik. ,vol. 32, pp. 129- 198 ,(1977) , 10.1070/SM1977V032N02ABEH002376
Harold Brown, John Leech, Computational Problems in Abstract Algebra Mathematics of Computation. ,vol. 25, pp. 193- ,(1971) , 10.2307/2005152
G.P. Huet, A unification algorithm for typed λ-calculus Theoretical Computer Science. ,vol. 1, pp. 27- 57 ,(1975) , 10.1016/0304-3975(75)90011-0