[Práctico 5] - Ejercicios 6.3 y 5.2

[Práctico 5] - Ejercicios 6.3 y 5.2

de Jairo Yamil Bonanata Silva -
Número de respuestas: 3

Hola,

No sé cómo hay que definir Memoria, yo la definí cómo:

Definition Memoria := nat -> Valor.

Parameter LookUp : ...

Sin embargo con estas definiciones no se me ocurre cómo hacer en el ejercicio 6.3 para definir update. ¿La idea es simplemente un parámetro con el tipo y después axiomas?

Parameter update : Memoria -> nat -> Valor -> Memoria.

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 5] - Ejercicios 6.3 y 5.2

de Carlos Luna -

Hola.

La idea es dar definiciones, como funciones, para lookup y update (en vez de definir axiomas para operadores que se podría definir con Parameter). Por ejemplo:

Definition lookup(mem: Memoria)(v:Var): Valor := mem v.

Pensá la definición de update, teniendo en cuenta que el resultado es una nueva memoria, que puede ser definida con fun (w:Var) => ...

Saludos, Carlos

 

 

En respuesta a Carlos Luna

Re: [Práctico 5] - Ejercicios 6.3 y 5.2

de Jairo Yamil Bonanata Silva -

Claro. ¿La idea entonces sería utilizar operaciones booleanas Or y And para de esta forma hacer lo que queremos?

¿Se puede utilizar el equal definido al principio del práctico?

Parameter equal : A -> A -> bool.
Axiom equal1 : forall x y : A, equal x y = true -> x = y.
Axiom equal2 : forall x : A, equal x x <> false.


Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 5] - Ejercicios 6.3 y 5.2

de Carlos Luna -

Hola.

Si, se puede usar equal con los dos axiomas referidos. También se puede definir una función equal para nat (las variables son naturales).

Saludos, Carlos