Nuprl Definition : nqsqrt3

nqsqrt3(n;q;r) ==
  eval n' = 10 * n in
  Y 
  (λnqsqrt3,r. eval s = (r + (q/r)/2) in
               let a,b = qrep(s) 
               in eval a' = (a * n') ÷ b in
                  let x ⟵ (a'/n')
                  in if q_less((x * x) - q;(1/n)) then x else nqsqrt3 <a', n'> fi ) 
  r


Definitions occuring in Statement :  q_less: q_less(r;s),  qsub: r - s,  qdiv: (r/s),  qrep: qrep(r),  qmul: r * s,  qadd: r + s,  callbyvalueall: callbyvalueall,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  ycomb: Y,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  divide: n ÷ m,  multiply: n * m,  natural_number: $n
Definitions occuring in definition :  ycomb: Y,  lambda: λx.A[x],  qadd: r + s,  spread: spread def,  qrep: qrep(r),  callbyvalue: callbyvalue,  divide: n ÷ m,  multiply: n * m,  callbyvalueall: callbyvalueall,  ifthenelse: if b then t else f fi ,  q_less: q_less(r;s),  qsub: r - s,  qmul: r * s,  qdiv: (r/s),  natural_number: $n,  apply: f a,  pair: <a, b>
FDL editor aliases :  nqsqrt3
Latex:
nqsqrt3(n;q;r)  ==
    eval  n'  =  10  *  n  in
    Y 
    (\mlambda{}nqsqrt3,r.  eval  s  =  (r  +  (q/r)/2)  in
                              let  a,b  =  qrep(s) 
                              in  eval  a'  =  (a  *  n')  \mdiv{}  b  in
                                    let  x  \mleftarrow{}{}  (a'/n')
                                    in  if  q\_less((x  *  x)  -  q;(1/n))  then  x  else  nqsqrt3  <a',  n'>  fi  ) 
    r


Date html generated: 2016_05_15-PM-11_39_30
Last ObjectModification: 2015_09_23-AM-08_30_47

Theory : rationals


Home Index