Revisión actual |
Tu texto |
Línea 3: |
Línea 3: |
| === a === | | === a === |
|
| |
|
| duplicar: secu(α) → secu(α) | | duplicar: secu(α)→secu(α) |
|
| |
|
| duplicar(s) ≡ if vacía?(s) then ⟨⟩ else prim(s) • prim(s) • duplicar(fin(s)) fi | | duplicar(s)≡if vacía?(s) then ⟨⟩ else prim(s)•prim(s)•duplicar(fin(s)) fi |
|
| |
|
| === b === | | === b === |
Línea 11: |
Línea 11: |
| •≤•: secu(α) x secu(α) → bool | | •≤•: 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 | | 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 === | | === c === |
Línea 37: |
Línea 37: |
| buscar: secu(α) x secu(α) → nat | | buscar: secu(α) x secu(α) → nat |
|
| |
|
| buscar(⟨⟩,t) ≡ 0 | | buscar(⟨⟩,t) ≡ true |
|
| |
|
| buscar(s, t) ≡ if esPrefijo?(s, t) then 0 else 1 + buscar(s, fin(t)) fi | | buscar(e • s,t) ≡ if esPrefijo?(e • s,t) then 0 else 1 + buscar(e • s,fin(t)) fi |
|
| |
|
| === g === | | === g === |
Línea 50: |
Línea 50: |
|
| |
|
| === h === | | === 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: secu(α) so x α → secu(α) {estaOrdenada?(so)} |
|
| |
|
| insertarOrdenada(⟨⟩, e) ≡ e • ⟨⟩ | | insertarOrdenada(⟨⟩,a) ≡ a • ⟨⟩ |
|
| |
|
| insertarOrdenada(a • s, e) ≡ if e ≤ a then e • a • s else a • insertarOrdenada(s, e) fi | | insertarOrdenada(e • s,a) ≡ if a ≤ e then a • e • s else e • insertarOrdenada(s,a) fi |
|
| |
|
| === i === | | === i === |
Línea 77: |
Línea 75: |
| esPermutación?: secu(α) x secu(α) → bool | | esPermutación?: secu(α) x secu(α) → bool |
|
| |
|
| esPermutación?(s,t) ≡ if long(s) = long(t) then aux(s,s,t) else false | | esPermutación?(s,t) ≡ aux(s,s,t) |
|
| |
|
| === k === | | === k === |
Línea 83: |
Línea 81: |
| combinar: secu(α) a x secu(α) b → secu(α) {estaOrdenada?(a) ∧ estaOrdenada?(b)} | | 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 | | combinar(s,t) ≡ if vacía(s) then t else combinar(s,insertarOrdenada(t,prim(s)) fi |
|
| |
|
| == Ejercicio 2 == | | == Ejercicio 2 == |
Línea 151: |
Línea 149: |
| ntn: conj(secu(α)) x secu(α) → conj(secu(α)) | | ntn: conj(secu(α)) x secu(α) → conj(secu(α)) |
|
| |
|
| [ToDo]
| | blablabla |
| | |
| 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)''''', <small>a,b:α, s,t:secu(α)</small>
| |
| * → Definir '''''ntn(Ag(a • s, w), b • t)'''''<small>, w: conj(secu(α))</small>
| |
| | |
| * 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 == | | == Ejercicio 5 == |
Línea 171: |
Línea 160: |
|
| |
|
| === b === | | === 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
| | blablabla |
|
| |
| 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 == | | == Ejercicio 6 == |
Línea 194: |
Línea 167: |
| === a === | | === a === |
|
| |
|
| altura: rosetree(α) → nat
| | altura: rosetree(α) → nat |
|
| | |
| altura(rose(r, ⟨⟩)) ≡ 1
| | altura(rose(r,⟨⟩)) ≡ 1 |
|
| | |
| altura(rose(r, e • s)) ≡ 1 + altura(masAlta(r, e • s))
| | altura(rose(r,e • s)) ≡ 1 + altura(masAlta(r,e • s)) |
|
| | |
| masAlta: α x secu(rosetree(α)) → rosetree(α)
| | masAlta: α x secu(rosetree(α)) → rosetree(α) |
|
| | |
| masAlta(a, s) ≡ if vacía?(s) then
| | 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 |
| rose(a,⟨⟩)
| |
| else if altura(prim(s)) > altura(masAlta(a, fin(s))) then
| |
| prim(s)
| |
| else
| |
| masAlta(a, fin(s))
| |
| fi
| |
| fi
| |
|
| |
|
| === b === | | === b === |
|
| |
|
| cantHojas: rosetree(α) → nat
| | cantHojas: rosetree(α) → nat |
|
| | |
| cantHojas(r) ≡ if esHoja?(r) then
| | cantHojas(r) ≡ if esHoja?(r) then 1 else sumarHojas(hijos(r)) fi |
| 1
| | |
| else
| | esHoja?: rosetree(α) → bool |
| sumarHojas(hijos(r))
| | |
| fi
| | esHoja?(r) ≡ vacía?(hijos(r)) |
|
| | |
|
| | sumarHojas: secu(rosetree(α)) → nat |
| esHoja?: rosetree(α) → bool
| | |
|
| | sumarHojas(s) ≡ if vacía?(s) then 0 else cantHojas(prim(s)) + sumarHojas(fin(s)) fi |
| 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 === | | === c === |
|
| |
|
| podar: rosetree(α) a → rosetree(α) {¬esHoja?(a)}
| | podar: rosetree(α) a → rosetree(α) {¬esHoja?(a)} |
|
| | |
| podar(r) ≡ rose(raíz(r), podadora(hijos(r)))
| | podar(r) ≡ rose(raíz(r),podadora(hijos(r))) |
|
| | |
|
| | podadora: secu(rosetree(α)) → secu(rosetree(α)) |
| 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 |
| 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 === | | === d === |
|
| |
|
| obtenerRamas: rosetree(α) → secu(secu((α))
| | obtenerRamas: rosetree(α) → secu(secu((α)) |
|
| | |
| obtenerRamas(r) ≡ if esHoja?(r) then
| | 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 |
| (raíz(r) • ⟨⟩) •⟨⟩
| | |
| else
| | insertarTodos: α x secu(secu(α)) → secu(secu(α)) |
| if long(hijos(r)) = 1 then
| | |
| insertarTodos(raíz(r), obtenerRamas(prim(hijos(r))))
| | insertarTodos(a,s) ≡ if vacía(s) then ⟨⟩ else (a • prim(s)) • insertarTodos(a,fin(s)) fi |
| 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 === | | === e === |
Línea 356: |
Línea 291: |
| ''Usa'' Bool, Nat, Cinta | | ''Usa'' Bool, Nat, Cinta |
|
| |
|
| ''Exporta'' Genero, Generadores, Observadores básicos, Otras operaciones | | ''Exporta'' Genero, Generadores, Observadores, Otras operaciones |
|
| |
|
| ''Axiomas'' | | ''Axiomas'' |
Línea 420: |
Línea 355: |
| ''Usa'' Bool, Nat | | ''Usa'' Bool, Nat |
|
| |
|
| ''Exporta'' Genero, Generadores, Observadores básicos, Otras operaciones | | ''Exporta'' Genero, Generadores, Observadores, Otras operaciones |
|
| |
|
| ''Otras operaciones'' | | ''Otras operaciones'' |
Línea 491: |
Línea 426: |
|
| |
|
| == Ejercicio 12 == | | == 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'''
| |
|
| |
|
| == Ejercicio 13 == | | == Ejercicio 13 == |