Bisection — bracket a root of a continuous function and halve
Given a bracket [a,b] with f(a)·f(b) < 0, the root lies between them; halve the interval toward whichever sub-bracket keeps the sign change. Converges linearly but never diverges. Here f(x) = x² − 2, whose positive root is √2.
A Soma program from the math part of the verified corpus: 61 lines, cells BisectionRoot, BisectTests. It passes soma check with soma 3.2.4.
How it is built
The cell BisectionRoot declares 3 signals in its face: f(x: Float) -> Float, bisect(a: Float, b: Float, tol: Float) -> Float and run() -> Map. Handlers: f (line 19), bisect (line 23) and run (line 47).
The file also holds 1 test cell (BisectTests) with 2 assertions, run by soma test.
The source
bisection_root.cell
// ============================================================================
// Bisection — bracket a root of a continuous function and halve
// ============================================================================
//
// Given a bracket [a,b] with f(a)·f(b) < 0, the root lies between them; halve
// the interval toward whichever sub-bracket keeps the sign change. Converges
// linearly but never diverges. Here f(x) = x² − 2, whose positive root is √2.
//
// soma run bisection_root.cell run
// ============================================================================
cell BisectionRoot {
face {
signal f(x: Float) -> Float
signal bisect(a: Float, b: Float, tol: Float) -> Float
signal run() -> Map
}
on f(x: Float) [native] {
return x * x - 2.0
}
on bisect(a: Float, b: Float, tol: Float) [native] {
let lo = a
let hi = b
let i = 0
while i < 200 {
let mid = (lo + hi) / 2.0
let fm = f(mid)
let width = hi - lo
if width < 0.0 { width = 0.0 - width }
if width < tol { return mid }
let flo = f(lo)
let same = 0
if flo < 0.0 {
if fm < 0.0 { same = 1 }
}
if flo >= 0.0 {
if fm >= 0.0 { same = 1 }
}
if same == 1 { lo = mid } else { hi = mid }
i = i + 1
}
return (lo + hi) / 2.0
}
on run() {
let r = bisect(0.0, 2.0, 0.0000000001)
return map("root", r, "f_root", f(r))
}
}
cell test BisectTests {
rules {
// positive root of x^2 - 2 is sqrt(2)
assert abs(bisect(0.0, 2.0, 0.0000000001) - 1.4142135623730951) < 0.00001
// f at the found root is ~0
assert abs(f(bisect(0.0, 2.0, 0.0000000001))) < 0.00001
}
}What the toolchain says
$ soma check bisection_root.cell
✓ All checks passed.$ soma test bisection_root.cell
[native] compiling 2 handler(s) for cell 'BisectionRoot'...
[native] compiled → .soma_cache/native/native_bisectionroot_fab867ab37eaf950.dylib
test BisectTests ...
✓ assert abs(bisect(0.0, 2.0, 0.0000000001) - 1.4142135623730951) < 0.00001
✓ assert abs(f(bisect(0.0, 2.0, 0.0000000001))) < 0.00001
2 tests: 2 passed, 0 failed$ soma verify bisection_root.cell
Verifying bisection_root.cell...
BisectionRoot/termination:
⚠ handler `bisect`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ `run` calls `BisectionRoot.bisect`, which may not terminate
0 passed, 2 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK$ soma run bisection_root.cell run
[native] using cached native_bisectionroot_fab867ab37eaf950.dylib for cell 'BisectionRoot'
{"root": 1.414213562355144, "f_root": -5.0773385495972434e-11}