Pattern calculus is a formalism for functional programming. Confluence is one of the most important desirable properties for such formalisms. Being established earlier for pattern calculi with unitary matching, it was a challenging task to nd conditions that guarantee con
uence when matching is nitary. We studied such an extension, considering a pattern calculus with sequence variables, where even syntactic matching is finitary. Even if one collects all alternative reductions into one term, con
uence does not hold in general and special conditions are need to guarantee it. The conditions that we established are sufficient not only for calculi with sequence matching, but for arbitrary calculi with finitary matching.
We gave three concrete instances of the matching function that satisfy these conditions: free and unordered sequence matchings, and the sequence matching with linear algebraic
patterns.

Project members:

• Jemal Antidze (Principal Investigator)

• Besik Dundua (Coordinator)