Nuprl Definition : poly-int-val
p@l==r if null(l) then p else let a,as = l in Σ(p[i]@as * a^||p|| - 1 - i | i < ||p||) fi 
p@l ==
  fix((λpoly-int-val,l,p. if null(l)
                         then p
                         else let a,as = l 
                              in Σ((poly-int-val as p[i]) * a^||p|| - 1 - i | i < ||p||)
                         fi )) 
  l 
  p
Definitions occuring in Statement : 
exp: i^n
, 
sum: Σ(f[x] | x < k)
, 
select: L[n]
, 
length: ||as||
, 
null: null(as)
, 
ifthenelse: if b then t else f fi 
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
multiply: n * m
, 
subtract: n - m
, 
natural_number: $n
Definitions occuring in definition : 
natural_number: $n
, 
length: ||as||
, 
subtract: n - m
, 
exp: i^n
, 
select: L[n]
, 
apply: f a
, 
multiply: n * m
, 
sum: Σ(f[x] | x < k)
, 
spread: spread def, 
null: null(as)
, 
ifthenelse: if b then t else f fi 
, 
lambda: λx.A[x]
, 
fix: fix(F)
FDL editor aliases : 
poly-int-val
poly-int-val
Latex:
p@l==r  if  null(l)  then  p  else  let  a,as  =  l  in  \mSigma{}(p[i]@as  *  a\^{}||p||  -  1  -  i  |  i  <  ||p||)  fi 
Latex:
p@l  ==
    fix((\mlambda{}poly-int-val,l,p.  if  null(l)
                                                  then  p
                                                  else  let  a,as  =  l 
                                                            in  \mSigma{}((poly-int-val  as  p[i])  *  a\^{}||p||  -  1  -  i  |  i  <  ||p||)
                                                  fi  )) 
    l 
    p
Date html generated:
2017_04_17-AM-09_04_15
Last ObjectModification:
2017_04_12-PM-03_59_09
Theory : list_1
Home
Index