A sequent calculus for a semi-associative law

Add to your list(s) Download to your calendar using vCal

• Noam Zeilberger, Birmingham Theory Group
• Wednesday 08 November 2017, 12:00-01:00
• CS 217.

If you have a question about this talk, please contact Dr Steve Vickers.

Time changed - sorry

The classical Tamari order is the partial order on fully-bracketed words obtained by assuming that multiplication is only “semi-associative” (ab)c <= a(bc). In the talk I will describe a simple proof-theoretic characterization of the Tamari order as a sequent calculus with a weakened version of Lambek’s left rule for the non-commutative product. The main result is a “focusing” property (a strengthening of cut-elimination) for this sequent calculus, which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. One novel combinatorial application of this coherence theorem is a new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice. Depending on the interests of the audience and if time permits, I may also discuss how some of these ideas relate to a natural notion of “left representable” multicategory, considered independently in recent work of Bourke and Lack on skew monoidal categories. (Based on a paper presented at FSCD 2017 .)

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Lab Lunch
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.