Programmation logique, unification et espace logarithmique
Clément Aubert
I2M, Aix-Marseille Université
https://aubert.perso.math.cnrs.fr/
Date(s) : 12/06/2014 iCal
14h00 - 15h00
Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique.
Un travail en collaboration avec Marc Bagnol, Paolo Pistone et Thomas Seiller.
Catégories
