Why isn't any kind of logic programming considered...
# thinking-together
n
Why isn't any kind of logic programming considered a model of computation? Why do we talk about Turing Machines and recursive functions as fundamental, but not inference? I can't find any resources discussing this disparity. It's like there are two classes of academics that don't talk to each other. Am I missing something?
☝️ 2
s
I'm not an expert, but logic programming a la prolog etc is usually based fundamentally on term rewriting, which is essentially what the untyped lambda calculus is. (Please correct me if I'm wrong, this is something I've been studying recently but I'm still quite new to the field)
n
Isn't term rewriting destructive, i.e. it consumes an input to produce an output?
s
I suppose? i am afraid I am not sure what the relation is and what you are getting at here. Would you consider beta-reduction "destructive"?
n
I guess a better question is: what is the "term" that is getting re-written in evaluating a logic program? Is it the entire program? As a conjunction of clauses? I guess the destructivity doesn't manifest in such a case because you're producing a "new program" (term) which you guarantee is going to be strictly larger than the last one (adding new deductions). That suggests term rewriting might be "too powerful" for logic programming though, because it can also model the deletion of facts (unless you want that capability, for some reason). But yeah, I'm now seeing how you could map inference to term rewriting!
a
Interesting. When logic shows up in the foundations of computing, it's usually in the context of the Curry-Howard isomorphism. From that perspective, logical inference is sort of... program synthesis, I think? More broadly, finding elements that occupy a type that represents a proposition. It could be that logical inference is (IIUC) inherently search-oriented, so people who make "models of computation" don't see it as a good primitive operation: too many steps and decisions behind the scenes. If that's the case, I think there's still some good mileage to be had from making a model where logical inference is stupid easy to write and tractable for an optimizer as well. (Uncoincidentally, this is an approach I'd like to do, but I don't know enough yet)
🤔 1
d
There probably are two classes of academics not talking, yes, and the logic folk seem to have lost the popularity race to the functional folk. You can implement functional programming with term rewriting or reduction and similarly you can use rewriting or reduction in proof systems. My memory of all this has faded since my university days mind you.
👍 1
Horn clauses are Turing Complete with tail recursion IIRC
s
http://maude.cs.illinois.edu/w/images/0/0d/Maude-book.pdf This may be of interest. I was pointed to it recently, and have been meaning to read it (though I haven't yet). As I understand it, it's a platform along the lines of Racket, except based on term rewriting rather than syntactic macros.
n
@S.M Mukarram Nainar I read some pages from that book just now, and the whole system looks overly complicated. Meanwhile the authors are using the words “simple”, “easy”, and “natural” everywhere, but I can’t find any good justification for why I should keep reading. The Wikipedia article is the same. It’s raising a lot of red flags.
🔥 1
@Andrew F Not all logic programming involves search. Each logic language comes with its own “standard” evaluation strategies, and by my understanding, each strategy effectively yields a different model of computation (including different time and space complexities).
☝️ 1
s
Well, it is an academic reference work. While unfortunate, I think that's pretty normal. I posted it because it is one of the few "production" systems based on term rewriting that I am aware of.
👍 1
p
@Nick Smith I think logic programming indeed began as identifying itself as a programming language: http://www-public.imtbs-tsp.eu/~gibson/Teaching/Teaching-ReadingMaterial/Kowalski74.pdf The extant thread of how this plays out I think is in the work of John Reynolds in the form of logic relations right now. But the present day incarnations that have the major mindshare happens to be Prolog variety of languages and I think its a fertile ground for bringing in novel work with it.