Automates implicites dans les -calcules III : fonctions affine planaires de transformation de chaînes à chaînes

Nous prouvons une caractérisation de la transduction de chaînes à chaînes de premier ordre via des -termes typés dans une logique affine non commutative qui calcule avec l'encodage de Church, prolongeant la caractérisation analogue connue des langages sans étoile. Nous montrons que chaque transduction de premier ordre peut être calculée par un -terme en utilisant un lemme de décomposition de style Krohn-Rhodes connu. La direction inverse est donnée par la compilation des -termes en transducteurs planaires réversibles à deux voies. La validité de cette traduction implique de montrer que les fonctions de transition de ces transducteurs vivent dans une catégorie monoidale fermée de diagrammes dans laquelle nous pouvons interpréter purement des -termes affines. Un défi est que l'unité du tenseur de la catégorie en question n'est pas un objet terminal. En conséquence, notre interprétation n'identifie pas les termes -équivalents, mais elle transforme les -réductions en inégalités dans un enrichissement en poset de la catégorie des diagrammes.