[Práctico 5] Ejercicio 5

[Práctico 5] Ejercicio 5

de Julian Tricanico Gadea -
Número de respuestas: 2

Buenas,

Hay un par de cosas de la letra que no me quedan del todo claras y prefiero preguntar.


  •  bool : = true | false
quisieron poner Valor := true | false ? (En la función lookup hablan de "Valor" pero no lo definen.)


  • qué quiere decir Var /\ Var o ~Var semánticamente?

Deberíamos simplemente no prestarle atención a eso? Al menos nuestro lenguaje nos deja hablar de esto.
Digo por la definición de BE := Var | bool | (BE /\ BE) | ~BE.


  • Memoria con mayúscula vs memoria con minúscula

La función lookup : Memoria -> Var -> Valor parece estar tomando alguien de tipo Memoria, pero no se habla de este tipo en la letra, sólo de una función con el nombre memoria.


Saludos!
En respuesta a Julian Tricanico Gadea

Re: [Práctico 5] Ejercicio 5

de Carlos Luna -

Hola.
Según la letra de este ejercicio, Var es nat y Valor es bool. Digamos:

Definition Valor := bool.

Definition Valor := bool.

No hay que confundir sintaxis de las expresiones con su semántica. Incialmente pide definir la sintaxis (el tipo BoolExpr):

Inductive BoolExpr : Set :=

  | be_var: Var -> BoolExpr

  | be_bool: bool -> BoolExpr

  | be_and: ...

...

Respecto a que quiere que quiere decir por ejemplo /\, notar que las expresiones son booleanas en este problema y que las variables (de tipo nat) toman valores booleanos en la memoria (Definition Memoria := Var -> Valor). Luego, /\ se interpreta como el “and” lógico/booleano. Volviendo a las variables, también están las funciones lookup (muy simple si se define a la memoria como una función) y update (de tipo: Memoria -> Var -> Valor -> Memoria).

La semántica de las expresiones booleanas está dada por BEVal, que podría definirse como una relación inductiva:

Inductive BEval : BoolExpr -> Memoria -> Valor -> Prop :=

| evar: forall (v: Var) (d: Memoria), BEval (be_var v) d (lookup d v)

…

...

Espero estas líneas sirvan de guía!

Saludos, Carlos