Re: A Decorations Challenge

[Arnold Neumaier <Arnold.Neumaier@xxxxxxxxxxxx>]

Arnold Neumaier wrote:
> John Pryce wrote:
> > Here is my challenge, If you, or anyone, can meet it, I will stop 
> > complaining (or complain less loudly, anyway). More importantly, the 
> > solution will provide checkable evidence that the P1788 decoration 
> > scheme supports the writing of provably correct algorithms.
>
> Here is my answer to your challenge.
>
> The following is pseudo-Matlab code. I didn't check whether it
> executes; maybe I also forgot some case. But it should be clear
> why it answers your reservations.

While it solved your challenge, it didn't have correct semantics since
the claim that x in [l,u] was not enforced. So below is an improved 
version. It also checks nonexistence of a fixed point.




% Consider an interval datatype that has for an interval x the
% floating-point data x.inf,x.sup, and optionally the integer x.dec
% (which makes the interval decorated).
%
% It is assumed that the following properties are invariants:
% Exactly one of the following holds:
%   (i) x.inf and x.sup satisfy x.inf<=x.sup; then x.dec<=2 if present.
%  (ii) x.inf and x.sup are NaN; then x.dec>=3 if present.
% Decorations are defined as in my recent position paper.

function x=interval(l,u)
  % constructs a decorated interval x
  % from given floating-point bounds l and u
  if l<=u,
    x.inf=l;x.sup=u;x.dec=isinf(u-l);
  else
    x.inf=NaN;x.sup=NaN;x.dec=4;
  end;

function x=domain(x)
  % declares an interval x to be a domain for a range computation
  x.dec=0;

function b=isEmpty(x)
  % checks emptiness of the interval x
  b=isnan(x.inf);

function b=subset(y,x)
  % checks whether y is a subset of x
  b=( y.inf>=x.inf && y.sup<=x.sup ) || isEmpty(y)

function b=isSafe(x)
  % checks a sufficient condition that the function f whose result
  % x=f(y) is passed as an argument is everywhere defined,
  % continuous, and bounded in the nonempty interval y
  if isfield(x,'dec'),
    b=(x.dec<1);
  else
    b=0;
  end;

function z=intersect(x,y)
  % intersects two intervals x and y;
  % the result z is a bare interval
  z.inf=max(x.inf,y.inf);
  z.sup=min(x.sup,y.sup);
  if z.inf>z.sup,
    z.inf=NaN;z.sup=NaN;
  end;

function z=add(x,y)
  % add two intervals x and y
  z.inf=x.inf+y.inf;
  z.sup=x.sup+y.sup;
  if isfield(x,'dec') && isfield(y,'dec'),
    z.dec=max(x.dec,y.dec);
  end;

function x=add(r,x)
  % add real number r and interval x
  x.inf=r+x.inf;
  x.sup=x.sup+inf;

function x=sqrt(x)
  % compute square root of interval x
  if x.inf>=0,
    x.inf=sqrt(x.inf);x.sup=sqrt(x.sup);
  elseif x.sup<0,
    x.inf=NaN;x.sup=NaN;
    if isfield(x,'dec'), x.dec=3; end;
  else
    x.inf=0;x.sup=sqrt(x.sup);
    if isfield(x,'dec'), x.dec=2; end;
  end;

function x=sqrtPlus1(x)
  % evaluates f(x):=1+sqrt(x) at an interval argument x
  x=add(1,sqrt(x));

function [info,x]=ExFixedPoint(f,l,u,nfmax);
  % given an input interval [l,u], and a function handle f,
  % an interval x is produced that lies in [l,u].
  % if info.fail=0, x contains a fixed point of the function f
  % if info.fail=-1, x is Empty and f has no fixed point in [l,u]
  % if info.fail=1, no conclusion can be drawn after nfmax evaluations
  %
  % info.nf counts the number of function evaluations,
  % and is bounded by nfmax
  %
  x=interval(l,u);
  info.fail=1;
  info.nf=0;
  while 1,
    y=domain(x);        % declares y to be a domain in which the
                        % fixed-point property is checked
    x=f(y);             % interval evaluation
    info.nf=info.nf+1;  % update count
    if subset(x,y) && isSafe(x),
      % Brouwer's fixed-point theorem guarantees the existence
      % of a fixed point in x
      info.fail=0;
      return;
    end;
    if info.nf>=nfmax, break;
    x=intersect(x,y);
    if isempty(x),
      info.fail=-1;
      return;
    end;
  end;

% It is easy to see that calling
%  [info,x]=ExFixedPoint(@(x) sqrtPlus1(x),-1,4,50)
% produces (in exact arithmetic)
%   info.fail=0
%   info.nf=3
%   x.inf=2
%   x.sup=1+sqrt(3)
%   x.dec=0
% as it should be.