@inproceedings{5df496092aaf460cb2e18e0823213b25,
title = "A sequent calculus for a semi-associative law",
abstract = "We introduce a sequent calculus with a simple restriction of Lambek{\textquoteright}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, tree 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. One combinatorial application of this coherence theorem is a new proof of the Tutte–Chapoton formula for the number of intervals in the Tamari lattice $Y_n$. Elsewhere, we have also used the sequent calculus and the coherence theorem to build a surprising bijection between intervals of the Tamari order and a natural fragment of lambda calculus, consisting of the beta-normal planar lambda terms with no closed proper subterms.",
keywords = "proof theory, combinatorics, substructural logic, coherence theorem",
author = "Noam Zeilberger",
year = "2017",
month = sep,
day = "10",
doi = "10.4230/LIPIcs.FSCD.2017.33",
language = "English",
isbn = "978-3959770477",
volume = "84",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl",
pages = "33:1--33:16",
editor = "Dale Miller",
booktitle = "Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)",
address = "Germany",
}