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 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

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)


(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?)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.