Several computation models have representative programming language counterparts, as, according to this answer, Snobol for rewriting systems, APL for combinators, Lisp/Scheme for lambda calculus, and off course the family of imperative languages for TMs (or more precisely RAMs). It seems to me that Prolog should also be a paradigmatic language for some model. Is this assumption true? If so, what is the name of that model?
-
2$\begingroup$ Logic programming. $\endgroup$Yuval Filmus– Yuval Filmus2018年04月08日 18:57:16 +00:00Commented Apr 8, 2018 at 18:57
-
1$\begingroup$ I mean something like "lambda calculus" for which there is a formal proof showing it's equivalent to a TM. $\endgroup$user_163417– user_1634172018年04月08日 19:04:50 +00:00Commented Apr 8, 2018 at 19:04
-
$\begingroup$ I would say inference systems (a. k. a. formal systems, deduction systems, proof systems (a special case)). $\endgroup$beroal– beroal2018年04月13日 18:49:52 +00:00Commented Apr 13, 2018 at 18:49
1 Answer 1
I think the computation model of Prolog is the SLDNF resolution of Horn clauses.
Prolog is actually very procedural. Kowalski 1974: "The interpretation of predicate logic as a programming language is based upon the interpretation of implications [...] as procedure declarations [...]" (emphasis mine)
https://www.doc.ic.ac.uk/~rak/papers/IFIP%2074.pdf
(However, lambda calculus, theorem provers, and Turing machines are term rewriting systems indeed. What is a computational model then, if everything is a term rewriting system?)