Flat matching

AbstractWe 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¯)≐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