Nuprl Lemma : constructing rroot

We didn't know whether the simple program for the i-th root of real x
was correct. Attempts to prove it correct had failed, so we made the
construction in this subdirectory and extracted a correct-by-construction
program  extracted-rroot: extracted-rroot(i;x).

This program is fairly efficient. Using it, we compute
50 decimal digits of the 12-root of 2,  ⌈50 decimal digits of extracted-rroot(12;r(2)) ⌉
in 531,134  computation steps, taking about 30 seconds.

However, the program rroot: rroot(i;x) is much simpler, and computes
⌈50 decimal digits of rroot(12;r(2)) ⌉
in only 7,690 steps, almost instantly.

We used the computations find-real-neq: find-real-neq(a;b) and find-real-neq2: find-real-neq2(a;b)
to experimentally check that the known correct ⌈extracted-rroot([i];[x])⌉
and the simpler ⌈rroot([i];[x])⌉ always 
(on many reals of various sizes and signs) computed the same integers
(or integers that differed by at most one).

This gave us confidence that the simpler program was also correct
and we were then able to prove that is was correct!.

⋅

Latex:
We  didn't  know  whether  the  simple  program  for  the  i-th  root  of  real  x
was  correct.  Attempts  to  prove  it  correct  had  failed,  so  we  made  the
construction  in  this  subdirectory  and  extracted  a  correct-by-construction
program    extracted-rroot:  extracted-rroot(i;x).

This  program  is  fairly  efficient.  Using  it,  we  compute
50  decimal  digits  of  the  12-root  of  2,    \mkleeneopen{}50  decimal  digits  of  extracted-rroot(12;r(2))  \mkleeneclose{}
in  531,134    computation  steps,  taking  about  30  seconds.

However,  the  program  rroot:  rroot(i;x)  is  much  simpler,  and  computes
\mkleeneopen{}50  decimal  digits  of  rroot(12;r(2))  \mkleeneclose{}
in  only  7,690  steps,  almost  instantly.

We  used  the  computations  find-real-neq:  find-real-neq(a;b)  and  find-real-neq2:  find-real-neq2(a;b)
to  experimentally  check  that  the  known  correct  \mkleeneopen{}extracted-rroot([i];[x])\mkleeneclose{}
and  the  simpler  \mkleeneopen{}rroot([i];[x])\mkleeneclose{}  always 
(on  many  reals  of  various  sizes  and  signs)  computed  the  same  integers
(or  integers  that  differed  by  at  most  one).

This  gave  us  confidence  that  the  simpler  program  was  also  correct
and  we  were  then  able  to  prove  that  is  was  correct!.

\mcdot{}


Date html generated: 2015_07_17-PM-06_21_49
Last ObjectModification: 2014_05_23-PM-00_48_20

Home Index