×

Unification of higher-order patterns modulo simple syntactic equational theories. (English) Zbl 0940.03017

Summary: We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by C. Kirchner. The algorithm by D. Miller for pattern unification, refined by T. Nipkow is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of C. Kirchner is adapted to pattern \(E\)-unification. If the syntactic algorithm for a theory \(E\) terminates in the first-order case, then our algorithm will also terminate for pattern \(E\)-unification. The result is a DAG-solved form plus some equations of the form \(\lambda x.F(x) = \lambda x. F(x^{\pi})\) where \(x^{\pi}\) is a permutation of \(x\). When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open.

MSC:

03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: EuDML EMIS