Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.prolog > #14121 > unrolled thread
| Started by | Mild Shock <janburse@fastmail.fm> |
|---|---|
| First post | 2024-08-01 18:13 +0200 |
| Last post | 2024-08-13 09:08 +0200 |
| Articles | 20 on this page of 22 — 1 participant |
Back to article view | Back to comp.lang.prolog
Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:13 +0200
Alan Kay's Dynabook fueled by Prolog? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:20 +0200
ZebralLogic for evaluating LLMs (Was: Alan Kay's Dynabook fueled by Prolog?) Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:24 +0200
Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-01 19:21 +0200
Biene Maya (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-01 22:26 +0200
A Challenge for Fixpoint Lovers (Was: Biene Maya) Mild Shock <janburse@fastmail.fm> - 2024-08-02 08:03 +0200
Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-09 14:42 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 12:25 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 12:59 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:03 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:14 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:19 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:32 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:41 +0200
Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:46 +0200
The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:03 +0200
Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:05 +0200
Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:19 +0200
Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 14:03 +0200
How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-13 15:48 +0200
Re: How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-13 15:49 +0200
Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-13 09:08 +0200
Page 1 of 2 [1] 2 Next page →
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-01 18:13 +0200 |
| Subject | Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] |
| Message-ID | <v8gc6e$l44p$1@solani.org> |
Hi, I remember Robert Stärk's disappearing from academic life at ETH Zurich all of a sudden. Did Ulrich Neumerkel now also disappeared not because the Scryer Prolog disaster, but after he figured out that failure slices are not hip enought? What could be more hip, are the modalities of Robert Stärk's logic more hip now and even useful? Automated Theorem Proving for Prolog Verification Fred Mesnard etc.. May 2024 https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf Disclaimer: I am not deep into this theory, it has some ingredients that were floating around the 80's / 80's, not only in the millieau of ETH Zurich, but also in the vincinity of Gehard Jaeger, Bern. There are many alternative formalizations that can express termination etc.. But maybe LPTP is especially suited for Prolog?
[toc] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-01 18:20 +0200 |
| Subject | Alan Kay's Dynabook fueled by Prolog? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v8gck9$l4e2$1@solani.org> |
| In reply to | #14121 |
Hi, The paper mentions: "Huge computing power of our modern laptops". If I look at my new iPad Pro M4 2024, I would say "Huge computing power of tablets", measurement have shown it is almost twice as fast as my laptops form ca. 2020. So lets do the following: Bring LPTP to Dogelog Player? Bye P.S.: This would give a new spin of Alan Key's vision of Dynabook. Can we run the Dynabook idea on Prolog? Joe Armstrong interviews Alan Kay https://www.youtube.com/watch?v=fhOHn9TClXY Mild Shock schrieb: > Hi, > > I remember Robert Stärk's disappearing from > academic life at ETH Zurich all of a sudden. > Did Ulrich Neumerkel now also disappeared not > > because the Scryer Prolog disaster, but after > he figured out that failure slices are not hip > enought? What could be more hip, are the modalities > > of Robert Stärk's logic more hip now and even useful? > > Automated Theorem Proving for Prolog Verification > Fred Mesnard etc.. May 2024 > https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf > > Disclaimer: I am not deep into this theory, > it has some ingredients that were floating around > the 80's / 80's, not only in the millieau of ETH Zurich, > > but also in the vincinity of Gehard Jaeger, Bern. > There are many alternative formalizations that > can express termination etc.. But maybe LPTP is > > especially suited for Prolog?
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-01 18:24 +0200 |
| Subject | ZebralLogic for evaluating LLMs (Was: Alan Kay's Dynabook fueled by Prolog?) |
| Message-ID | <v8gcro$l4g0$1@solani.org> |
| In reply to | #14122 |
Hi, A Prolog appendix could give a nice boost to your Edge Device Artificial Intelligence, possibly not having much problems with Zebra puzzles: A week ago, I posted that I was cooking a logical reasoning benchmark as a side project. Now it's finally ready! Introducing 🦓 𝙕𝙚𝙗𝙧𝙖𝙇𝙤𝙜𝙞𝙘, designed for evaluating LLMs with Logic Puzzles. https://x.com/billyuchenlin/status/1814254565128335705 LoL Bye Mild Shock schrieb: > Hi, > > The paper mentions: "Huge computing power > of our modern laptops". If I look at my > new iPad Pro M4 2024, I would say > > "Huge computing power of tablets", measurement > have shown it is almost twice as fast as my > laptops form ca. 2020. So lets do the following: > > Bring LPTP to Dogelog Player? > > Bye > > P.S.: This would give a new spin of Alan > Key's vision of Dynabook. Can we run the > Dynabook idea on Prolog? > > Joe Armstrong interviews Alan Kay > https://www.youtube.com/watch?v=fhOHn9TClXY > > Mild Shock schrieb: >> Hi, >> >> I remember Robert Stärk's disappearing from >> academic life at ETH Zurich all of a sudden. >> Did Ulrich Neumerkel now also disappeared not >> >> because the Scryer Prolog disaster, but after >> he figured out that failure slices are not hip >> enought? What could be more hip, are the modalities >> >> of Robert Stärk's logic more hip now and even useful? >> >> Automated Theorem Proving for Prolog Verification >> Fred Mesnard etc.. May 2024 >> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf >> >> >> Disclaimer: I am not deep into this theory, >> it has some ingredients that were floating around >> the 80's / 80's, not only in the millieau of ETH Zurich, >> >> but also in the vincinity of Gehard Jaeger, Bern. >> There are many alternative formalizations that >> can express termination etc.. But maybe LPTP is >> >> especially suited for Prolog? >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-01 19:21 +0200 |
| Message-ID | <v8gg7a$liqo$1@solani.org> |
| In reply to | #14121 |
Hi, Although the work itself might be solid work. the appeal to fixpoints should already ring a bell. What I wish from a logic framework and what would attract me is: - includes the concept of a model finder, to show things unprovable. - indeally a model finder, that can also find functions as counter models. - allows to express things in non-classical logic and can make good use of non-classical logic. - allows to express things in constructive function spaces and can make good use of constructive function spaces. Currently with fixpoints and classical logic, the approach is not enough advanced, doesn't utilize what type theory could offer. Bye Mild Shock schrieb: > Hi, > > I remember Robert Stärk's disappearing from > academic life at ETH Zurich all of a sudden. > Did Ulrich Neumerkel now also disappeared not > > because the Scryer Prolog disaster, but after > he figured out that failure slices are not hip > enought? What could be more hip, are the modalities > > of Robert Stärk's logic more hip now and even useful? > > Automated Theorem Proving for Prolog Verification > Fred Mesnard etc.. May 2024 > https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf > > Disclaimer: I am not deep into this theory, > it has some ingredients that were floating around > the 80's / 80's, not only in the millieau of ETH Zurich, > > but also in the vincinity of Gehard Jaeger, Bern. > There are many alternative formalizations that > can express termination etc.. But maybe LPTP is > > especially suited for Prolog?
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-01 22:26 +0200 |
| Subject | Biene Maya (Was: Holy Grail makes People Disappear) |
| Message-ID | <v8gr23$lcke$1@solani.org> |
| In reply to | #14124 |
Karel Gott - Rot und schwarz https://www.youtube.com/watch?v=R3qAGDchWWM So whats the fallacy in Robert Staerks modality? It has to do with the difference between computation and derivation, don't confuse the two! What also helps nowadays, don't take a philosopher on board who is totally clueless about non-classical logics. I don't want to say names, but being that ignorant is quite a feat. So how did Robert Staerk start? Well he possibly had first the problem that this here simple logic program: p :- \+ p. when classically translated is unsatisfiable, and therefore in classical logic, leads to Ex Falso Quodlibet. So they went with non-classical logic, but a cheap one, i.e. 3-valued logic, so that we have these two modalities: p_s : p succeeds p_f : p fails The fallacy is now to think a total computable function is the same as BIVALENCE, expressed here, using the further modality in the game: p_t -> p_s v p_f non-constructive logics would immediately see that p_s v p_f is problematic, since the above intoduces a disjunction, without a disjunction property. Now there is possibly the surprise with this overall fixpoint juggling we might have derivations that say p_t, but not in this sense: p_t : p terminates Just try an example with a non-continous fixpoint operator, derived from a Clark completion. I don't see in the slides that it is excluded? Might even try to provide a concrete example myself... Mild Shock schrieb: > Hi, > > Although the work itself might be solid work. > the appeal to fixpoints should already ring a > bell. What I wish from a logic framework and > > what would attract me is: > - includes the concept of a model finder, > to show things unprovable. > - indeally a model finder, that can also > find functions as counter models. > - allows to express things in non-classical > logic and can make good use of non-classical logic. > - allows to express things in constructive > function spaces and can make good use of constructive function spaces. > > Currently with fixpoints and classical logic, > the approach is not enough advanced, doesn't > utilize what type theory could offer. > > Bye > > Mild Shock schrieb: >> Hi, >> >> I remember Robert Stärk's disappearing from >> academic life at ETH Zurich all of a sudden. >> Did Ulrich Neumerkel now also disappeared not >> >> because the Scryer Prolog disaster, but after >> he figured out that failure slices are not hip >> enought? What could be more hip, are the modalities >> >> of Robert Stärk's logic more hip now and even useful? >> >> Automated Theorem Proving for Prolog Verification >> Fred Mesnard etc.. May 2024 >> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf >> >> >> Disclaimer: I am not deep into this theory, >> it has some ingredients that were floating around >> the 80's / 80's, not only in the millieau of ETH Zurich, >> >> but also in the vincinity of Gehard Jaeger, Bern. >> There are many alternative formalizations that >> can express termination etc.. But maybe LPTP is >> >> especially suited for Prolog? >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-02 08:03 +0200 |
| Subject | A Challenge for Fixpoint Lovers (Was: Biene Maya) |
| Message-ID | <v8hsr2$m6t2$1@solani.org> |
| In reply to | #14125 |
Here is a challenge that might appeal to all fixpoint lovers and non-classical logic lovers. Althought I expect them to be a rather rare species. Take the Clark completion and the 3-valued semantics. Then this logic program: foo(n) foo(s(X)) :- foo(X). bar(n). bar(s(X)) :- bar(X). bar(w) :- \+ (foo(X), \+ bar(X)). Here the quizz that makes up the challenge: - Whats the least fixpoint of bar/1, giving bar a domain that makes bar bivalent? - Does bar/1 have finite derivations, i.e. terminates, for each element taken from that domain? Have Fun! The exercise is inspired by this quote and paper: "The finite stages (JnP)n<w have a computational meaning." The theoretical foundations of LPTP Robert F. Stärk - 1998 https://www.sciencedirect.com/science/article/pii/S0743106697100139 Mild Shock schrieb: > > Karel Gott - Rot und schwarz > https://www.youtube.com/watch?v=R3qAGDchWWM > > So whats the fallacy in Robert Staerks modality? > It has to do with the difference between computation > and derivation, don't confuse the two! > > What also helps nowadays, don't take a philosopher > on board who is totally clueless about non-classical > logics. I don't want to say names, but being that > > ignorant is quite a feat. So how did Robert Staerk > start? Well he possibly had first the problem > that this here simple logic program: > > p :- \+ p. > > when classically translated is unsatisfiable, and > therefore in classical logic, leads to Ex Falso > Quodlibet. So they went with non-classical logic, > > but a cheap one, i.e. 3-valued logic, so that > we have these two modalities: > > p_s : p succeeds > p_f : p fails > > The fallacy is now to think a total computable > function is the same as BIVALENCE, expressed here, > using the further modality in the game: > > p_t -> p_s v p_f > > non-constructive logics would immediately see > that p_s v p_f is problematic, since the above > intoduces a disjunction, without a disjunction > > property. Now there is possibly the surprise > with this overall fixpoint juggling we might > have derivations that say p_t, but not in this sense: > > p_t : p terminates > > Just try an example with a non-continous fixpoint > operator, derived from a Clark completion. I don't > see in the slides that it is excluded? > > Might even try to provide a concrete example myself... > > Mild Shock schrieb: >> Hi, >> >> Although the work itself might be solid work. >> the appeal to fixpoints should already ring a >> bell. What I wish from a logic framework and >> >> what would attract me is: >> - includes the concept of a model finder, >> to show things unprovable. >> - indeally a model finder, that can also >> find functions as counter models. >> - allows to express things in non-classical >> logic and can make good use of non-classical logic. >> - allows to express things in constructive >> function spaces and can make good use of constructive function spaces. >> >> Currently with fixpoints and classical logic, >> the approach is not enough advanced, doesn't >> utilize what type theory could offer. >> >> Bye >> >> Mild Shock schrieb: >>> Hi, >>> >>> I remember Robert Stärk's disappearing from >>> academic life at ETH Zurich all of a sudden. >>> Did Ulrich Neumerkel now also disappeared not >>> >>> because the Scryer Prolog disaster, but after >>> he figured out that failure slices are not hip >>> enought? What could be more hip, are the modalities >>> >>> of Robert Stärk's logic more hip now and even useful? >>> >>> Automated Theorem Proving for Prolog Verification >>> Fred Mesnard etc.. May 2024 >>> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf >>> >>> >>> Disclaimer: I am not deep into this theory, >>> it has some ingredients that were floating around >>> the 80's / 80's, not only in the millieau of ETH Zurich, >>> >>> but also in the vincinity of Gehard Jaeger, Bern. >>> There are many alternative formalizations that >>> can express termination etc.. But maybe LPTP is >>> >>> especially suited for Prolog? >> >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-09 14:42 +0200 |
| Subject | Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v952rb$10h3e$1@solani.org> |
| In reply to | #14121 |
Just look at GitHub issues and sort by "recent update". I get for the last week the following figures: - New tickets: 7 new tickets - Closed tickets: 2 closed tickets To get a turn around you the the 2nd number bigger that the 1st number, and not the other way around. Mild Shock schrieb: > Hi, > > I remember Robert Stärk's disappearing from > academic life at ETH Zurich all of a sudden. > Did Ulrich Neumerkel now also disappeared not > > because the Scryer Prolog disaster, but after > he figured out that failure slices are not hip > enought? What could be more hip, are the modalities > > of Robert Stärk's logic more hip now and even useful? > > Automated Theorem Proving for Prolog Verification > Fred Mesnard etc.. May 2024 > https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf > > Disclaimer: I am not deep into this theory, > it has some ingredients that were floating around > the 80's / 80's, not only in the millieau of ETH Zurich, > > but also in the vincinity of Gehard Jaeger, Bern. > There are many alternative formalizations that > can express termination etc.. But maybe LPTP is > > especially suited for Prolog?
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 12:25 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97f6r$11l7k$1@solani.org> |
| In reply to | #14138 |
Hi, How many years does Scryer Prolog allocate to make a turn around? Lets say we have an explosion of new tickets at the beginning, so the new tickets history might have this time functions, plus some parameters that scale it: n(t) = 1 - exp(-t) And lets say tickets are closed at a constant speed, like in this fuction: c(t) = t Again c(t) has some parameters not shown, to scale it. But essently the project is completed when this one reaches zero: f(t) = n(t) - c(t) What can go wrong? Basically onec critical thing is c(t). If you don't have solutions or resources, c(t) might look very different, and a zero might never be reached. Bye Mild Shock schrieb: > > Just look at GitHub issues and sort by "recent update". > I get for the last week the following figures: > > - New tickets: 7 new tickets > - Closed tickets: 2 closed tickets > > To get a turn around you the the 2nd number bigger > that the 1st number, and not the other way around. > > Mild Shock schrieb: >> Hi, >> >> I remember Robert Stärk's disappearing from >> academic life at ETH Zurich all of a sudden. >> Did Ulrich Neumerkel now also disappeared not >> >> because the Scryer Prolog disaster, but after >> he figured out that failure slices are not hip >> enought? What could be more hip, are the modalities >> >> of Robert Stärk's logic more hip now and even useful? >> >> Automated Theorem Proving for Prolog Verification >> Fred Mesnard etc.. May 2024 >> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf >> >> >> Disclaimer: I am not deep into this theory, >> it has some ingredients that were floating around >> the 80's / 80's, not only in the millieau of ETH Zurich, >> >> but also in the vincinity of Gehard Jaeger, Bern. >> There are many alternative formalizations that >> can express termination etc.. But maybe LPTP is >> >> especially suited for Prolog? >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 12:59 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97h77$11m5e$1@solani.org> |
| In reply to | #14139 |
Hi, Some folks from Scryer Prolog asked the following question: > Current plan is to compile WAM using Cranelift. > However, GC must be done first. Maybe Prolog in > the future could be used to analyze Prolog programs > and produce optimizations (Prolog compiler in Prolog?) https://blog.adrianistan.eu/scryer-prolog-meetup-2023-notes/ There is no maybe, there is already a be, for both GC and Prolog compiler in Prolog. But you have to start with the idea, otherwise you probably cant make it. Just take Dogelog Player, it has the following: - Full Sweep Garbage Collector: In the major metronome tick. - Incremental Garbage Collector: In the minor metronome tick. - Read/Write 100% written in Prolog: From scanner to parser and unparse its all Prolog. - Compiler Front End 100% written in Prolog: This is in albufeira.p, this is a little higher level code generator that compiles Prolog clauses, including the cut and if-then-else inlining, some constant term optimizations and body indexing optimizations. - Compiler Back Ends 100% written in Prolog There are cross compiler back ends for JavaScript, Python and Java. And there is runtime back end, for the dynamic database and consult at runtime. The corresponding runtimes have cute neck optimization and last call optimization. Bye Mild Shock schrieb: > Hi, > > How many years does Scryer Prolog allocate to > make a turn around? Lets say we have an explosion > of new tickets at the beginning, so the new tickets > > history might have this time functions, plus > some parameters that scale it: > > n(t) = 1 - exp(-t) > > And lets say tickets are closed at a constant > speed, like in this fuction: > > c(t) = t > > Again c(t) has some parameters not shown, to > scale it. But essently the project is > > completed when this one reaches zero: > > f(t) = n(t) - c(t) > > What can go wrong? Basically onec critical thing > is c(t). If you don't have solutions or resources, > c(t) might look very different, and a zero > > might never be reached. > > Bye > > Mild Shock schrieb: >> >> Just look at GitHub issues and sort by "recent update". >> I get for the last week the following figures: >> >> - New tickets: 7 new tickets >> - Closed tickets: 2 closed tickets >> >> To get a turn around you the the 2nd number bigger >> that the 1st number, and not the other way around. >> >> Mild Shock schrieb: >>> Hi, >>> >>> I remember Robert Stärk's disappearing from >>> academic life at ETH Zurich all of a sudden. >>> Did Ulrich Neumerkel now also disappeared not >>> >>> because the Scryer Prolog disaster, but after >>> he figured out that failure slices are not hip >>> enought? What could be more hip, are the modalities >>> >>> of Robert Stärk's logic more hip now and even useful? >>> >>> Automated Theorem Proving for Prolog Verification >>> Fred Mesnard etc.. May 2024 >>> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf >>> >>> >>> Disclaimer: I am not deep into this theory, >>> it has some ingredients that were floating around >>> the 80's / 80's, not only in the millieau of ETH Zurich, >>> >>> but also in the vincinity of Gehard Jaeger, Bern. >>> There are many alternative formalizations that >>> can express termination etc.. But maybe LPTP is >>> >>> especially suited for Prolog? >> >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 13:03 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97het$11mct$1@solani.org> |
| In reply to | #14140 |
Hi, Currently I wish to add a C# sharp backend, and also show some Unity integration. But I am facing some health problems, some nasty virus infection, which still persists a little bit. Either I will be able to do it in 2024, or you wont here anything from me anymore... LoL Bye P.S.: Some enemies might be happy if I bite the dust, so it will be quite funny if I can make it. But who knows? Mild Shock schrieb: > Hi, > > Some folks from Scryer Prolog asked the following question: > > > Current plan is to compile WAM using Cranelift. > > However, GC must be done first. Maybe Prolog in > > the future could be used to analyze Prolog programs > > and produce optimizations (Prolog compiler in Prolog?) > https://blog.adrianistan.eu/scryer-prolog-meetup-2023-notes/ > > There is no maybe, there is already a be, for both > GC and Prolog compiler in Prolog. But you have to start > with the idea, otherwise you probably cant make it. > > Just take Dogelog Player, it has the following: > > - Full Sweep Garbage Collector: > In the major metronome tick. > > - Incremental Garbage Collector: > In the minor metronome tick. > > - Read/Write 100% written in Prolog: > From scanner to parser and unparse its all Prolog. > > - Compiler Front End 100% written in Prolog: > This is in albufeira.p, this is a little higher level > code generator that compiles Prolog clauses, including > the cut and if-then-else inlining, some constant term > optimizations and body indexing optimizations. > > - Compiler Back Ends 100% written in Prolog > There are cross compiler back ends for JavaScript, > Python and Java. And there is runtime back end, > for the dynamic database and consult at runtime. > The corresponding runtimes have cute neck optimization > and last call optimization. > > Bye > > Mild Shock schrieb: >> Hi, >> >> How many years does Scryer Prolog allocate to >> make a turn around? Lets say we have an explosion >> of new tickets at the beginning, so the new tickets >> >> history might have this time functions, plus >> some parameters that scale it: >> >> n(t) = 1 - exp(-t) >> >> And lets say tickets are closed at a constant >> speed, like in this fuction: >> >> c(t) = t >> >> Again c(t) has some parameters not shown, to >> scale it. But essently the project is >> >> completed when this one reaches zero: >> >> f(t) = n(t) - c(t) >> >> What can go wrong? Basically onec critical thing >> is c(t). If you don't have solutions or resources, >> c(t) might look very different, and a zero >> >> might never be reached. >> >> Bye >> >> Mild Shock schrieb: >>> >>> Just look at GitHub issues and sort by "recent update". >>> I get for the last week the following figures: >>> >>> - New tickets: 7 new tickets >>> - Closed tickets: 2 closed tickets >>> >>> To get a turn around you the the 2nd number bigger >>> that the 1st number, and not the other way around. >>> >>> Mild Shock schrieb: >>>> Hi, >>>> >>>> I remember Robert Stärk's disappearing from >>>> academic life at ETH Zurich all of a sudden. >>>> Did Ulrich Neumerkel now also disappeared not >>>> >>>> because the Scryer Prolog disaster, but after >>>> he figured out that failure slices are not hip >>>> enought? What could be more hip, are the modalities >>>> >>>> of Robert Stärk's logic more hip now and even useful? >>>> >>>> Automated Theorem Proving for Prolog Verification >>>> Fred Mesnard etc.. May 2024 >>>> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf >>>> >>>> >>>> Disclaimer: I am not deep into this theory, >>>> it has some ingredients that were floating around >>>> the 80's / 80's, not only in the millieau of ETH Zurich, >>>> >>>> but also in the vincinity of Gehard Jaeger, Bern. >>>> There are many alternative formalizations that >>>> can express termination etc.. But maybe LPTP is >>>> >>>> especially suited for Prolog? >>> >> >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 13:14 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97i30$11mn6$1@solani.org> |
| In reply to | #14141 |
Hi, The C# backend was already planned 3 years ago. But then we gave priority to a Python backend. But Python is the worst language on this planet. Their module approach doesn't really have export modifiers. Nevertheless they top TIOBE: Highest Position (since 2001): #1 in Aug 2024 https://www.tiobe.com/tiobe-index/python/ Superficially even Prolog has a better module system, although export restrictions are not enforced, you can pretend to do exports, via the module/2 directive. After we completed the Python backend, we recently did the Java backend. But this was not only done for the benefit of Java, but also as an intermediate step for the C# backend. We are pretty close to that everything has stabilized, and it would be a good timing to do the C# backend then. Bye Mild Shock schrieb: > Hi, > > Currently I wish to add a C# sharp backend, > and also show some Unity integration. > > But I am facing some health problems, some > nasty virus infection, which still persists > > a little bit. Either I will be able to do > it in 2024, or you wont here anything > > from me anymore... > > LoL > > Bye
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 13:19 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97icn$11mpq$1@solani.org> |
| In reply to | #14142 |
Hi,
A few days age we improved the cross referencer,
to deal with the many target platforms. The
old cross referencer for example showed:
xor/3 nova/Eval.java
nova/eval.mjs
nova/eval.py
Meaning the evaluable function xor/3 is
available in Java, JavaScript and Python.
What we now do, we simply show:
xor/3 nova/eval.*
Soon the wildcard will mean C# as well,
and not only Java, JavaScript and Python.
Extending the proof of concept for Prolog
compiler 100% written in Prolog itself.
Bye
Mild Shock schrieb:
> Hi,
>
> The C# backend was already planned 3
> years ago. But then we gave priority to
> a Python backend.
>
> But Python is the worst language on this
> planet. Their module approach doesn't
> really have export modifiers.
>
> Nevertheless they top TIOBE:
>
> Highest Position (since 2001): #1 in Aug 2024
> https://www.tiobe.com/tiobe-index/python/
>
> Superficially even Prolog has a better
> module system, although export restrictions
> are not enforced, you can pretend to do exports,
>
> via the module/2 directive. After we
> completed the Python backend, we recently
> did the Java backend. But this was not
>
> only done for the benefit of Java, but
> also as an intermediate step for the C#
> backend. We are pretty close to that
>
> everything has stabilized, and it would
> be a good timing to do the C# backend then.
>
> Bye
>
> Mild Shock schrieb:
>> Hi,
>>
>> Currently I wish to add a C# sharp backend,
>> and also show some Unity integration.
>>
>> But I am facing some health problems, some
>> nasty virus infection, which still persists
>>
>> a little bit. Either I will be able to do
>> it in 2024, or you wont here anything
>>
>> from me anymore...
>>
>> LoL
>>
>> Bye
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 13:32 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97j54$11n9o$1@solani.org> |
| In reply to | #14143 |
Hi, Generally I don't believe in things like SWI-Prolog Janus Python integration. This type of integration has the advantage that SWI-Prolog can run in full speed, on the other hand it has the disadvantage that one cannot take advantage of Python async, because SWI-Prolog itself has no async. I am talking about the single threaded async here. My experience single treaded async and multi-threaded Prolog are quite different pairs of shoes. So when doing the C# backend for Dogelog Player, I will be faced again to provide a complete async solution for the async part of Novacore. Woa! Bye Mild Shock schrieb: > Hi, > > A few days age we improved the cross referencer, > to deal with the many target platforms. The > old cross referencer for example showed: > > xor/3 nova/Eval.java > nova/eval.mjs > nova/eval.py > > Meaning the evaluable function xor/3 is > available in Java, JavaScript and Python. > What we now do, we simply show: > > xor/3 nova/eval.* > > Soon the wildcard will mean C# as well, > and not only Java, JavaScript and Python. > Extending the proof of concept for Prolog > > compiler 100% written in Prolog itself. > > Bye
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 13:41 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97jkv$118im$1@solani.org> |
| In reply to | #14144 |
Hi, Currently I have first hand experience how difficult it is to model single treaded async on top of multi-threaded Prolog, since I want to bring Dogelog Player async also to formerly Jekejeke Prolog. It wasn't so much a problem in the Dogelog Player for Java version, since I could replicate the JavaScript design. But it is a little nasty in the formerly Jekejeke Prolog case, since Thread identity from multi-threaded Prolog and Task identity from single treaded async are not the same, you have to dig deeper into stackfull and stackless coroutines, to get the Task identity notion correctly. I wasn't able to do it yet for formerly Jekejeke Prolog, there is still a pending ticket. Bye Mild Shock schrieb: > Hi, > > Generally I don't believe in things like > SWI-Prolog Janus Python integration. This > type of integration has the advantage > > that SWI-Prolog can run in full speed, > on the other hand it has the disadvantage > that one cannot take advantage of Python async, > > because SWI-Prolog itself has no async. I > am talking about the single threaded async here. > My experience single treaded async and multi-threaded > > Prolog are quite different pairs of shoes. So > when doing the C# backend for Dogelog Player, > I will be faced again to provide a complete > > async solution for the async part of Novacore. > > Woa! > > Bye > > Mild Shock schrieb: >> Hi, >> >> A few days age we improved the cross referencer, >> to deal with the many target platforms. The >> old cross referencer for example showed: >> >> xor/3 nova/Eval.java >> nova/eval.mjs >> nova/eval.py >> >> Meaning the evaluable function xor/3 is >> available in Java, JavaScript and Python. >> What we now do, we simply show: >> >> xor/3 nova/eval.* >> >> Soon the wildcard will mean C# as well, >> and not only Java, JavaScript and Python. >> Extending the proof of concept for Prolog >> >> compiler 100% written in Prolog itself. >> >> Bye
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-10 13:46 +0200 |
| Subject | Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) |
| Message-ID | <v97ju2$118im$2@solani.org> |
| In reply to | #14145 |
Hi, To stabilize Dogelog Player now, there are only a few important pending tickets, but the growing pains are basically to identify the low hanging fruits. I do not tend to throw a dice, it might take some time doing nothing, before a next important ticket is selected based on some rationalization of a priorization. Bye Mild Shock schrieb: > Hi, > > Currently I have first hand experience how > difficult it is to model single treaded async > on top of multi-threaded Prolog, > > since I want to bring Dogelog Player async > also to formerly Jekejeke Prolog. It wasn't > so much a problem in the Dogelog Player for > > Java version, since I could replicate the > JavaScript design. But it is a little > nasty in the formerly Jekejeke Prolog case, > > since Thread identity from multi-threaded > Prolog and Task identity from single treaded > async are not the same, you have to dig > > deeper into stackfull and stackless coroutines, > to get the Task identity notion correctly. > I wasn't able to do it yet for formerly > > Jekejeke Prolog, there is still a pending ticket. > > Bye
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-11 11:03 +0200 |
| Subject | The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) |
| Message-ID | <v99uo8$12eip$1@solani.org> |
| In reply to | #14138 |
But Scryer Prolog must nevertheless have somewhere
some good genes. Even it posted about a Prolog compiler
written in Prolog itself. Lets make some reality check:
/* Ichiban Prolog */
real 0m39.635s
user 0m59.684s
sys 0m7.891s
/* Dogelog Player for Java */
?- time((between(1,6001,_), nrev, fail; true)).
% Zeit 588 ms, GC 0 ms, Lips 5113263, Uhr 11.08.2024 10:47
true.
/* Trealla Prolog */
?- time((between(1,6001,_), nrev, fail; true)).
% Time elapsed 0.549s, 3000503 Inferences, 5.468 MLips
true.
/* Scryer Prolog */
?- time((between(1,6001,_), nrev, fail; true)).
% CPU time: 0.302s, 3_024_526 inferences
true.
/* SWI-Prolog */
?- time((between(1,6001,_), nrev, fail; true)).
% 2,994,499 inferences, 0.078 CPU in 0.089 seconds (88% CPU, 38329587 Lips)
true.
Dogelog Player has a Prolog compiler written in
Prolog itself. But the limiting factor is of course
always the runtime engine itself, that executes the
compiled code. You can inline and optimize whatever
you want, if the runtime engine, its architecture,
has some limitations performance wise, you won't
see aby speed. I don't know yet whether I will beat
SWI-Prolog in this test case ever in the near future?
Especially with some cheap effort?
Mild Shock schrieb:
>
> Just look at GitHub issues and sort by "recent update".
> I get for the last week the following figures:
>
> - New tickets: 7 new tickets
> - Closed tickets: 2 closed tickets
>
> To get a turn around you the the 2nd number bigger
> that the 1st number, and not the other way around.
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-11 11:05 +0200 |
| Subject | Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) |
| Message-ID | <v99utc$12eip$2@solani.org> |
| In reply to | #14153 |
But I am nevertheless convinced Scryer Prolog is dead. These good genes only appeared recently. But I was comparing oranges and apples. I compared Dogelog Player which has garbage collection to a Prolog system like Scryer Prolog which doesn't have garbage collection. A Prolog system that doesn't have garbage collection can run faster. The challenge is a runtime engine that is fast AND has garbage collection. Mild Shock schrieb: > > But Scryer Prolog must nevertheless have somewhere > some good genes. Even it posted about a Prolog compiler > written in Prolog itself. Lets make some reality check: > > /* Ichiban Prolog */ > real 0m39.635s > user 0m59.684s > sys 0m7.891s > > /* Dogelog Player for Java */ > ?- time((between(1,6001,_), nrev, fail; true)). > % Zeit 588 ms, GC 0 ms, Lips 5113263, Uhr 11.08.2024 10:47 > true. > > /* Trealla Prolog */ > ?- time((between(1,6001,_), nrev, fail; true)). > % Time elapsed 0.549s, 3000503 Inferences, 5.468 MLips > true. > > /* Scryer Prolog */ > ?- time((between(1,6001,_), nrev, fail; true)). > % CPU time: 0.302s, 3_024_526 inferences > true. > > /* SWI-Prolog */ > ?- time((between(1,6001,_), nrev, fail; true)). > % 2,994,499 inferences, 0.078 CPU in 0.089 seconds (88% CPU, 38329587 Lips) > true. > > Dogelog Player has a Prolog compiler written in > Prolog itself. But the limiting factor is of course > always the runtime engine itself, that executes the > > compiled code. You can inline and optimize whatever > you want, if the runtime engine, its architecture, > has some limitations performance wise, you won't > > see aby speed. I don't know yet whether I will beat > SWI-Prolog in this test case ever in the near future? > Especially with some cheap effort? > > Mild Shock schrieb: >> >> Just look at GitHub issues and sort by "recent update". >> I get for the last week the following figures: >> >> - New tickets: 7 new tickets >> - Closed tickets: 2 closed tickets >> >> To get a turn around you the the 2nd number bigger >> that the 1st number, and not the other way around.
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-11 11:19 +0200 |
| Subject | Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) |
| Message-ID | <v99vmr$12f56$1@solani.org> |
| In reply to | #14154 |
The test case that crashes all these new Prolog systems, is for example this one. It still crashes Scryer Prolog: $ ulimit -m 2000000 $ ulimit -v 2000000 $ target/release/scryer-prolog -v v0.9.4-135-g7cfe8ee5 $ target/release/scryer-prolog ?- [user]. app([], X, X). app([X|Y], Z, [X|T]) :- app(Y, Z, T). garbage(0, [0]) :- !. garbage(N, L) :- M is N-1, garbage(M, R), app(R, R, L). foo :- garbage(12,_), foo. ?- foo. memory allocation of 2147483648 bytes failed Aborted The above preferably runs indefinitely. For example SWI-Prolog can run it indefinitely. It also crashes other Prolog systems: $ ~/go/bin/1pl Top level for ichiban/prolog v1.2.1 This is for testing purposes only! See https://github.com/ichiban/prolog for more details. Type Ctrl-C or 'halt.' to exit. ?- ['bomb.p']. true. ?- foo. runtime: out of memory: cannot allocate 4194304-byte block (802816000 in use) Mild Shock schrieb: > > But I am nevertheless convinced Scryer Prolog > is dead. These good genes only appeared recently. > But I was comparing oranges and apples. > > I compared Dogelog Player which has garbage > collection to a Prolog system like Scryer Prolog > which doesn't have garbage collection. > > A Prolog system that doesn't have garbage collection > can run faster. The challenge is a runtime engine > that is fast AND has garbage collection. > > Mild Shock schrieb: >> >> But Scryer Prolog must nevertheless have somewhere >> some good genes. Even it posted about a Prolog compiler >> written in Prolog itself. Lets make some reality check: >> >> /* Ichiban Prolog */ >> real 0m39.635s >> user 0m59.684s >> sys 0m7.891s >> >> /* Dogelog Player for Java */ >> ?- time((between(1,6001,_), nrev, fail; true)). >> % Zeit 588 ms, GC 0 ms, Lips 5113263, Uhr 11.08.2024 10:47 >> true. >> >> /* Trealla Prolog */ >> ?- time((between(1,6001,_), nrev, fail; true)). >> % Time elapsed 0.549s, 3000503 Inferences, 5.468 MLips >> true. >> >> /* Scryer Prolog */ >> ?- time((between(1,6001,_), nrev, fail; true)). >> % CPU time: 0.302s, 3_024_526 inferences >> true. >> >> /* SWI-Prolog */ >> ?- time((between(1,6001,_), nrev, fail; true)). >> % 2,994,499 inferences, 0.078 CPU in 0.089 seconds (88% CPU, 38329587 >> Lips) >> true. >> >> Dogelog Player has a Prolog compiler written in >> Prolog itself. But the limiting factor is of course >> always the runtime engine itself, that executes the >> >> compiled code. You can inline and optimize whatever >> you want, if the runtime engine, its architecture, >> has some limitations performance wise, you won't >> >> see aby speed. I don't know yet whether I will beat >> SWI-Prolog in this test case ever in the near future? >> Especially with some cheap effort? >> >> Mild Shock schrieb: >>> >>> Just look at GitHub issues and sort by "recent update". >>> I get for the last week the following figures: >>> >>> - New tickets: 7 new tickets >>> - Closed tickets: 2 closed tickets >>> >>> To get a turn around you the the 2nd number bigger >>> that the 1st number, and not the other way around. >
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-11 14:03 +0200 |
| Subject | Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) |
| Message-ID | <v9a9ar$136g9$1@solani.org> |
| In reply to | #14155 |
Another prolog system which succumbs to
the bomb.p test case:
$ ulimit -m 2000000
$ ulimit -v 2000000
$ ./tpl -v
Trealla Prolog (c) Infradig 2020-2024, v2.55.18
$ ./tpl
?- ['bomb.p'].
?- foo.
throw(error(resource_error(memory),app/3)).
But on my side not everything is joy
that makes us unique. The matter is
difficult to adjust:
with Machine.GC_MAX_INFERS = 200000 it crashes:
/* Dogelog Player for Java */
?- foo.
Error: Execution aborted because out of memory.
with Machine.GC_MAX_INFERS = 100000 it does not crash:
/* Dogelog Player for Java */
?- foo.
%%% I can go for lunch and come back, it still runs.
How can I find the right value for GC_MAX_INFERS ?
Call a witch doctor and ask his oracle bones?
Mild Shock schrieb:
> The test case that crashes all these new
> Prolog systems, is for example this one.
> It still crashes Scryer Prolog:
>
> $ ulimit -m 2000000
> $ ulimit -v 2000000
> $ target/release/scryer-prolog -v
> v0.9.4-135-g7cfe8ee5
>
> $ target/release/scryer-prolog
> ?- [user].
> app([], X, X).
> app([X|Y], Z, [X|T]) :- app(Y, Z, T).
> garbage(0, [0]) :- !.
> garbage(N, L) :- M is N-1, garbage(M, R), app(R, R, L).
> foo :- garbage(12,_), foo.
>
> ?- foo.
> memory allocation of 2147483648 bytes failed
> Aborted
>
> The above preferably runs indefinitely. For
> example SWI-Prolog can run it indefinitely.
> It also crashes other Prolog systems:
>
> $ ~/go/bin/1pl
> Top level for ichiban/prolog v1.2.1
> This is for testing purposes only!
> See https://github.com/ichiban/prolog for more details.
> Type Ctrl-C or 'halt.' to exit.
>
> ?- ['bomb.p'].
> true.
> ?- foo.
> runtime: out of memory:
> cannot allocate 4194304-byte block (802816000 in use)
[toc] | [prev] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2024-08-13 15:48 +0200 |
| Subject | How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) |
| Message-ID | <v9fo70$166p1$1@solani.org> |
| In reply to | #14138 |
I can make a case of such a comparison,
DCG pipe dream versus proper look-ahead:
/* Scryer Prolog 0.9.4-135 */
?- time((between(1,1000,_), data(X), json_chars(Y,X,[]), fail; true)).
% CPU time: 0.283s, 2_506_022 inferences
true.
/* SWI-Prolog 9.3.8 */
?- time((between(1,1000,_), data(X), atom_json_term(X,Y,[]), fail; true)).
% 44,998 inferences, 0.016 CPU in 0.006 seconds (281% CPU, 2879872 Lips)
true.
I think the speed difference of a factor
20x is not because of native float parsing.
The example doesn’t have much float:
data("{ \"a\":123 }").
So whats the bug in the DCG parser by
Scryer Prolog? Why does the parser written by
Jan W. not have the same defect?
Why does the number of inferences differ so much?
[toc] | [prev] | [next] | [standalone]
Page 1 of 2 [1] 2 Next page →
Back to top | Article view | comp.lang.prolog
csiph-web