Comment by fizixer | Hacker News Reader

Comment by fizixer | Hacker News Reader

Parent Full thread

Rant alert: I've realized there is a big problem with logic programming: the two cultures of mathematical logic, and logic programming.

In math logic, you learn propositional/sentential logic, then spend a lot of time with predicate/first-order logic. At this point, you can "return to mathematics" to do any math stuff imaginable under the sun. However, if you want to spend more time being a logician, you can delve into a wide variety of topics, second-order logics, constructive logic, model theory, proof theory, etc, etc, etc.

Computer-science/logic-programmers on the other end?

First they don't start with prop or pred logic. Absolutely zero building-from-the-ground up about how you could do computations using prop, then maybe move to more sophisticated stuff like pred logic.

No, they will throw Hoare logic at you, and Horn clauses, and relational databases, and bound and free variables, and cuts, and what not. And if you complain, I guess you're just not cut out for logic programming. (I guess hardcore full-time mathematical logicians are not cut-out for that either, including Godel mind you).

You think they'd stop there. I'm afraid not, far from it.

Next they want you to spend all your time about learning about Church and Turing, and Curry-Howard correspondence, and to pretend like "real" logic started in 1933, and 1936, because anything before lambda-calculus is too inferior to be used in computers.

Oh but wait, they're not done yet.

Now they want you learning a brand new foundation of logic, math, and CS, that even mathematicians hardly need or use for 99% of their work. They want you to think in terms of type theory, and category theory. (So I guess when they say 'brand new foundation' they really mean 'brand new pair of foundations from which you can pick').

I'm starting to think there is something seriously wrong with the way logic is approached in theoretical CS, and logic programming. It's not minimal, and appears to serve as an elitist gatekeeping device, while mathematicians are going about their daily lives producing spectacular results with just prop+pred logic, and category theory has only started getting used in a tiny fraction of mathematical work.

You're right that it's hard. However, I think you're missing one significant point that, at least to some extent, justifies the hardness: computability.

Systems like Prolog are based on the idea of "proof search": given a logical statement, find a proof of that statement. Humans do this all the time with classical logic, you might say -- but then, there are very famous statements expressible purely in first-order logic that nobody has found a proof of. This is anathema to computing! We want an "effective method", a "decision procedure", that allows us to compute for finite time and terminate with a positive (or negative!) proof. And we know, thanks to Gödel, that no such procedure exists for first-order logic: any decision procedure will miss proofs for some first-order statements.

In order to give ourselves more options for proof search, we need to enrich our logics somehow. This enrichment usually comes in the form of restrictions relative to classical logic. For example, Horn clauses are a fragment of classical logic that we _can_ assign a reasonable decision procedure to -- of which the most basic is probably SLD resolution. But these restrictions traditionally sacrifice more power than we'd like, so we add various things back in, trading computational difficulty (but not decidability!) for expressivity. This is a significant source of complexity, no doubt!

Computational logic is hard because we're asking more of it. Classical logic has been around since at least Aristotle, so it's perhaps no surprise that it's been refined into such a simple, well-understood form. Even then, I think if you traveled into various classical modal logics, you'd find those just as inscrutable at first as the logics we use in logic programming.

> Hoare logic

Mmh... For the most part, Hoare logic is back on the "for humans" side of things, as it's about verifying software rather than implementing software. It brings to bear the full power of classical logic(1), but since you're applying it to programs, most of which have incredibly non-monotonic semantics, you have to consider truth at each point in the program. Most of the machinery in Hoare logic over classical logic is about relating all of those points -- all of those worlds, in a model-theoretic sense.

I personally find Hoare logic easier from a mathematical reasoning perspective than any of the logic systems designed for implementation. I think that makes sense, though, because Hoare logic is not about automation.

(1) You can instantiate Hoare logic over any particular logical system, so you could apply it for automated verification, but I don't think that's the case the parent was considering.

Some of your points are taken seriously! Think of purifying Prolog such that cuts and the like are (for many cases) no longer needed, yet you get comparable efficiency. See library(reif), library(pio), ...

Think about implication in propositional logic. Take two entirely unrelated propositions a and b. According to this logic either a → b or b → a is true. This, btw, cannot happen in Prolog.

Reply on news.ycombinator.com