Noam Zeilberger - A sequent calculus for a semi-associative law

lmcs:4406 - Logical Methods in Computer Science, February 5, 2019, Volume 15, Issue 1 -
A sequent calculus for a semi-associative lawArticle

Authors: Noam Zeilberger ORCID

    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, right 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. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice $Y_n$.

    Volume: Volume 15, Issue 1
    Published on: February 5, 2019
    Accepted on: January 11, 2019
    Submitted on: March 28, 2018
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,Mathematics - Combinatorics

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1502 times.
    This article's PDF has been downloaded 352 times.