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