Les logiques légères, comme la Logique Linéaire Légère (LLL) [Jean-Yves Girard 95] ou la Logique Intuitionniste Affine Légère (ILAL) [Andrea Asperti 98], sont des variantes de la logique linéaire. Elles proviennent d'une étude fine des exponentielles permettant de restreindre le nombre d'étapes de normalisation et permettent de caractériser le temps polynomial via l'isomorphisme de Curry-Howard : toute fonction calculable en temps polynomial est codable en un réseau de la logique légère et réciproquement tout réseau normalise en temps polynomial (dépendant d'une donnée géométrique, la profondeur).
Je propose dans cet exposé une extension ndILAL non déterministe de ILAL permettant de caractériser la complexité NP. Le non déterminisme est codé de manière très naturelle par une boîte somme (utilisée par Thomas Ehrhard et Laurent Regnier pour le lambda calcul différentiel et par Lorenzo Tortora de Falco dans sa notion de multi-boîte).
Dans cet exposé, j'introduirai ILAL et ndILAL puis montrerai la complétude pour le temps NP en utilisant au maximum la preuve de P-complétude pour ILAL. Je montrerai au passage la difficulté pour faire une construction similaire avec LLL.
Les constructions proposées étant largement axiomatiques, aucune capacité à lire ou écrire des & à l'envers n'est nécessaire pour cet exposé...