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
14 h 00 min - 15 h 00 min

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



Retour en haut 

Secured By miniOrange