Réalisabilité et calculabilité des types d’ordre supérieur

John Longley

COURS INTENSIF

La notion de fonction calculable sur les entiers positifs est bien connue. Beaucoup moins évidente est celle d’opération “calculable” de type supérieur, par exemple du type ((N → N) → N) → N. En effet, il n’est pas a priori clair qu’il existe des notions raisonnables de calculabilité pour les types d’ordre supérieur.

Néanmoins, létude de la calculabilité des types d’ordre supérieur s’avère mathématiquement fructueuse, et produit un petit nombre de notions différentes de calculabilité apparemment naturelles et robustes du point de vue mathématique. A part son intérêt conceptuel intrinsèque, ce sujet à des relations avec:

• La logique constructive et la metamathématique.

• La sémantique et la logique des langages de programmation.

• La théorie de la complexité.

• La calculabilité sur le corps des nombres réels.

• La calculabilité en physique.

A partir des années 50 le sujet a évolué de façon un peu chaotique, avec des lignes diverses assez éparpillées dans la litterature en théorie de la récursion, en logique constructive et en informatique. Néanmoins, en perspective, il est possible de donner une description cohérente, dans un cadre uniforme, de ce matériel.

Dans le premier exposé je ferai un bref tour d’horizon historique du sujet, comprenant les contributions de Kleene, Kreisel, Platek, Scott et beaucoup d’autres. Je décrirai alors quelques efforts récents destinés à donner une certaine cohérence à ce paysage. J’explorerai, dans un cadre abstrait simple, les diverses notions de fonctionnelle calculable de type supérieur et leurs relations. Je montrerai enfin comment certaines idées de la théorie de la réalisabilité constituent un cadre où il est possible de discuter des notions, même plus générales (par ex., nonextensionnelles) d’“opération calculable”.

Dans ce cours je mettrai l’accent sur l’interaction entre calculabilité et réalisabilité, et les applications potentielles en informatique.

Address: Division of Informatics, University of Edinburgh, JCMB, The King’s Buildings, Mayfield Road, Edinburgh EH9 3JZ, UK

E-mail: jrl@dcs.ed.ac.uk