Pattern-based calculi with finitary matching

20^th March 2018, 13:00 Ashton Lecture Theater
Dr. Temur Kutsia
Research Institute for Symbolic Computation
Johannes Kepler University Linz

Abstract

Finitary matching problems are those that have finitely many solutions. Pattern calculi generalize the lambda-calculus, replacing the abstraction over variables by an abstraction over terms that are called patterns. Consequently, reduction requires solving a pattern matching problem. The framework we describe in this talk considers the case when such problems are finitary. It is parametrized by the solving function, which is responsible for computing solutions to the matching problems. A concrete instance of the function gives a concrete version of the pattern calculus. We impose conditions on the solving function, obtaining a generic confluence proof for a class of pattern calculi with finitary matching. Instances of the solving function are presented.