CONCEPTION DE LANGAGE
                        ---------------------

                      Sémantique dénotationnelle

J1 -

	Langage de programmation

                  |
          syntaxe | sémantique
             ------------>
	          |
Interprétation: expression -> valeur          
(Evaluation, Exécution, Calcul)

Expression booléennes:

 lexique:
	{ 'true', 'false', '!', '&&', '||' }

 grammaire:
	BoolExp ::= 'true' 
		|   'false' 
		|   '!' BoolExp 
		|   BoolExp '&&' BoolExp 
		|   BoolExp '||' BoolExp

Domaine de valeurs

	 Val = {0, 1} (sous ensemble de N)

Fonction sémantique:

	 B: BoolExp -> Val

	 B[[ 'true' ]]     = 1
	 B[[ 'false' ]]    = 0
	 B[[ '!' b ]]      = 1 - B[[ b ]]
	 B[[ b1 '&&' b2 ]] = min(B[[ b1 ]], B[[ b2 ]])
	 B[[ b1 '||' b2 ]] = max(B[[ b1 ]], B[[ b2 ]])

Ajout des variables

 on se donne: X ens. de noms de variables

 on rajoute à la grammaire

    	BoolExp ::= ...
		|   X

 une variable en elle-même n'a pas de valeur: on se donne des environnements

 Env = X -> Val ensemble de fonctions de X dans Val

 Mais, il se peut qu'une variable n'aie pas de valeur: fonction partielle
 Mais la sémantique dénotationnelle n'aime pas les fonctions partielles:
 une valeur distinguée pour le 'non défini' #f (pour 'bottom')

 Val = {0, 1} U { #f }  ou Val = {0, 1} et Val# = {0, 1} U { #f }

 Env = X -> Val#

       	 B: BoolExp -> Env -> Val#

	 B[[ x ]]r          = r(x)
	 B[[ 'true' ]]r     = 1
	 B[[ 'false' ]]r    = 0
	 B[[ '!' b ]]r      = 1 - B[[ b ]]r
	 B[[ b1 '&&' b2 ]]r = min(B[[ b1 ]]r, B[[ b2 ]]r)
	 B[[ b1 '||' b2 ]]r = max(B[[ b1 ]]r, B[[ b2 ]]r)

NB: les opérations arithmétiques -, min et max doivent être étendue
    à la présence de #f: fonctions *strictes*
      #f - n = #f
      n - #f = #f
      min(#f, n) = #f
      max(n, #f) = #f
	    
Déclarations de constantes

 création d'environnement

  Env. vide : r0 = \x.#f
  Ajout d'une valeur: r[x:=v] tq
  	r[x:=v](x) = v
	r[x:=v](y) = r(y)  si x <> y

  lexique: { ..., 'Cste', '=', ';' }

  extension de la grammaire (nouvelles règles/non terminaux)
	BoolExp ::= ... 
        Dec ::= 'Cste' x '=' b ';'
	Decs ::= Decs Dec | Dec
	Prog ::= Decs BoolExp | BoolExp

 Nouvelles fonctions sémantiques

    D: Dec -> Env -> Env
    Ds : Decs -> Env
    P : Prog -> Val#
    
    P[[ b ]] = B[[ b ]]r0
    P[[ ds b ]] = B[[ b ]](Ds[[ ds ]])
    Ds[[ d ]] = D[[ d ]]r0
    Ds[[ ds d ]] = D[[ d ]](Ds[[ ds ]])
    D[[ 'Cste' x '=' b ';' ]]r = r[[ x := B[[ b ]]r ]] 

Expressions arithmétiques

    lexique:
	{ ..., '+', '*', '-', '/' }
	U NumCst = les constantes numériques (notation décimale)
	  == expressions régulières: '-'?['0'..'9']+

    grammaire:
	ArExp ::= X
	       |   ArExp '+' ArExp
	       |   ArExp '*' ArExp

 Domaine (1): on étend à l'ensemble des valeurs numériques (entières)

    Val = Z (entiers relatifs)

 Fonctions sémantiques

    VN: NumCst -> Val

    VN[[ n ]] non spécifié...

    A : ArExp -> Env -> Val#

    A[[ x ]]r = r(x)
    A[[ n ]]r = VN[[ n ]]
    A[[ a1 '+' a2 ]]r = A[[ a1 ]]r + A[[ a2 ]]r
    A[[ a1 '*' a2 ]]r = A[[ a1 ]]r x A[[ a2 ]]r
    A[[ a1 '-' a2 ]]r = A[[ a1 ]]r - A[[ a2 ]]r
    A[[ a1 '/' a2 ]]r = A[[ a1 ]]r / A[[ a2 ]]r
    
    D[[ 'Cste' x '=' a ';' ]]r = r[ x := A[[ a ]]r ]

    P[[ a ]] = A[[ a ]]r0
    P[[ ds a ]] = A[[ a ]](Ds[[ ds ]])

 Critique: quid des programmes ?

	Cste x = 5; !x
 	Cste x = 5; !(x+1)
 	Cste x = 5; Cste y = x; y+1
	x

   P[[ Cste x = 5; !x ]]
       = B[[ !x ]](r0[x:=5])
       = 1 - B[[ x ]](r0[x:=5])
       = 1 - 5
       = 4

   P[[ Cste x = 5; !(x+1) ]] 
       = B[[ !(x+1) ]](r0[x:=5])
       = 1 - B[[ x+1 ]](r0[x:=5])
       = ???

   P[[ Cste x = 5; Cste y = x; y+1 ]]
       = A[[ y+1 ]](DS[[ Cste x = 5; Cste y = x; ]])
       = A[[ y+1 ]](D[[ Cste y = x ]](DS[[ Cste x = 5 ]])
       = A[[ y+1 ]](r0[ x := 5][ y := ???[[ x ]]r0[ y := 5 ]])

   P[[ x ]]
       = ???[[ x ]]r0

 Typer

  Différencier 2 sous-ensembles disjoints de valeur.
  Union disjointe: Val = {0,1} + Z = ({1} x {0,1}) U ({2} x Z)

   Injection: inB : {0,1} -> Val
   	      inN : Z -> Val
   Projection: outB : Val -> {0,1}#
   	       outN : Val -> Z#

	outB(inB(x)) = x
	outB(inN(x)) = #f
	outN(inB(x)) = #f
	outN(inN(x)) = x

  Un seul ensemble d'expressions:

     Exp ::= BoolExp | ArExp

  Typer les opérateurs:
     lexique: Op1 = { '!' }
     	      Op2 = { '&&', '||', '+', '*', '-', '/' }

     fonctions sémantiques pour les opérateurs:

     O1: Op1 -> Val -> Val 
     O2: Op2 -> Val -> Val -> Val

     O1[[ '!' ]](x) = inB(1-b), si x=inB(b)
     	      	    = #f,	sinon

     notation 'ML-ienne':
     O1[[ '!' ]] =
        \x. case x:
	      inB(b) -> inB(1 - b)
	    | _ -> #f
    
     O2[[ '&&' ]] =
     	\x \y. case x,y:
	         inB(b1), inB(b2) -> inB(max(b1, b2))
	       | _ -> #f

     O2[[ '||' ]] =
     	\x \y. case x,y:
	         inB(b1), inB(b2) -> inB(min(b1, b2))
	       | _ -> #f

     O2[[ '+' ]] =
     	\x \y. case x,y:
	         inN(n1), inN(n2) -> inN(n1 + n2)
	       | _ -> #f

     O2[[ '*' ]] =
     	\x \y. case x,y:
	         inN(n1), inN(n2) -> inN(n1 x n2)
	       | _ -> #f

     O2[[ '-' ]] =
     	\x \y. case x,y:
	         inN(n1), inN(n2) -> inN(n1 - n2)
	       | _ -> #f

     O2[[ '/' ]] =
     	\x \y. case x,y:
	         inN(n1), inN(n2) -> inN(n1 / n2)
	       | _ -> #f

   Fonction sémantique pour les expressions:

     Exp = BoolExp U ArExp

     E: Exp -> Env -> Val

     E[[ x ]]r = r(x)

     E[[ 'true' ]]r     = inB(1)
     E[[ 'false' ]]r    = inB(0)
     E[[ '!' b ]]r      = O1[[ '!' ]] (E[[ b ]]r)
     E[[ e1 '&&' e2 ]]r = O2[[ '&&' ]] (E[[ e1 ]]r) (E[[ e2 ]]r)
     E[[ e1 '||' e2 ]]r = O2[[ '||' ]] (E[[ e1 ]]r) (E[[ e2 ]]r)

     VN[[ n ]] = inN(n)

     E[[ n ]]r = VN[[ n ]]
     E[[ e1 '+' e2 ]]r = O2[[ '+' ]] (E[[ e1 ]]r) (E[[ e2 ]]r)
     E[[ e1 '*' e2 ]]r = O2[[ '*' ]] (E[[ e1 ]]r) (E[[ e2 ]]r)
     E[[ e1 '-' e2 ]]r = O2[[ '-' ]] (E[[ e1 ]]r) (E[[ e2 ]]r)
     E[[ e1 '/' e2 ]]r = O2[[ '/' ]] (E[[ e1 ]]r) (E[[ e2 ]]r


   Revue des programmes
	Cste x = 5; !x
 	Cste x = 5; !(x+1)
 	Cste x = 5; Cste y = x; y+1
	x

   P[[ Cste x = 5; !x ]]
       = E[[ !x ]](r0[ x := (E[[ 5 ]]r0)])
       = E[[ !x ]](r0[ x := VN[[ 5 ]] ])
       = E[[ !x ]](r0[ x := inN(5)])
       = O1[[ '!' ]] (E[[ x ]](r0[x:=inN(5)]))
       = O1[[ '!' ]] (r[x:=inN(5)](x))
       - O1[[ '!' ]] (inN(5))
       = #f

   P[[ Cste x = 5; !(x+1) ]] 
       = E[[ !(x+1) ]](r0[x:=inN(5)])
       = O1[[ '!' ]] (E[[ x+1 ]](r0[x:=inN(5)]))
       = O1[[ '!' ]] 
       	    (O2[[ '+' ]] 
	       (E[[ x ]](r0[x:=inN(5)])) 
	       (E[[ 1 ]](r0[x:=inN(5)])))
       = O1[[ '!' ]] (O2[[ '+' ]] (inN(5)) (inN(1)))
       = O1[[ '!' ]] (inN(6))
       = #f

   P[[ Cste x = 5; Cste y = x; y+1 ]]
       = E[[ y+1 ]](DS[[ Cste x = 5; Cste y = x; ]])
       = E[[ y+1 ]](D[[ Cste y = x ]](DS[[ Cste x = 5 ]]))
       = E[[ y+1 ]](D[[ Cste y = x ]](D[[ Cste x = 5 ]]r0))
       = E[[ y+1 ]](D[[ Cste y = x ]](r0[ x := inN(5)])
       = E[[ y+1 ]](r0[ x := inN(5)][ y := E[[ x ]]r0[ x := inN(5) ]])
       = E[[ y+1 ]](r0[ x := inN(5)][ y := (r0[ x := inN(5) ](x)) ])
       = E[[ y+1 ]](r0[ x := inN(5)][ y := inN(5) ])
       = O2[[ '+' ]] 
       	    (E[[ y ]](r0[ x := inN(5)][ y := inN(5) ]))
	    (E[[ 1 ]](r0[ x := inN(5)][ y := inN(5) ]))
       = O2[[ '+' ]] (inN(5)) (inN(1))
       = inN(6)

   P[[ x ]]
       = E[[ x ]]r0
       = #f

Déclarations de fonctions

  lexique: { ..., ',' , 'Fun' }

  grammaire:

  Dec ::= ...
      | 'Fun' f '(' x1 ',' .. ')' '=' Exp ';'

  Exp ::= ...
      | f '(' e1, .. ')'

   où f, x1, ... sont des identificateurs

  domaine: un domaine fonctionnel: 

  	   F = Val* -> Val

  avec Val* = Val U Val x Val U Val x Val x Val U ...
       	    = U_n Val^n

  Fonctions sémantiques

  D[[ 'Fun' f '(' x1, .. ')' '=' e ]]r 
    = r[f := inF(\v1 .. E[[ e ]](r[x1 := v1, ..]))]

  E[[ f '(' e1, .. ')' ]]r
    = case r(f):
        inF(c) -> (c (E[[ e1 ]]r) ...)
      | _ -> #f	

Structure de contrôle: alternative

  lexique: { ..., 'if' }
  syntaxe:

     Exp ::= ...
     	 |   '(' 'if' BoolExp Exp Exp ')'

  Equation sémantique:

  E[[ '(' 'if' e1 e2 e3 ')' ]]r
    = case E[[e1]]r:
        inB(1) -> E[[e2]]r
      | inB(0) -> E[[e3]]r
      | _ -> #f	

J2 - 
Fonctions récursives

  Combinateur de point fixe: !f.t --> t[!f.t/f]

  Intuitivement:
  fac(n) = 1,		 si n=0
  	 = n * fac(n-1), sinon

  FAC = !f \n . (if (n=0) 1 (n * (f (n-1))))

  Réduction gauche: (!f.t u) --> (t[!f.t/f] u)

  (FAC 0) --> (\n . (if (n=0) 1 (n * (FAC (n-1)))) 0)
       	  --> (if (0=0) 1 (0 * (FAC (0-1))))
	  --> 1

  (FAC 1) --> (\n . (if (n=0) 1 (n * (FAC (n-1)))) 1)
       	  --> (if (1=0) 1 (1 * (FAC (1-1))))
	  --> (1 * (FAC 0))
	  --> (1 * 1)
	  --> 1
             
  Le combinateur de point fixe donne un moyen effectif de calculer
  le *point fixe* d'un opérateur sur les fonctions/ensembles.

  Rappel: du point de vue dénotationnelle, fonction(unaire) = ensemble
  de couples.

  Par exemple: \x. 2x+3 = {(n,m) | m=2n+3}

       	       FAC = {(n,m) | ((n=0) et (m=1))
	       	      	      ou ((n>0) et 
			          Ex m'.(n-1,m') elt FAC et m=n*m')}
	           = {(0,1)}
		     U {(n,m) | n>0 et Ex m'. (n-1,m') elt FAC et m=n*m'}
 
   FAC: Val -> Val, on cherche un opérateur Y:(Val->Val) -> (Val -> Val)
   	qui
		- permette le calcul par approximations successives de FAC

		Y(FAC) = {(0,1)}
		       	 U {(n,m) | n>0 et 
			   	    Ex m'. (n-1,m') elt FAC et m=n*m'}
 
		- aboutit, in fine à FAC = Y(FAC)

   Approximations:
	FAC0 = {(0,1)}

	FAC1 = Y(FAC0)
	     = {(0,1)}
		U {(n,m) | n>0 et Ex m'. (n-1,m') elt FAC0 et m=n*m'}
            
	    en utilisant (0,1) elt FAC0, (n-1,m')=(0,1) donne
	    m'=1 et n=1. D'où

	FAC1 = {(0,1); (1,1)}
	
	FACi+1 = Y(FACi)
	       = Y(Y(.... Y(FAC0) ...))

	On a FAC0 inclus FAC1 ... FACi inclus FACi+1 ...

	On pose FAC = U_i FACi
	On a que FAC est un point fixe de Y: FAC = Y(FAC)

	(n,m) elt FAC ssi (n,m) elt U_i FACi
	      	      ssi (n,m) elt FACi, pour un certain i
        - si (n,m) elt FAC0, alors (n,m)=(0,1) et
	  (0,1) elt FAC et (0,1) elt Y(FAC)
	- sinon:
	  (n,m) elt FACi+1 
	  	ssi (n,m) elt Y(FACi)
	  	ssi (n,m) elt {(0,1)}
			      U {(n,m) | n>0 et 
					 Ex m'. (n-1,m') elt FACi et m=n*m'}
	  	ssi (n,m) elt {(0,1)}
			      U {(n,m) | n>0 et 
					 Ex m'. (n-1,m') elt U_i FACi et m=n*m'}
	  	ssi (n,m) elt {(0,1)}
			      U {(n,m) | n>0 et 
					 Ex m'. (n-1,m') elt FAC et m=n*m'}
	  	ssi (n,m) elt Y(FAC)					 

   Le combinateur de point fixe en lambda-calcul:

      Y = \f.(\x.(f (x x)) \x.(f (x x)))

    on vérifie (Y t) <--> (t (Y t)) (EXERCICE)

      (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))

     En particulier: (Y \f.t) <--> (\f.t (Y \f.t))
                              -->  t[(Y \f.t)/f]
     en posant !f.t = (Y \f.t), on retrouve !f.t --> t[!f.t/f]

  Lexique et syntaxe;

   lexique: { ..., 'FunRec' }

   grammaire:

     Dec ::= ...
     	 |   'FunRec' f '(' x1 ',' ...')' '=' Exp ';'

  Equation sémantique des définitions récursives:

     D[[ 'FunRec' f '(' x1 ',' ...')' '=' Exp ]]r
       = r[ f := inF(!w.\v1 .. E[[ e ]]r[ f := inF(w), x1 := v1 ...])]

Impératif: bouleversement

  variables, affectation, séquence, bloc, alternative et boucle

  choix: conserver un langage d'expressions 
  	 ou distinguer expressions/instructions

  mon choix: distinguer, une expression calcule une valeur, une instruction
      	     produit un effet, modifie un état

  lexique: { ..., 'Var', ':=', 'else', 'while', '{', '}' }

  grammaire: 

  Prog ::= Decs Stat

  Dec ::= ...
      |	  'Var' x '=' Exp ';'

  Stat ::= x ':=' Exp
       |   '{' Stats '}'
       |   'if' '(' BoolExp ')' Stat 'else' Stat
       |   'while' '(' BoolExp ')' Stat
  Stats ::= Stat
  	|   Stat ';' Stats

  Domaines sémantiques

    état modifié == état mémoire ==> modéliser la mémoire

    Adr: ensemble d'adresses (infini abstrait)

    Données en mémoires: Data = B + N  (B={0,1} et N = Z)
      on pose : inD(x) = inB(x) ou inN(x)

    Mem = Adr -> Data# 	 (partielle)

    Opérations sur la mémoire: m

     mémoire vide: m0 = \a.#f

     accès: m(a)

     modification: m[a := d] 

     allocation: 
        new : Mem -> Adr

	Axiome: m(new(m)) = #f

    Val = B + N + Fun + Adr

    	avec inA, outA, isA

   Fonctions sémantiques (signatures et équations)

   Un programme calcule une mémoire
     P: Prog -> Mem

    Les déclarations calculent un environnement et une mémoire
     Ds : Decs -> Env * Mem
     D: Dec -> Env * Mem -> Env * Mem

    Les instructions calculent une mémoire
     S: Stat -> Env * Mem -> Mem 

    Les expressions calculent une donnée (valeur) en fonction 
    d'un environnement et d'une mémoire
     E: Exp -> Env * Mem -> Data#
 
(J3)

   Equations:

    P[[ ds s ]] = S[[ s ]](Ds[[ ds ]])

    Ds[[ d ]] = D[[ d ]](r0,m0)
    Ds[[ ds d ]] = D[[ d ]](Ds[[ ds]])

    D[[ 'Cst' x '=' e ]](r,m)
      = (r[ x := E[[ e ]](r,m) ], m)

    D[[ 'Fun' f '(' x1 .. ')' '=' e ]](r,m)
      = (r[ f := inF(\m'\v1 .. E[[ e ]](r[x1:=v1,..], m')) ], m)

    D[[ 'Var' x '=' e ]](r,m) 
      = let a = new(m) in
      	  ( r[x := inA(a)], m[a := E[[ e ]](r,m) )

    E[[ x ]](r,m) =
      case r(x):
        inA(a) -> m(a)
      | v -> v

    E[[ f '(' e1 ..')' ]](r,m) =
      case r(f):
        inF(c) -> c m (E[[e1]](r,m)) ..
      | _ -> #f

    Ss[[ s ';' ss ]](r,m)
      = Ss[[ ss ]](r, S[[ s ]](r,m))

    Ss[[ s ]](r,m) = S[[ s ]](r,m)

    S[[ '{' ss '}' ]](r,m) = Ss[[ ss ]](r,m)

    S[[ x ':=' e ]](r,m) 
      = case r(x):
          inA(a) -> m[ a := E[[ e ]](r,m) ]
	| _ -> #f

    S[[ 'if' '(' e ')' s1 'else s2 ]](r,m)
      = case E[[ e ]](r,m):
          inB(1) -> S[[ s1 ]](r,m)
	| inB(0) -> S[[ s2 ]](r,m)  
	| _ -> #f
      
   Le cas de la boucle:

    S[[ 'while' '(' e ')' s ]](r,m)
      == case E[[ e ]](r,m):
           inB(0) -> m
	 | inB(1) -> S[[ s ';' 'while' '(' e ')' s ]](r,m)
	 | _ -> #f

    Définition récursive infinie f(x) = ...f(x)...

    à s et r donnés, \m S[[s]](r,m): Mem -> Mem

    Définition récursive:

    \m.S[[ while '(' e ')' s ]](r,m)
    '----------------w-------------' 

      = \m.(if (E[[e]](r,m)) (S[[s; while '(' e ')' s]](r,m)) m)


      = \m.(if (E[[e]](r,m)) (S[[while '(' e ')' s]](r,S[[s]](r,m))) m)


      = \m.(if (E[[e]](r,m)) (\m'.[[while '(' e ')' s]](r,m') S[[s]](r,m)) m
                              '--------------w--------------' 

      = !w.\m'.(if (E[[e]](r,m')) (w S[[s]](r,m')) m') 

    d'où

    S[[ 'while' '(' e ')' s ]](r,m)
      = (!w.\m'
            case E[[ e ]](r,m'):
              inB(0) -> m'
	    | inB(1) -> w (S[[ s ]](r,m'))
	    | _ -> #f
         m)

Procédures

 Nouvelle instruction: agit sur la mémoire

  Lexique : 'Proc', 'ProcRec'

  Grammaire : avec p,x1:X et e1:Expr

   Dec ::= ...
       | 'Proc' p '(' x1 ',' ..  ')' '=' Stat 
       | 'ProcRec' p '(' x1 ',' ..  ')' '=' Stat 

   Stat ::= ...
   	| p '(' e1 ','  ')' ';'

  Domaine

   P = Mem -> Val* -> Mem
   Val += P

  Equations

   D[[ 'Proc' p '(' x1, ..')' '=' s ]](r,m)
     = (r[ p := inP(\m' \v1 .. S[[s]](r[ x1 := v1, ..],m') ], m)

   D[[ 'ProcRec' p '(' x1, ..')' '=' s ]](r,m)
     = (r[ p := inP(!c.\m'.\v1 .. S[[s]](r[ p:=c, x1 := v1, ..],m') ], m)

   S[[ p '(' e1, .. ')' ]](r,m)
     = case r(p):
         inP(c) -> c m (E[[e1]](r,m)) ..
       | _ -> #f   

 Passage de paramètre ? (en exo)

  Proc incr(x) = { x := x+1 };
  Var n = 0;
    { incr(n) }

  P[[Proc incr(x) = { x := x+1 }; Var n = 0; incr(n) ]]
   = S[[ incr(n) ]](Ds[[ Proc incr(x) = { x := x+1 }; Var n = 0 ]](r0,m0))
   = S[[ incr(n) ]](D[[ Var n = 0]](D[[  Proc incr(x) = { x := x+1 } ]](r0,m0)))
   = S[[ incr(n) ]]
        (D[[ Var n = 0]](r[ incr := inP(\m\v.S[[x:=x+1]](r0[x:=v],m))],m))
   = let a = new(m) in
     let r1,m1 = 
       (r0[ incr := inP(..); n := inA(a)], m0[ n := inN(0)]) 
     in
       S[[ incr(n) ]](r1,m1)
   = (\m\v.S[[x:=x+1]](r0[x:=v],m)  m1  (E[[n]](r1,m1)))
   = (\m\v.S[[x:=x+1]](r0[x:=v],m)  m1  inN(0))
   = S[[ x:=x+1 ]](r0[x:=inN(0)], m1)
   = #f

 Par valeur !

 En l'état, les procédures ne savent que modifier l'état global accessible
 depuis leur environnement de définition.

 Passage par référence: expliciter ? (cf in out en ADA)

   lexique = { .., '@' }

   grammaire 

    Prm ::= '@'x | x

    Dec ::= ...
      'Proc' p '(' Prm1, .., Prmn ')' '=' Stat ]] 

   Fonctions sémantiques auxiliaires pour le traitement de paramètres 
   formels (prm)

    by : Prm -> Mem -> Val -> Val

    by[[ '@'x ]] m u =
       case u:
         inA(_) -> u
       | _ -> #f
      
    by[[ x ]] m u =
       case u:
         inA(a) -> m(a)
       | _ -> u

    nm : Prm -> X

    nm[[ '@' x ]] = x
    nm[[ x ]] = x

    W : Exp -> Env*Mem -> Val

    W[[ x ]](r,m)
     = case r(x):
         inA(_) -> r(x)
       | v -> v

    W[[ e ]](r,m) = E[[ e ]](r,m)	dans les autres cas
   
  Fonctions sémantiques (redéfinitions)
   
    D[[ 'Proc' p '(' prm1 ',' .. ')' '=' s ]](r,m)
      = r[p := inP(\m'.\(u1,..).S[[ s ]](r[(nm prm1) := (by prm1 m' u1) ..], m'))]

    S[[ p '(' e1, .. ')']](r,m)
      = case r(p):
      	  inP(c) -> c m (W[[e1](r,m)) ..
	| _ -> #f

 Exemple
      
  Proc incr( @x) = { x := x+1 };
  Var n = 0;
    { incr(n) }

  P[[Proc incr(@x) = { x := x+1 }; Var n = 0; incr(n) ]]
   = S[[ incr(n) ]](Ds[[ Proc incr(@x) = { x := x+1 }; Var n = 0 ]](r0,m0))
   = S[[ incr(n) ]](D[[ Var n = 0]](D[[  Proc incr(@x) = { x := x+1 } ]](r0,m0)))
   = S[[ incr(n) ]]
        (D[[ Var n = 0]]
	   (r[ incr := inP(\m'\v.S[[x:=x+1]](r0[(nm @x):=(by[[@x]] m' v)],m'))]
            ,m))
   = S[[ incr(n) ]]
        (D[[ Var n = 0]]
	   (r[ incr := inP(\m'\v.S[[x:=x+1]](r0[x:=(by[[@x]] m' v)],m'))],m))
   = let a = new(m0) in
     let r1,m1 = 
       (r0[ incr := inP(..); n := inA(a)], m0[ a := inN(0)]) 
     in
       S[[ incr(n) ]](r1,m1)
   = (\m\v.S[[x:=x+1]](r0[x:=(by[[@x]] m v)],m) m1 (W[[n]](r1,m1)))
   = (\m\v.S[[x:=x+1]](r0[x:=(by[[@x]] m v)],m) m1 inA(a))
   = S[[ x:=x+1 ]](r0[x:=(by[[@x]] m1 inA(a))], m1)
   = S[[ x:=x+1 ]](r0[x:=inA(a)], m1)
   = case r0[x:=inA(a)](x):
       inA(a) -> m1[ a := E[[ x+1 ]](r0[x:=inA(a)], m1) ]
     | _ -> #f
   = case inA(a):
       inA(a) -> m1[ a := E[[ x+1 ]](r0[x:=inA(a)], m1) ]
     | _ -> #f
   = m1[ a := E[[ x+1 ]](r0[x:=inA(a)], m1) ]
   = m1[ a := O2[[ '+' ]] 
     	      	 (E[[ x ]](r0[x:=inA(a)], m1) 
		 (E[[ 1 ]](r0[x:=inA(a)], m1) ]
   = m1[ a := O2[[ '+' ]] 
                 (E[[ x ]](r0[x:=inA(a)], m0[ a := inN(0)])
		 (E[[ 1 ]](r0[x:=inA(a)], m1) ]
   = m1[ a := O2[[ '+' ]] inN(0) inN(1) ]
   = m1[ a := inN(1) ]

 On peut alors voir que E[[ n ]](r1, m1[ a := inN(1) ]) = inN(1)

(J4)
Liaisons locales

 Déclarations suivies expression|instruction == programme local

   syntaxe

     Exp ::= ..
     	 |   '{' Decs Exp '}'

     Stat ::= ..
     	  |   '{' Decs Stats '}'

     Prog ::= Stat

   sémantique

     XDs: Decs -> (Env*Mem) -> (Env*Mem)
     
     XDs[[ d ]](r,m) = D[[ d ]](r,m)
     XDs[[ ds d ]] = D[[ d ]](Xds[[ ds ]](r,m))

     P[[ ds s ]] = S[[ s ]](XDs[[ ds ]](r0,m0))

     E[[ '{' ds e '}' ]](r,m)
       = E[[ e ]](XDs[[ ds ]](r,m))

     S[[ '{' ds ss '}' ]](r,m)
       = Ss[[ ss ]](XDs[[ ds ]](r,m))

   exemples

   Fun f(a,b,c) =
      { 
        Cst s = (a + b + c) / 2;
	Fun g(x) = s-x;
     	  s * g(a) * g(b) * g(c)
      }

   D[[ Fun f(a,b,c) = .. ]](r0,m0)
     = (r0[ f = inF(\m\v1\v2\v3.E[[ { .. } ]](r0[a:=v1; b:=v2; c:=v3], m)) ]
   E[[ { Cst s = (a+b+c)/2; .. } ]](r0[a:=v1; b:=v2; c:=v3], m)
     = E[[ s * g(a) * g(b) * g(c) ]]
        (XDs[[ Cst s = (a+b+c)/2; .. ]](r0[a:=v1; b:=v2; c:=v3], m))
     = E[[ s * g(a) * g(b) * g(c) ]]
        (D[[ Fun g(x) = s-x ]]
           (r0[ a:=v1; b:=v2; c:=v3; 
	        s:= E[[ (a+b+c)/2 ]](r0[a:=v1; b:=v2; c:=v3], m) ],
            m))
     =  E[[ s * g(a) * g(b) * g(c) ]]
          (r0[ a:=v1; b:=v2; c:=v3; 
	       s:= E[[ (a+b+c)/2 ]](r0[a:=v1; b:=v2; c:=v3], m),
	       g := inF(\m'\v.E[[ s-x ]]
                                (r0[a:=v1; ..; s:= E[[ ..]] ], m')) ],
           m)
 
  Remarque: les variable allouées localement persistent,
    est-ce gênant ?

    Var x = 0;
      {
       {
         Var x = 1;
	   x := x+1
       };
       x := x+1
      }

    P[[ Var x = 0; { Var x = 1; x:=x+1 }; x:=x+1 ]](r0,m0)
     = S[[ { Var x = 1; x:=x+1 }; x:=x+1 ]](r0[x=inA(a1)], m0[a1=inN(0)])
     = S[[ x:=x+1 ]](r0[x=inA(a1)],
                     S[[ { Var x = 1; x:=x+1 } ]](r0[x=inA(a1)],
		     	       	      	          m0[a1=inN(0)]))
     = S[[ x:=x+1 ]](r0[x=inA(a1)],
	   	     S[[ x:=x+1 ]](XDs[[ Var x = 1 ]](r0[x=inA(a1)],
		     	       	      	              m0[a1=inN(0)])))
     = S[[ x:=x+1 ]](r0[x=inA(a1)],
	   	     S[[ x:=x+1 ]](r0[x=inA(a1)][x=inA(a2)],
		     	           m0[a1=inN(0)][a2=inN(1)]))
     = S[[ x:=x+1 ]](r0[x=inA(a1)],
       	   	     m0[a1=inN(0)][a2=inN(1)]
			[a2=E[[ x+1 ]](r0[x=inA(a1)][x=inA(a2)],
                                       m0[a1=inN(0)][a2=inN(1)])])
     = S[[ x:=x+1 ]](r0[x=inA(a1)],
       	   	     m0[a1=inN(0)][a2=inN(1)][a2=inN(2)])
     = m0[a1=inN(0)][a2=inN(1)][a2=inN(2)]
          [a1=E[[x+1]](r0[x=inA(a1)],
                       m0[a1=inN(0)][a2=inN(1)][a2=inN(2)])
     = m0[a1=inN(0)][a2=inN(1)][a2=inN(2)][a1=inN(1)]
     

    comment faire mieux: désallouer ?

D'autres domaines, d'autres valeurs

 Type produit: A * B
 Paire: (a,b) elt A * B lorsque a elt A et b elt B
 Projections:
     fst(x,y) = x
     snd(x,y) = y

 Egalité:
   (a,b) = (a',b') ssi a=a' et b=b'
   
 Construction fonctionnelle des paires (lambda-calcul)
   (a,b) == \f.(f a b)
   fst = \c.(c \x.\y.x)
   snd = \c.(c \x.\y.y)

 Liste: structure séquentielle
  	produit homogène + nil (nouvelle constante)

 Un ensemble: A 

 A0 = { nil }
 An+1 = A * An

 A* = U_n An

 liste [1,2,3,4] == (1,(2,(3,(4,nil))))

 Remarque = A3 = (A * (A * A)) <> ((A * A) * A)

   lexique: { ..., 'nil', 'cons', 'car', 'cdr', 'null?' }

   Expr ::= ...
   	|   'cons' '(' Exp ',' Exp ')'
	|   'car' '(' Exp ')'
	|   'cdr' '(' Exp ')'
	|   'null?' '(' Exp ')'

 Domaines:
    List = (B + Z)*

    Val = ... + List	(avec inL, outL)

 liste [1,2,3,4] == inL(1,(2,(3,(4,nil))))

 Fonctions sémantiques: opérateurs prédéfinis

   O0: Op0 -> Val

   O0[[ 'nil' ]] = inL(nil)

   O1[[ 'null?' ]] = 
      \x. case x:
      	    inL(nil) -> inB(1)
          | _ -> inB(0)

   O1[[ 'car' ]] = 
   	\x. case x:
	      inL(v,_) -> v
	    | _ -> #f

   O2[[ 'cdr' ]] = 
   	\x. case x:
	      inL(_,v) -> v
	    | _ -> #f

   O2[[ 'cons' ]] = 
   	\x.\y.case y:
		inL(z) -> inL(x,z)
	      | _ -> #f

   Paires pointées:
   O2[[ 'cons' ]] = 
   	\x.\y.case y:
		inL(z) -> inL(x,z)
	      | _ -> inL(x,y)
        	
   E[[ 'nil' ]](r,m) = O0[[ 'nil' ]]
   E[[ 'null?' '(' e ')' ]](r,m)
     = O1[[ 'null?' ]] (E[[e]](r,m))
   etc.

 Plus de listes: les S-expressions

  Nil = {} (ensemble vide)

  atomes: A = B + Z + Nil  

  SX0 = A
  SX1 = SX0 * SX0
  SX2 = SX1 U (SX0 * SX1) U (SX1 * SX0)

  SXn+3 = U_(i,j < n+3) (SXi * SXj)

  SX = U_n SXn

  Pour discriminer atomes et paires:

    Listp = U_(n+1) SXn

    Val = A + Listp (injection: inL)

    avec le 'cons' des paires pointées  

Tableau: allocation statique

  Vecteur d'adresses consécutives
     => hypothèse sur le domaine des adresses:
     	relation de succession 

  asucc : Adr -> Adr

  new: N * Mem -> Adr

  Axiome:
	si a = new(n,m) alors pour i=0..n-1, asucc^i(a)=#f

   abréviation : assuc^i(a) == a+i, avec assuc^0(a) = a+0 = a

  Syntaxe:

  mot clef et symbole: '[' ']' 'Vec'

  grammaire

  Dec ::= ..
      |	  'Vec' x '[' n ']' ';'

  Exp ::= ..
      |	  x '[' Exp ']'

  Stat ::= ..
       |   x '[' Exp ']' ':=' Exp 

  Sémantique

  Initialiser les vecteurs à la création avec une valeur par
  défaut universelle: NULL 

  	 Val += { NULL }	( injection inU(NULL) ou simplement NULL)

  D[[ Vec x[n] ]](r,m)
    = case E[[n]](r,m):
        inN(n) -> let a = new(n,m) in
	  	    (r[x:=a], m[ a, .., asucc^(n-1) := NULL ])
      | _ -> #f

  E[[ x[e] ]](r,m)
    = case r(x), E[[e]](r,m):
        inA(a), inN(i) -> m(a+i)
      | _ -> #f

  S[[ x[e1] := e2 ]](r,m)
    = case r(x), E[[e1]](r,m):
        inA(a), inN(i) -> m[ a+i := E[[e2]](r,m) ]
      | _ -> #f

Exos:

 - comparateurs arithmétiques
 - fonctions anonymes (lambda)
   vérifier compatibilité
     Fun f(x) = x+1
     Fun f = fun x -> x+1
 - fonction d'arité variable
     Fun f(x..) = e