Notions

We introduce several notations to explain Egison pattern-matching mechanism.
Here is a really brief explanation of each notation.
We will deepen the understanding of these notions, examining the examples in the following sections.

Matching State

Egison's pattern-matching is reduction of a collection of matching states.
Each matching-state has a stack of matching-trees and data to proceed pattern-matching.

Matching Tree

A matching-tree has two kinds of forms, a matching-atom and a matching-node.

Matching Atom

A matching atom is a tuple of a pattern, a target, and a matcher.

Matching Node

A matching-node has a stack of matching-trees as a matching-state.
The structure of matching-node is similar with a matching state.


Examples

Example 1. Non-Linear Patterns

Let us examine what will happen when Egison evaluates following pattern-matching expressions.

At first, the initial matching-state is generated. It is as follow.
The data constructor MState takes three arguments, a stack of matching-trees, an environment, and a result in the middle of the pattern-matching.
The env is the environment when the evaluation process enters the match-all expression.
The stack of matching-tree contains a single matching-atom whose pattern, target and matcher are same with the arguments of match-all.

The stack of the matching-tree contains only one matching-atom.
This matching atom is reduced with the matcher (multiset integer) as specified in the matching-atom.
The matching-states increases to 3 with this reduction as follow.

We focus on the first matching state, for now.
It is the following one.

This matching-state is reduced as follow in the next reduction step.
The matcher of the matching-atom of the top of the stack is changed to something from integer.
something is the built-in matcher of Egison.
It can match with a wildcard or a pattern variable.

This matching-state is reduced as follow in the next reduction step.
The matching atom of the top of the stack is popped out, and a new binding [m 2] is appended to the result of the middle of pattern-matching.
something can only append a new binding to the result of pattern-matching.

This matching-state is reduced as follow in the next reduction step.
The matching-states increases to 2 with this reduction.

In the above matching-states, ,m is pattern-matched with 8 and 2 respectively as integer.
When we do pattern-matching with the value pattern, the result of the middle of pattern-matching is used to evaluate it.
Therefore, in this case, m is evaluated to 2.
The first matching-state fails to pattern-match.
The second matching-state succeeds in pattern-matching and be reduced as follow in the next reduction step.

This matching-state is reduced as follow in the next reduction step.
The pattern is a wildcard and matches with any object.
No new binding is appended to the result of pattern-matching.

When the matching-tree stack is empty, the reduction finish.
This result of pattern-matching {[m 2]} is added to the final result.

Example 2. Or-Patterns

Let us examine what will happen when our system evaluates the following pattern-matching expression.

Our system reaches the following matching-state.

This matching-state is reduced as follow in the next reduction step.

Example 3. And-Patterns

Let us examine what will happen when our system evaluates the following pattern-matching expression.

Our system reaches the following matching-state.

This matching-state is reduced as follow in the next reduction step.

Example 4. Not-Patterns

Let us examine what will happen when our system evaluates the following pattern-matching expression.

Our system reaches the following matching-state.

When our system reaches the matching-state whose top matching-atom is a not-pattern, our system generates a new matching-state which contains only the matching-atom with the not-pattern as follow. All information of the matching-state and the matching-nodes except about the rest of matching-tree stack are retained.

Our system proceeds the pattern-matching on the new generated matching-state, and if it fails pattern-matching our system pops out the matching-atom of the not-pattern from the original matching-state as follow and proceeds the pattern-matching. Otherwise our system fails the pattern-matching.

In this case, the above matching-state succeeds pattern-matching. Therefore, the matching-state with the not-pattern is reduced as follow.

Example 5. Application of Pattern Function Inside Pattern

We explain how our system deals with modularization of patterns with this example.
Let us examine what will happen when our system evaluates the following pattern-matching expression.

Our system reaches the following matching-state.

This matching-state is reduced as follow in the next reduction step. A matching-node has extra information, a pattern-environment. In this case, the pattern-environment is {[pat1 $n] [pat2 _]}.

Our system reaches the following matching-state. When the top of the matching-tree stack of the matching-state is a matching-node, our system pops the matching-atom of the top of the matching-tree stack of the matching-node. If the top of the matching-tree stack of the matching-node is a matching-node again, our system pops out the matching-atom from the top of the matching-tree stack of that matching-node.

This matching-state is reduced as follow in the next reduction step.
pat1 is called a variable-pattern.
It can appear only in the body of pattern-functions.
When the matching-atom whose pattern is a variable-pattern is popped out, our system gets what pattern is bound to the variable-pattern from the pattern-environment, and push a new matching-atom to the matching-tree stack of the one level upper matching-node or matching-state.

The arguments of a pattern-function are handled in special way as above. This is the reason why the pattern-function can take only patterns. A pattern must be bound to a variable-pattern.

I'll stop the explanation of pattern-matching step here, for now.
I've explained most of the essential points, already.

Pattern-Matching with Infinite Results

We explain how our system executes pattern-matching which has infinite results. Let us examine what will happen when our system evaluate the following pattern-matching expression.

The following picture is the reduction tree of matching-states when we execute the pattern-matching above. Rectangles stand for matching-states. The rectangle at the upper left is the initial matching-state. Circles stand for final matching-states that succeed pattern-matching.

The width of a reduction tree of matching-states can be infinite because there are cases that a matching-state is reduced to infinite matching-states. The depth of a reduction tree also can be infinite if we use a recursive pattern-function in a pattern. We need to think on the order of reduction to examine all nodes of a reduction tree. The numbers on rectangles and circles denote the order of reduction. If we see a reduction tree obliquely, it can be regarded as a binary tree. Therefore, we can trace all nodes of reduction trees if we do breadth-first search on the tree, though it will use a lot of memory.