*Resources* * _Pattern Matching Pointers_: http://www.cs.purdue.edu/homes/stelo/pattern.html *Definition* 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. *Variations* 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 * AdaptivePatternMatching *Implementation* Efficient implementations of pattern matching pre-process the pattern into an efficient automaton that walks the subject tree only once. *References* Here are some references to papers on the subject: * aTermPatternMatchCompilerInspiredByFiniteAutomataTheory * AdaptivePatternMatching * ATypedPatternCalculus