[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #69

Originator: Claude Kirchner, J. Zhang
Date: June 1993

Summary: What is the syntactic type of (mid-, three-way) distributivity?

What is the syntactic type (maximum number of top-level steps needed in an equational proof [BC92]) of the distributivity axiom? What is the syntactic type of “three-way” commutativity:

  f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x)
  f(f(x, y, z), u, x) = f(x, y, f(z, u, x))

What are the unification type, decidability, and syntactic type of “mid-commutativity”: (x+y)+(u+v) = (x+u)+(y+v)?

References

[BC92]
Alexandre Boudet and Evelyne Contejean. On n-syntactic equational theories. In H. Kirchner and G. Levi, editors, Proceedings of the Third International Conference on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 446–457, Pisa, Italy, September 1992. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]