Bounded minimization
= Bounded minimization
{title2=$\mu y\leq b$}
Search over the finite interval $0\leq y\leq b$ for the least witness to a <primitive recursive> predicate, with an explicitly chosen default if there is none. The result is a <primitive recursive function>, by scanning this finite interval using <primitive recursion>. This differs from <unbounded minimization>, which may fail to terminate.