Sciweavers

Share
LPAR
2004
Springer

Second-Order Matching via Explicit Substitutions

10 years 4 months ago
Second-Order Matching via Explicit Substitutions
Abstract. Matching is a basic operation extensively used in computation. Second-order matching, in particular, provides an adequate environment for expressing program transformations and pattern recognition for automated deduction. The past few years have established the benefit of using explicit substitutions for theorem proving and higher-order unification. In this paper, we will make use of explicit substitutions to facilitate matching: we develop a second-order matching algorithm via the λσ-style of explicit substitutions. We introduce a convenient notation for matching in the λσ-calculus. This notation keeps the matching equations separated from the incremental graftings. We characterise an important class of second-order matching problems which is essential to prove termination of the algorithm. In addition, we illustrate how the algorithm works through some examples.
Flávio L. C. de Moura, Fairouz Kamareddine,
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LPAR
Authors Flávio L. C. de Moura, Fairouz Kamareddine, Mauricio Ayala-Rincón
Comments (0)
books