2022-03-21
TAD conjunto (a)
parámetros formales
géneros a
operaciones No se requiere ninguna en particular
géneros conj(a)
observadores básicos
. pertenece . : a x conj(a) -> bool
generadores
emptyset : -> conj(a)
Ag : a x conj(a) -> conj(a)
operaciones
emptyset? : conj(a) -> bool
# : conj(a) -> nat
Las operaciones que estamos axiomatizando son funciones → debemos evitar las inconsistencias. Para esto nos esforzaremos en evitar la sobre-especificación.
¿Cuánto hay que axiomatizar?
Una regla práctica consiste en axiomatizar los observadores básicos sobre todos los generadores no restringidos, para asegurar que cumplimos todo el dominio
Es un predicado entre instancias del tipo que nos dice cuándo son iguales desde el punto de vista de su comportamiento.
Para escribirla utilizaremos los observadores básicos.
La igualdad observacional nos permite
Recordamos que una función $f$ es congruente a una relación de equivalencia $\sim$ si
$$ \forall(x,y)~\big(x \sim y \iff f(x) \sim f(y)\big) $$
En el contexto de los TADs, una función rompe la congruencia si diferencia elementos que quedan en la misma clase de equivalencia de acuerdo con la igualdad observacional.