Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Nguyễn, Lê Thành Dũng; Pradic, Pierre https://www.dagstuhl.de/lipics License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-125426
URL:

;

Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic

pdf-format:


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.

BibTeX - Entry

@InProceedings{nguyn_et_al:LIPIcs:2020:12542,
  author =	{Lê Th{\`a}nh Dũng Nguyễn and Pierre Pradic},
  title =	{{Implicit Automata in Typed λ-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 =	{Artur Czumaj and Anuj Dawar and Emanuela Merelli},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12542},
  URN =		{urn:nbn:de:0030-drops-125426},
  doi =		{10.4230/LIPIcs.ICALP.2020.135},
  annote =	{Keywords: Church encodings, ordered linear types, star-free languages}
}

Keywords: Church encodings, ordered linear types, star-free languages
Seminar: 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Issue date: 2020
Date of publication: 29.06.2020


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI