A sequent calculus for a semi-associative law
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
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, 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.
Details
Original language | English |
---|---|
Title of host publication | Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) |
Editors | Dale Miller |
Publication status | Published - 10 Sep 2017 |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Publisher | Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik |
Volume | 84 |
ISSN (Print) | 1868-8969 |
Keywords
- proof theory, combinatorics, substructural logic, coherence theorem