A sequent calculus for a semi-associative law

Noam Zeilberger

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

4 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationProceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
EditorsDale Miller
PublisherSchloss Dagstuhl
Pages33:1-33:16
Number of pages16
Volume84
ISBN (Print)978-3959770477
DOIs
Publication statusPublished - 10 Sept 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

Fingerprint

Dive into the research topics of 'A sequent calculus for a semi-associative law'. Together they form a unique fingerprint.

Cite this