Automates implicites dans les -calculi III : fonctions string-à-string affines planaires

Nous prouvons une caractérisation de la transduction string-à-string de premier ordre via des -termes typés dans une logique affine non commutative qui calculent avec l'encodage de Church, étendant 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 de -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 close monoidale de diagrammes dans laquelle nous pouvons interpréter des -termes purement 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 de poset de la catégorie des diagrammes.