Nuprl Definition : find-hull

find-hull(g;xs) ==
  let L ⟵ [2, ||xs||)
  in eager-accum(hs,k.let p,q = find_transitions(λx,y. k L xy;hs) 
                      in if isl(p) ∧b isl(q)
                         then hs
                         else eval x = outr(p) in
                              eval y = outr(q) in
                                if x <z y
                                then let as ⟵ firstn(x + 1;hs)
                                     in let bs ⟵ nth_tl(y;hs)
                                        in as @ [k / bs]
                                else let as ⟵ firstn((x - y) + 1;nth_tl(y;hs))
                                     in [k / as]
                                fi 
                         fi ;[0; 1];L)


Definitions occuring in Statement :  left-test: i L jk,  from-upto: [n, m),  eager-accum: eager-accum(x,a.f[x; a];y;l),  find_transitions: find_transitions(f;L),  firstn: firstn(n;as),  length: ||as||,  nth_tl: nth_tl(n;as),  append: as @ bs,  cons: [a / b],  nil: [],  band: p ∧b q,  callbyvalueall: callbyvalueall,  callbyvalue: callbyvalue,  outr: outr(x),  ifthenelse: if b then t else f fi ,  isl: isl(x),  lt_int: i <z j,  lambda: λx.A[x],  spread: spread def,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  from-upto: [n, m),  length: ||as||,  eager-accum: eager-accum(x,a.f[x; a];y;l),  spread: spread def,  find_transitions: find_transitions(f;L),  lambda: λx.A[x],  left-test: i L jk,  band: p ∧b q,  isl: isl(x),  callbyvalue: callbyvalue,  outr: outr(x),  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  append: as @ bs,  callbyvalueall: callbyvalueall,  firstn: firstn(n;as),  add: n + m,  subtract: n - m,  nth_tl: nth_tl(n;as),  cons: [a / b],  natural_number: $n,  nil: []
FDL editor aliases :  find-hull
Latex:
find-hull(g;xs)  ==
    let  L  \mleftarrow{}{}  [2,  ||xs||)
    in  eager-accum(hs,k.let  p,q  =  find\_transitions(\mlambda{}x,y.  k  L  xy;hs) 
                                            in  if  isl(p)  \mwedge{}\msubb{}  isl(q)
                                                  then  hs
                                                  else  eval  x  =  outr(p)  in
                                                            eval  y  =  outr(q)  in
                                                                if  x  <z  y
                                                                then  let  as  \mleftarrow{}{}  firstn(x  +  1;hs)
                                                                          in  let  bs  \mleftarrow{}{}  nth\_tl(y;hs)
                                                                                in  as  @  [k  /  bs]
                                                                else  let  as  \mleftarrow{}{}  firstn((x  -  y)  +  1;nth\_tl(y;hs))
                                                                          in  [k  /  as]
                                                                fi 
                                                  fi  ;[0;  1];L)


Date html generated: 2017_10_02-PM-06_52_13
Last ObjectModification: 2017_08_06-PM-07_31_53

Theory : euclidean!plane!geometry


Home Index