13 septembre 2018, 11:00 : Séminaire

Lê Thành Dũng Nguyễn (LIPN, Paris 13), Évaluation sémantique en logique linéaire élémentaire

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.