Computable bound on halting time (source code)

= Computable bound on halting time
{title2=$t_M(n)\leq f(n)$}

A machine's halting times admit a <total computable function> as a bound on all inputs in its domain if and only if that domain is a <computable set>. A bound decides the domain by finite simulation; conversely, a domain decider allows returning zero outside the domain and the exactly simulated halting time inside it. In particular every machine computing a <total computable function> has an exact computable running-time function, while nontotal machines may or may not have total bounds.