Document Open Access Logo

A Sequent Calculus for a Semi-Associative Law

Author Noam Zeilberger

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.33.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • proof theory
  • combinatorics
  • coherence theorem
  • substructural logic
  • associativity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Noam Zeilberger. A Sequent Calculus for a Semi-Associative Law. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.33

Author Details

Noam Zeilberger

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Logic and Computation, 2(3):297-347, 1992. Google Scholar
  2. O. Bernardi and N. Bonichon. Intervals in Catalan lattices and realizers of triangulations. J. Combin. Theory Ser. A, 116(1):55-75, 2009. Google Scholar
  3. F. Chapoton. Sur le nombre d'intervalles dans les treillis de Tamari. Sém. Lothar. Combin., (B55f), 2006. 18 pp. (electronic). Google Scholar
  4. Robert Cori and Gilles Schaeffer. Description trees and Tutte formulas. Theoretical Computer Science, 292(1):165-183, 2003. Selected papers in honor of Jean Berstel. Google Scholar
  5. Wenjie Fang. Planar triangulations, bridgeless planar maps and Tamari intervals. arXiv:1611.07922, 2016. Google Scholar
  6. H. Friedman and D. Tamari. Problèmes d'associativité: une structure de treillis finis induite par une loi demi-associative. J. Combinatorial Theory, 2:215-242, 1967. Google Scholar
  7. Gerhard Gentzen. Investigations into logical deductions. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131. North-Holland, Amsterdam, 1969. Google Scholar
  8. S. Huang and D. Tamari. Problems of associativity: A simple proof for the lattice property of systems ordered by a semi-associative law. J. Combin. Theory Ser. A, 13(1):7-13, 1972. Google Scholar
  9. Stephen Lack and Ross Street. Triangulations, orientals, and skew monoidal categories. Advances in Math., 258:351-396, 2014. Google Scholar
  10. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154-170, 1958. Google Scholar
  11. Joachim Lambek. On the calculus of syntactic types. In R. Jakobson, editor, Structure of Lang. and its Math. Aspects, Proc. Symp. Appl. Math., XII, pages 166-178. AMS, 1961. Google Scholar
  12. Sergei K. Lando and Alexander K. Zvonkin. Graphs on Surfaces and Their Applications. Number 141 in Encyclopaedia of Mathematical Sciences. Springer-Verlag, 2004. Google Scholar
  13. Saunders Mac Lane. Natural associativity and commutativity. Rice University Studies, 49(4):28-46, 1963. Google Scholar
  14. M. L. Laplaza. Coherence for associativity not an isomorphism. J. Pure and Appl. Alg., 2(2):107-120, 1972. Google Scholar
  15. Paul-André Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In S. Tison, editor, Rewriting Techniques and Appl., volume 2378 of LNCS, pages 24-50. Springer, 2002. Google Scholar
  16. Richard Moot and Christian Retoré. The Logic of Categorical Grammars: A Deductive Account of Natural Language Syntax and Semantics, volume 6850 of LNCS. Springer, 2012. Google Scholar
  17. F. Müller-Hoissen and H.-O. Walther, editors. Associahedra, Tamari Lattices and Related Structures: Tamari Memorial Festschrift, volume 299 of Prog. in Math. Birkhauser, 2012. Google Scholar
  18. Jason Reed. Queue logic: An undisplayable logic? Unpublished manuscript, April 2009. Google Scholar
  19. Jason Reed and Frank Pfenning. Focus-preserving embeddings of substructural logics in intuitionistic logic. Unpublished manuscript, January 2010. Google Scholar
  20. D. D. Sleator, R. E. Tarjan, and W. P. Thurston. Rotation distance, triangulations, and hyperbolic geometry. J. Amer. Math. Soc., 1(3):647-681, 1988. Google Scholar
  21. N. J. A. Sloane. The On-Line Encyclopedia of Integer Sequences. URL: https://oeis.org.
  22. James Dillon Stasheff. Homotopy associativity of H-spaces, I. Trans. Amer. Math. Soc., 108:293-312, 1963. Google Scholar
  23. Ross Street. Skew-closed categories. J. Pure and Appl. Alg., 217(6):973-988, 2013. Google Scholar
  24. Kornél Szlachányi. Skew-monoidal categories and bialgebroids. Advances in Math., 231(3-4):1694-1730, 2012. Google Scholar
  25. Dov Tamari. Monoïdes préordonnés et chaînes de Malcev. Thèse, Université de Paris, 1951. Google Scholar
  26. Dov Tamari. Sur quelques problèmes d'associativité. Ann. sci. de Univ. de Clermont-Ferrand 2, Sér. Math., 24:91-107, 1964. Google Scholar
  27. W. T. Tutte. A census of planar triangulations. Canad. J. Math., 14:21-38, 1962. Google Scholar
  28. T. R. S. Walsh and A. B. Lehman. Counting rooted maps by genus III: Nonseparable maps. J. Combin. Theory Ser. B, 18:222-259, 1975. Google Scholar
  29. Noam Zeilberger. On the unity of duality. Ann. Pure and Appl. Log., 153(1-3):66-96, 2008. Google Scholar
  30. Noam Zeilberger. Linear lambda terms as invariants of rooted trivalent maps. J. Functional Programming, 26(e21), 2016. Google Scholar
  31. Noam Zeilberger. A sequent calculus for the Tamari order. arXiv:1701.02917, 2017. Google Scholar
  32. Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. Logical Methods in Comp. Sci., 11(3:22), 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact