Nuprl Definition : list_accum

accumulate (with value x and list item a):
 f[x; a]
over list:
  L
with starting value:
 y) ==
  fix((λlist_accum,y,L. eval v = L in
                        if v is a pair then let h,t = v 
                                            in list_accum f[y; h] t otherwise if v = Ax then y otherwise ⊥)) 
  y 
  L


Definitions occuring in Statement :  bottom: ⊥,  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  isaxiom: if z = Ax then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  spread: spread def,  apply: f a,  isaxiom: if z = Ax then a otherwise b,  bottom: ⊥
FDL editor aliases :  list_accum
Latex:
accumulate  (with  value  x  and  list  item  a):
  f[x;  a]
over  list:
    L
with  starting  value:
  y)  ==
    fix((\mlambda{}list$_{accum}$,y,L.  eval  v  =  L  in
                                              if  v  is  a  pair  then  let  h,t  =  v 
                                                                                      in  list$_{accum}$  f[y;  h]  t
                                              otherwise  if  v  =  Ax  then  y  otherwise  \mbot{})) 
    y 
    L


Date html generated: 2016_05_14-AM-06_26_57
Last ObjectModification: 2015_12_03-PM-02_04_48

Theory : list_0


Home Index