Confluence of the Pattern Matching Calculus
A mechanised confluence proof for the
Pattern Matching Calculus (PMC)
has been performed in
Isabelle-2003.
This proof is largely based on the
confluence proof for lambda-calculus performed in Isabelle-1999 by
James Brotherston and
René Vestergaard.
The formalisation consists of the following theories:
Among these, the central new theories are:
- PMC: The syntax of the Pattern Matching Calculus
- Reduction: The reduction rules of the Pattern Matching Calculus
- AczelPMCa: The Aczel-style parallel reduction relation used for
the confluence proof
- DiamondAczelPMCa: the diamond property of the Aczel-style parallel
reduction relation for PMC - this is the key to confluence of PMC
- Linear: Definition of linearity of patterns, expressions,
and matchings
- ExistsBCF: Proof of the existence of an alpha-reduction
into a Barendregt conventional form for every expression and matching
(required major adaptations because of linearity)
Only relatively minor adaptations
of Brotherston and Vestergaard's proof
were required to obtain
the final confluence result:
- RawConfluence: Confluence of the union of PMC reduction
and alpha conversion
- RawToReal: Confluence of PMC modulo alpha-equivalence classes
The Isabelle-generated output for these theories is
here.
Wolfram Kahl