Programmation logique, unification et espace logarithmique

Date(s) : 12/06/2014
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.

Page web C. Aubert« >Page web C. Aubert




Catégories Pas de Catégories



Retour en haut 

Secured By miniOrange