p(x) = a₀ + a₁x + … + aₙxⁿ, n ∈ ℕ, aᵢ ∈ ℤ.IMPORTS Integer, lo que mueve la exponenciación entera potencia fuera de Polinomio — resolviendo el único warning V1 que tenía la versión anterior (V1 le pedía a potencia axiomas sobre los constructores de Polinomio, lo cual no tenía sentido).
IMPORTS Integer:
potencia(x, n) = xⁿ es exponenciación entera: una operación que pertenece al tipo Integer, no a Polinomio.Polinomio" sin axiomas sobre cero/anadir.Polinomio declara IMPORTS Integer y usa potencia como operación importada — sin declararla ni re-axiomatizarla. Separación correcta de responsabilidades: Polinomio conoce solo sus propias operaciones; la aritmética entera vive en Integer.cero — el polinomio nulo p(x) = 0.anadir(p, coef, grado) — añade el monomio coef·x^grado a p. Precondición grado ≥ 0 (los grados son naturales; además garantiza que potencia se invoque siempre con exponente ≥ 0).evaluar, coeficiente, suma — operaciones derivadas.anadir(anadir(…anadir(cero(), c₁, g₁)…, cₙ, gₙ)).
anadir admite agregar varios monomios del mismo grado; coeficiente los acumula (suma los coeficientes de igual grado). Por eso anadir(anadir(cero(), 2, 1), 3, 1) y anadir(cero(), 5, 1) son observacionalmente iguales: ambos dan coeficiente 5 en grado 1. La igualdad de polinomios es observacional (vía coeficiente / evaluar), no sintáctica.
CLASS Polinomio
IMPORTS Integer
BASIC CONSTRUCTORS cero, anadir
EFFECTIVE
TYPE Polinomio
OPERATIONS
-- ─── Constructores básicos ─────────────────────────────
-- cero: el polinomio nulo p(x) = 0.
cero: -> Polinomio;
-- anadir(p, coef, grado): añade el monomio coef·x^grado a p.
-- Precondición: el grado debe ser un natural (≥ 0).
-- (Esto garantiza que `potencia` se invoque solo con n ≥ 0.)
anadir: Polinomio(p) * Integer(coef) * Integer(grado) -> Polinomio
pre: grado >= 0;
-- ─── Operaciones derivadas ─────────────────────────────
-- evaluar(p, x): valor numérico de p evaluado en x.
evaluar: Polinomio * Integer -> Integer;
-- coeficiente(p, g): coeficiente del monomio de grado g.
coeficiente: Polinomio * Integer -> Integer;
-- suma(p, q): polinomio suma de p y q.
suma: Polinomio * Polinomio -> Polinomio;
-- Nota: `potencia: Integer * Integer -> Integer` es una
-- operación del tipo Integer (importada vía IMPORTS Integer),
-- así que NO se declara aquí.
AXIOMS p, q: Polinomio; x, c, g, g1: Integer;
-- ──────────────────────────────────────────────────────
-- evaluar(p, x): valor del polinomio en x.
-- evaluar(cero, x) = 0
-- evaluar(anadir(p,c,g), x) = c·x^g + evaluar(p, x)
-- Cada monomio aporta c·x^g (usando `potencia` de Integer);
-- el resto se evalúa recursivamente.
-- ──────────────────────────────────────────────────────
evaluar(cero(), x) = 0;
evaluar(anadir(p, c, g), x) =
(c * potencia(x, g)) + evaluar(p, x);
-- ──────────────────────────────────────────────────────
-- coeficiente(p, g): coeficiente del monomio de grado g.
-- coeficiente(cero, g) = 0
-- coeficiente(anadir(p,c,g1), g) =
-- si g1 = g → c + coeficiente(p, g) (acumula)
-- si g1 ≠ g → coeficiente(p, g)
-- La acumulación garantiza que anadir varios monomios del
-- mismo grado equivale a anadir uno con la suma de coefs.
-- ──────────────────────────────────────────────────────
coeficiente(cero(), g) = 0;
(g1 = g) implies
coeficiente(anadir(p, c, g1), g) = c + coeficiente(p, g);
not (g1 = g) implies
coeficiente(anadir(p, c, g1), g) = coeficiente(p, g);
-- ──────────────────────────────────────────────────────
-- suma(p, q): suma de dos polinomios.
-- Inducción sobre el segundo argumento — cada monomio de q
-- se añade, uno por uno, sobre p.
-- suma(p, cero) = p
-- suma(p, anadir(q, c, g)) = anadir(suma(p, q), c, g)
--
-- Correctitud: coeficiente(suma(p,q), g)
-- = coeficiente(p, g) + coeficiente(q, g) ∀ g.
-- ──────────────────────────────────────────────────────
suma(p, cero()) = p;
suma(p, anadir(q, c, g)) = anadir(suma(p, q), c, g);
END-CLASS
| Operación | Origen / tipo | Axiomas |
|---|---|---|
cero |
constructor básico de Polinomio |
— (valor primitivo) |
anadir |
constructor básico pre: grado ≥ 0 | — (constructor) |
evaluar |
derivada | 2 — base sobre cero (= 0) + recursiva sobre anadir (c·x^g + evaluar(p,x)) |
coeficiente |
derivada | 3 — base sobre cero (= 0) + 2 implies sobre anadir según g1 = g |
suma |
derivada | 2 — inducción sobre el 2.º argumento: base suma(p, cero) = p + recursiva |
potencia |
importada — operación del tipo Integer (IMPORTS Integer) |
— (definida y axiomatizada en Integer, no aquí) |
Representación como término:
p = anadir(anadir(cero(), 3, 0), 2, 2)
└── monomio 3·x⁰ └── monomio 2·x²
evaluar(p, 5)| Paso | Reescritura |
|---|---|
| 1 | evaluar(anadir(anadir(cero(),3,0), 2,2), 5)→ 2 * potencia(5, 2) + evaluar(anadir(cero(),3,0), 5) |
| 2 | potencia(5, 2) = 25 (operación de Integer, importada) |
| 3 | evaluar(anadir(cero(),3,0), 5)→ 3 * potencia(5, 0) + evaluar(cero(), 5) = 3 * 1 + 0 = 3 |
| 4 | Total: 2 * 25 + 3 = 50 + 3 = 53 |
Verificación: p(5) = 3 + 2·5² = 3 + 50 = 53 ✓
coeficiente(p, 2)| Paso | Reescritura |
|---|---|
| 1 | coeficiente(anadir(anadir(cero(),3,0), 2,2), 2)g1 = 2, g = 2 → g1 = g ✓ → 2 + coeficiente(anadir(cero(),3,0), 2) |
| 2 | coeficiente(anadir(cero(),3,0), 2) g1 = 0, g = 2 → g1 ≠ g → coeficiente(cero(), 2) |
| 3 | coeficiente(cero(), 2) = 0 |
| 4 | Total: 2 + 0 = 2 ✓ (coeficiente de x²) |
suma(p, q) con q = 7xSea q = anadir(cero(), 7, 1) (el monomio 7·x¹):
suma(p, anadir(cero(), 7, 1)) = anadir(suma(p, cero()), 7, 1) -- axioma recursivo de suma = anadir(p, 7, 1) -- axioma base: suma(p, cero) = p = anadir(anadir(anadir(cero(),3,0), 2,2), 7, 1)
El resultado representa 3 + 7x + 2x². Verificación vía coeficiente:
| Grado | coeficiente(suma(p,q), g) | coef(p,g) + coef(q,g) |
|---|---|---|
| 0 | 3 | 3 + 0 = 3 ✓ |
| 1 | 7 | 0 + 7 = 7 ✓ |
| 2 | 2 | 2 + 0 = 2 ✓ |
suma: para todo grado g se cumple
coeficiente(suma(p, q), g) = coeficiente(p, g) + coeficiente(q, g).
Demostrable por inducción sobre q:
q = cero): coeficiente(suma(p, cero), g) = coeficiente(p, g) = coeficiente(p,g) + 0 = coeficiente(p,g) + coeficiente(cero,g).q = anadir(q', c, g')): coeficiente(anadir(suma(p,q'),c,g'), g) distribuye en los dos casos de coeficiente; por hipótesis inductiva coeficiente(suma(p,q'),g) = coeficiente(p,g)+coeficiente(q',g), y el monomio c se suma exactamente cuando g' = g — igual que en coeficiente(anadir(q',c,g'),g).evaluar ↔ coeficiente: evaluar(p, x) coincide con la suma Σ coeficiente(p, g)·x^g sobre todos los grados g presentes — porque ambos recorren la misma estructura de monomios. Esto valida que las dos "vistas observacionales" del polinomio son coherentes.
coeficiente: el axioma del caso g1 = g usa c + coeficiente(p, g) (no simplemente c). Esto hace que agregar dos monomios del mismo grado — anadir(anadir(cero(), 2, 1), 3, 1) — sea observacionalmente igual a agregar uno solo con el coeficiente sumado — anadir(cero(), 5, 1). La representación no canónica queda "normalizada" a nivel observacional.
IMPORTS: potencia no figura en OPERATIONS ni en AXIOMS de Polinomio. Es una operación del tipo Integer, importada. Polinomio la usa en el axioma de evaluar pero su definición y sus axiomas (potencia(x,0)=1, potencia(x,n)=x·potencia(x,n-1)) son responsabilidad de Integer. Esta es la forma correcta de modularizar: cada TDA conoce solo sus propias operaciones.