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?
$\begingroup$
$\endgroup$
-
2$\begingroup$ Logic programming. $\endgroup$ – Yuval Filmus Apr 8 '18 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$ – Kaveh Apr 8 '18 at 19:04
-
$\begingroup$ I would say inference systems (a. k. a. formal systems, deduction systems, proof systems (a special case)). $\endgroup$ – beroal Apr 13 '18 at 18:49
$\begingroup$
$\endgroup$
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?)
