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.
FTP: ftp.uni-bremen.de:/pub/Uni-Bremen/Institutes/ZKW/INFORM/qian/esom.ps.gz

For a hard copy send a message to Zhenyu Qian.