Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unification in Matching Logic -- Revisited

Ádám Kurucz, Péter Bereczky, Dániel Horpácsi

TL;DR

This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.

Abstract

Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. This is easily remedied by unification, for which an algorithm has already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.

Unification in Matching Logic -- Revisited

TL;DR

This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.

Abstract

Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. This is easily remedied by unification, for which an algorithm has already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.

Paper Structure

This paper contains 20 sections, 16 theorems, 9 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Matching Logic
  4. Syntax
  5. Semantics
  6. Sequent Calculus for Matching Logic
  7. Definedness
  8. Essential Theorems
  9. Unification
  10. Related Work
  11. Rule-based Unification
  12. Unification in Matching Logic
  13. Unification in an Applicative Matching Logic
  14. Abstract Unification Problem
  15. Injectivity.
  16. ...and 5 more sections

Key Result

Theorem 1

For all theories $\Gamma$, and patterns $\varphi_1, \dots, \varphi_k, \psi$, the derivability statement ${\Gamma} \blacktriangleright {\varphi_1,\ldots,\varphi_k} \vdash_\mathit{S} {\psi}$ holds if and only if $\Gamma \vdash \varphi_1 \to \dots \to \varphi_k \to \psi$.

Figures (4)

  • Figure 1: Sequent calculus for matching logic (theory-independent rules)
  • Figure 2: Specification of definedness
  • Figure 3: Deduction; and rules about equality. These rules assume that $\Gamma^\mathsf{DEF} \subseteq \Gamma$.
  • Figure 4: Comparison of old and new rules. Notice how $(a,\ y)$ and $(x,\ b)$ are not filtered out by either version of Symbol clash as they are not errors.

Theorems & Definitions (44)

  • Definition 1: Signature
  • Definition 2: Pattern
  • Definition 3: Substitution
  • Definition 4: Pattern context, application context
  • Definition 5: Model
  • Definition 6: Semantic consequence
  • Definition 7: Term patterns and predicate patterns
  • Definition 8: Sequents
  • Theorem 1: Correspondence
  • Theorem 2: Congruence
  • ...and 34 more