Évaluation sémantique en logique linéaire élémentaire
Tito Nguyen
LIPN, Université Paris 13
http://nguyentito.eu/
Date(s) : 13/09/2018 iCal
11h00 - 12h30
Après avoir passé en revue l’utilisation des techniques d’évaluation sémantique pour caractériser des classes de complexité en lambda-calcul simplement typé (en particulier les travaux de Hillebrand et Kanellakis), nous décrirons un nouveau résultat s’appliquant à une logique du second ordre : les langages décidés par des programmes en logique linéaire élémentaire (ELL) opérant sur des chaînes de Church et de type de sortie !!Bool sont exactement les langages rationnels. (En ajoutant des types récursifs, on obtient tout le temps polynomial, ce qu’a montré Baillot.) La preuve repose principalement sur l’existence d’une sémantique finie de la logique linéaire multiplicative du second ordre, obtenue par quotient observationnel. Ce premier résultat pourrait ouvrir la voie à une étude fine de la complexité dans les logiques allégées, tenant compte du contrôle exercé conjointement par les propriétés géométriques de la syntaxe et le typage, ce dernier étant reflété dans la sémantique. Ainsi, nous formulerons une caractérisation conjecturale de l’espace logarithmique dans ELL.
Travail réalisé avec Thomas Seiller.
Lê Thành Dũng Nguyễn aka Tito Nguyen
Catégories
