Bounded minimization

ID: bounded-minimization

Search over the finite interval 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.

New to topics? Read the docs here!