Semántica de un lenguaje
 
 Semántica de un mini-lenguaje El objetivo de esta lección es ilustrar con un ejemplo las funcionalidades del lenguaje de especificación Gallina asociado al cálculo de contrucciones inductivas e implementado en el Sistema de Prueba Coq desarrollado en el INRIA.
 
El ejemplo elegido trata de la semántica de un mini-lenguaje de programación imperativo (tipado, evaluación y semántica axiomática). Se proponen varias soluciones a la modelización de las diferentes nociones presentadas.
 

1  Introducción

Gallina es el nombre dado al lenguaje de especificación del sistema Coq (a Computer Aided Proof System). Permite definir: las definiciones que intervienen en la semántica de los lenguajes se representan particularmente bien en Gallina:

2  Presentación del problema

Nuestro lenguaje comprende los comandos siguientes, a partir de un conjunto de variables que denotaremos X :
                                    C ::=
  skip
| X:= E
| C1;C2
| if E then C1 else C2
| while E do C 
 
Figura 1: Sintáxis de los comandos
Las expresiones se forman a partir de enteros y boleanos simples con la sintáxis de la figura  2.

 
E ::=
  Xs Variables tipadas
| true |  false  Constantes boleanas
| E1 xor E2 O exclusivo
| n Constantes enteras
| null E Test de nulidad de enteros
| E1 op E2 Operación binaria sobre los enteros
 
s ::= nat | bool
op ::= + | - | * | ... 
 
Figura 2: Sintáxis de las expresiones
Se busca definir semánticas estáticas, operacionales naturales y axiomáticas para este lenguaje. Todas se representan en semántica natural por medio de la definición de una relación entre un programa y "valores"". Esta relación se describe con la ayuda de reglas de inferencia.

2.1  Semántica estática

Se trata de determinar de manera estática (sin ejecutarlo) que un programa está bien formado. Es preciso, por lo tanto, verificar que en las expresiones condicionales o de bucle, los tests se hacen sobre expresiones booleanas. Esto implica definir una relación de tipado sobre las expresiones. Los valores posibles serán de los dos tipos básicos   nat y bool.

La relación de tipado  E:s  se define por los axiomas y reglas de la figura 3.


Xs:s     true:bool     false:bool     n:nat
E1:bool   E2:bool
E1 xor E2:bool
 		  
E:nat
null E:bool
 		  
E1:nat   E2:nat
E1 op E2:nat
 
 
 
Figura 3: Semántica estática de las expresiones
Para los comandos, se define la relación  C: ok por las reglas de la figura  4.

skip: ok 
E:s
X:= E: ok
 		  
C1 : ok  C2 : ok
C1;C2: ok
 
 
E:bool  C1: ok  C2: ok
if E then C1 else C2: ok
 		  
E:bool  C: ok
while E do C:ok
 
 
 
Figura 4: Semántica estática de los comandos

2.2  Semántica operacional

La semántica operacional define el programa como una transformación del estado de la memoria. Esta memoria la veremos como una función que asocia a cada par formado por una variable y su tipo, un valor que será una constante entera  n o boleana b. Las dos operaciones sobre la memoria son la lectura y la actualización: si x es una variable y s un tipo, entonces m(x,s) representa el valor de la memoria para la variable  x  y el tipo s, si v es un valor, entonces m[x¬ v] representa la memoria donde la variable x ha sido actualizada al valor v. El tipo de la variable afectada no figura aquí explícitamente pero puede deducirse del tipo del valor  v.
Así pues:
(m[x¬ v])(x,s) = v.

Semántica de las expresiones

Se necesita una relación que asocie a cada memoria  m y expresión E un valor v que represente el resultado de la evaluación de E en la memoria m. Se denota esta relación
m |- E |> v
que podemos leer "en el estado m la expresión E  tiene el valor v".
    Se utilizarán constantes y funciones sobre el dominio de valores, que realicen las operaciones boleanas o artiméticas y las escribiremos en itálica utilizando el mismo identificador que en la sintáxis: así por ejemplo, a la construcción sintáctica xor le corresponderá la función semántica xor .

 
m|- Xs|>m(X,s)     m|- true|> true       m|- false|> false      m|- n|> n
m|- E1|> b1   m|- E2|> b2
m|- E1 xor E2|> b1 xor  b2
 		  
m|- E|> n
m|- null E |> null  n 
 		  
m|- E1|> n1   m|- E2|> n2
m|- E1 op E2|> n1 op  n2
 
 
 
Figura 5: Semántica de las expresiones

Semántica de los comandos

La relación
m |- C |> m'
expresa que el comando C se ejecuta en un estado m que se transforma en otro  m'. Esta relación se define por las reglas de inferencia de la figura  6.

m |- skip |> m 
m|- E |> v
m |- X:= E |> m[X¬ v]
 		  
m|- C1 |> m1   m1|- C2 |> m'
m|- C1 ; C2 |> m'
 
 
m|- E |> true    m|- C1|> m'
m|- if E then C1 else C2 |> m'
 		  
m|- E |> false    m|- C2|> m'
m|- if E then C1 else C2 |> m'
 
 
m|- E |> true    m|- C|> m1    m1|-while E do C |> m' 
m|- while E do C |> m'
 		  
m|- E |> false 
m|- while E do C |> m
 
 
 
Figure 6: Semática de los comandos

2.3  Semántica axiomática

Se trata de interpretar los comandos como transformaciones de predicados que especifican propiedades de la memoria o estado. Si P yQ son dos de tales predicados y C es un comando, entonces se define {P}C{Q} con la siguiente interpretación: la ejecución de C a partir de una memoria que satisface P conduce a una memoria que satisface Q.

La conjunción y la implicación de dos predicados se escribirán  P Ù Q y P Þ Q, si x es una variable y E una expresión, entonces  P[x¬ E] representa el predicado que a cualquier memoria  m le asocia  P(m[x¬ v]) donde v es el valor tal que m |- E |> v. Si w es un valor, entonces E=w representa el predicado que a todo m le asocia la propiedad v=w donde v es el valor tal que m |- E |> v.

La definición de esta relación está dada por las reglas de inferencia de la figura   7.


{P}skip{P}     {P[X¬ E]}X := E{P} 
{P}C1{P1}   {P1}C2{Q}
{P}C1 ; C2{Q}
 
 
{P Ù (E=true )}C1{Q}
{P}if E then C1 else C2{Q}
 		  
{P Ù (E=false )}C2{Q}
{P}if E then C1 else C2{Q}
 
 
{P Ù (E=true )}C{P}
{P}while E do C{ P Ù (E=false )}
 
 
P Þ P1    {P1}C{Q1}   Q1Þ Q
{P}C{Q}
 
 
 
Figure 7: Semántica axiomática de los comandos

2.4  Propiedades a demostrar

Entre las propiedades que interesa demostrar están:

3  Especificaciones en Gallina

Veamos ahora como se puede representar la teoría precedente en Gallina.

3.1  Las expresiones

Definiciones

Vamos a representar las variables y los operadores binarios por conjuntos paramétricos  que podrán instanciarse en una segunda etapa.  En cambio, las funciones boleanas se representan de manera concreta por un constructor de un tipo de datos. Esta elección permite ilustrar dos tratamientos posibles de los operadores del lenguaje que se trata de modelar.


Coq < Variable name : Set.
Variable name : Set.
Coq < Inductive sort : Set :=
      Sbool : sort | Snat : sort.
sort_ind is defined
sort_rec is defined
sort_rect is defined
sort is defined
Coq < Variable op : Set.
op is assumed
Coq < Inductive expr : Set :=
       Var   : name -> sort -> expr
     | Tr    : expr
     | Fa    : expr
     | Xor   : expr -> expr -> expr
     | Num   : nat  -> expr
     | Null  : expr -> expr
     | Opn   : op -> expr -> expr
               -> expr.
expr_ind is defined
expr_rec is defined
expr_rect is defined
expr is defined
 

Expresiones correctas

El predicado exprcorrect traduce la relación descrita en la figura 3. Cada regla de inferencia que define la relación se traduce en un constructor de la definición inductiva. Las variables libres de las definiciones aparecerán como variables cuantificadas universalmente en los constructores.

Coq < Inductive exprcorrect : sort -> expr -> Prop :=   
  corvar : (n:name)(s:sort)(exprcorrect s (Var n s))
 |cortr  : (exprcorrect Sbool Tr)
 |corfa  : (exprcorrect Sbool Fa)
 |corxor : (b,c:expr)(exprcorrect Sbool b)
                 ->(exprcorrect Sbool c)
                     ->(exprcorrect Sbool (Xor b c))
 |cornum : (n:nat)(exprcorrect Snat (Num n))
 |cornull: (e:expr)(exprcorrect Snat e)
                     ->(exprcorrect Sbool (Null e))
 |corop  : (o:op)(e,f:expr)(exprcorrect Snat e)
              ->(exprcorrect Snat f)
                ->(exprcorrect Snat (Opn o e f)).
exprcorrect_ind is defined
exprcorrect is defined
 
Coq < Check corxor.
corxor
     : (b,c:expr)
        (exprcorrect Sbool b)
         ->(exprcorrect Sbool c)->(exprcorrect Sbool (Xor b c))
 

Dominios Semánticos

Se trata de representar el dominio semántico de las variables. A cada tipo de variable le corresponde un conjunto en el sentido matemático, que se representa mediante un tipo de dato Coq, aquí, el tipo de los boleanos o de los enteros. El dominio semántico de los valores  semval se representa por la suma disjunta de los dos tipos.

Coq < Inductive semval : Set :=
       Bool : bool -> semval
     | Nat  : nat  -> semval.
semval_ind is defined
semval_rec is defined
semval_rect is defined
semval is defined
 

Interpretación de las funciones

Las funciones semánticas que corresponden a los operadores concretos pueden ser programadas explícitamente. En cambio, la semántica de las operaciones aritméticas (que se ven de manera paramétrica) debe pasarse como parámetro.

Coq < Definition boolxor : bool->bool->bool
    := [b1,b2]if b1 then if b2 then false else true else b2.
boolxor is defined

Coq < Eval Compute in (boolxor true false).
     = true
     : bool

Coq < Eval Compute in (boolxor true true).
     = false
     : bool

Coq <  Definition iszero : nat->bool
    := [n:nat]Cases n of O => true | (S n) => false end.
iszero is defined

Coq <   Variable semop : op->nat->nat->nat.
semop is assumed
 

Compatibilidad entre tipos y valores

Deberemos ligar la sort de las expresiones y el tipo de su interpretación semántica. Para ello, se define sort_val que es una función de los dominios semánticos en las clases, que a cada valor semántico le asocia la clase correspondiente.

Coq < Definition sort_val : semval -> sort
 := [v:semval]Cases v of (Bool b)=>Sbool
                    |(Nat n)=>Snat end.
sort_val is defined

Coq < Eval Simpl in (sort_val (Nat (S O))).
     = Snat
     : sort
 
Se utilizará igualmente una relación compat entre los valores y las clases, tal que  (compat Sbool  v) sea equivalente a  $ b:bool.v=(Bool b) (definida por el predicado  valbool) y (compat Snat v) equivalente a  $ n:nat.v=(Nat n) (definida por el predicado valnat).

Coq < Inductive valbool : semval->Prop
 := valbool_intro : (b:bool)(valbool (Bool b)).
valbool_ind is defined
valbool is defined
Coq < Inductive valnat : semval->Prop
 := valnat_intro : (n:nat)(valnat (Nat n)).
valnat_ind is defined
valnat is defined
Coq < Definition compat:sort -> semval -> Prop
:= [s,v]Cases s of Sbool => (valbool v)
                  | Snat => (valnat v) end.
compat is defined

Nótese que la definición inductiva de valbool es una codificación inductiva directa del predicado   [x:semval](EX b:bool | x=(Bool b)). Se puede probar fácilmente la correspondencia entre  compat y sort_val.

Coq < Theorem compat_sort_val
   : (s:sort)(v:semval)(compat s v)->
                        s = (sort_val v).
1 subgoal

  ============================
(s:sort)(v:semval)(compat s v)-> s=(sort_val v)
compat_sort_val < Intros s v.
1 subgoal

  s : sort
  v : semval
  ============================
   (compat s v)->s=(sort_val v)
compat_sort_val < Elim s.
2 subgoals

  s : sort
  v : semval
  ============================
   (compat Sbool v)->Sbool=(sort_val v)

subgoal 2 is:
 (compat Snat v)->Snat=(sort_val v)
compat_sort_val < Intro.
2 subgoals

  s : sort
  v : semval
  H : (compat Sbool v)
  ============================
   Sbool=(sort_val v)

subgoal 2 is:
 (compat Snat v)->Snat=(sort_val v)
compat_sort_val < Elim H.
2 subgoals

  s : sort
  v : semval
  H : (compat Sbool v)
  ============================
   (b:bool)Sbool=(sort_val (Bool b))

subgoal 2 is:
 (compat Snat v)->Snat=(sort_val v)
compat_sort_val < Simpl.
2 subgoals

  s : sort
  v : semval
  H : (compat Sbool v)
  ============================
   bool->Sbool=Sbool

subgoal 2 is:
 (compat Snat v)->Snat=(sort_val v)
compat_sort_val < Trivial.
1 subgoal

  s : sort
  v : semval
  ============================
   (compat Snat v)->Snat=(sort_val v)
compat_sort_val < Intro.
1 subgoal

  s : sort
  v : semval
  H : (compat Snat v)
  ============================
   Snat=(sort_val v)
compat_sort_val < Elim H.
1 subgoal

  s : sort
  v : semval
  H : (compat Snat v)
  ============================
   (n:nat)Snat=(sort_val (Nat n))
compat_sort_val < Simpl.
1 subgoal

  s : sort
  v : semval
  H : (compat Snat v)
  ============================
   nat->Snat=Snat

compat_sort_val < Intro.
1 subgoal

  s : sort
  v : semval
  H : (compat Snat v)
  n : nat
  ============================
   Snat=Snat
compat_sort_val < Trivial.
Subtree proved!

Alternativamente, la demostración puede compactarse como: Intros s v; Case s; Destruct 1; Trivial.
 
Ejercicio 1.  Probar que también: "s,v.(s=(sort_val v)) => (compat s v)
 
 
Una alternativa podría ser la de representar la noción de compatibilidad por un predicado inductivo:  

Coq < Inductive compat1:sort -> semval -> Prop :=  
 compat_bool : (b:bool)(compat1 Sbool (Bool b))  
 |compat_nat : (n:nat)(compat1 Snat (Nat n)).  

Las dos definiciones son equivalentes. Nótese que en el segundo caso, la propiedad  

(compat1 Snat  v) ® $ n : nat v=(Nat n)
necesita una inversión del predicado inductivo, mientras que en el caso de   compat esto es una simple consecuencia del cálculo de la expresión  Cases y de la definición de   valnat. 
 
 

La memoria

La memoria se representa como una función que a toda variable y clase le asocia un valor semántico. Será pues neccesario suponer que este valor es compatible con la clase

Coq < Definition memory := name->sort->semval.

Valor de una expresión

Para construir la relación entre una expresión y su valor, se puede dar una memoria como un parámetro en una ``Section'', cuando la sección se cierra, las nociones introducidas serán automáticamente abstraidas respecto a los parámetros de los que dependan.

Coq < Section Valexpr.

Coq < Variable memstate : memory.

Coq < Hypothesis memstate_correct :  (x:name)(s:sort)(compat s (memstate x s)).

La definición  exprval formaliza la semántica de las expresiones tal como se presentó en la figura  5.

Coq < Inductive exprval : expr -> semval -> Prop :=
 valvar  : (x:name)(s:sort)(exprval
               (Var x s)(memstate x s))
|valtr   : (exprval Tr (Bool true))
|valfa   : (exprval Fa (Bool false))
|valxor  : (f,g:expr)(bf,bg:bool)
(exprval f (Bool bf))-> (exprval g (Bool bg))
 ->(exprval (Xor f g) (Bool (boolxor bf bg)))
|valnum  : (n:nat)(exprval (Num n) (Nat n))
|valtzero: (f:expr)(nf:nat)(exprval f (Nat nf))
 ->(exprval (Null f) (Bool (iszero nf)))
|valopn  : (o:op)(f,g:expr)(nf,ng:nat)
   (exprval f (Nat nf))->(exprval g (Nat ng))
 ->(exprval (Opn o f g) (Nat (semop o nf ng))).

Ahora se puede enunciar el teorema que nos asegura que toda expresión correctamente tipada admite un valor.

Coq < Theorem expr_val_cor :
 (E:expr)(s:sort)(exprcorrect s E)->
             (EX v:semval | (exprval E v)).

La demostración por recurrencia necesita un lema más fuerte que diga que el valor calculado es compatible con la clase de la expresión.

coq < Lemma expr_val_cor_dom :
 (E:expr)(s:sort)(exprcorrect s E)
    ->(EX v:semval |
          (compat s v) & (exprval E v)).