Liste d'erreurs constatées dans le manuscrit de thèse ===================================================== (mise à jour mai 2006) Je remercie les personnes ayant contribué à pointer les erreurs. Chapitre 3 (LKT et le lambda-mu-calcul) --------------------------------------- 1) Typos : la conclusion à droite de Coup_M est A (au lieu de B) 2) Problèmes techniques : Le traitement de "mu beta[gamma]" est incorrect lorsque gamma est beta. Cela s'exprime en plusieurs endroits: - Définition de "beta est lié dans le champ d'un mu beta[gamma]" : remplacer par "beta est lié dans dans le champ d'un mu beta" - Définition de la mu-réduction : remplacer (mu beta [alpha]u) l -> mu beta [alpha](u[[beta]khi:=[beta](khi l)] par (mu beta [alpha]u) l -> mu beta ([alpha]u)[[beta]khi:=[beta](khi l)]. - Règle de changement de conclusion : ajouter la variante Gamma; |- Delta, B; A --------------------- pour A figurant dans Delta, B Gamma; |- Delta; B - Contrepartie logique de la mu-réduction : ajouter le cas Gamma; |- Delta, A; A --------------------- Chg Gamma; |- Delta; A Gamma; A |- Delta; C ------------------------------------------------ Coup_mu Gamma; |- Delta; C -> Gamma; |- Delta, A; A Gamma; A |- Delta; C --------------------------------------------- Coup_mu Gamma; |- Delta, C; A Gamma; A |- Delta; C ------------------------------------------------------------- Coup_T Gamma; |- Delta, C; C --------------------- Chg Gamma; |- Delta; C La meilleure approche est sans doute d'introduire la catégorie des commandes (de la forme [gamma]t) et redéfinir la syntaxe des expressions par t ::= ... | mu beta c | ... c ::= [alpha]t | c[x:=t] | c[[alpha]khi:=[alpha](khi l)] l ::= ... En particulier, la syntaxe des expressions normales est décrite par t ::= (x l) | (\x.t) | mu beta c c ::= [alpha]t l ::= [] | [t::l] Question typage, les commandes sont typées par des séquents de la forme "Gamma; |- Delta;" et la règle d'échange se décompose en une règle d'activation et une règle de contraction : Gamma; |- Delta, B; Gamma; |- Delta, B; B ------------------- Activ --------------------- Cont Gamma; |- Delta; B Gamma; |- Delta, B; De même, les règles de coupure Coup_mu et Coup_M se raffinent en Gamma; Pi |- Delta, A; Pi' Gamma; A |- Delta; B -------------------------------------------------- Coup_mu Gamma; Pi |- Delta; B; Pi' Gamma; |- Delta; A Gamma, A; Pi |- Delta; Pi' -------------------------------------------------- Coup_mu Gamma; Pi |- Delta; Pi' (à noter que Pi' non vide implique Pi non vide) Question réduction, la mu-réduction devient (mu beta c) l -> mu beta c[[beta]khi:=[beta](khi l)]. et les règles D_yes et D_no sont remplacées, sur les termes, par (mu beta c)[[alpha]khi:=[alpha](khi l)] -> mu beta (c[[alpha]khi:=[alpha](khi l)]) (pour beta frais) et sur les commandes par ([alpha]u)[[alpha]khi:=[alpha](khi l)] -> [alpha](u[[alpha]khi:=[alpha](khi l)] l) ([beta]u)[[alpha]khi:=[alpha](khi l)] -> [beta](u[[alpha]khi:=[alpha](khi l)]) (pour alpha distinct de beta)