Nuprl Definition : poly-approx-aux

poly-approx-aux(a;x;xM;M;n;k)
==r if (k =z 0)
    then a n M
    else eval u = poly-approx-aux(a;x;xM;M;n + 1;k - 1) in
         eval b = ((2 * |u|) ÷ M) + 1 in
         eval z = if (b =z 1) then xM else x (b * M) fi  in
         eval v = (u * z) ÷ 2 * b * M in
         eval t = a n M in
           v + t
    fi 
poly-approx-aux(a;x;xM;M;n;k) ==
  fix((λpoly-approx-aux,n,k. if (k =z 0)
                            then a n M
                            else eval u = poly-approx-aux (n + 1) (k - 1) in
                                 eval b = ((2 * |u|) ÷ M) + 1 in
                                 eval z = if (b =z 1) then xM else x (b * M) fi  in
                                 eval v = (u * z) ÷ 2 * b * M in
                                 eval t = a n M in
                                   v + t
                            fi )) 
  n 
  k


Definitions occuring in Statement :  absval: |i|,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  divide: n ÷ m,  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  absval: |i|,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  divide: n ÷ m,  natural_number: $n,  multiply: n * m,  callbyvalue: callbyvalue,  apply: f a,  add: n + m
FDL editor aliases :  poly-approx-aux
Latex:
poly-approx-aux(a;x;xM;M;n;k)
==r  if  (k  =\msubz{}  0)
        then  a  n  M
        else  eval  u  =  poly-approx-aux(a;x;xM;M;n  +  1;k  -  1)  in
                  eval  b  =  ((2  *  |u|)  \mdiv{}  M)  +  1  in
                  eval  z  =  if  (b  =\msubz{}  1)  then  xM  else  x  (b  *  M)  fi    in
                  eval  v  =  (u  *  z)  \mdiv{}  2  *  b  *  M  in
                  eval  t  =  a  n  M  in
                      v  +  t
        fi 

Latex:
poly-approx-aux(a;x;xM;M;n;k)  ==
    fix((\mlambda{}poly-approx-aux,n,k.  if  (k  =\msubz{}  0)
                                                        then  a  n  M
                                                        else  eval  u  =  poly-approx-aux  (n  +  1)  (k  -  1)  in
                                                                  eval  b  =  ((2  *  |u|)  \mdiv{}  M)  +  1  in
                                                                  eval  z  =  if  (b  =\msubz{}  1)  then  xM  else  x  (b  *  M)  fi    in
                                                                  eval  v  =  (u  *  z)  \mdiv{}  2  *  b  *  M  in
                                                                  eval  t  =  a  n  M  in
                                                                      v  +  t
                                                        fi  )) 
    n 
    k


Date html generated: 2018_05_22-PM-02_00_45
Last ObjectModification: 2017_10_25-PM-01_55_56

Theory : reals


Home Index