4 ms·

I didn't edit my original comment. Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power.

YeGoblynQueenne 1y ago
Then I misunderstood your comment, but at the same time your comment is correct but irrelevant to the OP. "In the general case" there are undecidable problems, and there may even be an infinite number of undecidable problems, but there are most likely an infinite number of decidable problems also. That is to say, undecidability is not like intractability. One can work around undecidability, and one can always find useful problems that can be solved without falling down undecidable holes. So for example, the Halting Problem may be undecidable, but we have computers we use all the time to do a whole bunch of very useful things. FOL is undecidable, but elementary Boolean logic is decidable and definite logic is semi-decidable. Any formal system powerful enough to represent integer arithmetic is undecidable but we use arithmetic, and higher-level maths based on arithmetic, all the time. And so on, and so forth. The OP is asking for a program synthesiser where they can enter a specification in a logic language and get back a program in some other language. That is perfectly doable in practice, there's an entire field of research that produces work along those lines, the field of Program Synthesis. Modern LLMs can to some extent do that, very unreliably, and of course like I say, a compiler is nothing but a (deductive) program synthesiser, your unwillingness to accept that well-understood truism non-withstanding. >> Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power. That's incorrect about Prolog. Prolog is SLD-Resolution, i.e. Linear Resolution with a Selection rule restricted to Definite clauses. Definite logic is a restriction of the first order predicate calculus that nevertheless retains its full expressive power, and is semi-decidable (all true statements in definite logic are provable). Most implementations of Prolog executed by Depth-First Search are incomplete because they get stuck in loops, but Prolog executed by SLG-Resolution (a.k.a. tabling) is refutation-complete. Prolog is probably the closest practical programming language that achieves what the OP is looking for (although not strictly in program synthesis terms) but the OP may also want to check out things like Z notation: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation
- emorning3 1y ago
  Wow! I was unfamiliar with Z and just spent an hour going down the Z and B-Method rabbit hole. That's exactly the kind of thing I was looking for, thanks!

YeGoblynQueenne 1y ago

Then I misunderstood your comment, but at the same time your comment is correct but irrelevant to the OP. "In the general case" there are undecidable problems, and there may even be an infinite number of undecidable problems, but there are most likely an infinite number of decidable problems also. That is to say, undecidability is not like intractability. One can work around undecidability, and one can always find useful problems that can be solved without falling down undecidable holes. So for example, the Halting Problem may be undecidable, but we have computers we use all the time to do a whole bunch of very useful things. FOL is undecidable, but elementary Boolean logic is decidable and definite logic is semi-decidable. Any formal system powerful enough to represent integer arithmetic is undecidable but we use arithmetic, and higher-level maths based on arithmetic, all the time. And so on, and so forth. The OP is asking for a program synthesiser where they can enter a specification in a logic language and get back a program in some other language. That is perfectly doable in practice, there's an entire field of research that produces work along those lines, the field of Program Synthesis. Modern LLMs can to some extent do that, very unreliably, and of course like I say, a compiler is nothing but a (deductive) program synthesiser, your unwillingness to accept that well-understood truism non-withstanding. >> Compilers are totally besides the point. Python, Java and even Prolog aren't FOL, they lack its expressive power. That's incorrect about Prolog. Prolog is SLD-Resolution, i.e. Linear Resolution with a Selection rule restricted to Definite clauses. Definite logic is a restriction of the first order predicate calculus that nevertheless retains its full expressive power, and is semi-decidable (all true statements in definite logic are provable). Most implementations of Prolog executed by Depth-First Search are incomplete because they get stuck in loops, but Prolog executed by SLG-Resolution (a.k.a. tabling) is refutation-complete. Prolog is probably the closest practical programming language that achieves what the OP is looking for (although not strictly in program synthesis terms) but the OP may also want to check out things like Z notation: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation

emorning3 1y ago
Wow! I was unfamiliar with Z and just spent an hour going down the Z and B-Method rabbit hole. That's exactly the kind of thing I was looking for, thanks!