Pattern-based calculi with finitary matching

• Type: Article in International Scientific Journal
• Date: 2018

Authors

Sandra Alves (Author) FCUP; Dundua, B (Author) Other; Florido, M (Author) FCUP; Kutsia, T (Author) Other

Journal

Title: Logic Journal of the IGPL

Vol. 26

Pages: 203-243

ISSN: 1367-0751

Publisher: Oxford University Press

Indexing

ISI Web of Knowledge - 1 Citation

Scopus - 2 Citations

Other information

Authenticus ID: P-00N-W6A

DOI: 10.1093/jigpal/jzx059

Abstract (EN): 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 41