Matching is the process of determining whether a pattern (an expression with or without variables) matches an instance (an expression without variables), i.e. whether the two expressions can be made identical by appropriate substitutions for the variables in the pattern.

A substitution is a finite mapping of variables to ground terms. In what follows,, we write substitutions as sets of replacement rules, like the one shown below. In each rule, the variable to which the arrow is pointing is to be replaced by the term from which the arrow is pointing. In this case, X is associated with a and Y is associated with b.

The result of applying a substitution σ to an expression φ is the expression φσ obtained from φ by replacing every occurrence of every variable with a binding in the substitution by the term to which it is bound.

A substitution is a matcher for a pattern and an instance if and only if applying the substitution to the pattern results in the given instance. One good thing about our language is that there is a simple and inexpensive procedure for computing a matcher of a pattern and an expression if it exists.

See below for a version of a matching procedure encoded in Javascript. The procedure assumes a representation of expressions as sequences of subexpressions. For example, the expression p(X,b) can be thought of as a sequence with three elements, viz. the predicate p, the variable X, and the symbol b.

We start the procedure with two expressions (the pattern and the instance) and a substitution (which is initially empty). We then recursively process the two expressions, comparing the subexpressions at each point. Along the way, we extend the substitution with variable assignments as described below.

1. If the pattern and the instance are the same, then the procedure succeeds, returning the unmodified substitution as result.


2. If the pattern is a variable with a binding, we compare the binding for the variable with the instance. If the pattern is a variable without a binding, we return the composition of the given substitution with a substitution in which the variable is bound to the expression in the given instance.


3. If either the pattern or the instance is a constant, then the procedure fails.


4. If the pattern and the instance have different lengths, we fail.


5. Otherwise, we iterate across the corresponding subexpressions of the pattern and the instance. If we fail to match a sub-pattern and a sub-instance at any point in this process, the procedure as a whole fails. If we finish this recursive comparison of the pattern and the instance, the procedure as a whole succeeds and the accumulated substitution at that point is the resulting matcher.

As an example of this procedure in operation, consider the process of matching the pattern p(X,Y) and the instance p(a,b) with the initial substitution {}. A trace of the execution of the procedure for this case is shown below. We show the beginning of a comparison with a line labelled Compare together with the expressions being compared and the input substitution. We show the result of each comparison with a line labelled Result. The indentation shows the depth of recursion of the procedure.

As another example, consider the process of matching the pattern p(X,X) and the instance p(a,a). A trace is shown below. By the time we compare the last arguments in the two expressions, X is bound to a, so the match succeeds.

As a final example, consider the process of trying to match the pattern p(X,X) and the expression p(a,b). The main interest in this example comes in comparing the last argument in the two expressions, viz. X and b. By the time we reach this point, X is bound to a and the corresponding instance is b. Since the pattern is a symbol and the instance is a different symbol, the match attempt fails.

This matching procedure is quite simple. However, it is worth understanding thoroughly, as it is the basis for more complicated matching procedures defined later.