3 ms·
On the other hand, ACL2 isn’t Turing complete but can express many interesting programs: https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.h
by fiddlerwoaroof 5y ago
On the other hand, ACL2 isn’t Turing complete but can express many interesting programs: https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=ACL2____TUTORIAL1-TOWERS-OF-HANOI https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-man...
- simulate-me 5y agoAre 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