le prochaine seminaire PPS est
Jeudi 11 Juin,
11h, salle 0C2:
Lorenzo Tortora de Falco (Roma)
Sémantique relationnelle et temps d'exécution en Logique Linéaire
Qu'est-ce qu'un calcul correct ? Une tentative de répondre à la question
est de donner un maximum de place aux calculs non corrects. On sera alors
amené à identifier des propriétés cruciales du calcul, qui seront les
témoins de sa correction (terminaison faible ou forte, confluence,
exécution en temps borné, etc...). En guise d'introduction, je discuterai
du point de vue de la logique linéaire (LL) sur la question, pour prendre
ensuite celui de la sémantique relationnelle sur lequel portera
l'essentiel de l'exposé. Je présenterai les résultats principaux d'un
travail en collaboration avec Daniel De Carvalho et Michele Pagani: 1) un
réseau de preuve de LL est normalisable ssi son interprétation
``exhaustive'' est non vide 2) à partir de l'interprétation de deux
réseaux sans coupures de LL on peut calculer le nombre exact d'étapes
d'élimination des coupures conduisant du réseau obtenu en coupant entre
eux les deux réseaux de départ et sa forme normale. Si le temps le permet,
je discuterai d'une possible amélioration de ce dernier résultat (travail
en cours avec Daniel De Carvalho).
Aucun commentaire:
Enregistrer un commentaire