3 Search Results for "Zeilberger, Noam"

Document
DOI: 10.4230/LIPIcs.FSCD.2023.17
Convolution Products on Double Categories and Categorification of Rule Algebras

Authors: Nicolas Behr, Paul-André Melliès, and Noam Zeilberger

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Motivated by compositional categorical rewriting theory, we introduce a convolution product over presheaves of double categories which generalizes the usual Day tensor product of presheaves of monoidal categories. One interesting aspect of the construction is that this convolution product is in general only oplax associative. For that reason, we identify several classes of double categories for which the convolution product is not just oplax associative, but fully associative. This includes in particular framed bicategories on the one hand, and double categories of compositional rewriting theories on the other. For the latter, we establish a formula which justifies the view that the convolution product categorifies the rule algebra product.
Cite as

Nicolas Behr, Paul-André Melliès, and Noam Zeilberger. Convolution Products on Double Categories and Categorification of Rule Algebras. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{behr_et_al:LIPIcs.FSCD.2023.17,
  author =	{Behr, Nicolas and Melli\`{e}s, Paul-Andr\'{e} and Zeilberger, Noam},
  title =	{{Convolution Products on Double Categories and Categorification of Rule Algebras}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17},
  URN =		{urn:nbn:de:0030-drops-180017},
  doi =		{10.4230/LIPIcs.FSCD.2023.17},
  annote =	{Keywords: Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.135
Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic

Authors: Lê Thành Dũng Nguyễn and Pierre Pradic

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages instead. A key ingredient in our approach – that it shares with higher-order model checking – is the use of Church encodings for inputs and outputs. Our result is, to our knowledge, the first use of non-commutativity in implicit computational complexity.
Cite as

Lê Thành Dũng Nguyễn and Pierre Pradic. Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 135:1-135:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.ICALP.2020.135,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng and Pradic, Pierre},
  title =	{{Implicit Automata in Typed \lambda-Calculi I: Aperiodicity in a Non-Commutative Logic}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{135:1--135:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.135},
  URN =		{urn:nbn:de:0030-drops-125426},
  doi =		{10.4230/LIPIcs.ICALP.2020.135},
  annote =	{Keywords: Church encodings, ordered linear types, star-free languages}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.33
A Sequent Calculus for a Semi-Associative Law

Authors: Noam Zeilberger

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

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

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)

Copy BibTex To Clipboard

@InProceedings{zeilberger:LIPIcs.FSCD.2017.33,
  author =	{Zeilberger, Noam},
  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 =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.33},
  URN =		{urn:nbn:de:0030-drops-77179},
  doi =		{10.4230/LIPIcs.FSCD.2017.33},
  annote =	{Keywords: proof theory, combinatorics, coherence theorem, substructural logic, associativity}
}
  • Refine by Author
  • 2 Zeilberger, Noam
  • 1 Behr, Nicolas
  • 1 Melliès, Paul-André
  • 1 Nguyễn, Lê Thành Dũng
  • 1 Pradic, Pierre

  • Refine by Classification
  • 1 Theory of computation → Algebraic language theory
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Linear logic

  • Refine by Keyword
  • 1 Categorical rewriting
  • 1 Church encodings
  • 1 associativity
  • 1 coherence theorem
  • 1 combinatorics
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2017
  • 1 2020
  • 1 2023

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact