5 ms·

λProlog: Logic programming in higher-order logic

167 points by ux266478 8mo ago

TheRoque 8mo ago
I remember learning it in univerisity. It's a really weird language to reason with IMO. But really fun. However I've heard the performances are not that good if you wanna make e.g. game AIs with it.
- pjmlp 8mo ago
  First of all, it helps to actually use a proper compiled Prolog implementation like SWI Prolog. Second you really need to understand and fine tune cuts, and other search optimization primitives. Finally in what concerns Game AIs, it is a mixture of algorithms and heuristics, a single paradigm language (first order logic) like Prolog, can't be a tool for all nails.
- anonzzzies 8mo ago
  λProlog or Prolog? Probably Prolog I guess?
  - wbolt 8mo ago
    No. It is actually λProlog which seems to be an extension of Prolog.
    - anonzzzies 8mo ago
      I was responding to @TheRoque GP; I know λProlog quite well and I would be pleasantly surprised if they saw that in university, but I think they got taught Prolog. If you mean to say that they saw Lambda Prolog and it is therefor a lot more popular than I believed it to be, then excellent and ignore this reply.
    - ux266478 8mo ago
      Not at all, it's a completely different language with a very different computational foundation. It's an SML-Haskell type situation.
  - TheRoque 8mo ago
    My bad. Was regular prolog yeah
- laksjhdlka 8mo ago
  With λProlog in particular I think it probably finds most of its use in specifying and reasoning about systems/languages/logics, e.g. with Abella. I don't think many people are running it in production as an implementation language.
  - OneDeuxTriSeiGo 8mo ago
    Yeah the main use of it is probably in ELPI which is a higher order structural reasoning and AST transform tool for Coq/Rocq.
- ux266478 8mo ago
  > It's a really weird language to reason with IMO I know you likely mean regular Prolog, but that's actually fairly easy and intuitive to reason with (code dependent). Lambda Prolog is much, much harder to reason about IMO and there's a certain intractability to it because of just how complex the language is.
  - cubefox 8mo ago
    What would be some applications it handles better than regular Prolog? Something that naturally requires second or higher order logic rather first order logic?
    - ux266478 8mo ago
      Lambda Prolog isn't a "pure" HOL. It's a very restricted form of HOL using Higher-Order Hereditary Herrop formulas, granting us pretty solid generalized mechanisms of implication and universal quantification, which itself more or less means we get contextual reasoning and scoping rules baked into the grammar for free. Implementing other programming languages and proving theorems are the low-hanging fruits since you get variable binding without name management, but I genuinely think it has profound implications for expert systems since it essentially removes a massive amount of complexity from contextual reasoning. Being able to account for patient history when providing a diagnosis, for example.
- tannhaeuser 8mo ago
  The term "AI" has changed in recent years but if you mean classic game logic such as complex rules and combinatorial opponents then there's plenty of Prolog game code on github eg. for Poker and other card or board games. Prolog is also as natural a choice for adventure puzzles as it gets with repository items and complicated conditions to advance the game. In fact, Amzi! Prolog uses adventure game coding as a topic for its classic (1980s) introductory Prolog learning book Adventure in Prolog ([1]). Based on a cursory look, most code in that book should run just fine on a modern ISO Prolog engine ([2]) in your browser. [1]: https://www.amzi.com/AdventureInProlog/advtop.php https://www.amzi.com/AdventureInProlog/advtop.php [2]: https://quantumprolog.sgml.net https://quantumprolog.sgml.net
- dyingkneepad 8mo ago
  I also learned Prolog in the university. In the Classsic AI course we had to implement gaming AI algorithms (A*, alpha-beta pruning, etc) and in Prolog for one specific assignment. After trying for a while, I got frustrated and asked the teacher if I could do it in Ruby instead. He agreed: he was the kind of person who just couldn't say no, he was too nice for his own good. I still feel bad about it. Rest In Peace, Alexandre.
  - iberator 8mo ago
    How is this fair to others?!
    - dyingkneepad 8mo ago
      University is not a competition, others have nothing to do with this? The unfairness here is between me and myself, as I was supposed force myself into doing it in Prolog.
yodsanklai 8mo ago
I'm curious to see how AI is going to reshape research in programming languages. Statically typed languages with expressive type systems should be even more relevant for instance.
- acjohnson55 8mo ago
  Why do you think that?
  - yodsanklai 8mo ago
    Because the type system gives you correctness properties, and gives fast feedback to the coding agent. Much faster to type check the code than let say write and run unit tests. One possible disadvantage of static types is that it can make the code more verbose, but agents really don't care, quite the opposite.
    - butokai 8mo ago
      Funnily enough, when programming with agents in statically typed languages I always find myself in need of reminding the agent to check for type errors from the LSP. Seems like it's something they're not so fond of.
upghost 8mo ago
I'm surprised how hard I had to dig for an actual example of syntax[1], so here you go. [1]: https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extract.html#htoc51 https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extra...
- Antibabelic 8mo ago
  There is also an implementation of 99 Bottles of Beer on Rosetta Code: https://rosettacode.org/wiki/99_bottles_of_beer#Lambda_Prolog https://rosettacode.org/wiki/99_bottles_of_beer#Lambda_Prolo...
- neuroelectron 8mo ago
  So brainfuck x lisp
- tmaly 8mo ago
  I have written stuff in Prolog, but I find this lambda Prolog syntax very difficult to grok.
- cpill 8mo ago
  Christ... it's incomprehensible... I guess that ones staying in academia :P
- cess11 8mo ago
  There are some examples in this tutorial PDF: https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/felty-tutorial-lprolog97.pdf https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/fe...
- Twey 8mo ago
  Constantly amused by the split in comments of any moderately innovative language post between ‘I don't care about all this explanation, just show me the syntax!’ and ‘I don't understand any of this syntax, what a useless language!’ If the language is ‘JavaScript but with square brackets instead of braces’ maybe the syntax is relevant. But in general concrete syntax is the least interesting (not least important, but easiest to change) thing in a programming language, and its similarity to other languages a particular reader knows less interesting still. JavaScript is not the ultimate in programming language syntax (I hope!) so it's still worth experimenting, even if the results aren't immediately comprehensible without learning.
Antibabelic 8mo ago
There is a great overview of λProlog from 1988: https://repository.upenn.edu/bitstreams/e91f803b-8e75-4f3c-9bf5-10ce15fe8186/download https://repository.upenn.edu/bitstreams/e91f803b-8e75-4f3c-9...
polairscience 8mo ago
I think that might be my favorite department/lab website I've ever come across. Really fun. Doesn't at all align with the contemporary design status quo and it shows just how good a rich website can be on a large screen. Big fan. https://www.lix.polytechnique.fr/ https://www.lix.polytechnique.fr/
boxfire 8mo ago
I am a huge fan of the work towards putting this in kanren as λKanren: https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e86195aba6a/1?pq-origsite=gscholar&cbl=18750&diss=y https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e8619... A few of my own experiments in this time with unification over the binders as variables themselves shows there’s almost always a post HM inference sitting there but likely not one that works in total generality. To me that spot of trying to binding unification in higher order logic constraint equations is the most challenging and interesting problem since it’s almost always decidable or decidably undecidable in specific instances, but provably undecidable in general. So what gives? Where is this boundary and does it give a clue to bigger gains in higher order unification? Is a more topological approach sitting just behind the veil for a much wider class of higher order inference? And what of optimal sharing in the presence of backtracking? Lampings algorithm when the unification variables is in the binder has to have purely binding attached path contexts like closures. How does that get shared? Fun to poke at, maybe just enough modern interest in logic programming to get there too…
big-chungus4 8mo ago
(1987)
big-chungus4 8mo ago
when I downloaded the example programs, they open up in my music player but don't play anything
- dyingkneepad 8mo ago
  As usual, try mplayer. It can play anything.
poppingtonic 8mo ago
Learning how to implement Prolog in pg's On Lisp was a fun way to spend multiple weeks programming. Doing this again this year should be a lot of fun.
abathologist 8mo ago
I did a few days of AoC in 2020 in λProlog (as a non-expert in the language), using the Elpi implementation. It provides a decent source of relatively digestable toy examples: https://github.com/shonfeder/aoc-2020 https://github.com/shonfeder/aoc-2020 (Caveat that I don't claim to be a λProlog or expert.) All examples showcase the typing discipline that is novel relative to Prolog, and towards day 10, use of the lambda binders, hereditary harrop formulas, and higher order niceness shows up.
naillang 8mo ago
[dead]
llsf 8mo ago
Did some modest development on Lambda Prolog back in 1999. I still have a vivid memory of feeling my brain expanding :) like rewiring how I approach programming and opening up new territory in my brain. It might sound weird and crazy, but it quite literally blew my mind at the time !
TZubiri 8mo ago
Anyone know why there seems to be a Prolog renaissance? I personally found it by asking for a specific language recommendation from ChatGPT, and one of the suggestions was Prolog.
011101101 8mo ago
[flagged]

167 points by ux266478 8mo ago

I remember learning it in univerisity. It's a really weird language to reason with IMO. But really fun. However I've heard the performances are not that good if you wanna make e.g. game AIs with it.

pjmlp 8mo ago
First of all, it helps to actually use a proper compiled Prolog implementation like SWI Prolog. Second you really need to understand and fine tune cuts, and other search optimization primitives. Finally in what concerns Game AIs, it is a mixture of algorithms and heuristics, a single paradigm language (first order logic) like Prolog, can't be a tool for all nails.
anonzzzies 8mo ago
λProlog or Prolog? Probably Prolog I guess?
- wbolt 8mo ago
  No. It is actually λProlog which seems to be an extension of Prolog.
  - anonzzzies 8mo ago
    I was responding to @TheRoque GP; I know λProlog quite well and I would be pleasantly surprised if they saw that in university, but I think they got taught Prolog. If you mean to say that they saw Lambda Prolog and it is therefor a lot more popular than I believed it to be, then excellent and ignore this reply.
  - ux266478 8mo ago
    Not at all, it's a completely different language with a very different computational foundation. It's an SML-Haskell type situation.
- TheRoque 8mo ago
  My bad. Was regular prolog yeah
laksjhdlka 8mo ago
With λProlog in particular I think it probably finds most of its use in specifying and reasoning about systems/languages/logics, e.g. with Abella. I don't think many people are running it in production as an implementation language.
- OneDeuxTriSeiGo 8mo ago
  Yeah the main use of it is probably in ELPI which is a higher order structural reasoning and AST transform tool for Coq/Rocq.
ux266478 8mo ago
> It's a really weird language to reason with IMO I know you likely mean regular Prolog, but that's actually fairly easy and intuitive to reason with (code dependent). Lambda Prolog is much, much harder to reason about IMO and there's a certain intractability to it because of just how complex the language is.
- cubefox 8mo ago
  What would be some applications it handles better than regular Prolog? Something that naturally requires second or higher order logic rather first order logic?
  - ux266478 8mo ago
    Lambda Prolog isn't a "pure" HOL. It's a very restricted form of HOL using Higher-Order Hereditary Herrop formulas, granting us pretty solid generalized mechanisms of implication and universal quantification, which itself more or less means we get contextual reasoning and scoping rules baked into the grammar for free. Implementing other programming languages and proving theorems are the low-hanging fruits since you get variable binding without name management, but I genuinely think it has profound implications for expert systems since it essentially removes a massive amount of complexity from contextual reasoning. Being able to account for patient history when providing a diagnosis, for example.
tannhaeuser 8mo ago
The term "AI" has changed in recent years but if you mean classic game logic such as complex rules and combinatorial opponents then there's plenty of Prolog game code on github eg. for Poker and other card or board games. Prolog is also as natural a choice for adventure puzzles as it gets with repository items and complicated conditions to advance the game. In fact, Amzi! Prolog uses adventure game coding as a topic for its classic (1980s) introductory Prolog learning book Adventure in Prolog ([1]). Based on a cursory look, most code in that book should run just fine on a modern ISO Prolog engine ([2]) in your browser. [1]: https://www.amzi.com/AdventureInProlog/advtop.php https://www.amzi.com/AdventureInProlog/advtop.php [2]: https://quantumprolog.sgml.net https://quantumprolog.sgml.net
dyingkneepad 8mo ago
I also learned Prolog in the university. In the Classsic AI course we had to implement gaming AI algorithms (A*, alpha-beta pruning, etc) and in Prolog for one specific assignment. After trying for a while, I got frustrated and asked the teacher if I could do it in Ruby instead. He agreed: he was the kind of person who just couldn't say no, he was too nice for his own good. I still feel bad about it. Rest In Peace, Alexandre.
- iberator 8mo ago
  How is this fair to others?!
  - dyingkneepad 8mo ago
    University is not a competition, others have nothing to do with this? The unfairness here is between me and myself, as I was supposed force myself into doing it in Prolog.

yodsanklai 8mo ago

I'm curious to see how AI is going to reshape research in programming languages. Statically typed languages with expressive type systems should be even more relevant for instance.

acjohnson55 8mo ago
Why do you think that?
- yodsanklai 8mo ago
  Because the type system gives you correctness properties, and gives fast feedback to the coding agent. Much faster to type check the code than let say write and run unit tests. One possible disadvantage of static types is that it can make the code more verbose, but agents really don't care, quite the opposite.
  - butokai 8mo ago
    Funnily enough, when programming with agents in statically typed languages I always find myself in need of reminding the agent to check for type errors from the LSP. Seems like it's something they're not so fond of.

upghost 8mo ago

I'm surprised how hard I had to dig for an actual example of syntax[1], so here you go. [1]: https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extract.html#htoc51 https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extra...

Antibabelic 8mo ago
There is also an implementation of 99 Bottles of Beer on Rosetta Code: https://rosettacode.org/wiki/99_bottles_of_beer#Lambda_Prolog https://rosettacode.org/wiki/99_bottles_of_beer#Lambda_Prolo...
neuroelectron 8mo ago
So brainfuck x lisp
tmaly 8mo ago
I have written stuff in Prolog, but I find this lambda Prolog syntax very difficult to grok.
cpill 8mo ago
Christ... it's incomprehensible... I guess that ones staying in academia :P
cess11 8mo ago
There are some examples in this tutorial PDF: https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/felty-tutorial-lprolog97.pdf https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/fe...
Twey 8mo ago
Constantly amused by the split in comments of any moderately innovative language post between ‘I don't care about all this explanation, just show me the syntax!’ and ‘I don't understand any of this syntax, what a useless language!’ If the language is ‘JavaScript but with square brackets instead of braces’ maybe the syntax is relevant. But in general concrete syntax is the least interesting (not least important, but easiest to change) thing in a programming language, and its similarity to other languages a particular reader knows less interesting still. JavaScript is not the ultimate in programming language syntax (I hope!) so it's still worth experimenting, even if the results aren't immediately comprehensible without learning.

Antibabelic 8mo ago

There is a great overview of λProlog from 1988: https://repository.upenn.edu/bitstreams/e91f803b-8e75-4f3c-9bf5-10ce15fe8186/download https://repository.upenn.edu/bitstreams/e91f803b-8e75-4f3c-9...

polairscience 8mo ago

I think that might be my favorite department/lab website I've ever come across. Really fun. Doesn't at all align with the contemporary design status quo and it shows just how good a rich website can be on a large screen. Big fan. https://www.lix.polytechnique.fr/ https://www.lix.polytechnique.fr/

boxfire 8mo ago

I am a huge fan of the work towards putting this in kanren as λKanren: https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e86195aba6a/1?pq-origsite=gscholar&cbl=18750&diss=y https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e8619... A few of my own experiments in this time with unification over the binders as variables themselves shows there’s almost always a post HM inference sitting there but likely not one that works in total generality. To me that spot of trying to binding unification in higher order logic constraint equations is the most challenging and interesting problem since it’s almost always decidable or decidably undecidable in specific instances, but provably undecidable in general. So what gives? Where is this boundary and does it give a clue to bigger gains in higher order unification? Is a more topological approach sitting just behind the veil for a much wider class of higher order inference? And what of optimal sharing in the presence of backtracking? Lampings algorithm when the unification variables is in the binder has to have purely binding attached path contexts like closures. How does that get shared? Fun to poke at, maybe just enough modern interest in logic programming to get there too…

big-chungus4 8mo ago

(1987)

big-chungus4 8mo ago

when I downloaded the example programs, they open up in my music player but don't play anything

dyingkneepad 8mo ago
As usual, try mplayer. It can play anything.

poppingtonic 8mo ago

Learning how to implement Prolog in pg's On Lisp was a fun way to spend multiple weeks programming. Doing this again this year should be a lot of fun.

abathologist 8mo ago

I did a few days of AoC in 2020 in λProlog (as a non-expert in the language), using the Elpi implementation. It provides a decent source of relatively digestable toy examples: https://github.com/shonfeder/aoc-2020 https://github.com/shonfeder/aoc-2020 (Caveat that I don't claim to be a λProlog or expert.) All examples showcase the typing discipline that is novel relative to Prolog, and towards day 10, use of the lambda binders, hereditary harrop formulas, and higher order niceness shows up.

naillang 8mo ago

[dead]

llsf 8mo ago

Did some modest development on Lambda Prolog back in 1999. I still have a vivid memory of feeling my brain expanding :) like rewiring how I approach programming and opening up new territory in my brain. It might sound weird and crazy, but it quite literally blew my mind at the time !

TZubiri 8mo ago

Anyone know why there seems to be a Prolog renaissance? I personally found it by asking for a specific language recommendation from ChatGPT, and one of the suggestions was Prolog.

011101101 8mo ago

[flagged]