build open-axiom
--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.
)abbrev category DVARCAT DifferentialVariableCategory
++ Author: William Sit
++ Date Created: 19 July 1990
++ Date Last Updated: 13 September 1991
++ Basic Operations:
++ Related Constructors:DifferentialPolynomialCategory
++ See Also:OrderedDifferentialVariable,
++ SequentialDifferentialVariable,
++ DifferentialSparseMultivariatePolynomial.
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, ranking, order, weight
++ References:Ritt, J.F. "Differential Algebra" (Dover, 1950).
++ Description:
++ \spadtype{DifferentialVariableCategory} constructs the
++ set of derivatives of a given set of
++ (ordinary) differential indeterminates.
++ If x,...,y is an ordered set of differential indeterminates,
++ and the prime notation is used for differentiation, then
++ the set of derivatives (including
++ zero-th order) of the differential indeterminates is
++ x,\spad{x'},\spad{x''},..., y,\spad{y'},\spad{y''},...
++ (Note: in the interpreter, the n-th derivative of y is displayed as
++ y with a subscript n.) This set is
++ viewed as a set of algebraic indeterminates, totally ordered in a
++ way compatible with differentiation and the given order on the
++ differential indeterminates. Such a total order is called a
++ ranking of the differential indeterminates.
++
++ A domain in this category is needed to construct a differential
++ polynomial domain. Differential polynomials are ordered
++ by a ranking on the derivatives, and by an order (extending the
++ ranking) on
++ on the set of differential monomials. One may thus associate
++ a domain in this category with a ranking of the differential
++ indeterminates, just as one associates a domain in the category
++ \spadtype{OrderedAbelianMonoidSup} with an ordering of the set of
++ monomials in a set of algebraic indeterminates. The ranking
++ is specified through the binary relation \spadfun{<}.
++ For example, one may define
++ one derivative to be less than another by lexicographically comparing
++ first the \spadfun{order}, then the given order of the differential
++ indeterminates appearing in the derivatives. This is the default
++ implementation.
++
++ The notion of weight generalizes that of degree. A
++ polynomial domain may be made into a graded ring
++ if a weight function is given on the set of indeterminates,
++ Very often, a grading is the first step in ordering the set of
++ monomials. For differential polynomial domains, this
++ constructor provides a function \spadfun{weight}, which
++ allows the assignment of a non-negative number to each derivative of a
++ differential indeterminate. For example, one may define
++ the weight of a derivative to be simply its \spadfun{order}
++ (this is the default assignment).
++ This weight function can then be extended to the set of
++ all differential polynomials, providing a graded ring
++ structure.
DifferentialVariableCategory(S:OrderedSet): Category ==
Join(OrderedSet, DifferentialSpace, RetractableTo S) with
-- Examples:
-- v:=makeVariable('s,5)
makeVariable : (S, NonNegativeInteger) -> $
++ makeVariable(s, n) returns the n-th derivative of a
++ differential indeterminate s as an algebraic indeterminate.
-- Example: makeVariable('s, 5)
order : $ -> NonNegativeInteger
++ order(v) returns n if v is the n-th derivative of any
++ differential indeterminate.
-- Example: order(v)
variable : $ -> S
++ variable(v) returns s if v is any derivative of the differential
++ indeterminate s.
-- Example: variable(v)
-- default implementation using above primitives --
weight : $ -> NonNegativeInteger
++ weight(v) returns the weight of the derivative v.
-- Example: weight(v)
add
import NumberFormats
coerce (s:S):$ == makeVariable(s, 0)
differentiate v == differentiate(v, 1)
differentiate(v, n) == makeVariable(variable v, n + order v)
retractIfCan v == (zero?(order v) => variable v; "failed")
v = u == (variable v = variable u) and (order v = order u)
coerce(v:$):OutputForm ==
a := variable(v)::OutputForm
zero?(nn := order v) => a
sub(a, outputForm nn)
retract v ==
zero?(order v) => variable v
error "Not retractable"
v < u ==
-- the ranking below is orderly, and is the default --
order v = order u => variable v < variable u
order v < order u
weight v == order v
-- the default weight is just the order
)abbrev domain ODVAR OrderlyDifferentialVariable
++ Author: William Sit
++ Date Created: 19 July 1990
++ Date Last Updated: 13 September 1991
++ Basic Operations:differentiate, order, variable,<
++ Related Domains: OrderedVariableList,
++ SequentialDifferentialVariable.
++ See Also: DifferentialVariableCategory
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, orderly ranking.
++ References:Kolchin, E.R. "Differential Algebra and Algebraic Groups"
++ (Academic Press, 1973).
++ Description:
++ \spadtype{OrderlyDifferentialVariable} adds a commonly used orderly
++ ranking to the set of derivatives of an ordered list of differential
++ indeterminates. An orderly ranking is a ranking \spadfun{<} of the
++ derivatives with the property that for two derivatives u and v,
++ u \spadfun{<} v if the \spadfun{order} of u is less than that
++ of v.
++ This domain belongs to \spadtype{DifferentialVariableCategory}. It
++ defines \spadfun{weight} to be just \spadfun{order}, and it
++ defines an orderly ranking \spadfun{<} on derivatives u via the
++ lexicographic order on the pair
++ (\spadfun{order}(u), \spadfun{variable}(u)).
OrderlyDifferentialVariable(S:OrderedSet):DifferentialVariableCategory(S)
== add
Rep := Record(var:S, ord:NonNegativeInteger)
makeVariable(s,n) == [s, n]
variable v == v.var
order v == v.ord
)abbrev domain SDVAR SequentialDifferentialVariable
++ Author: William Sit
++ Date Created: 19 July 1990
++ Date Last Updated: 13 September 1991
++ Basic Operations:differentiate, order, variable, <
++ Related Domains: OrderedVariableList,
++ OrderlyDifferentialVariable.
++ See Also:DifferentialVariableCategory
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, sequential ranking.
++ References:Kolchin, E.R. "Differential Algebra and Algebraic Groups"
++ (Academic Press, 1973).
++ Description:
++ \spadtype{OrderlyDifferentialVariable} adds a commonly used sequential
++ ranking to the set of derivatives of an ordered list of differential
++ indeterminates. A sequential ranking is a ranking \spadfun{<} of the
++ derivatives with the property that for any derivative v,
++ there are only a finite number of derivatives u with u \spadfun{<} v.
++ This domain belongs to \spadtype{DifferentialVariableCategory}. It
++ defines \spadfun{weight} to be just \spadfun{order}, and it
++ defines a sequential ranking \spadfun{<} on derivatives u by the
++ lexicographic order on the pair
++ (\spadfun{variable}(u), \spadfun{order}(u)).
SequentialDifferentialVariable(S:OrderedSet):DifferentialVariableCategory(S)
== add
Rep := Record(var:S, ord:NonNegativeInteger)
makeVariable(s,n) == [s, n]
variable v == v.var
order v == v.ord
v < u ==
variable v = variable u => order v < order u
variable v < variable u
)abbrev category DPOLCAT DifferentialPolynomialCategory
++ Author: William Sit
++ Date Created: 19 July 1990
++ Date Last Updated: 13 September 1991
++ Basic Operations:PolynomialCategory
++ Related Constructors:DifferentialVariableCategory
++ See Also:
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, ranking, differential polynomials,
++ order, weight, leader, separant, initial, isobaric
++ References:Kolchin, E.R. "Differential Algebra and Algebraic Groups"
++ (Academic Press, 1973).
++ Description:
++ \spadtype{DifferentialPolynomialCategory} is a category constructor
++ specifying basic functions in an ordinary differential polynomial
++ ring with a given ordered set of differential indeterminates.
++ In addition, it implements defaults for the basic functions.
++ The functions \spadfun{order} and \spadfun{weight} are extended
++ from the set of derivatives of differential indeterminates
++ to the set of differential polynomials. Other operations
++ provided on differential polynomials are
++ \spadfun{leader}, \spadfun{initial},
++ \spadfun{separant}, \spadfun{differentialVariables}, and
++ \spadfun{isobaric?}. Furthermore, if the ground ring is
++ a differential ring, then evaluation (substitution
++ of differential indeterminates by elements of the ground ring
++ or by differential polynomials) is
++ provided by \spadfun{eval}.
++ A convenient way of referencing derivatives is provided by
++ the functions \spadfun{makeVariable}.
++
++ To construct a domain using this constructor, one needs
++ to provide a ground ring R, an ordered set S of differential
++ indeterminates, a ranking V on the set of derivatives
++ of the differential indeterminates, and a set E of
++ exponents in bijection with the set of differential monomials
++ in the given differential indeterminates.
++
DifferentialPolynomialCategory(R:Ring,S:OrderedSet,
V:DifferentialVariableCategory S, E:OrderedAbelianMonoidSup):
Category ==
Join(PolynomialCategory(R,E,V),
DifferentialExtension R, RetractableTo S) with
-- Examples:
-- s:=makeVariable('s)
-- p:= 3*(s 1)**2 + s*(s 2)**3
-- all functions below have default implementations
-- using primitives from V
makeVariable: S -> (NonNegativeInteger -> $)
++ makeVariable(s) views s as a differential
++ indeterminate, in such a way that the n-th
++ derivative of s may be simply referenced as z.n
++ where z :=makeVariable(s).
++ Note: In the interpreter, z is
++ given as an internal map, which may be ignored.
-- Example: makeVariable('s); %.5
differentialVariables: $ -> List S
++ differentialVariables(p) returns a list of differential
++ indeterminates occurring in a differential polynomial p.
order : ($, S) -> NonNegativeInteger
++ order(p,s) returns the order of the differential
++ polynomial p in differential indeterminate s.
order : $ -> NonNegativeInteger
++ order(p) returns the order of the differential polynomial p,
++ which is the maximum number of differentiations of a
++ differential indeterminate, among all those appearing in p.
degree: ($, S) -> NonNegativeInteger
++ degree(p, s) returns the maximum degree of
++ the differential polynomial p viewed as a differential polynomial
++ in the differential indeterminate s alone.
weights: $ -> List NonNegativeInteger
++ weights(p) returns a list of weights of differential monomials
++ appearing in differential polynomial p.
weight: $ -> NonNegativeInteger
++ weight(p) returns the maximum weight of all differential monomials
++ appearing in the differential polynomial p.
weights: ($, S) -> List NonNegativeInteger
++ weights(p, s) returns a list of
++ weights of differential monomials
++ appearing in the differential polynomial p when p is viewed
++ as a differential polynomial in the differential indeterminate s
++ alone.
weight: ($, S) -> NonNegativeInteger
++ weight(p, s) returns the maximum weight of all differential
++ monomials appearing in the differential polynomial p
++ when p is viewed as a differential polynomial in
++ the differential indeterminate s alone.
isobaric?: $ -> Boolean
++ isobaric?(p) returns true if every differential monomial appearing
++ in the differential polynomial p has same weight,
++ and returns false otherwise.
leader: $ -> V
++ leader(p) returns the derivative of the highest rank
++ appearing in the differential polynomial p
++ Note: an error occurs if p is in the ground ring.
initial:$ -> $
++ initial(p) returns the
++ leading coefficient when the differential polynomial p
++ is written as a univariate polynomial in its leader.
separant:$ -> $
++ separant(p) returns the
++ partial derivative of the differential polynomial p
++ with respect to its leader.
if R has DifferentialRing then
InnerEvalable(S, R)
InnerEvalable(S, $)
Evalable $
makeVariable: $ -> (NonNegativeInteger -> $)
++ makeVariable(p) views p as an element of a differential
++ ring, in such a way that the n-th
++ derivative of p may be simply referenced as z.n
++ where z := makeVariable(p).
++ Note: In the interpreter, z is
++ given as an internal map, which may be ignored.
-- Example: makeVariable(p); %.5; makeVariable(%**2); %.2
add
p:$
s:S
makeVariable s == makeVariable(s,#1)::$
if R has IntegralDomain then
differentiate(p:$, d:R -> R) ==
ans:$ := 0
l := variables p
u : Union(R, "failed")
while (u:=retractIfCan(p)@Union(R, "failed")) case "failed" repeat
t := leadingMonomial p
lc := leadingCoefficient t
ans := ans + d(lc)::$ * (t exquo lc)::$
+ +/[differentiate(t, v) * (differentiate v)::$ for v in l]
p := reductum p
ans + d(u::R)::$
order (p:$):NonNegativeInteger ==
ground? p => 0
"max"/[order v for v in variables p]
order (p:$,s:S):NonNegativeInteger ==
ground? p => 0
empty? (vv:= [order v for v in variables p | (variable v) = s ]) => 0
"max"/vv
degree (p, s) ==
d:NonNegativeInteger:=0
for lp in monomials p repeat
lv:= [v for v in variables lp | (variable v) = s ]
if not empty? lv then d:= max(d, +/degree(lp, lv))
d
weights p ==
ws:List NonNegativeInteger := nil
empty? (mp:=monomials p) => ws
for lp in mp repeat
lv:= variables lp
if not empty? lv then
dv:= degree(lp, lv)
w:=+/[(weight v) * d for v in lv for d in dv]$(List NonNegativeInteger)
ws:= concat(ws, w)
ws
weight p ==
empty? (ws:=weights p) => 0
"max"/ws
weights (p, s) ==
ws:List NonNegativeInteger := nil
empty?(mp:=monomials p) => ws
for lp in mp repeat
lv:= [v for v in variables lp | (variable v) = s ]
if not empty? lv then
dv:= degree(lp, lv)
w:=+/[(weight v) * d for v in lv for d in dv]$(List NonNegativeInteger)
ws:= concat(ws, w)
ws
weight (p,s) ==
empty? (ws:=weights(p,s)) => 0
"max"/ws
isobaric? p == (# removeDuplicates weights p) = 1
leader p == -- depends on the ranking
vl:= variables p
-- it's not enough just to look at leadingMonomial p
-- the term-ordering need not respect the ranking
empty? vl => error "leader is not defined "
"max"/vl
initial p == leadingCoefficient univariate(p,leader p)
separant p == differentiate(p, leader p)
coerce(s:S):$ == s::V::$
retractIfCan(p:$):Union(S, "failed") ==
(v := retractIfCan(p)@Union(V,"failed")) case "failed" => "failed"
retractIfCan(v::V)
differentialVariables p ==
removeDuplicates [variable v for v in variables p]
if R has DifferentialRing then
makeVariable p == differentiate(p, #1)
eval(p:$, sl:List S, rl:List R) ==
ordp:= order p
vl := concat [[makeVariable(s,j)$V for j in 0..ordp]
for s in sl]$List(List V)
rrl:=nil$List(R)
for r in rl repeat
t:= r
rrl:= concat(rrl,
concat(r, [t := differentiate t for i in 1..ordp]))
eval(p, vl, rrl)
eval(p:$, sl:List S, rl:List $) ==
ordp:= order p
vl := concat [[makeVariable(s,j)$V for j in 0..ordp]
for s in sl]$List(List V)
rrl:=nil$List($)
for r in rl repeat
t:=r
rrl:=concat(rrl,
concat(r, [t:=differentiate t for i in 1..ordp]))
eval(p, vl, rrl)
eval(p:$, l:List Equation $) ==
eval(p, [retract(lhs e)@S for e in l]$List(S),
[rhs e for e in l]$List($))
)abbrev domain DSMP DifferentialSparseMultivariatePolynomial
++ Author: William Sit
++ Date Created: 19 July 1990
++ Date Last Updated: 13 September 1991
++ Basic Operations:DifferentialPolynomialCategory
++ Related Constructors:
++ See Also:
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, ranking, differential polynomials,
++ order, weight, leader, separant, initial, isobaric
++ References:Kolchin, E.R. "Differential Algebra and Algebraic Groups"
++ (Academic Press, 1973).
++ Description:
++ \spadtype{DifferentialSparseMultivariatePolynomial} implements
++ an ordinary differential polynomial ring by combining a
++ domain belonging to the category \spadtype{DifferentialVariableCategory}
++ with the domain \spadtype{SparseMultivariatePolynomial}.
++
DifferentialSparseMultivariatePolynomial(R, S, V):
Exports == Implementation where
R: Ring
S: OrderedSet
V: DifferentialVariableCategory S
E ==> IndexedExponents(V)
PC ==> PolynomialCategory(R,IndexedExponents(V),V)
PCL ==> PolynomialCategoryLifting
P ==> SparseMultivariatePolynomial(R, V)
SUP ==> SparseUnivariatePolynomial
SMP ==> SparseMultivariatePolynomial(R, S)
Exports ==> Join(DifferentialPolynomialCategory(R,S,V,E),
RetractableTo SMP)
Implementation ==> P add
retractIfCan(p:$):Union(SMP, "failed") ==
zero? order p =>
map(retract(#1)@S :: SMP, #1::SMP, p)$PCL(
IndexedExponents V, V, R, $, SMP)
"failed"
coerce(p:SMP):$ ==
map(#1::V::$, #1::$, p)$PCL(IndexedExponents S, S, R, SMP, $)
)abbrev domain ODPOL OrderlyDifferentialPolynomial
++ Author: William Sit
++ Date Created: 24 September, 1991
++ Date Last Updated: 7 February, 1992
++ Basic Operations:DifferentialPolynomialCategory
++ Related Constructors: DifferentialSparseMultivariatePolynomial
++ See Also:
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, ranking, differential polynomials,
++ order, weight, leader, separant, initial, isobaric
++ References:Kolchin, E.R. "Differential Algebra and Algebraic Groups"
++ (Academic Press, 1973).
++ Description:
++ \spadtype{OrderlyDifferentialPolynomial} implements
++ an ordinary differential polynomial ring in arbitrary number
++ of differential indeterminates, with coefficients in a
++ ring. The ranking on the differential indeterminate is orderly.
++ This is analogous to the domain \spadtype{Polynomial}.
++
OrderlyDifferentialPolynomial(R):
Exports == Implementation where
R: Ring
S ==> Symbol
V ==> OrderlyDifferentialVariable S
E ==> IndexedExponents(V)
SMP ==> SparseMultivariatePolynomial(R, S)
Exports ==> Join(DifferentialPolynomialCategory(R,S,V,E),
RetractableTo SMP)
Implementation ==> DifferentialSparseMultivariatePolynomial(R,S,V)
)abbrev domain SDPOL SequentialDifferentialPolynomial
++ Author: William Sit
++ Date Created: 24 September, 1991
++ Date Last Updated: 7 February, 1992
++ Basic Operations:DifferentialPolynomialCategory
++ Related Constructors: DifferentialSparseMultivariatePolynomial
++ See Also:
++ AMS Classifications:12H05
++ Keywords: differential indeterminates, ranking, differential polynomials,
++ order, weight, leader, separant, initial, isobaric
++ References:Kolchin, E.R. "Differential Algebra and Algebraic Groups"
++ (Academic Press, 1973).
++ Description:
++ \spadtype{SequentialDifferentialPolynomial} implements
++ an ordinary differential polynomial ring in arbitrary number
++ of differential indeterminates, with coefficients in a
++ ring. The ranking on the differential indeterminate is sequential.
++
SequentialDifferentialPolynomial(R):
Exports == Implementation where
R: Ring
S ==> Symbol
V ==> SequentialDifferentialVariable S
E ==> IndexedExponents(V)
SMP ==> SparseMultivariatePolynomial(R, S)
Exports ==> Join(DifferentialPolynomialCategory(R,S,V,E),
RetractableTo SMP)
Implementation ==> DifferentialSparseMultivariatePolynomial(R,S,V)