AED2 resumen 2C-17

Ejercicio 1

a

duplicar: secu(α)→secu(α)

duplicar(s)≡if vacía?(s) then ⟨⟩ else prim(s)•prim(s)•duplicar(fin(s)) fi

b

•≤•: secu(α) x secu(α) → bool

s ≤ t ≡ if ¬(vacía?(s) ∨ vacía?(t)) then prim(s) < prim(t) ∨ (prim(s)=prim(t) ∧ fin(s)≤fin(t)) else vacía?(s) fi

c

reverso: secu(α)→secu(α)

reverso(s) ≡ if vacía?(s) then s else reverso(fin(s)) º prim(s) fi

d

capicúa: secu(α)→bool

capicúa(s) ≡ s = reverso(s)

e

esPrefijo?: secu(α) x secu(α) → bool

esPrefijo?(⟨⟩,t) ≡ true

esPrefijo?(e • s,t) ≡ if vacía?(t) then false else e = prim(t) ∧ esPrefijo?(s,fin(t)) fi

f

buscar: secu(α) x secu(α) → nat

buscar(⟨⟩,t) ≡ 0

buscar(s, t) ≡ if esPrefijo?(s, t) then 0 else 1 + buscar(s, fin(t)) fi

g

estaOrdenada?: secu(α) → bool

estaOrdenada?(⟨⟩) ≡ true

estaOrdenada?(e • s) ≡ if vacía?(s) then true else e ≤ prim(s) ∧ estaOrdenada?(s) fi

h

InsertarOrdenada, que dados una secuencia so (que debe estar ordenada) y un elemento e (de género α) inserta e en so de manera ordenada.

insertarOrdenada: secu(α) so x α → secu(α) {estaOrdenada?(so)}

insertarOrdenada(⟨⟩, e) ≡ e • ⟨⟩

insertarOrdenada(a • s, e) ≡ if e ≤ a then e • a • s else a • insertarOrdenada(s, e) fi

i

cantidadApariciones: secu(α) x α → nat

cantidadApariciones(⟨⟩,a) ≡ 0

cantidadApariciones(e • s,a) ≡ if e = a then 1 + cantidadApariciones(s,a) else cantidadApariciones(s,a) fi

j

aux(s,s,t): secu(α) x secu(α) x secu(α) → bool

aux(⟨⟩,s,t) ≡ true

aux(e • u,s,t) ≡ cantidadApariciones(s,e) = cantidadApariciones(t,e) ∧ aux(u,s,t)

esPermutación?: secu(α) x secu(α) → bool

esPermutación?(s,t) ≡ if long(s) = long(t) then aux(s,s,t) else false

k

combinar: secu(α) a x secu(α) b → secu(α) {estaOrdenada?(a) ∧ estaOrdenada?(b)}

combinar(s,t) ≡ if vacía(s) then t else combinar(fin(s),insertarOrdenada(t,prim(s)) fi

Ejercicio 2

a

#hojas: ab(α) → nat

#hojas(nil) ≡ 0

#hojas(bin(a,e,b)) ≡ if esHoja?(bin(a,e,b)) then 1 else #hojas(a) + #hojas(b) fi

b

degeneradoAIzquierda: ab(α) → bool

degeneradoAIzquierda(a) ≡ nil?(a) ∨L if esHoja?(a) then true else nil?(der(a)) ∧ degeneradoAIzquierda(izq(a)) fi

c

zigZag: ab(α) → bool

zigZag(a) ≡ nil?(a) ∨L esHoja?(a) ∨L if nil?(izq(a)) then nil?(der(der(a))) ∧ zigZag(der(a)) else if nil?(izq(a)) then nil?(izq(izq(a))) ∧ zigZag(izq(a)) else false fi fi

d

ultimoNivelCompleto: ab(α) → nat

ultimoNivelCompleto(nil) ≡ 0

ultimoNivelCompleto(bin(a,e,b)) ≡ 1 + min(ultimoNivelCompleto(a),ultimoNivelCompleto(b))

e

espejo: ab(α) → ab(α)

espejo(a) ≡ if nil?(a) then a else bin(espejo(der(a)),raiz(a),espejo(izq(a)) fi

f

esSimétrico?: ab((α) → bool

esSimétrico?(a) ≡ a = espejo(a)

Ejercicio 3

a

agregarTodos: α x conj(conj(α)) → conj(conj(α))

agregarTodos(n,c) ≡ if ∅?(c) then Ag(Ag(n,∅),∅) else Ag(Ag(n,dameUno(c)),agregarTodos(n,sinUno(c))) fi

partesDe: conj(nat) → conj(conj(nat))

partesDe(c) ≡ if ∅?(c) then c else agregarTodos(dameUno(c),partesDe(sinUno(c))) ∪ partesDe(sinUno(c)) fi

b

combinacionesDeK: conj(α) x nat → conj(conj(α))

combinacionesDeK(∅, k) ≡ ∅

combinacionesDeK(Ag(e,c), k) ≡ if k = 0 ∨ #(Ag(e,c)) < k then ∅ else agregarTodos(e,combinacionesDeK(c,k-1)) ∪ combinacionesDeK(c,k) fi

Ejercicio 4

ntn: conj(secu(α)) x secu(α) → conj(secu(α))

[ToDo]

Necesito:

• Ver si CADA secuencia del conjunto de entrada es o no subsecuencia de la secuencia de entrada (2do param)
• → Definir función auxiliar esSubsecuencia(a • s, b • t), a,b:α, s,t:secu(α)
• → Definir ntn(Ag(a • s, w), b • t), w: conj(secu(α))

• Ver si CADA secuencia del conjunto DE SALIDA es o no subsecuencia de alguna otra secuencia del conjunto de salida
• → Puedo usar la misma función auxiliar esSubsecuencia()

Ejercicio 5

a

nivelNormal?: at(α) x nat k → bool { ¬ k = 0 }

nivelNormal?(a,k) ≡ nil?(a) ∨L if k = 1 then ¬(nil?(izq(a)) ∨ nil?(med(a)) ∨ nil?(der(a))) else nivelNormal?(izq(a),k-1) ∧ nivelNormal?(med(a),k-1) ∧ nivelNormal?(der(a),k-1) fi

b

   // Defino auxiliar que cuente cantNodos en una secuencia de arboles ternarios: 
   
   cantNodos: secu( at( α ) ) -> nat
   
   cantNodos( t · <> ) ≡ if t ≠ nil then 1 else 0
   cantNodos( t · s )  ≡ if t ≠ nil then 1 + cantNodos(s)
                                    else cantNodos(s)

   acotado?: at(α) x nat -> bool
   
   acotado?(nil, k) ≡ true
   
   // Recibo el arbol ternario como sus partes separadas: (izq,medio,der,raiz)
   
   acotado?(tern(i,m,d,r), k) ≡ if cantNodos(i · m · d · <>) ≤ k then
                                    acotado?(i) ∧ acotado?(m) ∧ acotado?(d)
                                else
                                    false

Ejercicio 6

a

   altura: rosetree(α) → nat
   
   altura(rose(r, ⟨⟩)) ≡ 1
   
   altura(rose(r, e • s)) ≡ 1 + altura(masAlta(r, e • s))
   
   masAlta: α x secu(rosetree(α)) → rosetree(α)
   
   masAlta(a, s) ≡ if vacía?(s) then
                       rose(a,⟨⟩)
                   else if altura(prim(s)) > altura(masAlta(a, fin(s))) then
                           prim(s)
                       else
                           masAlta(a, fin(s))
                       fi
                   fi

b

   cantHojas: rosetree(α) → nat
   
   cantHojas(r) ≡ if esHoja?(r) then 
                      1
                  else
                      sumarHojas(hijos(r))
                  fi
   
   esHoja?: rosetree(α) → bool
   
   esHoja?(r) ≡ vacía?(hijos(r))
   
   sumarHojas: secu( rosetree(α) ) → nat
   
   sumarHojas(s) ≡ if vacía?(s) then 
                       0
                   else
                       cantHojas(prim(s)) + sumarHojas(fin(s))
                   fi

c

podar: rosetree(α) a → rosetree(α) {¬esHoja?(a)}

podar(r) ≡ rose(raíz(r),podadora(hijos(r)))

podadora: secu(rosetree(α)) → secu(rosetree(α))

podadora(s) ≡ if vacía?(s) then s else if esHoja?(prim(s)) then podadora(fin(s)) else podar(prim(s)) • podadora(fin(s)) fi fi

d

obtenerRamas: rosetree(α) → secu(secu((α))

obtenerRamas(r) ≡ if esHoja?(r) then (raíz(r) • ⟨⟩) • ⟨⟩ else if long(hijos(r)) = 1 then insertarTodos(raíz(r),obtenerRamas(prim(hijos(r)))) else insertarTodos(raíz(r),obtenerRamas(prim(hijos(r)))) & obtenerRamas(rose(raíz(r),fin(hijos(r)))) fi fi

insertarTodos: α x secu(secu(α)) → secu(secu(α))

insertarTodos(a,s) ≡ if vacía(s) then ⟨⟩ else (a • prim(s)) • insertarTodos(a,fin(s)) fi

e

devolverNivel: nat n x rosetree(α) → secu(α) {¬ n = 0}

devolverNivel(n,r) ≡ agarrador(n,obtenerRamas(r))

agarrador: nat n x secu(secu(α)) → secu(α) {¬ n = 0}

agarrador(n,s) ≡ if vacía(s) then ⟨⟩ else if long(prim(s)) ≥ n then obtener(n,prim(s)) • agarrador(n,fin(s)) else agarrador(n,fin(s)) fi fi

obtener: nat n x secu(&alpha) s → α {(¬ n = 0) ∧ long(s) ≥ n}

obtener(n,s) ≡ if n = 1 then prim(s) else obtener(n-1,fin(s)) fi

f

masLargasConRepetidos: rosetree(α) → conj(secu(α))

masLargasConRepetidos(r) ≡ soloConRepetidos(soloUnTam(altura(r),obtenerRamas(r)))

tieneRepetido: secu(α) → bool

tieneRepetido(s) ≡ (¬ vacía(s)) ∧L (esta?(prim(s),fin(s)) ∨ tieneRepetido(fin(s)))

soloConRepetidos: secu(secu(α)) → conj(secu(α))

soloConRepetidos(s) ≡ if vacía(s) then ∅ else if tieneRepetido(prim(s)) then Ag(prim(s),soloConRepetidos(fin(s))) else soloConRepetidos(fin(s)) fi fi

soloUnTam: nat n x secu(secu(α)) → secu(secu(α)) {¬ n = 0}

soloUnTam(n,s) ≡ if vacía?(s) then ⟨⟩ else if long(s) = n then prim(s) • soloUnTam(n,fin(s)) else soloUnTam(n,fin(s)) fi fi

Ejercicio 7

evaluar(cte(a),n) ≡ a

evaluar(x,n) ≡ n

evaluar(a + b, n) ≡ evaluar(a,n) + evaluar(b,n)

evaluar(a . b, n) ≡ evaluar(a,n) . evaluar(b,n)

esRaíz: polinomio x nat → bool

esRaíz(a,n) ≡ 0 = evaluar(a,n)

Ejercicio 8

trayectoria(ubicar(c)) ≡ c • ⟨⟩

trayectoria(arriba(r)) ≡ ⟨π1(posiciónActual(r)),π2(posiciónActual(r)) + 1⟩ • trayectoria(r)

trayectoria(abajo(r)) ≡ ⟨π1(posiciónActual(r)),π2(posiciónActual(r)) - 1⟩ • trayectoria(r)

trayectoria(derecha(r)) ≡ ⟨π1(posiciónActual(r)) + 1,π2(posiciónActual(r))⟩ • trayectoria(r)

trayectoria(izquierda(r)) ≡ ⟨π1(posiciónActual(r)) - 1,π2(posiciónActual(r))⟩ • trayectoria(r)

posiciónActual(r) ≡ prim(trayectoria(r))

cuántasVecesPasó(c,r) ≡ cantidadApariciones(Trayectoria(r),c)

másALaDerecha(r) ≡ maxX(trayectoria(r))

maxX: secu(coordenada) s → coordenada {¬ vacía?(s)}

maxX(e • s) ≡if vacía?(s) then π1(e) else max(π1(e),π1(maxX(s)) fi

Ejercicio 9

TAD Electroimán

Igualdad observacional

(∀ i1:electroimán)((∀ i2:electroimán)(i1 =obs i2 ⇔ ((cinta(i1) = cinta(i2) ∧ imánPrendido?(i1) = imánPrendido?(i2)) ∧L (imánPrendido?(i1) ⇒L (imánCargado?(i1) = imánCargado?(i2))))))

Genero electroimán

Usa Bool, Nat, Cinta

Exporta Genero, Generadores, Observadores básicos, Otras operaciones

Axiomas

cinta(arrancar(c)) ≡ c

cinta(prender(e)) ≡ if celdaActualOcupada?(cinta(e)) then sacarElem(cinta(e)) else cinta(e) fi

cinta(apagar(e)) ≡ if imánCargado?(e) then ponerElem(cinta(e)) else cinta(e) fi

cinta(←(e)) ≡ ←(cinta(e))

cinta(→(e)) ≡ →(cinta(e))

imánPrendido?(arrancar(c)) ≡ false

imánPrendido?(prender(e)) ≡ true

imánPrendido?(apagar(e)) ≡ false

imánPrendido?(→(e)) ≡ imánPrendido?(e)

imánPrendido?(←(e)) ≡ imánPrendido?(e)

imánCargado?(prender(e)) ≡ celdaActualOcupada?(e)

imánCargado?(→(e)) ≡ imánCargado?(e) ∨ celdaActualOcupada?(→(e))

imánCargado?(←(e)) ≡ imánCargado?(e) ∨ celdaActualOcupada?(←(e))

celdaActualOcupada?(e) ≡ celdaActualOcupada?(cinta(e))

#giros←(arrancar(c) ≡ 0

#giros←(prender(e) ≡  #giros←(e)

#giros←(apagar(e) ≡  #giros←(e)

#giros←(→(e) ≡  #giros←(e)

#giros←(←(e) ≡ 1 + #giros←(e)

#giros→(arrancar(c) ≡ 0

#giros→(prender(e) ≡  #giros→(e)

#giros→(apagar(e) ≡  #giros→(e)

#giros→(→(e) ≡ 1 + #giros→(e)

#giros→(←(e) ≡ #giros→(e)

Fin TAD

TAD Cinta

Igualdad observacional

(∀ c1:cinta)((∀ c2:cinta)(c1 =obs c2 ⇔ (#celdas(c1) = #celdas(c2) ∧L (celdaActual(c1) = celdaActual(c2) ∧ #giros←(c1) = #giros←(c2) ∧ #giros→(c1) = #giros→(c2) ∧ (∀i:nat)(i<#celdas(c1) ⇒(celdaOcupada?(i,c1) = celdaOcupada?(i,c2)))))))

Genero cinta

Usa Bool, Nat

Exporta Genero, Generadores, Observadores básicos, Otras operaciones

Otras operaciones

cuentaOcupados: nat x cinta → nat

Axiomas

#celdas(arrancar(n)) ≡ n

#celdas(ponerElem(c)) ≡ #celdas(c)

#celdas(sacarElem(c)) ≡ #celdas(c)

#celdas(←(c)) ≡ #celdas(c)

#celdas(→(c)) ≡ #celdas(c)

#giros←(arrancar(n)) ≡ 0

#giros←(ponerElem(c)) ≡ #giros←(c)

#giros←(sacarElem(c)) ≡ #giros←(c)

#giros←(←(c)) ≡ 1 + #giros←(c)

#giros←(→(c)) ≡ #giros←(c)

#giros→(arrancar(n)) ≡ 0

#giros→(ponerElem(c)) ≡ #giros→(c)

#giros→(sacarElem(c)) ≡ #giros→(c)

#giros→(←(c)) ≡ #giros→(c)

#giros→(→(c)) ≡ 1 + #giros→(c)

celdaActual(arrancar(n)) ≡ 0

celdaActual(ponerElem(c)) ≡ celdaActual(c)

celdaActual(sacarElem(c)) ≡ celdaActual(c)

celdaActual(←(c)) ≡ if celdaActual(c) = 0 then #celdas(c) - 1 else celdaActual(c) - 1 fi

celdaActual(→(c)) ≡ if celdaActual(c) = #celdas(c) - 1 then 0 else celdaActual(c) + 1 fi

celdaOcupada?(n,arrancar(a)) ≡ false

celdaOcupada?(n,ponerElem(c)) ≡ if n = celdaActual(c) then true else celdaOcupada?(n,c) fi

celdaOcupada?(n,sacarElem(c)) ≡ if n = celdaActual(c) then false else celdaOcupada?(n,c) fi

celdaOcupada?(n,←(c)) ≡ celdaOcupada?(n,c)

celdaOcupada?(n,→(c)) ≡ celdaOcupada?(n,c)

celdaActualOcupada?(c) ≡ celdaOcupada?(celdaActual(c),c)

#elem(c) ≡ cuentaOcupados(0,c)

cuentaOcupados(n,c) ≡ if n < #celdas(c) then if celdaOcupada?(n,c) then 1 + cuentaOcupados(n+1,c) else cuentaOcupados(n+1,c) fi else 0 fi

Fin TAD

Ejercicio 12

TAD Producto es String

TAD Stock

Igualdad observacional

(∀ s1:stock)((∀ s2:stock)(s1 =obs s2 ⇔ ((∀ p:producto)(estaRegistrado(p,s1) ⇔ estaRegistrado(p,s2)) ∧L (∀ p1:producto)((∀ p2:producto)((estaRegistrado(p1,s1) ∧ estaRegistrado(p2,s1)) ⇒L (mínimo(p1,s1) = mínimo(p1,s2) ∧ compras(p1,s1) = compras(p1,s2) ∧ ventas(p1,s1) = ventas(p1,s2) ∧ esSus(p1,p2,s1) = esSus(p1,p2,s2)))))))

Genero stock

Usa Bool, Nat, Conj(α)

Exporta Genero, Generadores, Observadores básicos, stocksBajos

Observadores básicos

estaRegistrado: producto x stock → bool

esSus: producto a x producto b x stock s → bool {estaRegistrado(a,s) ∧ estaRegistrado(b,s)}

compras: producto p x stock s → nat {estaRegistrado(p,s)}

ventas: producto p x stock s → nat {estaRegistrado(p,s)}

mínimo: producto p x stock s → nat {estaRegistrado(p,s)}

Generadores

crearStock: . → stock

registrarProducto: producto p x nat x stock s → stock {¬ estaRegistrado(p,s)}

comprar: nat x producto p x stock s → stock {estaRegistrado(p,s)}

vender: nat n x producto p x stock s → stock {estaRegistrado(p,s) ∧L compras(p,s) ≥ n}

infSus: producto a x producto b x stock s → stock {(estaRegistrado(a,s) ∧ estaRegistrado(b,s)) ∧L ¬(∃ p:producto)(esSus(p,b,s)) ∧ a ≠ b}

OtrasOperaciones

stocksBajos: stock → conj(producto)

tieneSus: producto p x stock s → bool {estaRegistrado(p,s)}

obtenerSus: producto p x stock s → producto {estaRegistrado(p,s) ∧L tieneSus(p,s)}

productos: stock → conj(producto)

quitarBuenos: conj(producto) x stock → conj(producto)

Axiomas

estaRegistrado(p,crearStock) ≡ false

estaRegistrado(p,registrarProducto(a,n,s)) ≡ p = a ∨ estaRegistrado(p,s)

estaRegistrado(p,comprar(n,a,s)) ≡ estaRegistrado(p,s)

estaRegistrado(p,vender(n,a,s)) ≡ estaRegistrado(p,s)

estaRegistrado(p,infSus(a,b,s)) ≡ estaRegistrado(p,s)

compras(p,comprar(n,a,s)) ≡ if p = a then n + compras(p,s) else compras(p,s) fi

compras(p,registrarProducto(a,n,s)) ≡ if p = a then 0 else compras(p,s) fi

compras(p,vender(n,a,s)) ≡ compras(p,s)

compras(p,infSus(a,b,s)) ≡ compras(p,s)

ventas(p,vender(n,a,s)) ≡ if p = a then n + ventas(p,s) else ventas(p,s) fi

ventas(p,registrarProducto(a,n,s)) ≡ if p = a then 0 else ventas(p,s) fi

ventas(p,comprar(n,a,s)) ≡ ventas(p,s)

ventas(p,infSus(n,a,s)) ≡ ventas(p,s)

esSus(a,b,registrarProducto(c,n,s)) ≡ if a = c ∨ b = c then false else esSus(a,b,s) fi

esSus(a,b,infSus(c,d,s)) ≡ (a = c ∧ b = d) ∨ esSus(a,b,s)

esSus(a,b,comprar(n,c,s)) ≡ esSus(a,b,s)

esSus(a,b,vender(n,c,s)) ≡ esSus(a,b,s)

mínimo(p,registrarProducto(a,n,s)) ≡ if p = a then n else mínimo(p,s) fi

mínimo(p,comprar(n,a,s)) ≡ mínimo(p,s)

mínimo(p,vender(n,a,s)) ≡ mínimo(p,s)

mínimo(p,infSus(a,b,s)) ≡ mínimo(p,s)

stocksBajos(s) ≡ quitarBuenos(productos(s),s)

productos(crearStock) ≡ ∅

productos(comprar(n,a,s)) ≡ productos(s)

productos(vender(n,a,s)) ≡ productos(s)

productos(registrarProducto(a,n,s)) ≡ Ag(a,productos(s))

productos(infSus(a,b,s)) ≡ productos(s)

tieneSus(p,registrarProducto(a,n,s)) ≡ (¬ p = a) ∧L tieneSus(p,s)

tieneSus(p,comprar(n,a,s)) ≡ tieneSus(p,s)

tieneSus(p,vender(n,a,s)) ≡ tieneSus(p,s)

tieneSus(p,infSus(a,b,s)) ≡ p = b ∨ tieneSus(p,s)

obtenerSus(p,infSus(a,b,s)) ≡ if p = b then a else obtenerSus(p,s) fi

obtenerSus(p,registrarPruducto(a,n,s)) ≡ obtenerSus(p,s)

obtenerSus(p,comprar(n,a,s)) ≡ obtenerSus(p,s)

obtenerSus(p,vender(n,a,s)) ≡ obtenerSus(p,s)

quitarBuenos(∅,s) ≡ ∅

quitarBuenos(Ag(p,c),s) ≡ if tieneSus(p,s) then if mínimo(p,s) > compras(p,s) + compras(obtenerSus(p,s),s) - ventas(p,s) - ventas(obtenerSus(p,s),s) then Ag(p,quitarBuenos(c,s)) else quitarBuenos(c,s) fi else if mínimo(p,s) > compras(p,s) - ventas(p,s) then Ag(p,quitarBuenos(c,s)) else quitarBuenos(c,s) fi

Fin TAD