[Best Paper] Qu'est-ce qui est calculable par un ordinateur dans un temps réaliste en interrogeant un oracle ?

 
Publié le 11/07/2022 - Mis à jour le 18/07/2022

Des enseignants-chercheurs du laboratoire Loria (CNRS, Inria, Université de Lorraine) Emmanuel Hainry, Romain Péchoux, Jean-Yves Marion et Bruce Kapron (Université de Victoria, Canada) ont obtenu le prix EATCS du meilleur article à ETAPS 2022 (European Joint Conférence on Theory and Practice of Software). Dans cet article, un système de calcul est développé qui modélise  tous les calculs réalisés par une machine de Turing qui aurait accès aux décimales d'un nombre réel dans un temps de calcul réaliste. Ce travail est un aboutissement notamment des travaux de Stephen Cook dans les années 90 sur ce sujet.

ETAPS a eu lieu du 2 au 7 avril à Munich et réunissait chercheurs et industriels autour de la science des logiciels en regroupant quatre conférences : ESOP, FoSSaCS, FASE et TACAS. Les chercheurs ont été récompensés du prix EATCS (European Association for Theoretical Computer Science) du Best Theory Paper pour leur article Complete and tractable machine-independant characterizations of second-ordre polytime.

Ces travaux d'informatique théorique portent sur la complexité implicite, c'est-à-dire la caractérisation des classes de complexité des programmes informatiques pour déterminer leur performance.

Ces recherches s'ancrent dans un partenariat entre les équipes du Loria et un chercheur de l'Université de Victoria : "Il y a cinq ans, Bruce Kapron a trouvé une nouvelle caractérisation de l'équivalent à l'ordre 2 de la classe de complexité en temps polynomial (classe P) : les Basic Feasible Functions (BFF). Nous avons ainsi démarré avec lui une collaboration fructueuse dans ce domaine", explique Emmanuel Hainry.

Les travaux des quatre chercheurs décrivent un langage de programmation qui caractérise la classe BFF avec une procédure de typage permettant de déterminer si un programme se situe dans cette classe ou non.

Ce typage étant décidable en temps polynomial, le résultat a permis à l’équipe d’obtenir la première caractérisation tractable, complète et implicite de BFF. Bravo à nos quatre lauréats pour ce résultat qui résout un problème ouvert depuis 20 ans !