\documentclass{article} \usepackage{open-axiom} \begin{document} \title{\$SPAD/src/algebra equation2.spad} \author{Stephen M. Watt, Johannes Grabmeier} \maketitle \begin{abstract} \end{abstract} \tableofcontents \eject \section{domain EQ Equation} <>= import Type import SetCategory import AbelianSemiGroup import AbelianGroup import SemiGroup import Monoid import CoercibleTo Boolean import InnerEvalable import CommutativeRing import PartialDifferentialRing import Field import VectorSpace import Symbol import OutputForm import List )abbrev domain EQ Equation --FOR THE BENEFIT OF LIBAX0 GENERATION ++ Author: Stephen M. Watt, enhancements by Johannes Grabmeier ++ Date Created: April 1985 ++ Date Last Updated: May 19, 2013. ++ Basic Operations: = ++ Related Domains: ++ Also See: ++ AMS Classifications: ++ Keywords: equation ++ Examples: ++ References: ++ Description: ++ Equations as mathematical objects. All properties of the basis domain, ++ e.g. being an abelian group are carried over the equation domain, by ++ performing the structural operations on the left and on the ++ right hand side. -- The interpreter translates "=" to "equation". Otherwise, it will -- find a modemap for "=" in the domain of the arguments. Equation(S: Type): public == private where Ex ==> OutputForm public == Functorial S with =: (S, S) -> $ ++ a=b creates an equation. equation: (S, S) -> $ ++ equation(a,b) creates an equation. swap: $ -> $ ++ swap(eq) interchanges left and right hand side of equation eq. lhs: $ -> S ++ lhs(eqn) returns the left hand side of equation eqn. rhs: $ -> S ++ rhs(eqn) returns the right hand side of equation eqn. if S has InnerEvalable(Symbol,S) then InnerEvalable(Symbol,S) if S has SetCategory then SetCategory CoercibleTo Boolean if S has Evalable(S) then eval: ($, $) -> $ ++ eval(eqn, x=f) replaces x by f in equation eqn. eval: ($, List $) -> $ ++ eval(eqn, [x1=v1, ... xn=vn]) replaces xi by vi in equation eqn. if S has AbelianSemiGroup then AbelianSemiGroup +: (S, $) -> $ ++ x+eqn produces a new equation by adding x to both sides of ++ equation eqn. +: ($, S) -> $ ++ eqn+x produces a new equation by adding x to both sides of ++ equation eqn. if S has AbelianGroup then AbelianGroup leftZero : $ -> $ ++ leftZero(eq) subtracts the left hand side. rightZero : $ -> $ ++ rightZero(eq) subtracts the right hand side. -: (S, $) -> $ ++ x-eqn produces a new equation by subtracting both sides of ++ equation eqn from x. -: ($, S) -> $ ++ eqn-x produces a new equation by subtracting x from both sides of ++ equation eqn. if S has SemiGroup then SemiGroup *: (S, $) -> $ ++ x*eqn produces a new equation by multiplying both sides of ++ equation eqn by x. *: ($, S) -> $ ++ eqn*x produces a new equation by multiplying both sides of ++ equation eqn by x. if S has Monoid then Monoid leftOne : $ -> Union($,"failed") ++ leftOne(eq) divides by the left hand side, if possible. rightOne : $ -> Union($,"failed") ++ rightOne(eq) divides by the right hand side, if possible. if S has Group then Group leftOne : $ -> Union($,"failed") ++ leftOne(eq) divides by the left hand side. rightOne : $ -> Union($,"failed") ++ rightOne(eq) divides by the right hand side. if S has Ring then Ring BiModule(S,S) if S has CommutativeRing then Module(S) --Algebra(S) if S has IntegralDomain then factorAndSplit : $ -> List $ ++ factorAndSplit(eq) make the right hand side 0 and ++ factors the new left hand side. Each factor is equated ++ to 0 and put into the resulting list without repetitions. if S has PartialDifferentialRing(Symbol) then PartialDifferentialRing(Symbol) if S has Field then VectorSpace(S) /: ($, $) -> $ ++ e1/e2 produces a new equation by dividing the left and right ++ hand sides of equations e1 and e2. inv: $ -> $ ++ inv(x) returns the multiplicative inverse of x. if S has ExpressionSpace then subst: ($, $) -> $ ++ subst(eq1,eq2) substitutes eq2 into both sides of eq1 ++ the lhs of eq2 should be a kernel private ==> add Rep := Record(lhs: S, rhs: S) eq1,eq2: $ s : S l:S = r:S == [l, r] equation(l, r) == [l, r] -- hack! See comment above. lhs eqn == eqn.lhs rhs eqn == eqn.rhs swap eqn == [rhs eqn, lhs eqn] map(fn, eqn) == equation(fn(eqn.lhs), fn(eqn.rhs)) if S has InnerEvalable(Symbol,S) then s:Symbol ls:List Symbol x:S lx:List S eval(eqn,s,x) == eval(eqn.lhs,s,x) = eval(eqn.rhs,s,x) eval(eqn,ls,lx) == eval(eqn.lhs,ls,lx) = eval(eqn.rhs,ls,lx) if S has Evalable(S) then eval(eqn1:$, eqn2:$):$ == eval(eqn1.lhs, eqn2 pretend Equation S) = eval(eqn1.rhs, eqn2 pretend Equation S) eval(eqn1:$, leqn2:List $):$ == eval(eqn1.lhs, leqn2 pretend List Equation S) = eval(eqn1.rhs, leqn2 pretend List Equation S) if S has SetCategory then eq1 = eq2 == (eq1.lhs = eq2.lhs)@Boolean and (eq1.rhs = eq2.rhs)@Boolean coerce(eqn:$):Ex == eqn.lhs::Ex = eqn.rhs::Ex coerce(eqn:$):Boolean == eqn.lhs = eqn.rhs if S has AbelianSemiGroup then eq1 + eq2 == eq1.lhs + eq2.lhs = eq1.rhs + eq2.rhs s + eq2 == [s,s] + eq2 eq1 + s == eq1 + [s,s] if S has AbelianGroup then - eq == (- lhs eq) = (-rhs eq) s - eq2 == [s,s] - eq2 eq1 - s == eq1 - [s,s] leftZero eq == 0 = rhs eq - lhs eq rightZero eq == lhs eq - rhs eq = 0 0 == equation(0$S,0$S) eq1 - eq2 == eq1.lhs - eq2.lhs = eq1.rhs - eq2.rhs if S has SemiGroup then eq1:$ * eq2:$ == eq1.lhs * eq2.lhs = eq1.rhs * eq2.rhs l:S * eqn:$ == l * eqn.lhs = l * eqn.rhs eqn:$ * l:S == eqn.lhs * l = eqn.rhs * l -- We have to be a bit careful here: raising to a +ve integer is OK -- (since it's the equivalent of repeated multiplication) -- but other powers may cause contradictions -- Watch what else you add here! JHD 2/Aug 1990 if S has Monoid then 1 == equation(1$S,1$S) recip eq == (lh := recip lhs eq) case "failed" => "failed" (rh := recip rhs eq) case "failed" => "failed" [lh :: S, rh :: S] leftOne eq == (re := recip lhs eq) case "failed" => "failed" 1 = rhs eq * re rightOne eq == (re := recip rhs eq) case "failed" => "failed" lhs eq * re = 1 if S has Group then inv eq == [inv lhs eq, inv rhs eq] leftOne eq == 1 = rhs eq * inv rhs eq rightOne eq == lhs eq * inv rhs eq = 1 if S has Ring then characteristic == characteristic$S i:Integer * eq:$ == (i::S) * eq if S has IntegralDomain then factorAndSplit eq == (S has factor : S -> Factored S) => eq0 := rightZero eq [equation(rcf.factor,0) for rcf in factors factor lhs eq0] (S is Polynomial Integer) => eq0 := rightZero eq MF ==> MultivariateFactorize(Symbol, IndexedExponents Symbol, _ Integer, Polynomial Integer) p : Polynomial Integer := (lhs eq0) pretend Polynomial Integer [equation((rcf.factor) pretend S,0) for rcf in factors factor(p)$MF] [eq] if S has PartialDifferentialRing(Symbol) then differentiate(eq:$, sym:Symbol):$ == [differentiate(lhs eq, sym), differentiate(rhs eq, sym)] if S has Field then dimension() == 2 :: CardinalNumber eq1:$ / eq2:$ == eq1.lhs / eq2.lhs = eq1.rhs / eq2.rhs inv eq == [inv lhs eq, inv rhs eq] if S has ExpressionSpace then subst(eq1,eq2) == eq3 := eq2 pretend Equation S [subst(lhs eq1,eq3),subst(rhs eq1,eq3)] @ \section{package EQ2 EquationFunctions2} <>= import Type import Equation )abbrev package EQ2 EquationFunctions2 ++ Author: ++ Date Created: ++ Date Last Updated: June 3, 1991 ++ Basic Operations: ++ Related Domains: Equation ++ Also See: ++ AMS Classifications: ++ Keywords: equation ++ Examples: ++ References: ++ Description: ++ This package provides operations for mapping the sides of equations. EquationFunctions2(S: Type, R: Type): with map: (S ->R ,Equation S) -> Equation R ++ map(f,eq) returns an equation where f is applied to the sides of eq == add map(fn, eqn) == equation(fn lhs eqn, fn rhs eqn) @ \section{category FEVALAB FullyEvalableOver} <>= import SetCategory import Eltable import Evalable import InnerEvalable import Symbol import List import Equation )abbrev category FEVALAB FullyEvalableOver ++ Author: ++ Date Created: ++ Date Last Updated: May 19, 2013 ++ Basic Operations: ++ Related Domains: Equation ++ Also See: ++ AMS Classifications: ++ Keywords: equation ++ Examples: ++ References: ++ Description: ++ This category provides a selection of evaluation operations ++ depending on what the argument type R provides. FullyEvalableOver(R:SetCategory): Category == Functorial R with if R has Eltable(R, R) then Eltable(R, $) if R has Evalable(R) then Evalable(R) if R has InnerEvalable(Symbol, R) then InnerEvalable(Symbol, R) add if R has Eltable(R, R) then elt(x:$, r:R) == map(#1.r, x) if R has Evalable(R) then eval(x:$, l:List Equation R) == map(eval(#1, l), x) if R has InnerEvalable(Symbol, R) then eval(x:$, ls:List Symbol, lv:List R) == map(eval(#1, ls, lv), x) @ \section{License} <>= --Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. --All rights reserved. --Copyright (C) 2007-2013, Gabriel Dos Reis. --All rights reserved. -- --Redistribution and use in source and binary forms, with or without --modification, are permitted provided that the following conditions are --met: -- -- - Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- -- - Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in -- the documentation and/or other materials provided with the -- distribution. -- -- - Neither the name of The Numerical ALgorithms Group Ltd. nor the -- names of its contributors may be used to endorse or promote products -- derived from this software without specific prior written permission. -- --THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS --IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED --TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A --PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER --OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, --EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, --PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR --PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF --LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING --NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS --SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. @ <<*>>= <> <> <> <> @ \eject \begin{thebibliography}{99} \bibitem{1} nothing \end{thebibliography} \end{document}