2026-07-25T23:13:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12542 2025-05-14T15:17:15Z ddc:004 open_access

Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic Nguyễn, Lê Thành Dũng Pradic, Cécilia Church encodings ordered linear types star-free languages 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lê Thành Dũng Nguyễn and Cécilia Pradic 2020 Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2020.135 urn:nbn:de:0030-drops-125426 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.135 eng https://creativecommons.org/licenses/by/3.0/legalcode