Nuprl Definition : Longs-algorithm

`Longs-algorithm(h;n;a;b;c)`
`==r if a=0`
`       then h c`
`       else if (c) < (0)`
`               then 0`
`               else if (b) < (0)`
`                       then 0`
`                       else if b=0`
`                               then eval a' = a - 1 in`
`                                    eval c' = c - 1 in`
`                                    eval b' = (n a') - c in`
`                                      Longs-algorithm(h;n;a;b;c') + Longs-algorithm(h;n;a';b';c)`
`                               else eval b' = b - 1 in`
`                                    eval c' = c - 1 in`
`                                      Longs-algorithm(h;n;a;b';c) + Longs-algorithm(h;n;a;b;c')`

`Longs-algorithm(h;n;a;b;c) ==`
`  fix((λLongs-algorithm,a,b,c. if a=0`
`                                  then h c`
`                                  else if (c) < (0)`
`                                          then 0`
`                                          else if (b) < (0)`
`                                                  then 0`
`                                                  else if b=0`
`                                                          then eval a' = a - 1 in`
`                                                               eval c' = c - 1 in`
`                                                               eval b' = (n a') - c in`
`                                                                 (Longs-algorithm a b c') + (Longs-algorithm a' b' c)`
`                                                          else eval b' = b - 1 in`
`                                                               eval c' = c - 1 in`
`                                                                 (Longs-algorithm a b' c) + (Longs-algorithm a b c'))) `
`  a `
`  b `
`  c`

Definitions occuring in Statement :  callbyvalue: callbyvalue less: `if (a) < (b)  then c  else d` int_eq: `if a=b  then c  else d` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` subtract: `n - m` add: `n + m` natural_number: `\$n`
Definitions occuring in definition :  fix: `fix(F)` lambda: `λx.A[x]` less: `if (a) < (b)  then c  else d` int_eq: `if a=b  then c  else d` callbyvalue: callbyvalue subtract: `n - m` natural_number: `\$n` add: `n + m` apply: `f a`
FDL editor aliases :  Longs-algorithm
Latex:
Longs-algorithm(h;n;a;b;c)
==r  if  a=0
then  h  c
else  if  (c)  <  (0)
then  0
else  if  (b)  <  (0)
then  0
else  if  b=0
then  eval  a'  =  a  -  1  in
eval  c'  =  c  -  1  in
eval  b'  =  (n  a')  -  c  in
Longs-algorithm(h;n;a;b;c')  +  Longs-algorithm(h;n;a';b';c)
else  eval  b'  =  b  -  1  in
eval  c'  =  c  -  1  in
Longs-algorithm(h;n;a;b';c)  +  Longs-algorithm(h;n;a;b;c')

Latex:
Longs-algorithm(h;n;a;b;c)  ==
fix((\mlambda{}Longs-algorithm,a,b,c.  if  a=0
then  h  c
else  if  (c)  <  (0)
then  0
else  if  (b)  <  (0)
then  0
else  if  b=0
then  eval  a'  =  a  -  1  in
eval  c'  =  c  -  1  in
eval  b'  =  (n  a')  -  c  in
(Longs-algorithm  a  b  c')
+  (Longs-algorithm  a'  b'  c)
else  eval  b'  =  b  -  1  in
eval  c'  =  c  -  1  in
(Longs-algorithm  a  b'  c)
+  (Longs-algorithm  a  b  c')))
a
b
c

Date html generated: 2016_05_15-PM-10_02_40
Last ObjectModification: 2015_09_23-AM-08_21_53

Theory : power!series

Home Index