Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Cours de sémantique des jeux --- DEA Programmation
--- Olivier Laurent et Paul-Andre Melliès
Le modèle des bidomaines,
un modèle de PCF défini
par Gérard Berry en 1979,
est à la fois stable et extensionnel,
Ce modèle est linéarisé en 1995
par Pierre-Louis Curien, Gordon Plotkin et Glynn Winskel,
qui obtiennent ainsi un modèle nouveau
de la logique linéaire:
le modèle des bistructures.
Ce modèle de bistructures dévoile
une dualité encore incomprise
entre extensionnalité et stabilité.
Des développements récents
indiquent une connection intéressante avec la ``ludique''
de Jean-Yves Girard.
De plus, ce modèle statique, très proche
du modèle de cohérence, dispose
d'une composition dynamique, où
les cliques (pourtant statiques!) ``interagissent''.
Le projet du stage est d'étudier le modèle
à la manière d'une sémantique de jeu
--- mais une sémantique de jeu ``rétrograde''
où Joueur et Opposant interagissent pour définir
leur passé commun, au lieu de construire leur futur.
Stage 2. Réécriture.
Généralisation de la théorie axiomatique.
Dans un article ``Towards a proof-theory of rewriting:
the simply-typed 2-lambda-calculus'', Barnaby Hilken
caractérise les formes normales beta-eta-longues du lambda-calcul
de manière élégante:
ce sont les lambda-termes P tels que tout chemin
de beta-eta réduction P-->Q est accompagné
d'un chemin de réduction Q-->P tel que P-->Q-->P
soit l'identité.
La théorie de B. Hilken ne rentre pas dans le cadre axiomatique
de la réécriture que j'ai défini
dans une série d'articles (ART I, II, III et IV).
Le sujet du stage sera d'analyser la construction de B. Hilken,
en vue d'une généralisation ultérieure
de la théorie axiomatique.
Stage 3. Réécriture.
Lambda calcul avec substitutions explicites.
Dans tout système de réécriture axiomatique,
il est possible de caractériser catégoriquement
la notion de ``réductions de tete'' --- voir ART IV.
En fait, on démontre qu'à partir
de tout terme P, il existe un cone de telles
réductions h:P-->V qui transforment P
en une forme normale de tete V.
Dans le lambda-calcul, ce cone ne contient qu'une réduction au plus,
qu'on appelle la réduction de tete.
Mais en général, dans un système
de réécriture non d&'eterministe,
le cone contient plusieurs réductions incompatibles.
Dans le cas du lambda sigma calcul, un lambda calcul
avec substitutions explicites, il est possible de montrer
que toutes les réductions du cone à partir
d'un lambda-sigma terme P se projettent
par interprétation sur la réduction
de tete (unique) du lambda-calcul.
La démonstration donnée en ART II est syntaxique.
Le sujet du stage sera d'en trouver une présentation abstraite.