CONCEPTION DE LANGAGE --------------------- Sémantique dénotationnelle J1- Langage de programmation: exprimer - des données - des traitements => une syntaxe + une sémantique Syntaxe Ensemble des textes(suites de caractères) qui appartiennent au langage. 2 éléments de syntaxe: - le lexique - la grammaire 2 problèmes: - définir - reconnaître Lexique Ensemble des mots/unités lexicales/lexème admis Alphabet + règles de formation Formalisme de définition: les expressions régulières Propriété: expressions régulières == automates finis => algorithme de reconnaissance Mise en oeuvre: Lex et ses avatars Syntaxe Ensemble des phrases correctes du langage: assemblage de mots aux quel ont peut attribuer un sens; pour lesquels on a des régles d'interprétation/évaluation/compilation Lexique + règle de production Formalisme: grammaires ~~ automates à piles (selon la classe de grammaire) => algorithme de reconnaissance Mise en oeuvre: Yacc et ses avatars Utilisation ----------- Analyse lexicale et syntaxique (Lex+Yac) préalable au processus d'interprétation des sources d'un langage - définition de la sémantique - implantation d'un évaluateur - génération de code (octet/machine) Utilisation standard: passage de syntaxe "concrète" (texte du programme sous) à la syntaxe "abstraite" (structure arborescente) Rappel: l'expression (préfixe parenthésée) (+ (* 4 5) 3 (+ 1 7 8)) est équivalente à l'arbre + /|\ / | \ / 3 \ * + / \ /|\ 4 5 / | \ 1 7 8 Expressions régulières ---------------------- Un alphabet: A = {'0', '1'} Mots sur A: '' (mot vide) '0' '1' '00' '01' '10' '11' '000' '001' '010' '011' '100' '101' '110' '111' '0000' Concaténation: '01'.'01' = '0101' associative: '01'.('01'.'01') = ('01'.'01').'01' = '010101' Définition ensembliste (ensemble -W1 W2 W- de mots -w1 w2 w-) - mot vide {''} - singleton {'a' / a in A} (par abus, on note A) - concaténation W1.W2 = {w1.w2 / w1 in W1 et w2 in W2} - union W1|W2 = {w / w in W1 ou w in W2} - fermeture de Kleene W* = {} | W | W.W | W.W.W | W.W.W.W | ... définition récursive: - W^0 = {} - W^{n+1} = W^n | (W.W^n) W* = |_n W^n pour n de 0 à l'infini NB: tous les mots sur A = A* Ppte: W.W^n = W^n.W Exemples les mots binaires: (0|1)* dans les langages à expressions régulières: [01]* les entiers décimaux positifs: (0|1|2|3|4|5|6|7|8|9).(0|1|2|3|4|5|6|7|8|9)* abréviations: [0-9][0-9]* [0-9]+ les entiers décimaux relatifs: ([0-9]|-[0-9])[0-9]* abréviation: -?[0-9]+ avec point décimal: (caractère d'échapement \.) (-?[0-9]+)|(-?[0-9]+\.[0-9]*) équivalent: -?[0-9]+\.?[0-9]* NB: '.05' n'est pas dans le lexique Grammaire: Symboles "terminaux": mots clef, symboles réservés, unités lexicales (constantes, ident, etc.) Symboles "non terminaux": ensemble de suites de mots/partie du langage Règles de productions : non-terminal -> (terminal|non terminal)* Exemple: expressions arithmétiques préfixes parenthésées Terminaux: symboles réservés: + * ( ) unités lexicales (ensemble de): num = [0-9]* Non terminaux: E Es Règles: (définition récursive) E -> num R1 E -> (* Es) R2 E -> (+ Es) R3 Es -> E R4 Es -> E Es R5 Implicite: caractères séparateurs (esp. tab. crlf) Production de (+ (* 4 5) 3 (+ 1 7 8)) E -> (+ Es) par R3 -> (+ E Es) par R5 -> (+ (* Es) Es) par R2 -> (+ (* E Es) Es) par R5 -> (+ (* 4 Es) Es) par R1 -> (+ (* 4 E) Es) par R4 (sur le premier Es) -> (+ (* 4 5) Es) par R1 -> (+ (* 4 5) E Es) par R5 -> (+ (* 4 5) 3 Es) par R1 -> (+ (* 4 5) 3 (+ Es)) par R3 -> (+ (* 4 5) 3 (+ E Es)) par R5 -> (+ (* 4 5) 3 (+ 1 Es)) par R1 -> (+ (* 4 5) 3 (+ 1 E Es)) par R5 -> (+ (* 4 5) 3 (+ 1 7 Es)) par R1 -> (+ (* 4 5) 3 (+ 1 7 E)) par R4 -> (+ (* 4 5) 3 (+ 1 7 8)) par R1 Analyse: remonter les flèches l'expression appartient au langage ssi on remonte à E (+ 3 * 4 5) <- (+ 3 * 4 E) <- (+ 3 * 4 Es) <- (+ 3 * E Es) <- (+ 3 * Es) plus de règle applicable: échec Plusieurs production/analyse (+ 0 0) E -> (+ Es) -> (+ E Es) +-> (+ 0 Es) -> (+ 0 E) -> (+ 0 0) | +-> (+ E E) +-> (+ 0 E) -> (+ 0 0) | +-> (+ E 0) -> (+ 0 0) Grammaire ambigüe: expressions infixes (sans trop de paranthèses) E -> num E -> E + E E -> E * E E -> ( E ) Exemple: 1 + 2 * 3 peut venir de E + E ou E * E ==> opérateur principal différent ==> valeurs attendues/interprétation différentes = 1 + (2 * 3) ou (1 + 2) * 3 Cependant: on peut s'en satisfaire pour définir la sémantique. Un bête langage: déclarations et expressions Lexique Symboles réservés: op '(' ')' '=' ';' avec op = '*' '+' '-' '/' '%' '^' Mots clef : 'Cst' Nombres (num) : [0-9]+ Noms (ident) : [a-z][a-zA-Z]*[0-9]* Syntaxe Prog ::= Exp Prog | Decs Exp Decs ::= Dec | Dec Decs Dec ::= 'Cst' ident '=' Exp ';' Exp ::= num | ident | Exp op Exp | '(' Exp ')' ou plus simplement Prog ::= Exp | Dec Prog Dec ::= 'Cst' ident '=' Exp ';' Exp ::= num | ident | Exp op Exp | '(' Exp ')' Exemple Cst a = 1; Cst b = 2; Cst c = 3; Cst s = (a + b + c) / 2; s * (s - a) * (s - b) * (s - c) Sémantique (intuitivement) Fonction de l'ensemble des programmes dans un "domaine" de valeur Ensemble des programmes: Prog = { arbres de syntaxe abstraite des prog. } (vérifier que c'est compris) On note les arbres entre [[ et ]] on a aussi ensemble des déclaration Dec des suites de déclarations Decs des expressions Exp et aussi des identificateurs Ident des constantes numériques Num des opérateurs Op Ensemble de valeurs: Z (entiers relatifs) Mais aussi: ensemble des fonctions Z -> Z -> Z pour la sémantique des opérations. Lambda notation: \x.\y.(x+y) Pour chaque cas de construction des programmes, une fonction sémantique: Cas simple: pas de déclaration P: Prog -> Z E: Exp -> Z N: Num -> Z O: Op -> (Z -> Z -> Z) les programmes p sont réduits à une expression e P[[ e ]] = E[[ e ]] E[[ n ]] = N[[ n ]] avec n élément de Num E[[ e1 op e2 ]] = O[[ op ]] E[[ e1 ]] E[[ e2 ]] O[[ + ]] = \x.\y.(x+y) etc. Avec déclarations: environnement (2ième syntaxe) Env = Ident -> Z ensemble des fonctions des noms dans les valeurs Environnement vide: fonction jamais définie Deux opérations sur les environnements r accés: r(x) valeur de la constante de nom x dans l'environnement r ajout: r[x:=v] avec x Ident et v valeur nouvelle fonction Ident -> Z telle que r[x:=v](x) = v r[x:=v](y) = r(y) si y différent de x P: Prog -> Env -> Z E: Expr -> Env -> Z P[[ e ]] r = E[[ e ]] r P[[ Cst x = e; p ]] = P[[ p ]] r[x=E[[ e ]]r] E[[ x ]] r = r(x) E[[ n ]] r = N[[ n ]] E[[ e1 op e2 ]] r = O[[ op ]] (E[[ e1 ]] r) (E[[ e2 ]] r) Exercices: * sémantique de la 1ière syntaxe * syntaxe et sémantique avec définition de fonctions (non récursives) * définition de N: Num -> Z J2- Corrigé des exercices * 1ière syntaxe P: Prog -> Env -> Z Ds: Decs -> Env -> Env D: Dec -> Env -> Env E: Exp -> Env -> Z (inchangé) P[[ e ]] r = E[[ e ]] r P[[ ds e ]] r = E[[ e ]] (Ds[[ ds ]] r) Ds [[ d ]] r = D[[ r ]] r Ds [[ d ds ]] = Ds[[ ds ]] (D[[ d ]] r) D[[ Cst x = e ]] r = r[x:=E[[ e ]] r] Autre formulation P: Prog -> Z (puisque l'environnement est issu de Ds) Ds: idem D: idem E: idem On note r0 l'environnement vide: fonction jamais définie P[[ e ]] = E[[ e ]] r0 P[[ ds e ]] = E[[ e ]] (Ds[[ ds ]] r0) * avec définition de fonctions (non récursives) Syntaxe Nouveau mot clef: 'Fun' symbole réservé: ',' Dec ::= 'Cst' ident '=' Exp ';' | 'Fun' ident '(' Prs ')' '=' Exp ';' Prs ::= ident | ident ',' Prs Sémantique (intuitivement) associer à la déclaration [[ Fun f(x1, .., xn) = e ]] la fonction \x1..\xn. e et ajouter la liaison entre le nom f et la fonction \x1..\xn. e) à l'environnement. Mais attention, e peut contenir des constantes/fonctions définies avant (variables libre): il faut s'en souvenir fermeture = fonction + environnement On note: <\x1..\xn. e, r> Nouvelle définition des environnements: Valeur immédiate: Z Fonctions : Z^n -> Z Fermeture: Z^n -> Z * Env Env = Z | (Z^n -> Z * Env) Nouveau cas de défintion de D D[[ Fun f (x1, ..,xn) = e ]] r = r[f:=<\x1..\xn.e, r>] Autre conséquence: les expressions Syntaxe Exp ::= ... | ident '(' Exps ')' Exps ::= Exp | Exp ',' Exps Sémantique (intuitivement) si f est définie par \x1..\xn.e dans l'environnement r' l'application f(e1, .., en) dans l'environnement r vaut l'application (\x1, .., xn. e (E[[ e1 ]]r) .. (E[[ en ]]r)) dans l'environnement r' Lapplication (\x1, .., \xn. e (E[[ e1 ]]r) .. (E[[ en ]]r)) vaut e dans l'environnement [x1:=(E[[ e1 ]]r),.. , xn:=(E[[ en ]]r)] dans l'environnement r' E[[ f(e1, .., en) ]] r = E[[ e ]] [x1:=(E[[ e1 ]]r)] .. [xn:=(E[[ en ]]r)]r' On fera mieux par la suite. Lambda calcul Modèle définition/application de fonction Expliciter les arguments: lambda/abstraction x + y est l'expression qui dénote la somme de x et de y \x. \y. x + y est la fonction qui associe à tout x et y leur somme Application: (f x) préfixée abréviation (f x y) pour ((f x) y) (\x.\y.(+ x y) 1 2) est l'application qui donne la somme de 1 et de 2 Evaluation: beta-réduction remplacer les paramètres formels par les paramètres d'appel (((\x.\y.(+ x y) 1) 2)) --> ((\y.(+ 1 y) 2) --> (+ 1 2) --> 1+2 = 3 Application partielle: (\x.\y.(+ x y) 1) --> \y.(+ 1 y) fonction "successeur" Renommage: alpha-équivalence \y.(+ 1 y) == \x.(+ 1 x) (\y.(+ 1 y) 2) --> 1+2 <-- (\x.(+ 1 x) 2) Variables libres/liées: lambda = lieur x est lié dans \x.x x est libre dans \y.x si x est libre dans t alors x est lié dans \x.t Attention: diff nom/occurence x est libre et lié dans (\x.x x) (lire \x.x appliqué à x) 1ier x: lié (celui de \x.x) 2ième x: libre Justif: alpha-équivalence (\x.x x) == (\y.y x) Mais attention: (\x.x x) <> (\x.x y) on ne renomme pas les variables libres ! Encore attention: \y.(+ y x) <> \x.(+ x x) capture de variable (libre) change la fonction (\y.(+ y x) 1) --> (+ 1 x) il reste une inconnue (\x.(+ x x) 1) --> (+ 1 1) = 2 plus d'inconnue Beta-reduction: substitution (\x.t u) --> t[x:=u] lire 't dans lequel u remplace x' plus précisément 't dans lequel u remplace les occurences libres de x' (\x.(\x.x x) u) --> (\x.x u) --> u (\x.(\x.x x) u) == (\x.(\y.y x) u) --> (\y.y u) --> u attention aux captures: renommages (\x.\y.x y) <> \y.y (\x.\y.x y) == (\x.\z.x y) --> \z.y Définitions: Ensemble des lambdas-termes: soit X un ensemble infini déniombrable de variables. L'ensembles des lambda-termes est définiton par induction: - les variables sont des lambda termes - si t et u sont des lambda-termes alors (t u) est un lambda-terme - si x est une variable et t un lambda-terme alors \x.t est un lambda-terme Variables libres (occurences de): on définit 'x est libre dans t' par induction sur la forme de t - si t est une variable alors x est libre dans t ssi t est égal à x - si t est égal à (t1 t2) alors x est libre dans t ssi x est libre dans t1 ou x est libre dans t2 - si t est égal à \y.t1 avec y différent de x alors x est libre dans t ssi x est libre dans t1 NB: 'x est libre dans t' veut dire 'il existe des occurences de x dans t qui sont libres' (\x. x x) Variables liées: (occurence de) si x est libre dans t alors x est lié dans \x.t NB: toutes les occurences de x sont liées dans \x.t Substitution (aux occurences libres): on définit t[x:=u] par induction sur la forme de t - si t est la variable x t[x:=u] = u - si t est une variable y avec y différent de x t[x:=u] = y - si t est égal à (t1 t2) t[x:=u] = (t1[x:=u] t2[x:=u]) - si t est égal à \x.t1 t[x:=u] = t - si t est égal à \y.t1 avec y différent de x t[x:=u] = \z.t1[y:=z][x:=u] avec z non libre dans u (pourquoi?) Beta-reduction: on définit t --> u par induction sur la forme de t - si t est égal à \x.t1 t --> \x.u1 si t1 --> u1 - si t est égal à (t1 t2) régles générale t --> (u1 t2) si t1 --> u1 t --> (t1 u2) si t2 --> u2 redex si t1 est égal à \x.t3 t --> t3[x:=t2] NB: les variables ne sont pas réduites x --> x Beta-équivalence Itération de la beta-réduction: t --> u1 --> u2 --> u3 --> .. -> un on note t -n-> un on note t -*-> u s'il existe n tel que t -n-> u (avec n possiblement nul) (clôture réfléxive et transitive) On note t <--> u, on lit t est beta-équivalent à u ou t et u sont beta-équivalents On définit: t et u sont beta-équivalents ssi il existe w tel que t -*-> w et u -*-> w abréviation t -*-> w <-*- u Forme normale Un terme est en 'forme normale' si on ne peut pas le réduire ie: il ne contient aucun redex Les variables sont en forme normale. Si t -*-> v et v en forme normale alors v 'est la forme normale de' t Thm (confluence): si v est la forme normale de t alors v est unique Ppte: il existe des termes qui n'ont pas de forme normale (\x.(x x) \x.(x x)) --> (\x.(x x) \x.(x x)) Variantes: L'application 2 façons de réduire réduction droite/appel par valeur: (t1 t2) --> (t1 v2) si t1 -*-> v2 réduction gauche/appel par nom: (t1 t2) --> (v1 t2) si t1 -*-> v1 L'abstraction réduction faible/forme normale faible on n'utilise pas la règle \x.t1 --> \x.u1 on ne réduit pas sous les lambdas \x.t est en forme normale faible quelque soit t Point fixe: Ppte: il existe un terme Y tel que (Y t) <--> (t (Y t)) soit Y = \f.\x.((f (x x)) \x.(f (x x))) Exercice: vérifier (Y t) <--> (t (Y t)) (Y t) = (\f.(\x.(f (x x)) \x.(f (x x))) t) --> (\x.(t (x x)) \x.(t (x x))) --> (t (\x.(t (x x)) \x.(t (x x)))) <-- (t (\f.\x.(f (x x)) \x.(f (x x)) t)) = (t (Y t)) Codage de la récurrence: fonction récursive: f(x) = f(x+1) on a f(0) = f(1) = f(2) = f(3) = etc. codage: on pose F = \r.\x.(r (+ x 1)) et f = (Y F) on peut vérifier (f 0) <--> (f (+ 0 1)) <--> (f (+ (+ 0 1) 1)) <--> etc. montrons: ((Y F) t) <--> ((Y F) (+ t 1)) ((Y F) t) --> ((F (\x.(F (x x)) \x.(F (x x)))) t) --> ((\r.\x.(r (+ x 1)) (\x.(F (x x)) \x.(F (x x)))) t) --> (\x.((\x.(F (x x)) \x.(F (x x))) (+ x 1)) t) --> ((\x.(F (x x)) \x.(F (x x))) (+ t 1)) <-- ((\f.\x.(f (x x)) \x.(f (x x)) F) (+ t 1)) = ((Y F) (+ t 1)) (f 0) = ((Y F) 0) <--> ((Y F) (+ 0 1)) = (f (+ 0 1)) <--> ((Y F) (+ (+ 0 1) 1) = (f (+ (0 1) 1)) etc. Application Utilisation de lex/yacc (ocaml) Langage: dec-cstes + exp --Ast (arbre de syntaxe abstraite) type op = Plus | Mult | Sub | Div type prog = ASTExp of exp | ASTCst of string * exp * prog and exp = ASTNum of string | ASTId of string | ASTApp of op * exp * exp --Lex { open Parser open Ast } rule token = parse [' ' '\t' '\n'] {token lexbuf} |eof {END} |'=' {EQ} |';' {SEMICOL} |'(' {LPAR} |')' {RPAR} |'+' {OP Plus} |'*' {OP Mult} |'-' {OP Sub} |'/' {OP Div} |"Cst" {CST} |(['a'-'z''A'-'Z'])(['a'-'z''A'-'Z''0'-'9''?'])* {IDENT(Lexing.lexeme lexbuf)} |('-'?)['0'-'9']+ {NUM(Lexing.lexeme lexbuf)} --Yacc %{ open Ast %} %token END %token CST SEMICOL %token EQ %token LPAR RPAR %token OP %token NUM %token IDENT %start prog %type prog %% prog: exp END {ASTExp($1)} | CST IDENT EQ exp SEMICOL prog {ASTCst($2,$4,$6)} ; exp: NUM {ASTNum($1)} | IDENT {ASTId($1)} | LPAR exp RPAR { $2 } | exp OP exp {ASTApp($2, $1, $3)} ; --Sem open Ast let empty_env = fun x -> failwith "Empty env." let add_env x v r = fun y -> if (x=y) then v else (r y) let semNum = int_of_string let semOp op = match op with Plus -> (fun x -> fun y -> x+y) | Mult -> (fun x -> fun y -> x*y) | Sub -> (fun x -> fun y -> x-y) | Div -> (fun x -> fun y -> x/y) let rec semProg p r = match p with ASTExp(e) -> semExp e r | ASTCst(x,e,p) -> semProg p (add_env x (semExp e r) r) and semExp e r = match e with ASTNum n -> semNum n | ASTId x -> r x | ASTApp(op, e1, e2) -> (semOp op) (semExp e1 r) (semExp e2 r) ;; if Array.length(Sys.argv) < 2 then output_string stderr "Usage: sem \n" else let ic = open_in Sys.argv.(1) in let lexbuf = Lexing.from_channel ic in let p = Parser.prog Lexer.token lexbuf in Format.printf"Eval = %d@." (semProg p empty_env) Exercice: une implantation plus réaliste des environnements J3- Lambda calcul (fin) Normalisation/évaluation substitution ~~ environnement Thm: si t -*-> u alors t[x:=v] -*-> u[x:=v] (avec x non libre dans v) si t -*->, il existe n tel que t -n-> u. Par récurrence sur n - si n=0, ie. t -0-> u, ie. t=u: on a bien t[x:=v] = u[x:=v] - sinon on peut exclure le cas où t est une variable on a n = n1+n2 avec n1 < n et n2 < n. Par cas restant sur t: - si t=\y.t1 -n1-> \y.u1 -n2-> u avec t1 -n1-> u1 et x<>y (tjrs possible) par HR: t1[x:=v] -n1-> u1[x:=v] par HR: (\y.u1)[x:=v] -n2-> u[x:=v] ie. \y.u1[x:=v] -n2-> u[x:=v] t[x:=v] = (\y.t1)[x:=v] = \y.t1[x:=v] -n1-> \y.u1[x:=v] -n2-> u[x:=v] - si t=(t1 t2) -n1-> (u1 t2) -n2-> u avec t1 -n1-> u1. par HR: (u1 t2)[x:=v] -n2-> u[x:=v] par HR: t1[x:=v] -n1-> u1[x:=v] t[x:=v] = (t1 t2)[x:=v] = (t1[x:=v] t2[x:=v]) = (t1[x:=v] t2[x:=v]) -n1-> (u1[x:=v] t2[x:=v]) = (u1 t2)[x:=v]) -n2-> u[x:=v] - si t=(t1 t2) -n1-> (t1 u2) -n2-> u avec t2 -n1-> u2. ~~idem - si t=(\y.t1 t2) --> t1[y:=t2] -(n-1)-> u avec y différent de x par HR: t1[y:=t2][x:=v] -(n-1)-> u[x:=v] (\y.t1 t2)[x:=v] = (\y.t1[x:=v] t2[x:=v]) --> t1[x:=v][y:=t2[x:=v]] --> t1[y:=t2[x:=v]][x:=v] (lem subst. x<>y) --> t1[y:=t2][x:=v] (lem subst.) donc t[x:=v] --> t1[y:=t2][x:=v] -(n-1)-> u[x:=v] Moralité: on peut retarder les substitutions ==> environnement Sémantique des lambda-termes Syntaxe Lam ::= ident | '(' Lam Lam ')' | '\' ident '.' Lam L: Lam -> Env -> Env avec Env = ident -> Lam L[[ x ]]r = r(x) L[[ (t u) ]]r = (L[[ t ]]r L[[u]]r) L[[(\x.t u)]]r = L[[ t ]](r[x:=L[[u]]r]) évaluateur des lambda-termes. Domaines Ensemble des valeurs: - des valeurs de bases - des opérateurs sur les ensembles - produit cartésien: A * B constr: (x,y) accés: fst(x,y) snd(x,y) - produit généralisé: A* avec A^0 = unit A* = unit U A U A * A U A * A * A U etc. - union disjointe: A + B constr: injections inA: A -> A + B inB: B -> A + B accés: projections outA: A + B -> A outB: A + B -> B recon: isA: A + B -> bool isB: A + B -> bool codage: A + B = {0}*A U {1}*B si A={a1, a2, ...} et B={b1, b2, ...} A+B={(0,a1), (1,b1), (0,a2), (1,b2), ...} - flèche fonctionnelle: A -> B (fonctions totales) A -> B inclus A*B tq pour tout (a,b) dans A -> B, on n'a pas (a,b') dans A -> B avec b<>b' (ie: image unique pour a) si f dans A -> B, A domaine et B codomaine de f - élément puit/erreur: un élément distingué #f ajout d'une valeur d'erreur: A U {#f} noté A# A -> B#: fonction partielle de A dans B si f dans A -> B#: domaine = { a dans A | f(a) <> #f } Unions disjointes/types sommes soit A + B si x in A + B alors ou bien isA(x) est vrai et il existe a dans A tq x = inA(a) et outA(x) = a ou bien isB(x) est vrai et il existe b dans B tq x = inB(b) et outB(x) = b pptes algébriques isA(inA(a)) est vrai et outA(inA(a)) = a isB(inB(x)) est vrai et outB(inB(b)) = b retrouver la valeur de x dans A + B si isA(x) alors outA(x) sinon outB(x) syntaxe à la ML case x: inA(a) -> a | inB(b) -> b Abus: on étendra la syntxe du filtrage à la ML au cas #f case x: inA(a) -> e1 | inB(b) -> e2 | #f -> e3 Sémantique revisitée (avec fonctions): Environnement: Env = Ident -> Val avec Val = Data + Fun Types de base: Data = Z (inData, isData) Fermetures: Fun = Data* -> Data inData: Data -> Val inFun: (Data* -> Data) -> Val Fonctions de gestion de l'environnement getEnv : Ident -> Env -> Val# getEnv x r == r(x) setEnv : Ident -> Val -> Env -> Env setEnv x v r == r[x:=v] D: Dec -> Env -> Env D[[ Cst x = e ]] r = setEnv x inData(E[[e]]r) r D[[ Fun f(x1, ..) = e ]] = let c = \v1..(E[[e]] (setEnv x1 inData(v1) .. r)) in setEnv f inFun(c) r --> expliciter la construction de l'environnement d'appel ~~ compilation, empilement des valeurs d'appel Noter comment: l'environnement est capturé les noms sont capturés E: Exp -> Env -> (Data+Fun)# (fonction partielle) E[[x]] r = case (getEnv x r): inData(v) -> v | InFun() | #f -> #f E[[f(e1, ..)]] r = case (getEnv f r): inFun(c) -> c (E[[e1]]r) .. | inData(v) | #f -> #f J4- Liaison dynamique Pas d'environnement de définition Les definiens sont évalués dans leur environnement d'appel Val = (Env -> Data)+(Data* -> Env -> Data) avec inData: (Env -> Data) -> Val inFun: (Data* -> Env -> Data) -> Val noter les parenthèses -- arguments fonctionnels Grammaire Prog ::= Decs Exp Env = Ident -> Val# Noter: bonne fondation Env = Ident -> ((Env -> Data)+(Data* -> Env -> Data))# r0 = \x.#f setEnv: Ident -> Val -> Env -> Env getEnv: Ident -> Env -> Val P: Prog -> Data P[[ e ]] = E[[e]] r0 P[[ ds e ]] = E[[e]](Ds[[ds]]r0) DS: Decs -> Env -> Env Ds[[ d ds ]] r -> Ds[[ ds ]](D[[ d ]] r) Ds[[ d ]] r = D[[ d ]]r D: dec -> Env -> Env D[[ Cst x = e ]] r = setEnv x inData(E[[e]]) r D[[ Fun f(x1, ..) = e ]] r = setEnv f inFun(\v1.. \r'.E[[e]](setEnv x1 inData(v1) .. r')) r Noter application partielle/typage: E[[e]]: Env -> Data E: Exp -> Env -> Data# (fonction partielle) E[[x]] r = case (getEnv x r): inData(v) -> v r | InFun() | #f -> #f E[[f(e1, ..)]] r = case (getEnv f r): inFun(c) -> c (E[[e1]]r) .. r | inData() | #f -> #f Exercice: implanter le langage avec définition de fonction avec une implantation plus réaliste des environnement (si ocaml) a) liaison statique b) liaison dynamique si on a le temps Extension du langage: types + conditionnelle Ajout de booléens: B = {true, false} Data = Z + B => inInt, inBool ==> typage sur les données Lexique Mots clefs: 'true' 'false' 'if' 'and' 'or' 'not' Syntaxe Exp ::= IntExp | BoolExp IntExp ::= idem+ | 'if' '(' BoolExp ',' IntExp ',' IntExp ')' BoolExp ::= 'true' | 'false' | BoolExp 'and' BoolExp | BoolExp 'or' BoolExp | 'not' BoolExp | '(' BoolExp ')' Noter: comment on force le typage dans la grammaire (pas obligé) Rajouter des relations Lexique Symboles réservés: rel = {'=' '<>' '<' '> '<=' '>='} Syntaxe (exercice) BoolExp ::= idem+ | IntExp rel IntExp Sémantique O: Op -> (Data -> Data -> Z#) O[[ '+' ]] = \d1 \d2. case d1, d2: inInt(v1), inInt(v2) -> (v1 + v2) | _ -> #f etc. R[[ '<' ]] = \d1 \d2. case d1, d2: inInt(v1), inInt(v2) -> (v1 < v2) | _ -> #f etc. Nota: on aura inInt(#f) = inBool(#f) = #f E: Exp -> Env -> Data# E[[ n ]] r = inInt(N[[n]]) E[[ b ]] r = inBool(B[[b]]) avec b et B ce qu'on attend E[[ x ]] r = getEnv x r E[[ e1 op e2 ]] r = intInt(O[[op]] (E[[e1]]r) (E[[e2]]r)) E[[ e1 rel r2 ]] r = inBool(R[[rel]] (E[[e1]]r) (E[[e2]]r)) E[[ e1 'and' e2 ]] r = inBool((E[[e1]]r) & (E[[e2]]r)) etc. E[[ if(e, e1, e2) ]] r = case E[[e]] r: inBool(true) -> E[[e1]] r | inBool(false) -> E[[e2]] r | _ -> #f Nota: on aurait pu factoriser op/rel tuning syntaxe/sémantique Type/surcharge Une seule classe d'expressions + surcharge: '+' pour la disjonction '*' pour la conjonction '~' pour la négation Syntaxe Exp ::= | '~' Exp Sémantique O: Op -> (Data -> Data -> Data#) O[[ '+' ]] = \d1 \d2. case d1, d2: inInt(v1), inInt(v2) -> v1 + v2 | inBool(v1), inBool(v2) -> v1 & v2 | _ -> #f etc. ~~ vérification dynamique de type Point fixe et fonctions récursives Syntaxe: nouveau mot clef 'FunRec' Dec ::= ... | 'FunRec' ident '(' Prs ')' '=' Exp ';' Codage des définitions récursives/solutions d'équations récursives FunRec fac(n) = if (n = 0, 1, n * fac(n-1)); --> Y(\fac. \n.(if (= n 0) 1 (* n (fac (- n 1))))) en abrégé: !f.t == Y(\f.t) fac := !f.\n.(if (= n 0) 1 (* n (f (- n 1))))) Exercice: vérifier fac(0) <--> 1 fac(n+1) <--> n * fac(n) Sématique: D: Dec -> Env -> Env D[[ Fun f(x1, ..) = e ]] = let c = !f.\v1..(E[[e]] (setEnv x1 inData(v1) .. r)) in setEnv f inFun(c) r Impératif Séquence et affectation, puis alternative et boucle Valeurs modifiables: environnement dynamique Choix: - tout statique: exclus - tout dynamique: plus de constantes, y compris fonctions perte de transparence référentielle - statique + dynamique: choix: - un seul environnement avec liaisons différenciées (modifiable ou non) - deux environnements: choix: - séparation complète - indirection (valeur/adresse) Proposition 2.2.2: séquence + affectation Lexique: mot clef: 'Var' symbole réservé: ':=' Syntaxe: Prog ::= Decs Stat Decs ::= | Dec Decs Dec ::= | 'Var' ident '=' Exp ';' Stat ::= ident ':=' Exp ';' | Stat ';' Stat Nota: variante sans initialisation (exo) Sémantique: Domaine des valeurs: Val = Data + Fun + Adr Mémoire: Mem = Adr -> Data Mémoire vide: \a.#f Opérations: newMem : Data -> Mem -> Adr * Mem setMem : Adr -> Data -> Mem -> Mem getMem : Adr -> Mem -> Data# Axiome: si a,m' = newMem(d, m) alors getMem(a,m) = #f et getMem(a,m') = d Signatures sémantiques Un programme calcule une mémoire P: Prog -> Mem Les déclarations calculent un environnement et une mémoire D: Dec -> Env * Mem -> Env * Mem Les instruction calculent une mémoire S: Stat -> Env * Mem -> Mem Les expressions calculent une donnée en fonction d'un environnement et une mémoire E: Exp -> Env * Mem -> Data# Fonction sémantiques P[[ ds ss ]] = Ss[[ ss ]](Ds[[ ds ]](r0, m0)) Ds[[ d ds ]](r,m) = Ds[[ ds ]](D[[d]](r,m)) Ds[[ d ]](r,m) = D[[d]](r,m) D[[ 'Var' x '=' e ]](r,m) = let a, m' = newMem(E[[e]](r,m), m) in (setEnv x inAdr(a) r, m') S[[ s1 ';' s2 ]](r,m) = S[[s2]](r, S[[s1]](r,m)) S[[ x ':=' e ]](r,m) = case getEnv x r: inAdr(a) -> (setMem a (E[[e]](r,m)) m) | _ -> #f E[[ x ]](r,m) = case getEnv x r: inData(v) -> v | inAdr(a) -> getMem a m | _ -> #f Alternative Lexique: mots clef: 'if' 'then' 'else' symboles réservés : '{' '}' Syntaxe: Stat ::= ... | 'if' BoolExp 'then' Stat 'else' Stat | '{' Stat '}' Sémantique S[[ 'if' e 'then' s1 'else' s2 ]](r,m) = case E[[e]](r,m): inBool(true) -> S[[s1]](r,m) | inBool(false) -> S[[s2]](r,m) | _ -> #f Boucle Lexique: mots clef: 'while' 'do' Syntaxe Stat ::= ... | 'while' '(' BoolExp ')' 'do' Stat Sémantique S[[ 'while' '(' e ')' 'do' s ]](r,m) = (!w.\m'. case (E[[e]](r,m): inBool(true) -> w (S[[s]](r,m'))) | inBool(false) -> m' | _ -> #f) m) Justification: NB: on écrit (if e t1 t2) pour (case e: inBool(true)->t1 | inBool(fasle)->t2) \m.S[[ while e do s ]](r,m) '------------w------------' = \m.(if (E[[e]](r,m)) (S[[s; while e do s]](r,m)) m) = \m.(if (E[[e]](r,m)) (S[[while e do s]](r,S[[s]](r,m))) m) = \m.(if (E[[e]](r,m)) (\m'.[[while e do s]](r,m') S[[s]](r,m)) m '-----------w-------------' = !w.\m'.(if (E[[e]](r,m')) (w S[[s]](r,m')) m') J5 - Continuations Expliciter le flux de contrôle Intuition: pile d'instructions/commandes _ pile vide c:p commande c puis pile p S[[ s1 ';' s2 ]](p,r,m) = S[[ s1 ]](S[[s2]]:p, r, m) Noter: S[[s2]] : Stack -> Env -> Mem -> Mem S[[ x ':=' e ]](c:p, r, m) = c(p, r, setMem x (E[[e]](r,m)) m)) S[[ 'if' e1 'then' s1 'else' s2 ]](p,r,m) = case E[[e]](r,m): inBool(true) -> S[[ s1 ]](p, r, m) | inBool(false) -> S[[ s2 ]](p, r, m) | _ -> #f S[[ 'while' e 'do' s ]](c:p, r, m) = case E[[e]](r,m): inBool(true) -> S[[s]](S[['while' e 'do' s]]:p, r, m) | inBool(false) -> c(p, r, m) | _ -> #f Cas pile vide: on arrête là S[[ s ]](_, r, m) = m Faire de la pile une fonction: continuation Cont = Mem -> Mem (cf cas pile vide) k: Cont S: Cont -> Env -> Mem -> Mem S[[ s1 ';' s2 ]](k, r, m) = [[ s1 ]](\m'.[[s2]](k,r,m'), r m) S[[ x ':=' e ]](k, r, m) = k (setMem x (E[[e]](r,m)) m)) S[[ 'if' e 'then' s1 'else' s2 ]](k, r, m) = case E[[e]](r,m): inBool(true) -> S[[ s1 ]](k, r, m) | inBool(false) -> S[[ s2 ]](k, r, m) | _ -> #f S[[ 'while' e 'do' s ]](k, r, m) = case E[[e]](r,m): inBool(true) -> S[[s]](\m'.S[['while' e 'do' s]](k,r,m'), r, m) | inBool(false) -> (k m) | _ -> #f Point fixe: \m.S[[ 'while' e 'do' s ]](k,r,m) '---------------k_w---------------' S[[ 'while' e 'do' s ]](k, r, m) = (!k'.\m'. (case E[[e]](r,m'): inBool(true) -> S[[s]](k', r, m') | inBool(false) -> (k m') | _ -> #f) m) Pile vide: la continuation qui s'arrête :) k0 = \m.m Exos: un 'switch' Exemple (schématiquement) on écrit True pour inBool(true) et False pour inBool(false) Soit le programme [[ x:=1; while (x=1) do x:=0 ]] l'environnement r tel que r(x) = a la mémoire m S[[ x:=1; while (x=1) do x:=0 ]](k0, r, m) = S[[ x:=1 ]](\m'.S[[while (x=1) do x:=0 ]](k0, r, m'), r, m) = (\m'.S[[while (x=1) do x:=0 ]](k0, r, m') m1) avec m1(a) = 1 = S[[while (x=1) do x:=0 ]](k0, r, m1) = (!k'.\m'.case E[[x=1]](r,m'): True -> [[x:=0]](k',r,m') | False -> k0(m') m1) posons K = !k'.\m'.case E[[x=1]](r,m'): True -> [[x:=0]](k',r,m') | False -> k0(m') (K m1) = case E[[x=1]](r,m1): True -> [[x:=0]](K,r,m1) | False -> (k0 m1) = [[x:=0]](K,r,m1) car m1(a) = 1 = (K m2) avec m2(a) = 0 = case E[[x=1]](r,m2): True -> [[x:=0]](K,r,m2) | False -> (k0 m2) = (k0 m2) car m1(a) = 0 Rupture et continuation 'try' s1 'with' x 'do' s2 Associer une continuation à un nom Continuation = fonction = valeur ==> continuation dans l'environnement Val = Data + Fun + Adr + Cont Provoquer la rupture: 'raise' x Equations sémantiques: S[[ 'try' s1 'with' x 'do' s2 ]](k, r, m) = S[[ s1 ]](k, (setEnv x inCont(\m'.[[s2]](k,r,m')) r), m) S[[ 'raise' x ]](k, r, m) = case (getEnv x r): inCont(c) -> (c m) | _ -> #f J++ Langage à objets (tentative) Classe/instance == champs + méthodes champ = nom+donnée (valeur immédiate) méthode = nom+fonction (valeur fonctionnelle) ==> Classe == suite d'associations nom/valeur **environnement** Les environnements deviennent des valeurs Val += Env Déclaration de classe, sémantique 1 D[[ 'Class' c ds ]]r = setEnv x inEnv(Ds[[ ds ]]r) r Instance: quelque chose qui attend des méthodes **fonction** Inst = Ident -> Val Création d'instance, sémantique 1 E: Expr -> Env -> Data|Inst E[[ 'New' c ]]r = case getEnv c r: inEnv(r') -> inInst(\f. getEnv f r') | _ -> #f Appel de méthode: ~ application avec m: Ident E[[ o '.' m ]]r = case E[[ o ]]r: inInst(i) -> i m | _ -> #f Défaut: liaison statique: - ordre de définition des champs/méthodes Ca interdit Class c = x = y+1; y = 3; en revanche y = 23 Class c = x = y+1; y = 3; (New c).x --> 24 (New c).y --> 3 Liaison dynamique "Valeurs dynamiques" DData = Env -> Data DFun = Env -> Data* -> Data Val += DData + DFun DD : Dec -> Env -> Env -> Env DD[[ 'Cst' x '=' e ]]r ri= setEnv x inDData(\r'.E[[e]]r'@ri) avec getEnv x (r'@ri) == getEnv x r' si défini getEnv x ri sinon DD[[ 'Fun' f '(' x1 .. ')' '=' e ]]r ri = let c = \r'.\v1 .. E[[ e ]](setEnv x1 v1 .. (r'@ri))) in setEnv f inDFun(c) r Déclaration de classe: sémantique 2 D[[ 'Class' c ds ]]r = setEnv c inEnv(DDs[[ ds ]] r0 r) r Création d'instance, sémantique 2 (inchangé) E[[ 'New' c ]]r = case getEnv c r: inEnv(r') -> inInst(\f. getEnv f r') | _ -> #f Appel de méthode; sémantique 2 E[[ o '.' m ]]r = case E[[ o ]]r: inInst(i) -> ( case (i m): inDData(d) -> d i |inDFun(f) -> f i ) | _ -> #f On a avec Class c = Cst x = y+1; Cst y = 3. (New c).x --> 4 même si y = 23 Class c = x = y+1; y = 3. (New c).x --> 4 "Default is 'this'" Héritage: redéfinition ou extension D[[ 'Class' c c' ds ]]r = case getEnv c' r: inEnv(r') -> setEnv c inEnv(DDs[[ ds ]] r' r) r | _ -> #f et c'est tout. ==> liaison retardée m définie dans c' est masquée par m redéfinie dans c Comment faire ? y = 23 Class c = x = y + this.y; y = 3. Que 'this' existe Déclaration de classe: sémantique 2.0 D[[ 'Class' c ds ]]r = let rec r' = DDs[[ ds ]] (setEnv 'this' inInst(\f.getEnf f r') r0) r in inEnv c inEnv(r') c'est-à-dire D[[ 'Class' c ds ]]r = let r' = !r'.DDs[[ ds ]] (setEnv 'this' inInst(\f.getEnf f r') r0) r in inEnv c inEnv(r') on rajoute E[[ 'this' ]]r = inInst(i) -> i