License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.33
URN: urn:nbn:de:0030-drops-77179
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7717/
Go to the corresponding LIPIcs Volume Portal

Zeilberger, Noam

A Sequent Calculus for a Semi-Associative Law

pdf-format:
LIPIcs-FSCD-2017-33.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{zeilberger:LIPIcs:2017:7717,
  author =	{Noam Zeilberger},
  title =	{{A Sequent Calculus for a Semi-Associative Law}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7717},
  URN =		{urn:nbn:de:0030-drops-77179},
  doi =		{10.4230/LIPIcs.FSCD.2017.33},
  annote =	{Keywords: proof theory, combinatorics, coherence theorem, substructural logic, associativity}
}

Keywords: proof theory, combinatorics, coherence theorem, substructural logic, associativity
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI