Nuprl Definition : binary-search

binary-search(f;a;b)
==r if b=a + 1
       then a
       else eval c = a + ((b - a) ÷ 2) in
            if f c then binary-search(f;a;c) else binary-search(f;c;b) fi

binary-search(f;a;b) ==
  fix((λbinary-search,a,b. if b=a + 1
                              then a
                              else eval c = a + ((b - a) ÷ 2) in

                                   if f c then binary-search a c else binary-search c b fi ))

a
b

Definitions occuring in Statement : callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , int_eq: if a=b then c else d, apply: f a, fix: fix(F), lambda: λx.A[x], divide: n ÷ m, subtract: n - m, add: n + m, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], int_eq: if a=b then c else d, callbyvalue: callbyvalue, add: n + m, divide: n ÷ m, subtract: n - m, natural_number: $n, ifthenelse: if b then t else f fi , apply: f a
FDL editor aliases : binary-search

Latex:
binary-search(f;a;b) ==r if b=a + 1 then a else eval c = a + ((b - a) \mdiv{} 2) in if f c then binary-search(f;a;c) else binary-search(f;c;b) fi

Latex:
binary-search(f;a;b) == fix((\mlambda{}binary-search,a,b. if b=a + 1 then a else eval c = a + ((b - a) \mdiv{} 2) in if f c then binary-search a c else binary-search c b fi )) a b Date html generated: 2016_05_14-AM-07_27_37 Last ObjectModification: 2015_09_22-PM-05_46_22 Theory : int_2 Home Index