OKlibrary  0.2.1.6
general.hpp File Reference

Plans regarding Ramsey-type problems in general. More...

Go to the source code of this file.


Detailed Description

Plans regarding Ramsey-type problems in general.

Todo:
Architectures of the systems for showing/computing Ramsey-type 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:
    1. In general we have the notion of a "parameter tuple" P, and the main function N(P) (for example vanderwaerden(P).
    2. N(P) either computes a natural number, in which case this is the Ramsey-type number, or a pair [a,b], where a is a natural number and b is a natural number >= a or inf, meaning that the Ramsey-type number is in the closed interval from a to b.
    3. That the underlying number could actually be inf allows the possibility, that actually no underlying Ramsey-type theorem holds (while still some numbers < inf can be computed).
    4. If we however know that the number if finite (i.e., an underlying Ramsey-type theorem holds), then we use the upper bound inf-1 (to express "< inf"; see "Handling lower bounds" below).
    5. To check that a Maxima-term t is a parameter tuple, the predicate N_p(t) is provided which is true is t is a parameter tuple, and false otherwise.
    6. N(P) shall contain all the knowledge we have currently in our system.
  • The "side" functions:
    1. Mostly, N(P) delegates the computation to "side functions" S(P).
    2. These side-functions 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 well-defined single case.
    3. Furthermore, the S actually typically do not take the parameter tuple P, but a non-empty list of parameters which more naturally (and typically more compactly) encode the class of parameter tuples considered by S.
    4. 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 (non-empty) 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 Ramsey-type-number 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 Ramsey-type-theorem.
  • However, that N is finite can also be represented by the upper bound, inf-1, using inf-1 < inf, while n < inf-1 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:
    1. In case we don't conjecture the lower bound ">= b", one could use the lower bound "(b-1)+1", where b-1 is evaluated, but the "+1" not.
    2. However so the distinction between "just a lower bound" and "conjectured precise bound" is only visible in the source code.
    3. 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"?
    4. 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 default-value false, when when activated switches annotations on for the various bounds-functions 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 "ad-hoc" by each of the side-functions 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:
    1. How to get the history of a computation?
    2. At least at Lisp-level one can have a "hidden" annotation (that's the point of oklib_load_annotation!) --- how to use this?

Definition in file general.hpp.