aboutsummaryrefslogtreecommitdiff
path: root/src/algebra/equation2.spad.pamphlet
blob: a621d9f970f72d8630e861d32d3577fe99b249d2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
\documentclass{article}
\usepackage{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}

<<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: 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
    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}

<<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}

<<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: 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}