TY - JOUR
T1 - A sequent calculus for a semi-associative law
AU - Zeilberger, Noam
PY - 2019/2/5
Y1 - 2019/2/5
N2 - 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 .
AB - 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 .
KW - Tamari lattice
KW - associativity
KW - coherence theorem
KW - combinatorics
KW - proof theory
UR - http://www.scopus.com/inward/record.url?scp=85070823185&partnerID=8YFLogxK
U2 - 10.23638/LMCS-15(1:9)2019
DO - 10.23638/LMCS-15(1:9)2019
M3 - Article
SN - 1860-5974
VL - 15
SP - 9:1-9:23
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 1
M1 - 9
ER -