A sequent calculus for the Tamari order

TL;DR

This paper introduces a sequent calculus that characterizes the Tamari order, proving a coherence theorem and providing new combinatorial insights, including a novel proof for counting Tamari lattice intervals and a bijection with lambda calculus terms.

Contribution

It presents a new sequent calculus for the Tamari order, establishes a focusing property and coherence theorem, and connects Tamari intervals to lambda calculus.

Findings

Proves a coherence theorem for the sequent calculus.

Provides a new proof of the Tutte-Chapoton formula for Tamari intervals.

Establishes a bijection between Tamari intervals and certain lambda calculus terms.

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$. We also apply the sequent calculus and the coherence theorem to build a surprising bijection between intervals of the Tamari order and a certain fragment of lambda calculus, consisting of the $\beta$-normal planar lambda terms with no closed proper subterms.