Nuprl Definition : exp-ratio

exp-ratio(a;b;n;p;q)
==r if p <then else eval n' in eval p' in eval q' in   exp-ratio(a;b;n';p';q') fi 

exp-ratio(a;b;n;p;q) ==
  fix((λexp-ratio,n,p,q. if p <q
                        then n
                        else eval n' in
                             eval p' in
                             eval q' in
                               exp-ratio n' p' q'
                        fi )) 
  
  
  q



Definitions occuring in Statement :  callbyvalue: callbyvalue ifthenelse: if then else fi  lt_int: i <j apply: a fix: fix(F) lambda: λx.A[x] multiply: m add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] ifthenelse: if then else fi  lt_int: i <j add: m natural_number: $n callbyvalue: callbyvalue multiply: m apply: a
FDL editor aliases :  exp-ratio
Latex:
exp-ratio(a;b;n;p;q)
==r  if  p  <z  q
        then  n
        else  eval  n'  =  n  +  1  in
                  eval  p'  =  a  *  p  in
                  eval  q'  =  b  *  q  in
                      exp-ratio(a;b;n';p';q')
        fi 


Latex:
exp-ratio(a;b;n;p;q)  ==
    fix((\mlambda{}exp-ratio,n,p,q.  if  p  <z  q
                                                then  n
                                                else  eval  n'  =  n  +  1  in
                                                          eval  p'  =  a  *  p  in
                                                          eval  q'  =  b  *  q  in
                                                              exp-ratio  n'  p'  q'
                                                fi  )) 
    n 
    p 
    q



Date html generated: 2018_05_21-PM-01_02_47
Last ObjectModification: 2018_01_28-PM-02_12_45

Theory : num_thy_1


Home Index