9.3 SeriesOrder
This is an auxiliary domain to ease the implementation of order computations.
In fact, we want to model that an order of a series can be a non-negative integer,
∞, or unknown. So we have, natural numbers with two more values, infinity and
unknown.
Type Constructor
SeriesOrder
Description
Models computations with orders or series.
The domain models ℕ ∪
where ∞ and ? are two new symbols.
The symbol ∞ models the order of the zero series. Its arithmetic is given
by
| min(∞,x) | = x | ∀x | ∈ ℕ ∪ , | (106)
|
| ∞ + x | = ∞ | ∀x | ∈ ℕ ∪ , | (107)
|
| ∞⋅ x | = ∞ | ∀x | ∈ ℕ ∪ . | (108)
|
| x ⋅∞ | =  | | | (109) |
Since we deal with a lazy implementation of series, it might be the case that the
order of a series is not yet known. The symbol ? models the fact that the order is not
known. Its arithmetic is given by
| min(?,x) | = ? | ∀x | ∈ ℕ ∪ , | (110)
|
| ? + x | = ? | ∀x | ∈ ℕ ∪ , | (111)
|
| ? ⋅ x | = ? | ∀x | ∈ ℕ ∪ . | (112) |
The above operations are commutative and associative and extend the corresponding
operations on
ℕ.
Corresponding to the differentiation and integration of a formal power series, we
have:
See also
FormalPowerSeries, OrdinaryGeneratingSeries, ExponentialGeneratingSeries
289⟨dom: SeriesOrder 289⟩≡ (196)
SeriesOrder: with {
PrimitiveType;
OutputType;
⟨exports: SeriesOrder 292a⟩
} == I add {
Rep == I;
import from Rep;
⟨implementation: SeriesOrder 292b⟩
}
Defines:
SeriesOrder, used in chunks 101a, 132, 133, 204, 205, 207, 214, 217, 242, 243, 245, 251,
253a, 257–60, 263a, 264a, 266b, 268, 269, 281b, 300b, 303, 342, 345b, 361, 363, 685,
688, 689, 692b, 702, and 703.
Uses I 47 and OutputType 570.
Exports of SeriesOrder
-
-
unknown: % An order if the order is not known.
-
-
infinity: % The order of the zero series.
-
-
0: % The order of the series 1.
-
-
1: % The order of the series x.
-
-
coerce: MachineInteger -> % Create an order from a natural number.
-
-
coerce: % -> MachineInteger Coercion of an order to a MachineInteger.
-
-
=: (%, %) -> Boolean Compares two orders.
-
-
min: (%, %) -> % Compute the order of the sum of two series.
-
-
+: (%, %) -> % Compute the order of the product of two series.
-
-
*: (%, %) -> % Compute the order of the composition of two series.
-
-
boundedDecrement: % -> % Compute the order of the derivative of a series.
-
-
increment: % -> % Compute the order of the integral of a series.
9.3.1 Constructors
292b⟨implementation: SeriesOrder 292b⟩≡ (289) 293b ⊳
unknown: % == {i: I := -2; per i}
Uses I 47.
9.3.2 Coercion
9.3.3 Equality
Export of SeriesOrder
=: (%, %) -> Boolean
Description
Compares two orders.
298b⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲297b 299 ⊳
(x: %) = (y: %): Boolean == rep x = rep y;
ToDo ⊲ 50 ⊳ rhx ⊲ 42 ⊳ 10-Sep-2006: No idea why we cannot inherit
<< from
MachineInteger. But somehow the produced code complains about
Looking in MachineInteger for coerce with code 978932010
|
while trying to print ’unknown’ inside a TRACE statement.
299⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲298b 300b ⊳
(tw: TextWriter) << (x: %): TextWriter == {
import from String;
x = unknown => tw << "unknown";
x = infinity => tw << "infinity";
tw << (rep x);
}
Uses String 65.
9.3.4 Arithmetic
Export of SeriesOrder
min: (%, %) -> %
Description
Compute the order of the sum of two series.
In general, the order of the sum of two series x and y is coverned by the inequality
 |
(115)
|
We take equality as an approximation of that order and thus guarantee at least
a reasonable part of the knowledge about the series.
The operation min turns SeriesOrder into a commutative semigroup.
See also
+, *, boundedDecrement, increment
300b⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲299 303 ⊳
min(x: %, y: %): % == {
TRACE("SeriesOrder min x = ", x);
TRACE("SeriesOrder min y = ", y);
x = unknown or y = unknown => unknown;
x = infinity => y;
y = infinity => x;
per min(rep x, rep y);
}
Uses SeriesOrder 289.
Export of SeriesOrder
+: (%, %) -> %
Description
Compute the order of the product of two series.
In general, the order of the product of two series x and y is coverned by the equation
 |
(116)
|
We take this equation as the definition of the order of the product of two
series.
The operation + together with 0 turns SeriesOrder into a commutative
monoid.
See also
min, *, boundedDecrement, increment
303⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲300b 304b ⊳
(x: %) + (y: %): % == {
TRACE("SeriesOrder + x = ", x);
TRACE("SeriesOrder + y = ", y);
x = unknown or y = unknown => unknown;
x = infinity or y = infinity => infinity;
per (rep x + rep y);
}
Uses SeriesOrder 289.
Export of SeriesOrder
*: (%, %) -> %
Description
Compute the order of the composition of two series.
In general, the order of the composition of two series x and y is coverned by the
equation
 |
(117)
|
if
y
0. We take this equation as the definition of the order of the product of
two series.
The operation * together with 1 turns SeriesOrder into a commutative
monoid.
See also
min, +, boundedDecrement, increment
304b⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲303 305b ⊳
(x: %) * (y: %): % == {
x = unknown or y = unknown => unknown;
x = infinity => infinity;
y = infinity => if zero? rep x then x else infinity;
per (rep x * rep y);
}
Export of SeriesOrder
boundedDecrement: % -> %
Description
Compute the order of the derivative of a series.
The order of the derivative of a series x is given by
 |
(118)
|
Of course, this is only an approximate value, since if
x1 = 0 then the order of
the derivative is certainly
≥ 1. We take this equation as the definition of the
(
approximate) order of the derivative of a series.
See also
min, +, *, increment
305b⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲304b 306b ⊳
boundedDecrement(x: %): % == {
x = unknown or x = infinity => x;
per max(0, prev rep x);
}
Export of SeriesOrder
increment: % -> %
Description
Compute the order of the integral of a series.
The order of the integral of a series x is given by
 |
(119)
|
We take this equation as the definition of the order of the integral of a series.
Note, that we here assume that the integration constant is 0.
See also
min, +, *, boundedDecrement
306b⟨implementation: SeriesOrder 292b⟩+
≡ (289) ⊲305b
increment(x: %): % == x + 1;
,