Plans regarding Ramseytype problems in general.
More...
Go to the source code of this file.
Detailed Description
Plans regarding Ramseytype problems in general.
 Todo:
 Architectures of the systems for showing/computing Ramseytype numbers

A system with the basics completed one finds in ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/Numbers.mac.

Basically the same system is ComputerAlgebra/RamseyTheory/Lisp/GreenTao/Numbers.mac (to be completed).

A different system is ComputerAlgebra/RamseyTheory/Lisp/Ramsey/Numbers.mac (which needs update): Here there are no transversal numbers.

The "main" function:

In general we have the notion of a "parameter tuple" P, and the main function N(P) (for example vanderwaerden(P).

N(P) either computes a natural number, in which case this is the Ramseytype number, or a pair [a,b], where a is a natural number and b is a natural number >= a or inf, meaning that the Ramseytype number is in the closed interval from a to b.

That the underlying number could actually be inf allows the possibility, that actually no underlying Ramseytype theorem holds (while still some numbers < inf can be computed).

If we however know that the number if finite (i.e., an underlying Ramseytype theorem holds), then we use the upper bound inf1 (to express "< inf"; see "Handling lower bounds" below).

To check that a Maximaterm t is a parameter tuple, the predicate N_p(t) is provided which is true is t is a parameter tuple, and false otherwise.

N(P) shall contain all the knowledge we have currently in our system.

The "side" functions:

Mostly, N(P) delegates the computation to "side functions" S(P).

These sidefunctions typically consider a restricted domain of parameter tuples, and also they typically do not consider all the possibilities for computing bounds, but they consider only a welldefined single case.

Furthermore, the S actually typically do not take the parameter tuple P, but a nonempty list of parameters which more naturally (and typically more compactly) encode the class of parameter tuples considered by S.

A function S_a(P) is provided for a side function, with domain all parameter tuples, returning [] if P is not in the domain of the parameter tuples considered by S, and otherwise a (nonempty) list L such that apply(S,L) is applicable. (All possible parameter lists L for S can be obtained by S_a(P).)
 Todo:
 Handling bounds

Currently we use intervals [a,b], meaning a <= N <= b for the corresponding Ramseytypenumber N.

Instead we could use a < N < b, which for the lower bound would correspond to the way they are presented in the literature, and for the upper bound would represent the corresponding Ramseytypetheorem.

However, that N is finite can also be represented by the upper bound, inf1, using inf1 < inf, while n < inf1 for all natural n.

DONE These properties should be put into our test system, since likely Maxima doesn't guarantee them?

Handling of strict lower bounds:

In case we don't conjecture the lower bound ">= b", one could use the lower bound "(b1)+1", where b1 is evaluated, but the "+1" not.

However so the distinction between "just a lower bound" and "conjectured precise bound" is only visible in the source code.

Is there a way to enter (conveniently), say, 328+1 in the source code, which under normal circumstances just becomes 329, but if asked explicitly, then we can get back "328+1"?

Perhaps this is handled by the annotations discussed below?
 Todo:
 How to annotate numbers with justifications?

Once the computations get a bit more involved, the need arises to annotate the computed bounds/numbers with justifications (how did the system compute them?).

Perhaps we introduce a global boolean variable "oklib_term_annotation", with defaultvalue false, when when activated switches annotations on for the various boundsfunctions involved.

Then the old value (either an integer or a pair of integers/inf) is replaced by a pair, where the first component is the old value, while the second component is the annotation.

It seems annotations must be performed "adhoc" by each of the sidefunctions and by the main function (see above)  using some general scheme very likely it gets unreadable.

In order to avoid that the functions become hard to read, likely they invoke a global switch at the beginning: normally without annotation, while when annotation is activated then the code is repeated but now using resp. providing the annotations.

Likely we can not use the Maxima mechanisms, however as an additional aid they could be useful:

How to get the history of a computation?

At least at Lisplevel one can have a "hidden" annotation (that's the point of oklib_load_annotation!)  how to use this?
Definition in file general.hpp.