aboutsummaryrefslogtreecommitdiff
path: root/src/algebra/equation2.spad.pamphlet
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2007-08-14 05:14:52 +0000
committerdos-reis <gdr@axiomatics.org>2007-08-14 05:14:52 +0000
commitab8cc85adde879fb963c94d15675783f2cf4b183 (patch)
treec202482327f474583b750b2c45dedfc4e4312b1d /src/algebra/equation2.spad.pamphlet
downloadopen-axiom-ab8cc85adde879fb963c94d15675783f2cf4b183.tar.gz
Initial population.
Diffstat (limited to 'src/algebra/equation2.spad.pamphlet')
-rw-r--r--src/algebra/equation2.spad.pamphlet325
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}