A sequent calculus for a semi-associative law
Research output: Contribution to journal › Article › peer-review
Authors
Colleges, School and Institutes
Abstract
We introduce a sequent calculus with a simple restriction of Lambek's product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, right rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice Yn .
Details
Original language | English |
---|---|
Article number | 9 |
Pages (from-to) | 9:1-9:23 |
Number of pages | 23 |
Journal | Logical Methods in Computer Science |
Volume | 15 |
Issue number | 1 |
Publication status | Published - 5 Feb 2019 |
Keywords
- Tamari lattice, associativity, coherence theorem, combinatorics, proof theory