Skip to article frontmatterSkip to article content
Site not loading correctly?

This may be due to an incorrect BASE_URL configuration. See the MyST Documentation for reference.

Especificaciones algebraicas completas 2

Universidad Nacional de Rio Negro - Sede Andina

Especificaciones algebraicas avanzadas

Objetivos observables

Este capitulo completa el catalogo algebraico de la parte con cuatro familias que aparecen todo el tiempo en la practica: sets, diccionarios, arboles y grafos. La idea no es fijar una unica implementacion, sino mostrar como se expresa el contrato de cada estructura, que variantes son habituales y cual es la version simplificada que conviene usar cuando queres enseñar la idea sin cargar demasiada maquinaria.

En todos los casos, la tecnica es la misma: definir sorts, operaciones, axiomas e invariantes. Lo que cambia es el vocabulario de cada familia.

TDA Set

Un set representa una coleccion finita de elementos sin repetidos y sin orden observable. La igualdad no depende de la forma de construccion, sino del contenido.

Sorts y signatura

Sorts:Set,Element,Bool,NGeneradores:empty:SetModificadores:add:Set×ElementSetremove:Set×ElementSetObservadores:contains:Set×ElementBoolsize:SetNisEmpty:SetBoolunion:Set×SetSetintersect:Set×SetSetdifference:Set×SetSetsubsetEq:Set×SetBool\begin{align} \text{Sorts:} \quad & \mathtt{Set}, \mathtt{Element}, \mathtt{Bool}, \mathbb{N} \\ \\ \text{Generadores:} \\ \quad & \text{empty} : \to \mathtt{Set} \\ \\ \text{Modificadores:} \\ \quad & \text{add} : \mathtt{Set} \times \mathtt{Element} \to \mathtt{Set} \\ \quad & \text{remove} : \mathtt{Set} \times \mathtt{Element} \to \mathtt{Set} \\ \\ \text{Observadores:} \\ \quad & \text{contains} : \mathtt{Set} \times \mathtt{Element} \to \mathtt{Bool} \\ \quad & \text{size} : \mathtt{Set} \to \mathbb{N} \\ \quad & \text{isEmpty} : \mathtt{Set} \to \mathtt{Bool} \\ \quad & \text{union} : \mathtt{Set} \times \mathtt{Set} \to \mathtt{Set} \\ \quad & \text{intersect} : \mathtt{Set} \times \mathtt{Set} \to \mathtt{Set} \\ \quad & \text{difference} : \mathtt{Set} \times \mathtt{Set} \to \mathtt{Set} \\ \quad & \text{subsetEq} : \mathtt{Set} \times \mathtt{Set} \to \mathtt{Bool} \end{align}

Axiomas

Axioma 1 (empty no contiene elementos).

contains(empty,e)=false\text{contains}(\text{empty}, e) = \text{false}

Axioma 2 (add agrega presencia).

contains(add(s,e),e)=true\text{contains}(\text{add}(s, e), e) = \text{true}

Axioma 3 (add es idempotente).

add(add(s,e),e)=add(s,e)\text{add}(\text{add}(s, e), e) = \text{add}(s, e)

Axioma 4 (remove elimina presencia).

contains(remove(s,e),e)=false\text{contains}(\text{remove}(s, e), e) = \text{false}

Axioma 5 (remove de un elemento ausente no cambia el set).

contains(s,e)=false    remove(s,e)=s\text{contains}(s, e) = \text{false} \implies \text{remove}(s, e) = s

Axioma 6 (union con empty).

union(s,empty)=sunion(empty,s)=s\text{union}(s, \text{empty}) = s \quad \land \quad \text{union}(\text{empty}, s) = s

Axioma 7 (extensionalidad).

subsetEq(s1,s2)=true    e, contains(s1,e)contains(s2,e)\text{subsetEq}(s_1, s_2) = \text{true} \iff \forall e,\ \text{contains}(s_1, e) \Rightarrow \text{contains}(s_2, e)

Axioma 8 (igualdad por contenido).

s1=s2    e, contains(s1,e)=contains(s2,e)s_1 = s_2 \iff \forall e,\ \text{contains}(s_1, e) = \text{contains}(s_2, e)

Variantes comunes

VarianteRasgo distintivoQue suele cambiar en el contrato
Set mutablePermite add y remove sobre el mismo estado abstractoLa especificacion debe dejar claro si remove sobre un elemento ausente es identidad.
Set ordenadoExpone un orden observable sobre los elementosAparecen observadores como min, max, predecessor y successor.
Set acotadoTrabaja sobre un universo finito y conocidocontains puede razonarse como un vector booleano finito.
Set persistenteCada operacion devuelve un set nuevo sin mutar el anteriorLas ecuaciones deben expresar comparticion semantica, no mutacion.

Estas variantes cambian la manera de leer el contrato, pero no el principio central: dos sets son iguales si contienen los mismos elementos. Cuando el set deja de ser “solo pertenencia” y empieza a exponer orden o finitud, la signatura gana observadores nuevos.

Variante simplificada

La version simplificada mas util es el set sobre universo finito. En vez de modelar cualquier elemento, se toma un universo fijo U={0,,n1}U = \{0, \dots, n-1\} y el set se especifica solo con una interfaz minima:

add, remove, contains, empty\text{add},\ \text{remove},\ \text{contains},\ \text{empty}

En esa version, basta con dejar explícitos cuatro hechos:

  1. empty no contiene nada.

  2. add vuelve verdadera la pertenencia del elemento agregado.

  3. remove vuelve falsa la pertenencia del elemento removido.

  4. add es idempotente.

Eso reduce el esfuerzo de axiomatizacion porque contains se comporta como acceso a una posicion booleana. Si queres formalizar un set un poco mas rico sin perder simplicidad, esta es la variante de partida.

TDA Dictionary

Un diccionario asocia claves con valores. La clave es unica; el valor puede cambiar con una insercion nueva sobre la misma clave.

Sorts y signatura

Sorts:Dict,Key,Value,Bool,Nat,MaybeValueGeneradores:empty:Dictnone:MaybeValuesome:ValueMaybeValueModificadores:put:Dict×Key×ValueDictremove:Dict×KeyDictObservadores:lookup:Dict×KeyMaybeValuecontainsKey:Dict×KeyBoolsize:DictNat\begin{align} \text{Sorts:} \quad & \mathtt{Dict}, \mathtt{Key}, \mathtt{Value}, \mathtt{Bool}, \mathtt{Nat}, \mathtt{MaybeValue} \\ \\ \text{Generadores:} \\ \quad & \text{empty} : \to \mathtt{Dict} \\ \quad & \text{none} : \to \mathtt{MaybeValue} \\ \quad & \text{some} : \mathtt{Value} \to \mathtt{MaybeValue} \\ \\ \text{Modificadores:} \\ \quad & \text{put} : \mathtt{Dict} \times \mathtt{Key} \times \mathtt{Value} \to \mathtt{Dict} \\ \quad & \text{remove} : \mathtt{Dict} \times \mathtt{Key} \to \mathtt{Dict} \\ \\ \text{Observadores:} \\ \quad & \text{lookup} : \mathtt{Dict} \times \mathtt{Key} \to \mathtt{MaybeValue} \\ \quad & \text{containsKey} : \mathtt{Dict} \times \mathtt{Key} \to \mathtt{Bool} \\ \quad & \text{size} : \mathtt{Dict} \to \mathtt{Nat} \end{align}

Axiomas

Axioma 1 (empty no contiene claves).

containsKey(empty,k)=false\text{containsKey}(\text{empty}, k) = \text{false}

Axioma 2 (put hace visible la clave).

containsKey(put(m,k,v),k)=true\text{containsKey}(\text{put}(m, k, v), k) = \text{true}

Axioma 3 (lookup de una clave cargada devuelve su valor).

lookup(put(m,k,v),k)=some(v)\text{lookup}(\text{put}(m, k, v), k) = \text{some}(v)

Axioma 4 (put sobre una clave distinta preserva el resto).

kk    lookup(put(m,k,v),k)=lookup(m,k)k \neq k' \implies \text{lookup}(\text{put}(m, k, v), k') = \text{lookup}(m, k')

Axioma 5 (remove elimina la clave).

containsKey(remove(m,k),k)=false\text{containsKey}(\text{remove}(m, k), k) = \text{false}

Axioma 6 (remove de una clave ausente no cambia el diccionario).

containsKey(m,k)=false    remove(m,k)=m\text{containsKey}(m, k) = \text{false} \implies \text{remove}(m, k) = m

Axioma 7 (size cuenta claves distintas).

size(put(m,k,v))={size(m)si containsKey(m,k)=truesize(m)+1si containsKey(m,k)=false\text{size}(\text{put}(m, k, v)) = \begin{cases} \text{size}(m) & \text{si } \text{containsKey}(m, k) = \text{true} \\ \text{size}(m) + 1 & \text{si } \text{containsKey}(m, k) = \text{false} \end{cases}

Variantes comunes

VarianteRasgo distintivoQue suele cambiar en el contrato
Map o diccionario simpleCada clave tiene un solo valor asociadoput reemplaza el valor anterior y lookup devuelve a lo sumo un resultado.
Diccionario ordenadoLas claves tienen orden observableAparecen consultas por rango y extremos.
MultidiccionarioUna clave puede tener varios valoreslookup devuelve una coleccion y remove puede eliminar una ocurrencia o todas.
Diccionario hashLa ubicacion depende de una funcion de dispersionLa especificacion suele ocultar el almacenamiento y solo exigir acceso promedio eficiente.

En el diccionario simple, la propiedad clave es que la igualdad de mapas depende de pares clave -> valor, no de la historia de inserciones. Cuando agregas orden, el contrato deja de ser solo asociativo y pasa a incluir recorridos. Cuando agregas multiplicidad, lookup ya no puede seguir siendo un unico valor.

Variante simplificada

La version simplificada mas didactica es el diccionario parcial sobre claves acotadas. Se fija un universo de claves finito y se evita modelar iteradores, vistas o estructura interna. El contrato minimo queda asi:

empty, put, remove, lookup, containsKey\text{empty},\ \text{put},\ \text{remove},\ \text{lookup},\ \text{containsKey}

Los axiomas esenciales son:

  1. lookup(empty, k) = none.

  2. put sobre una clave nueva produce some(v).

  3. put sobre una clave existente reemplaza el valor.

  4. remove elimina la clave y hace que containsKey vuelva a falso.

Con eso alcanza para enseñar el contrato semantico sin sumar complejidad accidental. Es la version mas util cuando queres conectar algebra de TDAs con estructuras de mapas concretas.

TDA Tree

Un arbol representa una estructura jerarquica con una raiz y subarboles. La especificacion cambia segun si el arbol es general, binario o binario de busqueda.

Sorts y signatura

Sorts:Tree,Element,MaybeElement,Bool,NatGeneradores:empty:Treenone:MaybeElementsome:ElementMaybeElementleaf:ElementTreenode:Element×Tree×TreeTreeObservadores:root:TreeMaybeElementleft:TreeTreeright:TreeTreeisEmpty:TreeBoolisLeaf:TreeBoolsize:TreeNatheight:TreeNat\begin{align} \text{Sorts:} \quad & \mathtt{Tree}, \mathtt{Element}, \mathtt{MaybeElement}, \mathtt{Bool}, \mathtt{Nat} \\ \\ \text{Generadores:} \\ \quad & \text{empty} : \to \mathtt{Tree} \\ \quad & \text{none} : \to \mathtt{MaybeElement} \\ \quad & \text{some} : \mathtt{Element} \to \mathtt{MaybeElement} \\ \quad & \text{leaf} : \mathtt{Element} \to \mathtt{Tree} \\ \quad & \text{node} : \mathtt{Element} \times \mathtt{Tree} \times \mathtt{Tree} \to \mathtt{Tree} \\ \\ \text{Observadores:} \\ \quad & \text{root} : \mathtt{Tree} \to \mathtt{MaybeElement} \\ \quad & \text{left} : \mathtt{Tree} \to \mathtt{Tree} \\ \quad & \text{right} : \mathtt{Tree} \to \mathtt{Tree} \\ \quad & \text{isEmpty} : \mathtt{Tree} \to \mathtt{Bool} \\ \quad & \text{isLeaf} : \mathtt{Tree} \to \mathtt{Bool} \\ \quad & \text{size} : \mathtt{Tree} \to \mathtt{Nat} \\ \quad & \text{height} : \mathtt{Tree} \to \mathtt{Nat} \end{align}

Axiomas

Axioma 1 (empty no tiene raiz).

root(empty)=none\text{root}(\text{empty}) = \text{none}

Axioma 2 (leaf tiene raiz y es hoja).

root(leaf(e))=some(e)isLeaf(leaf(e))=true\text{root}(\text{leaf}(e)) = \text{some}(e) \quad \land \quad \text{isLeaf}(\text{leaf}(e)) = \text{true}

Axioma 3 (node conserva la raiz).

root(node(e,l,r))=some(e)\text{root}(\text{node}(e, l, r)) = \text{some}(e)

Axioma 4 (empty no tiene hijos).

left(empty)=emptyright(empty)=empty\text{left}(\text{empty}) = \text{empty} \quad \land \quad \text{right}(\text{empty}) = \text{empty}

Axioma 5 (size suma subarboles).

size(node(e,l,r))=1+size(l)+size(r)\text{size}(\text{node}(e, l, r)) = 1 + \text{size}(l) + \text{size}(r)

Axioma 6 (height toma el mayor camino).

height(node(e,l,r))=1+max(height(l),height(r))\text{height}(\text{node}(e, l, r)) = 1 + \max(\text{height}(l), \text{height}(r))

Variantes comunes

VarianteRasgo distintivoQue suele cambiar en el contrato
Arbol generalUn nodo puede tener cualquier cantidad de hijosLa operacion children reemplaza a left y right.
Arbol binarioCada nodo tiene a lo sumo dos hijosLa estructura de nodo queda fijada por raiz, izquierdo y derecho.
Arbol binario de busquedaEl orden de las claves queda restringido por la raizEl contrato agrega la propiedad de orden total entre subarboles.
Arbol balanceadoMantiene una cota sobre la alturaAparecen axiomas sobre rotaciones y altura acotada.
TrieLa forma del arbol sigue prefijos de clavesLa ruta desde la raiz representa una clave compuesta.

En arboles, la variante elegida cambia mucho mas que el nombre: cambia la forma en que se interpreta la jerarquia. Un arbol general sirve para modelar pertenencia estructural; un BST agrega orden; un balanceado agrega restriccion sobre la forma; un trie agrega prefijos.

Variante simplificada

La version simplificada mas clara es el arbol binario puro, donde solo importan la raiz y los dos hijos. Se omiten el orden de busqueda, el balanceo y cualquier politica de rebalanceo. El contrato minimo queda reducido a:

empty, leaf, node, root, left, right, size, height\text{empty},\ \text{leaf},\ \text{node},\ \text{root},\ \text{left},\ \text{right},\ \text{size},\ \text{height}

Los axiomas que conviene conservar son:

  1. empty no tiene raiz.

  2. leaf(e) tiene raiz e y altura uno.

  3. node(e, l, r) conserva la raiz e.

  4. size suma uno mas los tamanos de ambos hijos.

  5. height toma el maximo de las alturas de sus hijos mas uno.

Con esa base se puede escalar despues hacia arboles de busqueda, heaps o arboles balanceados sin cambiar la idea central del contrato.

TDA Graph

Un grafo modela relaciones entre vertices. Segun el caso, esas relaciones pueden ser dirigidas, ponderadas o multiples.

Sorts y signatura

Sorts:Graph,Vertex,Bool,Nat,WeightGeneradores:empty:GraphModificadores:addVertex:Graph×VertexGraphremoveVertex:Graph×VertexGraphaddEdge:Graph×Vertex×VertexGraphremoveEdge:Graph×Vertex×VertexGraphObservadores:hasVertex:Graph×VertexBooladjacent:Graph×Vertex×VertexBoolneighbors:Graph×VertexSetdegree:Graph×VertexNatorder:GraphNat\begin{align} \text{Sorts:} \quad & \mathtt{Graph}, \mathtt{Vertex}, \mathtt{Bool}, \mathtt{Nat}, \mathtt{Weight} \\ \\ \text{Generadores:} \\ \quad & \text{empty} : \to \mathtt{Graph} \\ \\ \text{Modificadores:} \\ \quad & \text{addVertex} : \mathtt{Graph} \times \mathtt{Vertex} \to \mathtt{Graph} \\ \quad & \text{removeVertex} : \mathtt{Graph} \times \mathtt{Vertex} \to \mathtt{Graph} \\ \quad & \text{addEdge} : \mathtt{Graph} \times \mathtt{Vertex} \times \mathtt{Vertex} \to \mathtt{Graph} \\ \quad & \text{removeEdge} : \mathtt{Graph} \times \mathtt{Vertex} \times \mathtt{Vertex} \to \mathtt{Graph} \\ \\ \text{Observadores:} \\ \quad & \text{hasVertex} : \mathtt{Graph} \times \mathtt{Vertex} \to \mathtt{Bool} \\ \quad & \text{adjacent} : \mathtt{Graph} \times \mathtt{Vertex} \times \mathtt{Vertex} \to \mathtt{Bool} \\ \quad & \text{neighbors} : \mathtt{Graph} \times \mathtt{Vertex} \to \mathtt{Set} \\ \quad & \text{degree} : \mathtt{Graph} \times \mathtt{Vertex} \to \mathtt{Nat} \\ \quad & \text{order} : \mathtt{Graph} \to \mathtt{Nat} \end{align}

Axiomas

Axioma 1 (empty no tiene vertices ni aristas).

hasVertex(empty,v)=falseadjacent(empty,u,v)=false\text{hasVertex}(\text{empty}, v) = \text{false} \quad \land \quad \text{adjacent}(\text{empty}, u, v) = \text{false}

Axioma 2 (addVertex hace visible el vertice).

hasVertex(addVertex(g,v),v)=true\text{hasVertex}(\text{addVertex}(g, v), v) = \text{true}

Axioma 3 (addEdge requiere vertices visibles).

adjacent(addEdge(g,u,v),u,v)=true\text{adjacent}(\text{addEdge}(g, u, v), u, v) = \text{true}

Axioma 4 (removeEdge elimina la adyacencia).

adjacent(removeEdge(g,u,v),u,v)=false\text{adjacent}(\text{removeEdge}(g, u, v), u, v) = \text{false}

Axioma 5 (removeVertex elimina toda incidencia).

hasVertex(removeVertex(g,v),v)=false\text{hasVertex}(\text{removeVertex}(g, v), v) = \text{false}

Axioma 6 (degree cuenta vecinos).

degree(g,v)=neighbors(g,v)\text{degree}(g, v) = |\text{neighbors}(g, v)|

Axioma 7 (order cuenta vertices).

order(addVertex(g,v))={order(g)si hasVertex(g,v)=trueorder(g)+1si hasVertex(g,v)=false\text{order}(\text{addVertex}(g, v)) = \begin{cases} \text{order}(g) & \text{si } \text{hasVertex}(g, v) = \text{true} \\ \text{order}(g) + 1 & \text{si } \text{hasVertex}(g, v) = \text{false} \end{cases}

Variantes comunes

VarianteRasgo distintivoQue suele cambiar en el contrato
Grafo simpleNo tiene lazos ni aristas repetidasadjacent es una relacion booleana entre vertices distintos.
Grafo dirigidoLa relacion depende del sentidoHay que distinguir outNeighbors de inNeighbors.
Grafo ponderadoCada arista tiene un pesoEl contrato agrega weight y restricciones sobre la existencia de peso.
MultigrafoPuede repetir aristas entre verticesedgeCount y multiplicidad pasan a ser observables.
Grafo con lazosPermite aristas de un vertice hacia si mismoadjacent(g, v, v) deja de ser un caso prohibido.

La variante simple es la base pedagogica mas estable. Las otras se usan cuando el problema real exige direccion, costo o multiplicidad. En todos los casos, la pregunta algebraica sigue siendo la misma: que significa que dos grafos sean iguales, y que operaciones cambian realmente el estado.

Variante simplificada

La version simplificada mas util es el grafo simple no dirigido y no ponderado. En esa version, basta con una interfaz reducida:

empty, addVertex, removeVertex, addEdge, removeEdge, adjacent, neighbors\text{empty},\ \text{addVertex},\ \text{removeVertex},\ \text{addEdge},\ \text{removeEdge},\ \text{adjacent},\ \text{neighbors}

El contrato minimo deberia dejar claros estos puntos:

  1. addVertex hace visible al vertice.

  2. addEdge solo agrega incidencia entre vertices existentes.

  3. removeEdge elimina una incidencia concreta.

  4. neighbors devuelve exactamente los vertices adyacentes.

  5. adjacent es simetrica porque el grafo es no dirigido.

Eso alcanza para enseñar conectividad, recorrido y razonamiento sobre incidencia sin mezclar pesos ni orientacion. Si despues queres agregar direccion o ponderacion, la simplificacion sirve como punto de partida limpio.

Resumen

Los cuatro TDAs comparten la misma forma de especificacion, pero cambian los axiomas que definen identidad, ausencia, reemplazo y relacion entre observadores.

La version simplificada de cada uno sirve para introducir la idea sin arrastrar variantes de implementacion o detalles de uso que distraen del contrato algebraico.

Ejercicios

Proximo paso

Si queres seguir, el paso natural es aplicar estas especificaciones a una implementacion concreta y verificar que los tests reproduzcan los axiomas.