#### 9.3 SeriesOrder

9.3.1 Constructors
9.3.2 Coercion
9.3.3 Equality
9.3.4 Arithmetic

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

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:

 boundedDecrement(x) = x ∀x ∈, (113) increment(x) = x ∀x ∈ (114)

289dom: SeriesOrder 289  (196)
SeriesOrder: with {
PrimitiveType;
OutputType;
exports: SeriesOrder 292a
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

Export of SeriesOrder

unknown: %

Description

An order if the order is not known.

292aexports: SeriesOrder 292a  (289)  293a
unknown: %;
292bimplementation: SeriesOrder 292b  (289)  293b
unknown: % == {i: I := -2; per i}

Uses I 47.

Export of SeriesOrder

infinity: %

Description

The order of the zero series.

293aexports: SeriesOrder 292a+   (289)  292a  294a
infinity: %;
293bimplementation: SeriesOrder 292b+   (289)  292b  294b
infinity: % == {i: I := -1; per i}

Uses I 47.

Export of SeriesOrder

0: %

Description

The order of the series 1.

294aexports: SeriesOrder 292a+   (289)  293a  295a
0: %;
294bimplementation: SeriesOrder 292b+   (289)  293b  295b
0: % == per(0\$I);

Uses I 47.

Export of SeriesOrder

1: %

Description

The order of the series x.

295aexports: SeriesOrder 292a+   (289)  294a  296a
1: %;
295bimplementation: SeriesOrder 292b+   (289)  294b  296b
1: % == per(1\$I);

Uses I 47.

Export of SeriesOrder

coerce: MachineInteger -> %

Description

Create an order from a natural number.

296aexports: SeriesOrder 292a+   (289)  295a  297a
coerce: MachineInteger -> %;

Uses MachineInteger 67.
296bimplementation: SeriesOrder 292b+   (289)  295b  297b
coerce(i: MachineInteger): % == {
assert(i >= 0);
per i;
}

Uses MachineInteger 67.
##### 9.3.2 Coercion

Export of SeriesOrder

coerce: % -> MachineInteger

Description

Coercion of an order to a MachineInteger.

ToDo 49
rhx 41 16-Sep-2006: Describe what happens for unknown (maybe that should be unspecified) and infinity (-1).

297aexports: SeriesOrder 292a+   (289)  296a  298a
coerce: % -> MachineInteger;

Uses MachineInteger 67.
297bimplementation: SeriesOrder 292b+   (289)  296b  298b
coerce(x: %): MachineInteger == rep x;

Uses MachineInteger 67.
##### 9.3.3 Equality

Export of SeriesOrder

=: (%, %) -> Boolean

Description

Compares two orders.

298aexports: SeriesOrder 292a+   (289)  297a  300a
=: (%, %) -> Boolean;
298bimplementation: 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.

299implementation: 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.

300aexports: SeriesOrder 292a+   (289)  298a  302
min: (%, %) -> %;
300bimplementation: 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.

302exports: SeriesOrder 292a+   (289)  300a  304a
+: (%, %) -> %;
303implementation: 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 y0. 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.

304aexports: SeriesOrder 292a+   (289)  302  305a
*: (%, %) -> %;
304bimplementation: 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.

305aexports: SeriesOrder 292a+   (289)  304a  306a
boundedDecrement: % -> %;
305bimplementation: 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.