Nuprl Definition : fastpi

fastpi(n) ==
  primrec(n;λn.eval m = 4 * n in
               (m * 314159265358979323846) ÷ 400000000000000000000;λi,x. eval j = i + 1 in
                                                                         eval N = 2 * 10^20 * 3^j in
                                                                           (radd_rcos(x) within 1/N))


Definitions occuring in Statement :  radd_rcos: radd_rcos(x),  rational-approx: (x within 1/n),  primrec: primrec(n;b;c),  callbyvalue: callbyvalue,  lambda: λx.A[x],  divide: n ÷ m,  multiply: n * m,  add: n + m,  natural_number: $n,  fastexp: i^n
Definitions occuring in definition :  radd_rcos: radd_rcos(x),  rational-approx: (x within 1/n),  natural_number: $n,  fastexp: i^n,  multiply: n * m,  callbyvalue: callbyvalue,  add: n + m,  lambda: λx.A[x],  divide: n ÷ m,  primrec: primrec(n;b;c)
FDL editor aliases :  fastpi
Latex:
fastpi(n)  ==
    primrec(n;\mlambda{}n.eval  m  =  4  *  n  in
                              (m  *  314159265358979323846)  \mdiv{}  400000000000000000000;\mlambda{}i,x.  eval  j  =  i  +  1  in
                                                                                                                                                  eval  N  =  2  *  10\^{}20  *  3\^{}j  in
                                                                                                                                                      (radd\_rcos(x)  within  1/N)\000C)


Date html generated: 2016_10_26-PM-00_21_33
Last ObjectModification: 2016_09_12-PM-05_42_13

Theory : reals_2


Home Index