Pattern-based calculi with finitary matching. (29th December 2017)

• Record Type: Journal Article
• Authors: Alves, Sandra; Dundua, Besik; Florido, Mário; Kutsia, Temur
• Is Part Of: Logic journal of the IGPL. Volume 26:Number 2(2018:Apr.)
• Page Start: 203
• Page End: 243
• Publication Date: 2017-12-29
• Subjects: Lambda calculus -- pattern calculus -- finitary matching -- confluence -- functional programming; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/JIGPAL/jzx059
• Languages: English
• ISSNs: 1367-0751

Abstract

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 described in this paper 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.