A sequent calculus for a semi-associative law

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationProceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
EditorsDale Miller
Publication statusPublished - 10 Sep 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Volume84
ISSN (Print)1868-8969

Keywords

  • proof theory, combinatorics, substructural logic, coherence theorem