Skip to content

Instantly share code, notes, and snippets.

@scvalex
Created March 21, 2010 11:16
Show Gist options
  • Save scvalex/339244 to your computer and use it in GitHub Desktop.
Save scvalex/339244 to your computer and use it in GitHub Desktop.
Binary search division
ultraDiv ∷ Integer → Integer → (Integer, Integer)
-- pre: 1 <= d <= n
-- post: a*d + b == n
-- && (A) x > d . (a*x > n)
-- where
-- (a, b) = ultraDiv n d
ultraDiv n d = bDiv n d 1 n
where
-- pre: same as ultraDiv
-- && d * lower <= n && d * upper > n
-- post: same as ultraDiv
-- invariant: lower <= middle < upper
-- && (A) x in [0, lower] . (x * d <= n)
-- && (A) x in (upper..] . (x * d > n)
-- variant: upper-lower
bDiv n d lower upper
| lower ≡ upper-1 = (lower, n - d*lower)
| middle*d > n = bDiv n d lower middle
| otherwise = bDiv n d middle upper
where
middle = (upper + lower) `div` 2
ultraDiv2 ∷ Integer → Integer → (Integer, Integer)
-- pre: 1 <= d <= n
-- post: a*d + b == n
-- && (A) x > d . (a * x > n)
-- where
-- (a, b) = ultraDiv2 n d
ultraDiv2 n d = bDiv n d 1 n
where
-- pre: same as ultraDiv2
-- && d * lower <= n && d * (lower+i) >= n
-- post: same as ultraDiv2
-- invariant: lower <= lower+i
-- && (A) x in [0, lower] . (x * d <= n)
-- && (A) x in [lower+i..] . (x * d >= n)
-- variant: i
bDiv n d lower i
| i ≡ 0 = (lower, n - d*lower)
| (lower+i)*d ≤ n = bDiv n d (lower+i) (i `div` 2)
| otherwise = bDiv n d lower (i `div` 2)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment