Re:Grappling with Infinity in Constraint Solvers
by Animats on Sunday November 17, 2019 @04:21PM
(#21560121)
Nice.
Recursive functions are possible in a total system as long as the recursion depth is bounded. The original Boyer-Moore theorem prover (1978) had that. You had to prove termination for every recursive function by giving a depth value, which could be a function of the inputs. For example,
(times x y)
defined as
(if (zerop x) 0 (add (y (times (sub1 x) y))
would have a depth limit of "x". (Note that in this world, x and y are nonnegative integers and (sub1 0) is 0.)
There's a lot to be said for working with total functions and finite arithmetic. No undecidability, no halting problem.
Recursive functions are possible in a total system as long as the recursion depth is bounded. The original Boyer-Moore theorem prover (1978) had that. You had to prove termination for every recursive function by giving a depth value, which could be a function of the inputs. For example,
defined as would have a depth limit of "x". (Note that in this world, x and y are nonnegative integers and (sub1 0) is 0.)There's a lot to be said for working with total functions and finite arithmetic. No undecidability, no halting problem.