Para hacer nuestro derivador de funciones primero definiremos un TAD
que permita representar expresiones de forma eficiente. Nos limitaremos
a expresiones que tengan sólo una variable (digamos x), números
naturales (para usar el TAD NAT), logaritmos, exponenciales, sumas, restas,
multiplicaciones, divisiones, senos, cosenos y potenciación.
A continuación se presentan las iniciales y constructoras de
nuestro TAD, al que llamaremos Expr :
ADT Expr [ ]INITIALS
varX : -> FUN /* Variable x */
num : NAT -> FUN /* Números */
CONSTRUCTORSmenos : FUN -> FUN /* Menos unario */
log : FUN -> FUN /* Logaritmo natural */
exp : FUN -> FUN /*
sen : FUN -> FUN
cos : FUN -> FUN
suma : FUN * FUN -> FUN
resta : FUN * FUN -> FUN
mult : FUN * FUN -> FUN
div : FUN * FUN -> FUN
pot : FUN * FUN -> FUN
SELECTORS
deriva : FUN(i)
-> FUN
reduce : FUN(i)
-> FUN
EQ_FUN : FUN(i) * FUN(i)
-> BOOL
AXIOMS
Deriva(X) = NUM(SUC(ZERO))
Deriva(NUM(N1)) = NUM(ZERO)
Deriva(Menos(F1)) = Menos(Deriva(F1))
Deriva(Log(F1)) = Div(Deriva(F1),F1)
Deriva(Exp(F1)) = Mult(Deriva(F1),Exp(F1))
Deriva(Sin(F1)) = Mult(Deriva(F1),Cos(F1))
Deriva(Cos(F1)) = Menos(Mult(Deriva(F1),Sin(F1)))
Deriva(Suma(F1,F2)) = Suma(Deriva(F1),Deriva(F2))
Deriva(Resta(F1,F2)) = Resta(Deriva(F1),Deriva(F2))
Deriva(Mult(F1,F2)) = Suma(Mult(Deriva(F1),F2),Mult(F1,Deriva(F2)))
Deriva(Div(F1,F2)) = Div(Resta(Mult(Deriva(F1),F2),Mult(F1,Deriva(F2))),Mult(F2$Deriva(Pot(F1,F2))
= Mult(Pot(F1,F2),Suma(Mult(Deriva(F2),Log(F1)),Div(Mult(F2,$
Reduce(X) = X
Reduce(NUM(N1)) = NUM(N1)
Reduce(Menos(NUM(ZERO))) = NUM(ZERO)
Reduce(Menos(F1)) = Menos(Reduce(F1))
Reduce(Log(NUM(SUC(ZERO)))) = NUM(ZERO)
Reduce(Log(Exp(F1))) = Reduce(F1)
Reduce(Log(F1)) = Log(Reduce(F1))
Reduce(Exp(NUM(ZERO))) = NUM(SUC(ZERO))
Reduce(Exp(Log(F1))) = Reduce(F1)
Reduce(Exp(F1)) = Exp(Reduce(F1))
Reduce(Sin(F1)) = Sin(Reduce(F1))
Reduce(Sin(NUM(ZERO))) = NUM(ZERO)
Reduce(Cos(F1)) = Cos(Reduce(F1))
Reduce(Cos(NUM(ZERO))) = NUM(SUC(ZERO))
Reduce(Suma(NUM(F1),NUM(F2))) = NUM(ADD(F1,F2))
Reduce(Suma(NUM(ZERO),F2)) = Reduce(F2)
Reduce(Suma(F1,NUM(ZERO))) = Reduce(F1)
Reduce(Suma(F1,F2)) = Suma(Reduce(F1),Reduce(F2))
Reduce(Resta(NUM(ZERO),F2)) = Menos(Reduce(F2))
Reduce(Resta(F2,NUM(ZERO))) = Reduce(F2)
Reduce(Resta(F1,F2)) = Resta(Reduce(F1),Reduce(F2))
Reduce(Mult(NUM(ZERO),F2)) = NUM(ZERO)
Reduce(Mult(F1,NUM(ZERO))) = NUM(ZERO)
Reduce(Mult(NUM(SUC(ZERO)),F2)) = Reduce(F2)
Reduce(Mult(F1,NUM(SUC(ZERO)))) = Reduce(F1)
Reduce(Mult(F1,F2)) = Mult(Reduce(F1),Reduce(F2))
Reduce(Div(F1,NUM(ZERO))) = ERROR
Reduce(Div(NUM(ZERO),F2)) = NUM(ZERO)
Reduce(Div(F1,NUM(SUC(ZERO)))) = Reduce(F1)
Reduce(Div(F1,F2)) = Div(Reduce(F1),Reduce(F2))
Reduce(Pot(NUM(ZERO),NUM(ZERO))) = ERROR
Reduce(Pot(F1,NUM(ZERO))) = NUM(SUC(ZERO))
Reduce(Pot(F1,NUM(SUC(ZERO)))) = Reduce(F1)
Reduce(Pot(NUM(SUC(ZERO)),F2)) = NUM(SUC(ZERO))
Reduce(Pot(F1,F2)) = Pot(Reduce(F1),Reduce(F2))
EQ_FUN(X,X) = TRUE
EQ_FUN(X,NUM(N1)) = FALSE
EQ_FUN(X,Menos(F1)) = FALSE
EQ_FUN(X,Log(F1)) = FALSE
EQ_FUN(X,Exp(F1)) = FALSE
EQ_FUN(X,Sin(F1)) = FALSE
Como EQ_FUN(X,Cos(F1)) = FALSE
EQ_FUN(X,Suma(F1,F2)) = FALSE
EQ_FUN(X,Resta(F1,F2)) = FALSE
EQ_FUN(X,Mult(F1,F2)) = FALSE
EQ_FUN(X,Div(F1,F2)) = FALSE
EQ_FUN(X,Pot(F1,F2)) = FALSE
EQ_FUN(NUM(N1),X) = FALSE
EQ_FUN(NUM(N1),NUM(N2)) = EQ_NAT(N1,N2)
EQ_FUN(NUM(N1),Menos(F2)) = FALSE
EQ_FUN(NUM(N1),Log(F2)) = FALSE
EQ_FUN(NUM(N1),Exp(F2)) = FALSE
EQ_FUN(NUM(N1),Sin(F2)) = FALSE
EQ_FUN(NUM(N1),Cos(F2)) = FALSE
EQ_FUN(NUM(N1),Suma(F2,F3)) = FALSE
EQ_FUN(NUM(N1),Resta(F2,F3)) = FALSE
EQ_FUN(NUM(N1),Mult(F2,F3)) = FALSE
EQ_FUN(NUM(N1),Div(F2,F3)) = FALSE
EQ_FUN(NUM(N1),Pot(F2,F3)) = FALSE
EQ_FUN(Menos(F1),X) = FALSE
EQ_FUN(Menos(F1),NUM(N2)) = FALSE
EQ_FUN(Menos(F1),Menos(F2)) = EQ_FUN(F1,F2)
EQ_FUN(Menos(F1),Log(F2)) = FALSE
EQ_FUN(Menos(F1),Exp(F2)) = FALSE
EQ_FUN(Menos(F1),Sin(F2)) = FALSE
EQ_FUN(Menos(F1),Cos(F2)) = FALSE
EQ_FUN(Menos(F1),Suma(F2,F3)) = FALSE
EQ_FUN(Menos(F1),Resta(F2,F3)) = FALSE
EQ_FUN(Menos(F1),Mult(F2,F3)) = FALSE
EQ_FUN(Menos(F1),Div(F2,F3)) = FALSE
EQ_FUN(Menos(F1),Pot(F2,F3)) = FALSE
EQ_FUN(Log(F1),X) = FALSE
EQ_FUN(Log(F1),NUM(N2)) = FALSE
EQ_FUN(Log(F1),Menos(F2)) = FALSE
EQ_FUN(Log(F1),Log(F2)) = EQ_FUN(F1,F2)
EQ_FUN(Log(F1),Exp(F2)) = FALSE
EQ_FUN(Log(F1),Sin(F2)) = FALSE
EQ_FUN(Log(F1),Cos(F2)) = FALSE
EQ_FUN(Log(F1),Suma(F2,F3)) = FALSE
EQ_FUN(Log(F1),Resta(F2,F3)) = FALSE
EQ_FUN(Log(F1),Mult(F2,F3)) = FALSE
EQ_FUN(Log(F1),Div(F2,F3)) = FALSE
EQ_FUN(Log(F1),Pot(F2,F3)) = FALSE
EQ_FUN(Exp(F1),X) = FALSE
EQ_FUN(Exp(F1),NUM(N2)) = FALSE
EQ_FUN(Exp(F1),Menos(F2)) = FALSE
EQ_FUN(Exp(F1),Log(F2)) = FALSE
EQ_FUN(Exp(F1),Exp(F2)) = EQ_FUN(F1,F2)
EQ_FUN(Exp(F1),Sin(F2)) = FALSE
EQ_FUN(Exp(F1),Cos(F2)) = FALSE
EQ_FUN(Exp(F1),Suma(F2,F3)) = FALSE
EQ_FUN(Exp(F1),Resta(F2,F3)) = FALSE
EQ_FUN(Exp(F1),Mult(F2,F3)) = FALSE
EQ_FUN(Exp(F1),Div(F2,F3)) = FALSE
EQ_FUN(Exp(F1),Pot(F2,F3)) = FALSE
EQ_FUN(Sin(F1),X) = FALSE
EQ_FUN(Sin(F1),NUM(N2)) = FALSE
EQ_FUN(Sin(F1),Menos(F2)) = FALSE
EQ_FUN(Sin(F1),Log(F2)) = FALSE
EQ_FUN(Sin(F1),Exp(F2)) = FALSE
EQ_FUN(Sin(F1),Sin(F2)) = EQ_FUN(F1,F2)
EQ_FUN(Sin(F1),Cos(F2)) = FALSE
EQ_FUN(Sin(F1),Suma(F2,F3)) = FALSE
EQ_FUN(Sin(F1),Resta(F2,F3)) = FALSE
EQ_FUN(Sin(F1),Mult(F2,F3)) = FALSE
EQ_FUN(Sin(F1),Div(F2,F3)) = FALSE
EQ_FUN(Sin(F1),Pot(F2,F3)) = FALSE
EQ_FUN(Cos(F1),X) = FALSE
EQ_FUN(Cos(F1),NUM(N2)) = FALSE
EQ_FUN(Cos(F1),Menos(F2)) = FALSE
EQ_FUN(Cos(F1),Log(F2)) = FALSE
EQ_FUN(Cos(F1),Exp(F2)) = FALSE
EQ_FUN(Cos(F1),Sin(F2)) = FALSE
EQ_FUN(Cos(F1),Cos(F2)) = EQ_FUN(F1,F2)
EQ_FUN(Cos(F1),Suma(F2,F3)) = FALSE
EQ_FUN(Cos(F1),Resta(F2,F3)) = FALSE
EQ_FUN(Cos(F1),Mult(F2,F3)) = FALSE
EQ_FUN(Cos(F1),Div(F2,F3)) = FALSE
EQ_FUN(Cos(F1),Pot(F2,F3)) = FALSE
EQ_FUN(Suma(F1,F2),X) = FALSE
EQ_FUN(Suma(F1,F2),NUM(N3)) = FALSE
EQ_FUN(Suma(F1,F2),Menos(F3)) = FALSE
EQ_FUN(Suma(F1,F2),Log(F3)) = FALSE
EQ_FUN(Suma(F1,F2),Exp(F3)) = FALSE
EQ_FUN(Suma(F1,F2),Sin(F3)) = FALSE
EQ_FUN(Suma(F1,F2),Cos(F3)) = FALSE
EQ_FUN(Suma(F1,F2),Suma(F3,F4)) = AND(EQ_FUN(F1,F3),EQ_FUN(F2,F4))
EQ_FUN(Suma(F1,F2),Resta(F3,F4)) = FALSE
EQ_FUN(Suma(F1,F2),Mult(F3,F4)) = FALSE
EQ_FUN(Suma(F1,F2),Div(F3,F4)) = FALSE
EQ_FUN(Suma(F1,F2),Pot(F3,F4)) = FALSE
EQ_FUN(Resta(F1,F2),X) = FALSE
EQ_FUN(Resta(F1,F2),NUM(N3)) = FALSE
EQ_FUN(Resta(F1,F2),Menos(F3)) = FALSE
EQ_FUN(Resta(F1,F2),Log(F3)) = FALSE
EQ_FUN(Resta(F1,F2),Exp(F3)) = FALSE
EQ_FUN(Resta(F1,F2),Sin(F3)) = FALSE
EQ_FUN(Resta(F1,F2),Cos(F3)) = FALSE
EQ_FUN(Resta(F1,F2),Suma(F3,F4)) = FALSE
EQ_FUN(Resta(F1,F2),Resta(F3,F4)) = AND(EQ_FUN(F1,F3),EQ_FUN(F2,F4))
EQ_FUN(Resta(F1,F2),Mult(F3,F4)) = FALSE
EQ_FUN(Resta(F1,F2),Div(F3,F4)) = FALSE
EQ_FUN(Resta(F1,F2),Pot(F3,F4)) = FALSE
EQ_FUN(Mult(F1,F2),X) = FALSE
EQ_FUN(Mult(F1,F2),NUM(N3)) = FALSE
EQ_FUN(Mult(F1,F2),Menos(F3)) = FALSE
EQ_FUN(Mult(F1,F2),Log(F3)) = FALSE
EQ_FUN(Mult(F1,F2),Exp(F3)) = FALSE
EQ_FUN(Mult(F1,F2),Sin(F3)) = FALSE
EQ_FUN(Mult(F1,F2),Cos(F3)) = FALSE
EQ_FUN(Mult(F1,F2),Suma(F3,F4)) = FALSE
EQ_FUN(Mult(F1,F2),Resta(F3,F4)) = FALSE
EQ_FUN(Mult(F1,F2),Mult(F3,F4)) = AND(EQ_FUN(F1,F3),EQ_FUN(F2,F4))
EQ_FUN(Mult(F1,F2),Div(F3,F4)) = FALSE
EQ_FUN(Mult(F1,F2),Pot(F3,F4)) = FALSE
EQ_FUN(Div(F1,F2),X) = FALSE
EQ_FUN(Div(F1,F2),NUM(N3)) = FALSE
EQ_FUN(Div(F1,F2),Menos(F3)) = FALSE
EQ_FUN(Div(F1,F2),Log(F3)) = FALSE
EQ_FUN(Div(F1,F2),Exp(F3)) = FALSE
EQ_FUN(Div(F1,F2),Sin(F3)) = FALSE
EQ_FUN(Div(F1,F2),Cos(F3)) = FALSE
EQ_FUN(Div(F1,F2),Suma(F3,F4)) = FALSE
EQ_FUN(Div(F1,F2),Resta(F3,F4)) = FALSE
EQ_FUN(Div(F1,F2),Mult(F3,F4)) = FALSE
EQ_FUN(Div(F1,F2),Div(F3,F4)) = AND(EQ_FUN(F1,F3),EQ_FUN(F2,F4))
EQ_FUN(Div(F1,F2),Pot(F3,F4)) = FALSE
EQ_FUN(Pot(F1,F2),X) = FALSE
EQ_FUN(Pot(F1,F2),NUM(N3)) = FALSE
EQ_FUN(Pot(F1,F2),Menos(F3)) = FALSE
EQ_FUN(Pot(F1,F2),Log(F3)) = FALSE
EQ_FUN(Pot(F1,F2),Exp(F3)) = FALSE
EQ_FUN(Pot(F1,F2),Sin(F3)) = FALSE
EQ_FUN(Pot(F1,F2),Cos(F3)) = FALSE
EQ_FUN(Pot(F1,F2),Suma(F3,F4)) = FALSE
EQ_FUN(Pot(F1,F2),Resta(F3,F4)) = FALSE
EQ_FUN(Pot(F1,F2),Mult(F3,F4)) = FALSE
EQ_FUN(Pot(F1,F2),Div(F3,F4)) = FALSE
EQ_FUN(Pot(F1,F2),Pot(F3,F4)) = AND(EQ_FUN(F1,F3),EQ_FUN(F2,F4))
ejemplo representaremos el TAD Cola con el TAD Pila, para lo cual primero debe definirse el TAD Cola y después representarse con el TAD Pila.
Signatura:
La ventaja de ser tan formales radicará en la posibilidad de
demostrar formalmente que los axiomas del TAD COL, siguen valiendo
una vez representados con el TAD PIL.
Salga del menú de tipos y entre al menú
de representaciones. Elija Nuevo, el sistema le pedirá entonces
el TAD que va a representar (para este ejemplo COL), y después
el TAD con el cual lo va a representar (en este caso PIL).
![]() Como nombre de la función de representación
puede emplear PC. Una representación puede
definirse como composición de otras dos o de forma inductiva, en
nuestro caso haremos una representación inductiva. El parámetro
X
del TAD PIL, corresponderá al paramétro
X
del TAD COL.
![]() Los programas de nuestra representación son:
adicCOL(PC(P1),X2) = PC(adicPIL(P1,X2)) elimCOL(PC(P1)) = PC(elimPIL(P1)) infoCOL(PC(P1)) = infoPIL(P1) esCOLVacia(PC(P1)) = esPILVacia(P1) EQ_COL(PC(P1),cp(P2)) = EQ_PIL(P1,P2) Una vez haya definido la representación, puede comprobar que los axiomas del TAD COL siguen valiendo. Elija Probar del menu de representaciones ![]() ManTa usará el demostrador para probar que los 10 axiomas del TAD COL valen con la representación. Después le permitirá examinar las pruebas en el editor de texto configurado.
|
En la versión 3.1 de ManTa las representaciones no se usan en el momento de generar código en C. Esta limitación se solucionará en una próxima versión de ManTa. Una vez completado el mecanismo, el usuario podrá definir TADs muy complejos y representarlos con TADs incluidos en el sistema que cuenten con una buena implementación en C, entonces el nuevo TAD tendrá la eficiencia del TAD con el cual se represente.