Nuprl Definition : find-xover

find-xover(f;m;n;step)

==r if f n then <n, m> else eval step' = 2 * step in eval k = n + step in   find-xover(f;n;k;step') fi

find-xover(f;m;n;step) ==
  fix((λfind-xover,m,n,step. if f n
                            then <n, m>
                            else eval step' = 2 * step in
                                 eval k = n + step in
                                   find-xover n k step'
                            fi ))
  m
  n
  step

Definitions occuring in Statement : callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , apply: f a, fix: fix(F), lambda: λx.A[x], pair: <a, b>, multiply: n * m, add: n + m, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], ifthenelse: if b then t else f fi , pair: <a, b>, multiply: n * m, natural_number: $n, callbyvalue: callbyvalue, add: n + m, apply: f a
FDL editor aliases : find-xover

Latex:
find-xover(f;m;n;step) ==r if f n then <n, m> else eval step' = 2 * step in eval k = n + step in find-xover(f;n;k;step') fi

Latex:
find-xover(f;m;n;step) == fix((\mlambda{}find-xover,m,n,step. if f n then <n, m> else eval step' = 2 * step in eval k = n + step in find-xover n k step' fi )) m n step Date html generated: 2016_05_14-AM-07_27_53 Last ObjectModification: 2015_09_22-PM-05_46_23 Theory : int_2 Home Index