DEA 01/02
DEA 16/10/01
Résumé: cours du 16/10/01
cours précédent ........ cours suivant..........tous les cours
Contenu du cours: Règles de typage. Algorithme de typage (Church puis
Curry). Propriétés pour une notion de réduction:
normalisation forte et faible, confluence, diamant, confluence faible.
Enoncé des théorème de normalisation forte et de
confluence. Notion de réduction parallèle.
Exercices.
Résoudre, dans les types, l'équation à deux
inconnues: $X->Y =Y->X; $X -> Y->X=(Y->Y)->X$.
Résoudre, dans les types, l'équation à quatre
inconnues: $X -> Y->Y=(Z->Z)->T$.
On donne quatre types simples $P, Q, R, S$. Donner un terme clos de type
$P -> (P->Q) ->(P->R)-> (Q->R->S)->S$. Dessiner l'arbre de preuve du jugement de
typage.
Est-ce que $2.2$ ( où $2$ est l'entier de Church revu par Curry) est
typable? Est-ce qu'il se réduit sur $4$?
Trouver tous les types de $lam x. lam y. x y x$,
$lam x. lam y. x (y x)$, $lam f. lam x. f (f x)$, $lam f. lam x. x (f (f x))$,
$lam f. lam g. lam x. x (g (f x))$,
$lam f. lam g. lam x. f x (g x)$.
Dans quels environnements $x y x $ et $x (y x)$,
$x (g (f x))$, $x g (f x)$, $x f (f x)$, $x f lam f.(f x)$,
$x f lam g.(f x)$.
Démontrer soigneusement que si une notion de réduction
$delta$ (sur un ensemble quelconque)
a la
propriété du diamant, alors $delta*$ est confluente.
Définir pour tout terme $P$ un terme $G(P)$ qui mérite le nom
de gamma-réduit maximal de $P$. Essayer de formuler
la propriété de maximalité qui le caractérise.
cours précédent ........ cours suivant..........tous les cours
Andre.HIRSCHOWITZ
Last modified: Oct 17