Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Flat matching

Temur Kutsia
Organization: Research Institute for Symbolic Computation
Department: Johannes Kepler University
Journal / Anthology

Journal of Symbolic Computation
Year: 2008
Volume: 43
Issue: 12
Page range: 858-873

We study matching in flat theories both from theoretical and practical points of view. A flat theory is defined by the axiom f .x; f .y/; z/ :D f .x; y; z/ that indicates that nested occurrences of the function symbol f can be flattened out. From the theoretical side, we design a procedure to solve a system of flat matching equations and prove its soundness, completeness, and minimality. The minimal complete set of matchers for such a system can be infinite. The procedure enumerates this set and stops if it is finite. We identify a class of problems on which the procedure stops. From the practical point of view, we look into restrictions of the procedure that give an incomplete terminating algorithm. From this perspective, we give a set of rules that, in our opinion, describes the precise semantics for the flat matching algorithm implemented in the Mathematica system.