Nuprl Definition : poly-val-fun

poly-val-fun(p) ==
  tree_ind(p;
           tree_leaf(x)⇒ λl.x;
           tree_node(a,b)⇒ ra,rb.λl.eval t = tl(l) in
                                     eval av = ra t in
                                     eval bv = rb l in
                                       if bv=0  then av  else eval h = hd(l) in av + (h * bv)) 


Definitions occuring in Statement :  tree_ind: tree_ind,  hd: hd(l),  tl: tl(l),  callbyvalue: callbyvalue,  int_eq: if a=b  then c  else d,  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  tree_ind: tree_ind,  lambda: λx.A[x],  tl: tl(l),  apply: f a,  int_eq: if a=b  then c  else d,  natural_number: $n,  callbyvalue: callbyvalue,  hd: hd(l),  add: n + m,  multiply: n * m
FDL editor aliases :  poly-val-fun
Latex:
poly-val-fun(p)  ==
    tree\_ind(p;
                      tree\_leaf(x){}\mRightarrow{}  \mlambda{}l.x;
                      tree\_node(a,b){}\mRightarrow{}  ra,rb.\mlambda{}l.eval  t  =  tl(l)  in
                                                                          eval  av  =  ra  t  in
                                                                          eval  bv  =  rb  l  in
                                                                              if  bv=0    then  av    else  eval  h  =  hd(l)  in  av  +  (h  *  bv)) 


Date html generated: 2017_10_01-AM-08_32_26
Last ObjectModification: 2017_05_02-PM-04_47_20

Theory : integer!polynomial!trees


Home Index