diff options
Diffstat (limited to 'src/algebra/equation2.spad.pamphlet')
-rw-r--r-- | src/algebra/equation2.spad.pamphlet | 325 |
1 files changed, 325 insertions, 0 deletions
diff --git a/src/algebra/equation2.spad.pamphlet b/src/algebra/equation2.spad.pamphlet new file mode 100644 index 00000000..8ae385bb --- /dev/null +++ b/src/algebra/equation2.spad.pamphlet @@ -0,0 +1,325 @@ +\documentclass{article} +\usepackage{axiom} +\begin{document} +\title{\$SPAD/src/algebra equation2.spad} +\author{Stephen M. Watt, Johannes Grabmeier} +\maketitle +\begin{abstract} +\end{abstract} +\eject +\tableofcontents +\eject +\section{domain EQ Equation} +<<domain EQ Equation>>= +)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: June 3, 1991; September 2, 1992 +++ 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 ==> Type 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. + map: (S -> S, $) -> $ + ++ map(f,eqn) constructs a new equation by applying f to both + ++ sides of 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 + 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] + [eq] + 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 + 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 has 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} +<<package EQ2 EquationFunctions2>>= +)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} +<<category FEVALAB FullyEvalableOver>>= +)abbrev category FEVALAB FullyEvalableOver +++ Author: +++ Date Created: +++ Date Last Updated: June 3, 1991 +++ 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 == with + map: (R -> R, $) -> $ + ++ map(f, ex) evaluates ex, applying f to values of type R in ex. + 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} +<<license>>= +--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. +--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. +@ +<<*>>= +<<license>> + +<<domain EQ Equation>> +<<package EQ2 EquationFunctions2>> +<<category FEVALAB FullyEvalableOver>> +@ +\eject +\begin{thebibliography}{99} +\bibitem{1} nothing +\end{thebibliography} +\end{document} |