4 ms·

Prolog being tied to this very specific execution model of SLD resolution is somewhat root to the problems you have described. The promise of declerative progra

by maweki 3y ago

Prolog being tied to this very specific execution model of SLD resolution is somewhat root to the problems you have described. The promise of declerative programming in general, and logic and constraint programming specifically is, that programs are easier to reason about because the execution model is abstracted away and there's a relatively simple and mathematically pure definition of the model(s) of a program. But again and again one uses extralogical constructs in Prolog programming. Case in point: basically all your mentioned alternatives (Datalog, SMT, I'd add ASP) have implementations that use the Prolog syntax or something close to it with very similar semantics. But not being tied to that specific execution model can give you (better) answers or more complete answers, termination guarantees, or other things we might need.

usgroup 3y ago
I don’t think is true because ASP is not more popular than Prolog but it is essential (or at least much moreso) declarative. I think Prologs big strength amongst others is the meta interpreter and higher order functions which I think are essentially tied to SLD.
- discarded1023 3y ago
  Higher order functions! -- in Prolog! oh my. Prolog has predicates, not functions. (It has uninterpreted function symbols -- aka functors in this context.) It's based on first-order logic, i.e., it has nothing higher order in it, if you want to take it (formally) seriously. But of course there is `call/1` and so forth, which are just hacks... err, "non declarative". There are some interesting higher-order logic programming languages, e.g. Mercury. I like the approach taken by HiLog [1] as it struck me as (semantically) honest and simple. I don't know if it's usable. [1] https://en.wikipedia.org/wiki/HiLog https://en.wikipedia.org/wiki/HiLog
  - usgroup 3y ago
    * Higher order predicates. Prolog has them.
  - YeGoblynQueenne 3y ago
    Prolog is not first-order. That's how it's described but it lacks the fundamental distinction between predicate and function symbols that makes First-Order Logic, first-order. To clarify. A FOL language begins with an "alphabet" (sometimes called a "signature") of predicate symbols, function symbols (including constants), variables, the five logical connectives (¬, ∧, ∨, →, and ↔) and punctuation (left and right parens, comma, dot, colon). The sets of predicate, function and variable symbols are disjoint. Function symbols are used to define terms, inductively, as follows. A variable is a term; a constant is a term; if f is a function symbol and t_1, ..., t_n are terms, then f(t_1, ..., t_n) is a term. Terms are used to define formulae as follows: If P is a predicate symbol and t_1, ..., t_n are terms, then P(t_1, ..., t_n) is an atomic formula, or atom. If φ is a formula, then ¬φ is a formula. If φ, ψ are formulae, then φ ∧ ψ, φ ∨ ψ, φ → ψ, and φ ↔ ψ are formulae. Literals and clauses are defined as follows: if A is an atom, then A is a positive literal and ¬A is a negative literal. A clause is a disjunction of literals. A clause with a single positive literal is definite. A definite clause with no function symbols other than constants is datalog. Now, if you squint a bit at all of the above and then at a Prolog program you will see a serious violation of the rules of FOL syntax. Observe: This is Prolog: p(x, y):- q(r(x),z), r(p(x,z)). See? r/1 and p/2 are used both as the symbols of terms and as the symbols of atomic formulae. That is a violation of FOL syntax. What's more, it's a violation of the "first-order" nature of FOL, where functions are "at a lower order" than predicates. That is, in FOL, terms map to entities in the domain of discourse, whereas formulae map to relations over entities in the domain of discourse. But Prolog doesn't care. Prolog doesn't care if an object is a predicate, or a function, if it's a mapping, or a relation. For Prolog there's no distinction, and because there's no distinction it can treat everything as an argument to everything else: an atomic formula can be "passed" to an atomic formula, and taken apart, and put back together again. For example, you can do this sort of thing: ?- T_ =.. [p,X,Y,Z], T =.. [r,T_]. T_ = p(X, Y, Z), T = r(p(X, Y, Z)). That is no first-order functionality! In fact, in Prolog you can write this sort of thing: prove(L):- true. prove(L,Ls):- prove(L), prove(Ls). prove(L):- L \= (_,_), clause(L,Bs), prove(Bs). And that is a Prolog interpreter written in Prolog. A program that evaluates programs? Toto, I don't think we're in FOL anymore.
    - discarded1023 3y ago
felixyz 3y ago
As I mentioned in another comment, SLG resolution (implemented in XSB Prolog and more recently in SWI-Prolog) does alter the execution model in a way that makes it easier to avoid extralogical constructs. And the wide availability of deeply integrated CLP modules for eg SWI-Prolog also makes it easier to keep programs purely logical.
- maweki 3y ago
  You are correct. Though in my institution we do not get around to teaching that in that one semester of elective LP.
YeGoblynQueenne 3y ago
>> Case in point: basically all your mentioned alternatives (Datalog, SMT, I'd add ASP) have implementations that use the Prolog syntax or something close to it with very similar semantics. But not being tied to that specific execution model can give you (better) answers or more complete answers, termination guarantees, or other things we might need. To clarify, datalog is a restriction of Prolog excluding functions of more than 0 arguments (i.e. constants). For example, P(x,y) :- Q(f(x), g(y)) is Prolog but not datalog. There's also a restriction in the sharing of variables between head and body literals that ensures termination. The point of datalog is that because of its function-free structure it's decidable. You could simply ground a datalog program and get its entire Herbrand model. SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint solving. I don't know why it (or SAT) is compared to Prolog which has nothing to do with boolean satisfiability problems. ASP also has nothing much to do with Prolog. It's a strictly first-order language (Prolog is higher-order) that is based on the idea of stable model semantics. Very briefly, a stable model is often the set of queries to which Prolog will answer "true" (or "yes" depending on the interpreter). ASP programs share some syntax with Prolog, but are not definite programs. For one thing, ASP allows classical negation, alongside Prolog's Negation-As-Failure. ASP is said to be well-suited to optimisation problems but to me it's more interesting as a formal treatment of reasoning under uncertainty in a strictly logic framework. Note that datalog is incomplete (obviously, since it doesn't have functions) and ASP solvers are NP-complete. They are also special-purpose languages, so for example nobody is going to write a web server in ASP anytime soon. By comparison, the SWI-Prolog website runs on a web server written in Prolog (https://eu.swi-prolog.org/dogfood.html https://eu.swi-prolog.org/dogfood.html).
- chriswarbo 3y ago
  > SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint solving. I don't know why it (or SAT) is compared to Prolog which has nothing to do with boolean satisfiability problems. SMT and SAT are certainly less expressive than Prolog (or more abstract systems, like LambdaProlog, Isabelle/HOL, etc.), so they cannot express the same structures/abstractions. However, given any "concrete" query/program, we can collapse all of its structure, in-line/unroll all of its higher-order parts, etc. to get a SAT formula (modulo the halting problem). The resulting term is usually exponentially-larger than the original; but SAT solvers have become fast enough to handle such giant problems. (SMT solvers are usually wrappers around a SAT solver too)

by maweki 3y ago

usgroup 3y ago

I don’t think is true because ASP is not more popular than Prolog but it is essential (or at least much moreso) declarative. I think Prologs big strength amongst others is the meta interpreter and higher order functions which I think are essentially tied to SLD.

discarded1023 3y ago
Higher order functions! -- in Prolog! oh my. Prolog has predicates, not functions. (It has uninterpreted function symbols -- aka functors in this context.) It's based on first-order logic, i.e., it has nothing higher order in it, if you want to take it (formally) seriously. But of course there is `call/1` and so forth, which are just hacks... err, "non declarative". There are some interesting higher-order logic programming languages, e.g. Mercury. I like the approach taken by HiLog [1] as it struck me as (semantically) honest and simple. I don't know if it's usable. [1] https://en.wikipedia.org/wiki/HiLog https://en.wikipedia.org/wiki/HiLog
- usgroup 3y ago
  * Higher order predicates. Prolog has them.
- YeGoblynQueenne 3y ago
  Prolog is not first-order. That's how it's described but it lacks the fundamental distinction between predicate and function symbols that makes First-Order Logic, first-order. To clarify. A FOL language begins with an "alphabet" (sometimes called a "signature") of predicate symbols, function symbols (including constants), variables, the five logical connectives (¬, ∧, ∨, →, and ↔) and punctuation (left and right parens, comma, dot, colon). The sets of predicate, function and variable symbols are disjoint. Function symbols are used to define terms, inductively, as follows. A variable is a term; a constant is a term; if f is a function symbol and t_1, ..., t_n are terms, then f(t_1, ..., t_n) is a term. Terms are used to define formulae as follows: If P is a predicate symbol and t_1, ..., t_n are terms, then P(t_1, ..., t_n) is an atomic formula, or atom. If φ is a formula, then ¬φ is a formula. If φ, ψ are formulae, then φ ∧ ψ, φ ∨ ψ, φ → ψ, and φ ↔ ψ are formulae. Literals and clauses are defined as follows: if A is an atom, then A is a positive literal and ¬A is a negative literal. A clause is a disjunction of literals. A clause with a single positive literal is definite. A definite clause with no function symbols other than constants is datalog. Now, if you squint a bit at all of the above and then at a Prolog program you will see a serious violation of the rules of FOL syntax. Observe: This is Prolog: p(x, y):- q(r(x),z), r(p(x,z)). See? r/1 and p/2 are used both as the symbols of terms and as the symbols of atomic formulae. That is a violation of FOL syntax. What's more, it's a violation of the "first-order" nature of FOL, where functions are "at a lower order" than predicates. That is, in FOL, terms map to entities in the domain of discourse, whereas formulae map to relations over entities in the domain of discourse. But Prolog doesn't care. Prolog doesn't care if an object is a predicate, or a function, if it's a mapping, or a relation. For Prolog there's no distinction, and because there's no distinction it can treat everything as an argument to everything else: an atomic formula can be "passed" to an atomic formula, and taken apart, and put back together again. For example, you can do this sort of thing: ?- T_ =.. [p,X,Y,Z], T =.. [r,T_]. T_ = p(X, Y, Z), T = r(p(X, Y, Z)). That is no first-order functionality! In fact, in Prolog you can write this sort of thing: prove(L):- true. prove(L,Ls):- prove(L), prove(Ls). prove(L):- L \= (_,_), clause(L,Bs), prove(Bs). And that is a Prolog interpreter written in Prolog. A program that evaluates programs? Toto, I don't think we're in FOL anymore.
  - discarded1023 3y ago

felixyz 3y ago

As I mentioned in another comment, SLG resolution (implemented in XSB Prolog and more recently in SWI-Prolog) does alter the execution model in a way that makes it easier to avoid extralogical constructs. And the wide availability of deeply integrated CLP modules for eg SWI-Prolog also makes it easier to keep programs purely logical.

maweki 3y ago
You are correct. Though in my institution we do not get around to teaching that in that one semester of elective LP.

YeGoblynQueenne 3y ago

>> Case in point: basically all your mentioned alternatives (Datalog, SMT, I'd add ASP) have implementations that use the Prolog syntax or something close to it with very similar semantics. But not being tied to that specific execution model can give you (better) answers or more complete answers, termination guarantees, or other things we might need. To clarify, datalog is a restriction of Prolog excluding functions of more than 0 arguments (i.e. constants). For example, P(x,y) :- Q(f(x), g(y)) is Prolog but not datalog. There's also a restriction in the sharing of variables between head and body literals that ensures termination. The point of datalog is that because of its function-free structure it's decidable. You could simply ground a datalog program and get its entire Herbrand model. SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint solving. I don't know why it (or SAT) is compared to Prolog which has nothing to do with boolean satisfiability problems. ASP also has nothing much to do with Prolog. It's a strictly first-order language (Prolog is higher-order) that is based on the idea of stable model semantics. Very briefly, a stable model is often the set of queries to which Prolog will answer "true" (or "yes" depending on the interpreter). ASP programs share some syntax with Prolog, but are not definite programs. For one thing, ASP allows classical negation, alongside Prolog's Negation-As-Failure. ASP is said to be well-suited to optimisation problems but to me it's more interesting as a formal treatment of reasoning under uncertainty in a strictly logic framework. Note that datalog is incomplete (obviously, since it doesn't have functions) and ASP solvers are NP-complete. They are also special-purpose languages, so for example nobody is going to write a web server in ASP anytime soon. By comparison, the SWI-Prolog website runs on a web server written in Prolog (https://eu.swi-prolog.org/dogfood.html https://eu.swi-prolog.org/dogfood.html).

chriswarbo 3y ago
> SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint solving. I don't know why it (or SAT) is compared to Prolog which has nothing to do with boolean satisfiability problems. SMT and SAT are certainly less expressive than Prolog (or more abstract systems, like LambdaProlog, Isabelle/HOL, etc.), so they cannot express the same structures/abstractions. However, given any "concrete" query/program, we can collapse all of its structure, in-line/unroll all of its higher-order parts, etc. to get a SAT formula (modulo the halting problem). The resulting term is usually exponentially-larger than the original; but SAT solvers have become fast enough to handle such giant problems. (SMT solvers are usually wrappers around a SAT solver too)