What is matching?

It is very common in mathematics to say that one mathematical expression "is of the form" of another. For example, we might say that $2x^2-5$ is of the form $A-B$, where what we mean is that substituting $A=2x^2$ and $B=5$ into $A-B$ produces the expression $2x^2-5$.

For us to be able to speak this way requires no special treatment of the first expression (in this case, the expression $2x^2-5$), but the other expression (in this case, the expression $A-B$) must be treated as a structure or pattern into which we may do substitutions.

Given two mathematical expressions, pattern matching (or just matching) is the act of determining the substitution (like $A=2x^2$ and $B=5$ from that example) that demonstrates that one expression is of the form of the other.

Terminology

When performing pattern matching, one of the two expressions is the one intended for substitution, and the other expression is the goal to be built by doing the substitution. The one into which substitution happens is called the pattern and the other is simply the expression.

The symbols that will be replaced by substitution ($A$ and $B$ in the example above) have a special status; we call them metavariables. Not all symbols in the pattern are metavariables; for example, the operator $-$ in the expression $A-B$ is not a metavariable, because the intent is not to replace it with another operator; it should remain unchanged. (We would not say that $2^k$ is of the form $A-B$, even though both are a binary operator applied to two operands.)

In mathematics, one usually figures out what is a metavariable from context and common sense, but in software, it will be important to mark out metavariables explicitly. To that end, this module imports all the tools defined in the metavariables module and exposes them to clients. For more information about determining metavariables from context, see the Formula namespace.

Thus the problem of matching can be stated like so: Given a pattern $P$ and an expression $E$, where $P$ may contain metavariables and $E$ may not, find a mapping $S$ from the metavariables in $P$ into the space of all expressions such that $S(P)=E$ (or determine that no such $S$ exists). This is the simplest way to state the problem, but it is actually slightly more complex.

Expression functions

In mathematics, we often want to perform matching while paying attention to certain key parameters. For example, we could express the general rule for mathematical induction as $$(P(0)\text{ and }\mathrm{\forall }k,P(k)\Rightarrow P(k+1))\Rightarrow \mathrm{\forall }n,P(n).$$ Here, it is important that $P$ be a metavariable that takes a single parameter, and that $P(0)$, $P(k)$, and $P(n)$ be the expressions obtained by substituting $0$, $k$, and $n$ (respectively) in for that parameter.

We call such a $P$ an expression function, because it takes an expression as input and generates another expression as output. We call an expression like $P(0)$ an expression function application because it applies an expression function to an argument, and thus represents the output expression of $P$ applied to $0$. To handle these details, this module imports all the tools defined in the ExpressionFunctions module and exposes them to clients.

Providing support for expression functions makes the job of matching more difficult. For example, consider performing matching with $P=Q(x)$ and $E=3x+e^x$, and $Q$ the only metavariable, also an expression function. Which of the following is the correct substitution $S$?

• $S(Q)$ is the expression function $t\mapsto 3t+e^t$
• $S(Q)$ is the expression function $t\mapsto 3x+e^t$
• $S(Q)$ is the expression function $t\mapsto 3t+e^x$
• $S(Q)$ is the expression function $t\mapsto 3x+e^x$

The answer is that all are correct, and thus there is more than one correct answer to the question, and thus there must be more than one output from the matching algorithm.

Thus the matching algorithm takes as input a pattern-expression pair $(P,E)$ as stated above, but its output is a set of substitutions $\{S_1,\dots ,S_n\}$, with $n=0$ (empty set) if the problem has no solutions. But it's actually one step more complex than that, also.

Matching, fully stated

We will often want to match multiple pattern-expression pairs at the same time. For example, a user might claim that a conclusion $X$ follows from some premises $J\Rightarrow X$ and $J$ using the law of modus ponens, typically written $A$, $A\Rightarrow B$, therefore $B$. We thus have not one matching problem, but three in one; we want to know whether there is a substitution $S$ that maps the tuple $(A,A\Rightarrow B,B)$ to the tuple $(J,J\Rightarrow X,X)$. Certainly, we could simply put a dummy wrapper around the tuples to create a single expression, as in $$Wrapper(A,A\Rightarrow B,B)\text{ and }Wrapper(J,J\Rightarrow X,X).$$ But it is more natural to simply support multiple inputs to the matching algorithm in the first place.

Thus we come to the following final statement of the problem: The matching algorithm takes as input a set of pairs $\{(P_1,E_1),\dots ,(P_n,E_n)\}$, where each $P_i$ is a pattern (may contain metavariables) and each $E_i$ is an expression (may not contain metavariables). It returns a set $S=\{S_1,\dots ,S_m\}$ of solutions such that for all $i,j$, we have $S_j(P_i)=E_i$. Furthermore, the set $S$ is comprehensive, in that any possible solution is either present in the set $S$ or can be obtained by composing $S$ with another function. (I.e., $S$ is the set of most general solutions.)

We call a set of inputs $\{(P_1,E_1),\dots ,(P_n,E_n)\}$ a matching problem, and we define the Problem class to let clients create matching problems and call an algorithm to solve them. Each pair $(P_i,E_i)$ is called a constraint and can be represented by an instance of the Constraint class.

We call each $S_j$ a matching solution and we define the Solution class to represent such objects; the output of the matching algorithm will be a JavaScript array of Solutions. Each pair $a\mapsto b$ in a solution mapping is called a substitution, and will be represented by a member of the Substitution class. To apply a Substitution or a Solution to an LogicConcept, see the Formula namespace.

Technical details

A substitution that would cause variable capture does not count as a solution to a matching problem. This is for two reasons: First, the very definition of substitution does not permit variable capture. Second, the mathematical uses to which we will put the algorithm do not want such solutions anyway. Consider the following example.

A standard rule of predicate logic is universal instantiation, which says that from $\mathrm{\forall }x,P(x)$, one can conclude any instance $P(t)$. However, if we were to consider the premise $\mathrm{\forall }x,\mathrm{\exists }y,y=x+1$, we cannot from it conclude $\mathrm{\exists }y,y=y+1$. We might try to justify such an inference by pointing out that it is indeed an instance of the rule in question, by way of the substitution $S(x)=y$. But such a substitution replaces $x$ with $y$ at a location where $y$ is not free to replace $x$, and thus introduces variable capture. So such an $S$ is not actually a solution to the matching problem inherent in that attempted inference.

To ensure that our matching algorithm does not introduce variable capture, we use de Bruijn indices to represent patterns and expressions internally during the matching process.

Recall the example above, in which an expression function $Q$ was assigned the value $t\mapsto 3t+e^t$. This dummy variable $t$ was chosen because it did not appear anywhere in the problem, so it could not be confused with any variable already in use. There are many times in the course of working with expressions and matching when it is convenient to have a source that can generate an arbitrary number of unused variables. We thus also have the NewSymbolStream class, for that purpose.