Cécilia Pradic ; Ian Price - Implicit automata in {\lambda}-calculi III: affine planar string-to-string functions

entics:14804 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14804
Implicit automata in {\lambda}-calculi III: affine planar string-to-string functionsArticle

Authors: Cécilia Pradic ; Ian Price

    We prove a characterization of first-order string-to-string transduction via $\lambda$-terms typed in non-commutative affine logic that compute with Church encoding, extending the analogous known characterization of star-free languages. We show that every first-order transduction can be computed by a $\lambda$-term using a known Krohn-Rhodes-style decomposition lemma. The converse direction is given by compiling $\lambda$-terms into two-way reversible planar transducers. The soundness of this translation involves showing that the transition functions of those transducers live in a monoidal closed category of diagrams in which we can interpret purely affine $\lambda$-terms. One challenge is that the unit of the tensor of the category in question is not a terminal object. As a result, our interpretation does not identify $\beta$-equivalent terms, but it does turn $\beta$-reductions into inequalities in a poset-enrichment of the category of diagrams.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 20, 2024
    Submitted on: November 19, 2024
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,68N18, 03B40, 68Q55, 68Q45, 03B47

    Consultation statistics

    This page has been seen 25 times.
    This article's PDF has been downloaded 9 times.