P1788 state of play
P1788 members
The Christmas festivities have kept me away from intervals. I spent five days at the house of Kate (ex wife) and Joy (daughter) amid an atmosphere of harmony, which is good. Now P1788 work beckons again.
I believe the text is nearly ready for the sponsor ballot phase. Here are the crucial outstanding issues that I see.
Text
----
(A) (§7, urgent.) Before motion 61 can go to vote, the §7 definition of interval hull must be made flavor-independent. At present there are statements that only apply to a set-based flavor -- for the Kaucher flavor, e.g., they aren't meaningful. This is reflected in §4.2 Definitions too.
I'll make this my next task.
(B) (§4.2, important. Less urgent but must be done before sponsor-ballot.) Separate the Definitions in §4.2 into flavor-independent ones, and those specific to the set-based flavor (and in due course, hopefully, the Kaucher flavor). After off-line discussion, this will be done by keeping them in the current sequence, and giving each one a label to say what kind it is.
I would much value help from other editors to finish this task quickly.
(C) (§6, important, less urgent.) Vincent Lefevre has some detailed suggestions to remove minor inconsistencies between the 3 definitions of an expression.
I would be most grateful if Vincent himself would make the needed changes to the text and submit it for approval.
(D) (§10 - §12, important, less urgent.) Act on detailed comments on §12, made by Michel Hack, Dmitry Nazhedin, Vincent Lefevre & others. Also, I think, some on §10 and §11 -- I've some catching up to do so I'm not sure.
I think these don't impact on basic principles, and are similar to changes that will be asked for during sponsor ballot, so I am happy to do them in slow time.
Principles
----------
(E) (FTIA, very important, maybe not urgent.) Ned Nedialkov visited me over Christmas - his PhD student has put a proof of the FTIA, using an older version of the decoration system, into the formal language Coq. Ned & I updated it to the current system. More significant, we overcame the one remaining obstacle to a proof that puts the "ill" decoration on the same footing as the other four. This answers Guillaume Melquiond's valid objections to my previous understanding of "ill".
The resulting proof is elegant and quite brief. The proof of the pudding will be when Ned puts it into Coq, but I foresee no serious difficulties. Maybe some technicalities to do with the formal logic model, e.g. "Is the nowhere-defined function R^n -> R the same object for all n = 0,1,2,..., or is there a different one for each n?"
More details below for those who want it.
Best wishes to you all for the New Year.
John Pryce
============More on the FTIA proof and "ill"============
In summary:
1. Arnold Neumaier's insight that "ill" can be defined as the property
Dom(f)=Empty of (f,xx) pairs, is correct.
2. We know the proof is by induction over the number N of operations in
an expression, and the difficulty has always been in how to state
the base case, N=0.
3. I use notation `f to denote an expression. Actual arguments (intervals)
for interval-evaluation are labeled by the dummy arguments (variables)
they replace, instead of positionally. So the order of arguments
doesn't matter: for the expression x*z+y one might describe an interval-
evaluation by saying "x=[1,2]", "y=[3,4]" and "z=[5,6]", in any order.
4. V(`f) means the set of variables occurring in `f, regarded as symbols,
e.g. V(x*z+y) is {x,y,z}.
5. We assume an "input box" XX is given, meaning an assignment of an interval
xx_v to each variable v occurring in the overall expression we are
evaluating.
We could enumerate those variables as v_1, ..., v_n, thus thinking of XX
as a normal box (xx_1, ..., xx_n); but prefer not to.
6. The inductive hypothesis is that, for an expression `f with N operations,
one has constructed a pair
(f; ff_df) (**)
where the first is conceptual, the second is computed (at Level 2):
f is the real function of n variables defined by `f, where n is
the number of elements in V(`f).
ff_df is a decorated interval such that
ff \supseteq Rge(f | XX) and p_df(f, XX) is true.
So far, this looks like the previous FTIA argument. And the inductive step, that if this holds for subexpressions of `f then it holds for `f, is unchanged. (This has the interesting meat of the FTIA, using stuff like "the composition of continuous functions is continuous".)
Our observation was that
- the inputs xx_v are ordinary (undecorated) intervals;
- "ill" doesn't normally get introduced *during* the induction.
Hence the only (normal) place for "ill" to arise is in an Initialization Stage that happens *between* supplying the inputs xx_v and doing the induction.
We therefore specify the Induction Base Case as follows.
Each input xx_v, call it xx for short, is initialized to a pair (f; ff_df) as in (**) above, where
f is some function;
ff = Rge(f | xx);
df = dec(f, xx) = strongest decoration s.t. p_df(f, xx) is true;
and that only two f's are permitted at this point (conceivably others might have practical use):
- Id, the identity function Id(x)=x for real x, which produces ff=xx
and df = dec(Id, xx). This is exactly the effect of the standard's
initializing function newDec(xx).
- Un, the nowhere defined function of real x, which produces ff_df =
Empty_ill = NaI, for *any* input interval xx.
Comments:
- The current spec of decorated constructor thus amounts to
"The Initialization Stage uses Id if the constructor succeeds,
and Un if it fails",
which seems sensible.
- AFAICS this makes the theory match closely with how one writes code,
which must be a good thing.
- This formalism makes NaI always the result of *doing something to an
ordinary bare interval xx*, and that result *is* Empty_ill,
independent of what xx was.