A sequent calculus for a semi-associative law
From MaRDI portal
Publication:6299644
arXiv1803.10080MaRDI QIDQ6299644FDOQ6299644
Authors: Noam Zeilberger 
Publication date: 27 March 2018
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 .
Cut-elimination and normal-form theorems (03F05) Combinatorics of partially ordered sets (06A07) Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
This page was built for publication: A sequent calculus for a semi-associative law
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6299644)
