Nuprl Definition : awf_sum

awf_sum(n;s) ==
  fix((λawf_sum,n,s. case s
                     of inl(z) =>
                     z
                     | inr(L) =>
                     if (n =z 0)
                     then 0
                     else eval m = n - 1 in
                          accumulate (with value x and list item s):
                           x + (awf_sum m s)
                          over list:
                            L
                          with starting value:
                           0)
                     fi )) 
  n 
  s


Definitions occuring in Statement :  list_accum: list_accum,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  callbyvalue: callbyvalue,  subtract: n - m,  list_accum: list_accum,  add: n + m,  apply: f a,  natural_number: $n
FDL editor aliases :  awf_sum
Latex:
awf\_sum(n;s)  ==
    fix((\mlambda{}awf$_{sum}$,n,s.  case  s
                                        of  inl(z)  =>
                                        z
                                        |  inr(L)  =>
                                        if  (n  =\msubz{}  0)
                                        then  0
                                        else  eval  m  =  n  -  1  in
                                                  accumulate  (with  value  x  and  list  item  s):
                                                    x  +  (awf$_{sum}$  m  s)
                                                  over  list:
                                                      L
                                                  with  starting  value:
                                                    0)
                                        fi  )) 
    n 
    s


Date html generated: 2016_05_15-PM-07_27_35
Last ObjectModification: 2015_09_23-AM-08_15_25

Theory : general


Home Index