3 ms·
Are you sure ACL2 isn't Turing complete? I can't seem to find a proof of this.
by simulate-me 5y ago
Are you sure ACL2 isn't Turing complete? I can't seem to find a proof of this.
- fiddlerwoaroof 5y agoIt’s embedded in a Turing complete language, but you can’t prove theorems about programs written in a Turing-complete language (Rice’s Theorem) so the ACL2 language itself has to be limited to programs that can be determined to halt. The J-Bob language from the book The Little Prover might be a better example. There’s a whole programming paradigm here of languages that aren’t Turing complete: https://en.m.wikipedia.org/wiki/Total_functional_programming https://en.m.wikipedia.org/wiki/Total_functional_programming