Term pattern matching comes in many variations. The basic problem is that of matching a term pattern (term with variables) against a ground subject term (without variables), producing a substition mapping the variables to the corresponding subterms in the subject term.

More often a subject term is matched against a set of patterns and the matching pattern or patterns has to be found.


The matching problem problem comes in many different guises. The basic problem considers matching a term at the root

  • match term against pattern

  • match term against set of patterns; at most one pattern can match

  • match term against set of patterns; more than one pattern can match

  • match term against ordered sequence of patterns; find the first pattern in the sequence that matches

  • for each subterm find out which pattern from a set of patterns matches it

Properties of the patterns

  • linear: variable occurs once in pattern

  • NonLinearPatternMatching?: variable may occur mor than once

  • LazyPatternMatching?

  • FirstOrderPatternMatching?

  • HigherOrderPatternMatching?

  • SecondOrderPatternMatching?

  • PatternMatchingModuloEquations?

  • StrategicPatternMatching?

  • PatternMatchingAndAbstraction?


Efficient implementations of pattern matching pre-process the pattern into an efficient automaton that walks the subject tree only once.


Here are some references to papers on the subject:

Revision: r1.1 - 05 May 2001 - 22:35 - EelcoVisser
Transform > PatternMatching
Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback