Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Re: A Decorations Challenge

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.


% 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 in y everywhere defined,
  % continuous, and bounded
  if isfield(x,'dec'),
    b=(x.dec<1);
  else
    b=0;
  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 contain a fixed point of the function f
  %
  % 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
      info.fail=0;
      return;
    end;
    if info.nf>=nfmax, break;
  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.








On 10 Oct 2010, at 12:15, Arnold Neumaier wrote:

========================================================================
It is proposed that precisely the following five decorations shall be available:

dec = 0:  safe = everywhere defined, continuous, and bounded)
dec = 1:  everywhere defined
dec = 2:  possibly everywhere defined
dec = 3:  nowhere defined
dec = 4:  not valid

In all interval exchange formats, a decoration is encoded by an
unsigned integer dec taking one of the values 0, 1, 2, 3, or 4.
The encoding in a datatype is left to the implementor.


The following unary predicates shall be provided for bare decorations
and for decorated intervals of any supported idatatype:

isValid               dec<4
possiblyNonempty      dec<3
everywhereDefined     dec<2
isSafe                dec<1

notValid              dec>3
isEmpty               dec>2
possiblyUndefined     dec>1
notSafe               dec>0
======================================================================