6 ms·

I've been looking at the Clojure implementation, core.logic, but can never figure out what to use this paradigm for. Can anybody name the cases where logic prog

I've been looking at the Clojure implementation, core.logic, but can never figure out what to use this paradigm for. Can anybody name the cases where logic programming really shines?

CJefferson 8y ago
It is useful for problems where the solution is difficult to find -- any kind of problem with many constraints which conflict, and maybe an optimisation condition. Such problems are very difficult from most programming, when it tends to be way to find what you want (although of course you can always optimise it further).
- weberc2 8y ago
  This sounds like a layout engine for a GUI toolkit. If you have a bunch of widgets with optional min and max widths and other constraints and you put them all in the same row, the layout engine needs to compute the real size of each widget (also constrained by the width of the parent widget, which is also dynamic and resolved by the layout engine save for the top level window widget) so it can be rendered.
  - typon 8y ago
    You can use standard constraint solvers for these kinds of problems. Although, you can use minikanren in such an application, you are missing out on a lot of its power if you do that. An example where such systems shine is program generation, theorem proving, knowledge databases, program verification and other applications where the search space is huge but the rules are relatively simple.
- simongray 8y ago
  Ok, thanks for answering. I guess what I'm really looking for are some practical use cases that can serve as an example, otherwise it will never cross my mind to use logic programming when I need to decide on technologies.
  - Blackthorn 8y ago
    Basically -- anything that you'd use SQL for. SQL is probably the most widely-used logic programming language.
    - typon 8y ago
      SQL does way less things than a full-blown logic programming system
      - Blackthorn 8y ago
        With common table expressions and windowing, SQL is Turing complete.
        typon 8y ago
        So is LaTeX...but people aren't implementing logic programs in it.
        Blackthorn 8y ago
        The argument is that minikanren does more than SQL. I strongly disagree.
        haolez 8y ago
        Care to elaborate? Genuinely curious.
        yorwba 8y ago
        Languages of all kinds of paradigms are Turing complete. But we still use different languages for different purposes, because some programs are more convenient to write in a certain paradigm that maps well to their problem domain. In Prolog for example, you can easily define concatenation of cons-lists as concatenate(nil, Ys, Ys). concatenate(cons(X, Xs), Ys, cons(X, Zs)) :- concatenate(Xs, Ys, Zs). and then generate all 4 possible solutions for the query concatenate(X, Y, cons(1, cons(2, cons(3, nil)))). Of course Prolog has built-in lists that'd allow simply writing append(X, Y, [1, 2, 3]), but the ease of defining certain simple algorithms and then running them backwards is what makes logic programming so useful in my opinion. If SQL can express an equivalent program equally succinctly, I'd very much like to see how.
kimi 8y ago
Solving Sudoku :-)
agumonkey 8y ago
IMO it sits at quite a higher level of programming. You use logic programming to explore ~infinite program states; all that in extremely concise (near fully declarative of course) ways. In Bratko's prolog book you quickly get to do graph processing, some algorithms are 4 clauses and almost word for word what you have in mind. It's mind boggling to me. You also have bidirectional reasoning, you don't have to write a function A => B and then another one for B => A. It's even more telling with multivariate functions. I knew a guy who needed something similar for a large application. He needed a way to reason backward with incomplete parameters.
otabdeveloper1 8y ago
"Logic programming" is a misnomer. It's really a kind of parallel reality database query language. It's not used much because relational databases and SQL won in the end. (I guess back in the day people imagined computers as knowledge graphs and logical predicates on them, not tabular data and joins.)
- convolvatron 8y ago
  why a misnomer? its exactly what programming would look like if you wanted to try to implement computing as predicate calculus.
a-saleh 8y ago
I would look at uKanren, the smallest mini-kanren cousin. I like Bodil Stokke's [1] introduction, but if you are not afraid of lisp, you can read/re-implement the original(?) [2] paper :) It is basically bunch of combinators for depth-first search? So if you think "I kinda want to brute-force solution for these hard-coded constraints", you might instead want to create a simple logic-programming environment first :-) Last time I played with these, I used it for implementing a toy cryptograhic protocol verification system for a term project. It have barely worked :D A.f.a.i.k. type-checkers often use some sort of logic programming at their core. [1] https://paperswelove.org/2015/video/bodil-stokke-%CE%BCkanren/ https://paperswelove.org/2015/video/bodil-stokke-%CE%BCkanre... [2] http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
KirinDave 8y ago
Sure, I can name one I've prototyped (but never gotten to deploy in prod) in industry. I proposed an embedded μKanren in an Authorization framework for API endpoints. It relied on a system like JWT (or, preferably something less broken like Macaroons) to provide a series of "auth grants" on the request, auth grants being parameterized lines like: (= :user-id 16) (bu.admin-grant (group 10)) (is-super-admin) A few more like this. Then, you could use Python annotations on API methods to specify this kind of setup on API endpoints: (= :group_id request.group-id) (bu.admin_grant (group :group-id)) The system would then perform a kind of logical unification with the request, the cryptographically validated request token, and the API policy. When a request comes in, the request token is merged a "all is forbidden" default set (which is not a literal hash table, it's a policy annotation for the map that contains them). Thus, it's very easy to create arbitrarily complex security policies and so long as they're logically consistent, the interpreter can tell you so (and if it fails, it can tell you why the request doesn't have access). What's also interesting was that you could unify the API endpoint annotations with an empty set of grants, and then it'd produce a series of example permissions that would be valid (or you could merge it with a user's invalid grants, and it could tell you what access they need to go through). This worked well for internal documentation and I had hoped that it'd be applicable to internal tooling to explain to an operator of a tool what access they needed to go request to use the tool (and even where to do it). If you're curious, for most requests the time complexity and memory costs were very modest (approaching but not passing 1ms in the worst case I saw, which for API endpoints written in Python is usually dwarfed by garbage like JSON serialization).
tom_mellior 8y ago
Here is mediKanren (from the same authors): https://github.com/webyrd/mediKanren https://github.com/webyrd/mediKanren It's used for automated search through medical databases for drug discovery: https://www.uab.edu/mix/stories/a-high-speed-dr-house-for-medical-breakthroughs https://www.uab.edu/mix/stories/a-high-speed-dr-house-for-me... Here is the Gerrit code review system: https://www.gerritcodereview.com/ https://www.gerritcodereview.com/ It allows you to specify complex rules for workflows, who may sign off on what patches etc. Those rules are written in Prolog, but I guess they might as well be written in some other logic language. Here is (or rather, will be) Gigahorse, an Ethereum smart contract decompiler: https://2019.icse-conferences.org/event/icse-2019-technical-papers-gigahorse-thorough-declarative-decompilation-of-smart-contracts https://2019.icse-conferences.org/event/icse-2019-technical-... The abstract doesn't say what "declarative, logic-based specification" is used in the implementation, but I know that two of the authors do a lot of work in Datalog, so it's Datalog.
avhon1 8y ago
I took a class with Daniel Friedman, the creator of Minikanren and author of The [Little|Seasoned|Reasoned] Schemer. One of the homework assignments was to write a typechecker for the simply-typed lambda calculus in minikanren. (Most of the semester, we were writing interpreters for the lambda calculus, and doing things like rewriting the interpreter in continuation-passing-style (so that every recursive call was a tail call).)

I've been looking at the Clojure implementation, core.logic, but can never figure out what to use this paradigm for. Can anybody name the cases where logic programming really shines?

CJefferson 8y ago

It is useful for problems where the solution is difficult to find -- any kind of problem with many constraints which conflict, and maybe an optimisation condition. Such problems are very difficult from most programming, when it tends to be way to find what you want (although of course you can always optimise it further).

weberc2 8y ago
This sounds like a layout engine for a GUI toolkit. If you have a bunch of widgets with optional min and max widths and other constraints and you put them all in the same row, the layout engine needs to compute the real size of each widget (also constrained by the width of the parent widget, which is also dynamic and resolved by the layout engine save for the top level window widget) so it can be rendered.
- typon 8y ago
  You can use standard constraint solvers for these kinds of problems. Although, you can use minikanren in such an application, you are missing out on a lot of its power if you do that. An example where such systems shine is program generation, theorem proving, knowledge databases, program verification and other applications where the search space is huge but the rules are relatively simple.
simongray 8y ago
Ok, thanks for answering. I guess what I'm really looking for are some practical use cases that can serve as an example, otherwise it will never cross my mind to use logic programming when I need to decide on technologies.
- Blackthorn 8y ago
  Basically -- anything that you'd use SQL for. SQL is probably the most widely-used logic programming language.
  - typon 8y ago
    SQL does way less things than a full-blown logic programming system
    - Blackthorn 8y ago
      With common table expressions and windowing, SQL is Turing complete.
      - typon 8y ago
        So is LaTeX...but people aren't implementing logic programs in it.
        Blackthorn 8y ago
        The argument is that minikanren does more than SQL. I strongly disagree.
        haolez 8y ago
        Care to elaborate? Genuinely curious.
      - yorwba 8y ago
        Languages of all kinds of paradigms are Turing complete. But we still use different languages for different purposes, because some programs are more convenient to write in a certain paradigm that maps well to their problem domain. In Prolog for example, you can easily define concatenation of cons-lists as concatenate(nil, Ys, Ys). concatenate(cons(X, Xs), Ys, cons(X, Zs)) :- concatenate(Xs, Ys, Zs). and then generate all 4 possible solutions for the query concatenate(X, Y, cons(1, cons(2, cons(3, nil)))). Of course Prolog has built-in lists that'd allow simply writing append(X, Y, [1, 2, 3]), but the ease of defining certain simple algorithms and then running them backwards is what makes logic programming so useful in my opinion. If SQL can express an equivalent program equally succinctly, I'd very much like to see how.

kimi 8y ago

Solving Sudoku :-)

agumonkey 8y ago

IMO it sits at quite a higher level of programming. You use logic programming to explore ~infinite program states; all that in extremely concise (near fully declarative of course) ways. In Bratko's prolog book you quickly get to do graph processing, some algorithms are 4 clauses and almost word for word what you have in mind. It's mind boggling to me. You also have bidirectional reasoning, you don't have to write a function A => B and then another one for B => A. It's even more telling with multivariate functions. I knew a guy who needed something similar for a large application. He needed a way to reason backward with incomplete parameters.

otabdeveloper1 8y ago

"Logic programming" is a misnomer. It's really a kind of parallel reality database query language. It's not used much because relational databases and SQL won in the end. (I guess back in the day people imagined computers as knowledge graphs and logical predicates on them, not tabular data and joins.)

convolvatron 8y ago
why a misnomer? its exactly what programming would look like if you wanted to try to implement computing as predicate calculus.

a-saleh 8y ago

I would look at uKanren, the smallest mini-kanren cousin. I like Bodil Stokke's [1] introduction, but if you are not afraid of lisp, you can read/re-implement the original(?) [2] paper :) It is basically bunch of combinators for depth-first search? So if you think "I kinda want to brute-force solution for these hard-coded constraints", you might instead want to create a simple logic-programming environment first :-) Last time I played with these, I used it for implementing a toy cryptograhic protocol verification system for a term project. It have barely worked :D A.f.a.i.k. type-checkers often use some sort of logic programming at their core. [1] https://paperswelove.org/2015/video/bodil-stokke-%CE%BCkanren/ https://paperswelove.org/2015/video/bodil-stokke-%CE%BCkanre... [2] http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

KirinDave 8y ago

Sure, I can name one I've prototyped (but never gotten to deploy in prod) in industry. I proposed an embedded μKanren in an Authorization framework for API endpoints. It relied on a system like JWT (or, preferably something less broken like Macaroons) to provide a series of "auth grants" on the request, auth grants being parameterized lines like: (= :user-id 16) (bu.admin-grant (group 10)) (is-super-admin) A few more like this. Then, you could use Python annotations on API methods to specify this kind of setup on API endpoints: (= :group_id request.group-id) (bu.admin_grant (group :group-id)) The system would then perform a kind of logical unification with the request, the cryptographically validated request token, and the API policy. When a request comes in, the request token is merged a "all is forbidden" default set (which is not a literal hash table, it's a policy annotation for the map that contains them). Thus, it's very easy to create arbitrarily complex security policies and so long as they're logically consistent, the interpreter can tell you so (and if it fails, it can tell you why the request doesn't have access). What's also interesting was that you could unify the API endpoint annotations with an empty set of grants, and then it'd produce a series of example permissions that would be valid (or you could merge it with a user's invalid grants, and it could tell you what access they need to go through). This worked well for internal documentation and I had hoped that it'd be applicable to internal tooling to explain to an operator of a tool what access they needed to go request to use the tool (and even where to do it). If you're curious, for most requests the time complexity and memory costs were very modest (approaching but not passing 1ms in the worst case I saw, which for API endpoints written in Python is usually dwarfed by garbage like JSON serialization).

tom_mellior 8y ago

Here is mediKanren (from the same authors): https://github.com/webyrd/mediKanren https://github.com/webyrd/mediKanren It's used for automated search through medical databases for drug discovery: https://www.uab.edu/mix/stories/a-high-speed-dr-house-for-medical-breakthroughs https://www.uab.edu/mix/stories/a-high-speed-dr-house-for-me... Here is the Gerrit code review system: https://www.gerritcodereview.com/ https://www.gerritcodereview.com/ It allows you to specify complex rules for workflows, who may sign off on what patches etc. Those rules are written in Prolog, but I guess they might as well be written in some other logic language. Here is (or rather, will be) Gigahorse, an Ethereum smart contract decompiler: https://2019.icse-conferences.org/event/icse-2019-technical-papers-gigahorse-thorough-declarative-decompilation-of-smart-contracts https://2019.icse-conferences.org/event/icse-2019-technical-... The abstract doesn't say what "declarative, logic-based specification" is used in the implementation, but I know that two of the authors do a lot of work in Datalog, so it's Datalog.

avhon1 8y ago

I took a class with Daniel Friedman, the creator of Minikanren and author of The [Little|Seasoned|Reasoned] Schemer. One of the homework assignments was to write a typechecker for the simply-typed lambda calculus in minikanren. (Most of the semester, we were writing interpreters for the lambda calculus, and doing things like rewriting the interpreter in continuation-passing-style (so that every recursive call was a tail call).)