Excellent point, but perhaps termination is just a detail. We already know that it's unsolvable. What's the rush?
Next you'll be telling me that different polynomials in P matter, like O(n^27) is too slow or at least requires attention to constants and scale.
This construction also solves the divide-by-zero problem very elegantly. When we promote Natural Zero to Real, we make sure that it's something like:
(1, λ_:Unit. (1/2, λ_:Unit. (1/3, λ...)))
This makes division by zero a legal operation (pointwise division of sequences) if we extend our tolerance to sequences without the Cauchy property (and why not? It's just bits).
Next you'll be telling me that different polynomials in P matter, like O(n^27) is too slow or at least requires attention to constants and scale.
This construction also solves the divide-by-zero problem very elegantly. When we promote Natural Zero to Real, we make sure that it's something like:
This makes division by zero a legal operation (pointwise division of sequences) if we extend our tolerance to sequences without the Cauchy property (and why not? It's just bits).