Grappling with Infinity in Constraint Solvers

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.

This is Chris Patuzzo! His work does not get enough attention.

He mentioned Sentient Lang in the article. It is really, really cool. Its a compile-to-JS declarative logic language that can do some fucking neat stuff. Think Prolog or Mercury, but with much more comprehensible syntax.

https://sentient-lang.org/

I reached out to him a month or two ago after stumbling upon his work, and he took the time to respond and have a conversation with me.

Incredibly brilliant and genuine guy, happy to see more of his stuff posted here.

Edit: He has done more stuff besides Sentient. Check out his work in the general area of computational logic/automated theorem proving.

It is also possible to build a model of Presburger arithmetic extended with infinity. We did that a few years back, you can try it out online here - http://loris-5.d2.comp.nus.edu.sg/SLPAInf/

Very interesting, thank you for this writeup!

Regarding the following considerations:

"After a few seconds this program terminates which seems wrong. Why should a problem that has infinitely many solutions ever terminate? Shouldn’t it run forever?"

Yes, conceptually, it should of course run forever. However, at some point, even when using unbounded integers (which it, in my view, also should do), it will eventually run out of memory because the representations of involved bounds will exceed what can be stored.

In such cases, from a correctness perspective, it is inadmissible to simply stop "silently", because that would be indistinguishable from cases in which there are no (further) solutions.

Instead, some kind of error should be raised, indicating that it was not possible to search further than that. And when using bounded integers, likewise an error should be raised if some internal range is exceeded when searching for solutions.

This seems like a tricky problem to solve. I think a practical use of constraint solvers would have some criteria by which a solution would be seen as desirable.

For eg if I’m designing something in the real world I’d want to optimize for material or cost in terms of time or money.

Sometimes I’m just interested in seeing if a solution exists.

So the solution here seems to be able to add soft constraints on what kinds of solutions are desired to guide the search.