Efficient Second-order Matching
The standard second-order matching algorithm by Huet may be expansive
in matching a flexible-rigid pair. On one hand, many fresh free
variables may need to be introduced; on the other hand, attempts are
made to match the heading free variable on the flexible side with
every ``top layer'' on the rigid side and every argument of the
heading free variable with every subterm covered by the ``top layer''.
We propose a new second-order matching algorithm, which introduces no
fresh free variables and just considers some selected ``top layers'',
arguments of the heading free variable and subterms covered by the
corresponding ``top layers''. A first implementation shows that the
new algorithm is more efficient both in time and space than the
standard one for a great number of matching problems.
The paper is here.