Overengineered in my view, what is wrong with `x | f` is `f(x)`? Then `x | f | g` can be read as `g(f(x))` and you're done. I don't see any reason to make it more complicated than that.
> If you don't know why set theory is important, it is because set theory is the foundation of all of mathematics.
Sorry to burst your bubble, but as far as we know, that isn't true in the slightest. It's a logical positivist view abandoned after Goedel and Turing.
At best: What we hope is true is that there often is some axiomatic system where a specific mathematical lemma makes sense when redefined into something similar but not the same.
The problem with Prolog is that it's based on unification, and small unification engines can be expressed in a few lines in any functional programming language.
That narrows down the already small niche where one would choose Prolog by probably a few orders.
Is this in the same sense that "one could write lisp in 99 lines of c"?
In my opinion, this does not imply that proper lisp (and correspondingly prolog) implementations are useless, just because a simple implementation can be written in a different, "more expressive" language.
There is a very practical embedable logic-programming engine called miniKanren for many programming languages that can be used to add the logic-programming techniques of Prolog to other languages.
No, not really. A lisp in 99 lines of C would barely be useful. In contrast, Prolog mostly shines where you need reasoning/unification over a database of facts -happens pretty often,- but that's just too easily expressed in any proper functional language. And with a bit more pain in an imperative/OO language.
What makes Prolog, Prolog is not unification on its own but SLD-Resolution with unification, where "SLD" stands for [L]inear Resolution with a [S]election rule restricted to [D]efinite clauses. If you know your Resolution typology, that means soundness and refutation-completeness (or completeness with subsumption) [1].
I don't think I've ever seen a discussion of Resolution in functional programming textbook implementations of "Prolog". They typically just bodge some depth-first search with backtracking and unification in polish notation and call it "Prolog", or "logic programming". A bit like if I wrote a "lisp" with eval(X):- call(X), then completely ignored all that jazz about lambda calculus and concentrated on garbage collection and linked lists.
A good starting point instead, if one wishes to understand Prolog and not just dismiss it out of hand, is to try and understand Resolution, and what unification does for Resolution, and why it ended up in Prolog (and how) in the first place. I'd start, well, at the beginning:
A Machine-Oriented Logic Based on the Resolution Principle
Where you can follow the progress from ground Resolution, to unification, the Resolution theorem, and all the way to the (pre-modern) Subsumption Theorem. It's a long way to Prolog from there, but that's where it all begins.
_______________
[1] Although Prolog implemented by DFS is not complete if Prolog implemented by DFS is not complete (etc).
I've been using Prolog daily for the past 1.5 years. I've also implemented and used a Kanren in Elm, and there is simply a world of practical difference.
This isn't news to any logician or people working in formal methods. More like a mathematician getting his head around what has been thought about for decades, if not centuries.
