Practico 5 -ej5 -parte2

Practico 5 -ej5 -parte2

de Joel Gabriel Vazquez Dos Santos -
Número de respuestas: 1

Hola,

1- Memoria la definimos como una función de Variable a valor: Variable Memoria:(Var->Valor).

que papel juega la función lookup? es la aplicación de memoria a un Var? no es exactamente la misma memoria?   

2-Como definimos una relación de evaluación? usamos (Inductive BEval:BExpr->Prop) , es esto correcto?

Saludos y muchas gracias!

En respuesta a Joel Gabriel Vazquez Dos Santos

Re: Practico 5 -ej5 -parte2

de Carlos Luna -

Hola.

Respecto a:

1) Está bien. lookup es precisamente la aplicación de la función a su argumento (de tipo Var).

2) Podría ser definida como una relación inductiva:

Inductive BEval(m:Memoria):BoolExpr->Valor->Prop :=

  | evar:forall v:Var, BEval m (varExpr v) (lookup m v) 

  | eboolt: BEval m (boolExpr true) true

  | ...

Saludos, Carlos