Module sem_ex

Syntaxe des programmes Un programme est ensemble de clauses gardées formées d'une garde et d'une suite d'affectations de termes à des variables

Les variables, constantes et symboles de fonctions binaires sont des paramètres abstraits

Variables var, cte, fun : Set.

Définition inductive des termes

Inductive term : Set :=
          Var : var -> term
        | Cte : cte -> term
        | Fun : fun -> term -> term -> term.

Une affectation multiple de termes à des variables, se représente comme une liste de couples formés d'une variable et d'un terme appelée une substitution

Definition substitution := (list (var * term)).

Une clause est formée d'une terme représentant la garde (vraie si elle ne s'évalue pas en 0) et d'une substitution

Definition clause := term * substitution.

Definition programme := (list clause).

Sémantique des programmes Les programmes sont interprétés comme des transformations sur les valuations qui représentent l'état de la mémoire

Une valuation est une interprétation des variables par des entiers

Definition valuation := var -> nat.

On se donne une interprétation des constantes et symboles de fonctions

Variable cte_sem : cte -> nat.
Variable fun_sem : fun -> nat -> nat -> nat.

Chaque expression représente un entier

Fixpoint term_sem [val:valuation;t:term] : nat
  := Cases t of
      (Var v) => (val v)
    | (Cte c) => (cte_sem c)
    | (Fun f t1 t2) => (fun_sem f (term_sem val t1) (term_sem val t2))
      end.

Une substitution definit une transformation sur les valuations. La sémantique d'une substitution est définie par récurrence sur la longueur de la substitution. Pour la construire il faut supposer que l'égalité est décidable sur les variables

Variable eq_var_dec : (v,v':var){v=v'}+{~v=v'}.

Cette propriété permet de definir des fonctions par cas sur l'égalité de deux variables : if (eq_var_dec v v') then [_]a else [_]b

Fixpoint aff_sem [val:valuation;aff:substitution] : valuation :=
 Cases aff of nil => [v:var](val v)
           | (cons (v',t) rest) =>
                [v:var]if (eq_var_dec v v') then [_](term_sem val t)
                       else [_](aff_sem val rest v)
 end.

Sémantique des clauses

Definition clause_sem : valuation -> clause -> valuation :=
   [val,c]let(g,aff)=c in
          if (zerob (term_sem val g)) then val else (aff_sem val aff).

La sémantique d'un programme est non déterministe par rapport à la clause qui sera exécutée et doit être représentée par une relation sur les valuations

Transition associée à une clause : la garde doit être vraie


Definition evolve : clause -> valuation -> valuation -> Prop
   := [c,val1,val2]
      let (g,aff) = c in (~(term_sem val1 g)=O /\ (aff_sem val1 aff)=val2).

Definition trans_prog : programme -> valuation -> valuation -> Prop
   := [prog,val1,val2](EX c:clause | (In c prog) & (evolve c val1 val2)).

End Abstract.