### Nuprl Definition : exp-ratio

`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 `

`exp-ratio(a;b;n;p;q) ==`
`  fix((λ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`

Definitions occuring in Statement :  callbyvalue: callbyvalue ifthenelse: `if b then t else f fi ` lt_int: `i <z j` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` multiply: `n * m` add: `n + m` natural_number: `\$n`
Definitions occuring in definition :  fix: `fix(F)` lambda: `λx.A[x]` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` add: `n + m` natural_number: `\$n` callbyvalue: callbyvalue multiply: `n * m` apply: `f 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: 2016_05_15-PM-04_07_13
Last ObjectModification: 2015_09_23-AM-07_46_38

Theory : general

Home Index