Algebraic manipulations as a unification and matching strategy for linear equations in signed binary trees: application to LISP program synthesis and derecursivation
Claude Kirchner, Claude Kirchner, Jean-Pierre Jouannaud · 1981
We study the unification and matching problems in the signed binary trees theory. We show that any equation tl1=t2 can be transformed into an equivalent one x=t. If x does not occur in t then (x > t) is the unique most general unifier in the theory (up to an isomorphism). We apply this technique to find recurrence relations between sets of terms. These relations are used to synthesize LISP programs from a set of input traces.