Nuprl Definition : half-pi
This definition of π/2 is the real that rcos-seq(n) converges to as n -> ∞.
It is displayed with (slower) because we later define another real number
that is equal to this one but computes faster (and we take that to be our
"official" definition of π/2.⋅
π/2(slower) ==
λn.eval m = 4 * n in
eval n = exp-ratio(1;3164556962025316455;0;m;1000000000) + 1 in
(rcos-seq(n) m) ÷ 4
Definitions occuring in Statement :
rcos-seq: rcos-seq(n),
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
add: n + m,
natural_number: $n,
exp-ratio: exp-ratio(a;b;n;p;q)
Definitions occuring in definition :
natural_number: $n,
rcos-seq: rcos-seq(n),
apply: f a,
divide: n ÷ m,
exp-ratio: exp-ratio(a;b;n;p;q),
add: n + m,
callbyvalue: callbyvalue,
multiply: n * m,
lambda: λx.A[x]
FDL editor aliases :
half-pi
Latex:
\mpi{}/2(slower) ==
\mlambda{}n.eval m = 4 * n in
eval n = exp-ratio(1;3164556962025316455;0;m;1000000000) + 1 in
(rcos-seq(n) m) \mdiv{} 4
Date html generated:
2016_11_09-AM-06_22_55
Last ObjectModification:
2016_11_09-AM-00_35_26
Theory : reals_2
Home
Index