2026-07-23T00:26:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7717 2024-03-06T10:41:05Z ddc:004 open_access

A Sequent Calculus for a Semi-Associative Law Zeilberger, Noam proof theory combinatorics coherence theorem substructural logic associativity 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, 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Noam Zeilberger 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.33 urn:nbn:de:0030-drops-77179 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.33 eng https://creativecommons.org/licenses/by/3.0/legalcode