The convinced me again that they hate logic and
logic programming, especially Backtracking. They
write nonsense like this:

"Choice and determinism. Choice is a fundamental feature
of all functional logic languages. In VC, choice is expressed in the
syntax of the term (“laid out in space”) rather than, as is more typical,
handled by non-deterministic rewrites and backtracking

(“laid out in time”). This makes VC completely deterministic,
nlike most functional logic languages which are non-deterministic
by design (Section 6.1). Inspired by their idea, we present a new
rewrite system for functional logic programs that reifies logical

variables and unification into the term itself, and replaces non-
deterministic search with a (deterministic) tree of successful results."
https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf

So they rediscovered OLD resolution? Didn't check the rest of
the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
They don't know the advantage of DPLL algorithms implemented

with Backtracking, concerning time versus space tradeoff?

Anyway, what is OLD resolution?

H. Tamaki and T. Sato. OLD resolution with tabulation.
In Proceedings of the Third International Conference on Logic
Programming, pages 84–98. Springer Verlag, 1986. Lecture
Notes in Computer Science, No. 225.
https://www.researchgate.net/publication/220986525

Here is a paper that mentions both SLD and OLD. Unfortunately
they get SLD wrong. What they show as solve/1 is not SLD?
Its only the Vanilla interpreter. How would SLD look like?

PROLOG Interpreter for First-Order Intuitionistic Logic
(Extended Abstract). January 1994
L. Thorne McCartyLeon A. Shklar
https://www.researchgate.net/publication/221135513

Mostowski Collapse schrieb am Samstag, 17. Dezember 2022 um 03:31:15 UTC+1:
> Now I am convinced, functional programming language
> designers must hate logic and logic programming:
>
> The Verse Calculus: a Core Calculus for Functional Logic Programming
> https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf
>
> LoL
> Mostowski Collapse schrieb am Samstag, 17. Dezember 2022 um 10:20:51 UTC+11:
> > Let's challenge the WAM, like here:
> >
> > A Hitchhiker’s Guide to Reinventing a Prolog Machine
> > Paul Tarau - 2018 (Open Access)
> > https://drops.dagstuhl.de/opus/volltexte/2018/8453/
> >
> > Interestingly Dogelog Player has adopted some of the ideas:
> >
> > Dogelog Player is a Prolog interpreter that is 100% written
> > in Prolog itself. This also extends to the code generator that
> > produces 6 instructions that are responsible for term unification
> > and/or term building. In the upcoming release we will again
> > only generate 5 instructions in a new way.
> >
> > We were able to extended the singleton analysis to a lifetime
> > analysis of each variable. The results for our usual core
> > benchmarks speak a mixed language. Many more change
> > of point of view experiments are needed in the near future.
> >
> > Paul Taraus Reinventing a Prolog Machine Revisited
> > https://twitter.com/dogelogch/status/1602228707623477248
> >
> > Paul Taraus Reinventing a Prolog Machine Revisited
> > https://www.facebook.com/groups/dogelog
> > geoffrey.a...@gmail.com schrieb am Samstag, 17. Dezember 2022 um 09:36:36 UTC+11:
> > > Thank you for the references. Here's an archived version of the wambook: https://web.archive.org/web/20220119110941/http://wambook.sourceforge.net/. It's also currently being hosted at https://github.com/a-yiorgos/wambook.

DPLL is not really a trade-off between time and space.
Its more the insight that if you can lay out in time,
instead lay out in space, you can safe a lot of memory.

https://en.wikipedia.org/wiki/DPLL_algorithm

The backtracking is here:

return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});

The way the "or" can be practically implemented.

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 12:47:50 UTC+2:
> The convinced me again that they hate logic and
> logic programming, especially Backtracking. They
> write nonsense like this:
>
> "Choice and determinism. Choice is a fundamental feature
> of all functional logic languages. In VC, choice is expressed in the
> syntax of the term (“laid out in space”) rather than, as is more typical,
> handled by non-deterministic rewrites and backtracking
>
> (“laid out in time”). This makes VC completely deterministic,
> nlike most functional logic languages which are non-deterministic
> by design (Section 6.1). Inspired by their idea, we present a new
> rewrite system for functional logic programs that reifies logical
>
> variables and unification into the term itself, and replaces non-
> deterministic search with a (deterministic) tree of successful results."
> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>
> So they rediscovered OLD resolution? Didn't check the rest of
> the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> They don't know the advantage of DPLL algorithms implemented
>
> with Backtracking, concerning time versus space tradeoff?
>
> Anyway, what is OLD resolution?
>
> H. Tamaki and T. Sato. OLD resolution with tabulation.
> In Proceedings of the Third International Conference on Logic
> Programming, pages 84–98. Springer Verlag, 1986. Lecture
> Notes in Computer Science, No. 225.
> https://www.researchgate.net/publication/220986525
>
> Here is a paper that mentions both SLD and OLD. Unfortunately
> they get SLD wrong. What they show as solve/1 is not SLD?
> Its only the Vanilla interpreter. How would SLD look like?
>
> PROLOG Interpreter for First-Order Intuitionistic Logic
> (Extended Abstract). January 1994
> L. Thorne McCartyLeon A. Shklar
> https://www.researchgate.net/publication/221135513
> Mostowski Collapse schrieb am Samstag, 17. Dezember 2022 um 03:31:15 UTC+1:
> > Now I am convinced, functional programming language
> > designers must hate logic and logic programming:
> >
> > The Verse Calculus: a Core Calculus for Functional Logic Programming
> > https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf
> >
> > LoL
> > Mostowski Collapse schrieb am Samstag, 17. Dezember 2022 um 10:20:51 UTC+11:
> > > Let's challenge the WAM, like here:
> > >
> > > A Hitchhiker’s Guide to Reinventing a Prolog Machine
> > > Paul Tarau - 2018 (Open Access)
> > > https://drops.dagstuhl.de/opus/volltexte/2018/8453/
> > >
> > > Interestingly Dogelog Player has adopted some of the ideas:
> > >
> > > Dogelog Player is a Prolog interpreter that is 100% written
> > > in Prolog itself. This also extends to the code generator that
> > > produces 6 instructions that are responsible for term unification
> > > and/or term building. In the upcoming release we will again
> > > only generate 5 instructions in a new way.
> > >
> > > We were able to extended the singleton analysis to a lifetime
> > > analysis of each variable. The results for our usual core
> > > benchmarks speak a mixed language. Many more change
> > > of point of view experiments are needed in the near future.
> > >
> > > Paul Taraus Reinventing a Prolog Machine Revisited
> > > https://twitter.com/dogelogch/status/1602228707623477248
> > >
> > > Paul Taraus Reinventing a Prolog Machine Revisited
> > > https://www.facebook.com/groups/dogelog
> > > geoffrey.a...@gmail.com schrieb am Samstag, 17. Dezember 2022 um 09:36:36 UTC+11:
> > > > Thank you for the references. Here's an archived version of the wambook: https://web.archive.org/web/20220119110941/http://wambook.sourceforge..net/. It's also currently being hosted at https://github.com/a-yiorgos/wambook.

But the idea of doing (“laid out in space”) instead of
(“laid out in time”) seems to be endemic for certain
functional programming camps. It even made its way into

Fundamental Proof Methods in Computer Science
by Konstantine Arkoudas and David Musser. As a
pinnacle it contains a Prolog interpreter, cast as

OLD resolution? Even if you would have some lazy
lists, I doubt it would be SLD resolution? Also it begs
the question whether lazy lists are (“laid out in space”)

and not rather (“laid out in time”)? Whats so
difficult in formal treatment of backtracking.
Does logic not have disjunction?

Fundamental Proof Methods in Computer Science
Konstantine Arkoudas and David Musser - 2017
https://www.amazon.com/dp/0262035537

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 12:57:21 UTC+2:
> DPLL is not really a trade-off between time and space.
> Its more the insight that if you can lay out in time,
> instead lay out in space, you can safe a lot of memory.
>
> https://en.wikipedia.org/wiki/DPLL_algorithm
>
> The backtracking is here:
>
> return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});
>
> The way the "or" can be practically implemented.
> Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 12:47:50 UTC+2:
> > The convinced me again that they hate logic and
> > logic programming, especially Backtracking. They
> > write nonsense like this:
> >
> > "Choice and determinism. Choice is a fundamental feature
> > of all functional logic languages. In VC, choice is expressed in the
> > syntax of the term (“laid out in space”) rather than, as is more typical,
> > handled by non-deterministic rewrites and backtracking
> >
> > (“laid out in time”). This makes VC completely deterministic,
> > nlike most functional logic languages which are non-deterministic
> > by design (Section 6.1). Inspired by their idea, we present a new
> > rewrite system for functional logic programs that reifies logical
> >
> > variables and unification into the term itself, and replaces non-
> > deterministic search with a (deterministic) tree of successful results."
> > https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
> >
> > So they rediscovered OLD resolution? Didn't check the rest of
> > the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> > They don't know the advantage of DPLL algorithms implemented
> >
> > with Backtracking, concerning time versus space tradeoff?
> >
> > Anyway, what is OLD resolution?
> >
> > H. Tamaki and T. Sato. OLD resolution with tabulation.
> > In Proceedings of the Third International Conference on Logic
> > Programming, pages 84–98. Springer Verlag, 1986. Lecture
> > Notes in Computer Science, No. 225.
> > https://www.researchgate.net/publication/220986525
> >
> > Here is a paper that mentions both SLD and OLD. Unfortunately
> > they get SLD wrong. What they show as solve/1 is not SLD?
> > Its only the Vanilla interpreter. How would SLD look like?
> >
> > PROLOG Interpreter for First-Order Intuitionistic Logic
> > (Extended Abstract). January 1994
> > L. Thorne McCartyLeon A. Shklar
> > https://www.researchgate.net/publication/221135513
> > Mostowski Collapse schrieb am Samstag, 17. Dezember 2022 um 03:31:15 UTC+1:
> > > Now I am convinced, functional programming language
> > > designers must hate logic and logic programming:
> > >
> > > The Verse Calculus: a Core Calculus for Functional Logic Programming
> > > https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf
> > >
> > > LoL
> > > Mostowski Collapse schrieb am Samstag, 17. Dezember 2022 um 10:20:51 UTC+11:
> > > > Let's challenge the WAM, like here:
> > > >
> > > > A Hitchhiker’s Guide to Reinventing a Prolog Machine
> > > > Paul Tarau - 2018 (Open Access)
> > > > https://drops.dagstuhl.de/opus/volltexte/2018/8453/
> > > >
> > > > Interestingly Dogelog Player has adopted some of the ideas:
> > > >
> > > > Dogelog Player is a Prolog interpreter that is 100% written
> > > > in Prolog itself. This also extends to the code generator that
> > > > produces 6 instructions that are responsible for term unification
> > > > and/or term building. In the upcoming release we will again
> > > > only generate 5 instructions in a new way.
> > > >
> > > > We were able to extended the singleton analysis to a lifetime
> > > > analysis of each variable. The results for our usual core
> > > > benchmarks speak a mixed language. Many more change
> > > > of point of view experiments are needed in the near future.
> > > >
> > > > Paul Taraus Reinventing a Prolog Machine Revisited
> > > > https://twitter.com/dogelogch/status/1602228707623477248
> > > >
> > > > Paul Taraus Reinventing a Prolog Machine Revisited
> > > > https://www.facebook.com/groups/dogelog
> > > > geoffrey.a...@gmail.com schrieb am Samstag, 17. Dezember 2022 um 09:36:36 UTC+11:
> > > > > Thank you for the references. Here's an archived version of the wambook: https://web.archive.org/web/20220119110941/http://wambook.sourceforge.net/. It's also currently being hosted at https://github.com/a-yiorgos/wambook.

On Wednesday, 26 April 2023 at 12:47:50 UTC+2, Mostowski Collapse wrote:
> The convinced me again that they hate logic and
> logic programming, especially Backtracking. They
> write nonsense like this:
>
> "Choice and determinism. Choice is a fundamental feature
> of all functional logic languages. In VC, choice is expressed in the
> syntax of the term (“laid out in space”) rather than, as is more typical,
> handled by non-deterministic rewrites and backtracking
> (“laid out in time”). This makes VC completely deterministic,
> unlike most functional logic languages which are non-deterministic
> by design (Section 6.1). Inspired by their idea, we present a new
> rewrite system for functional logic programs that reifies logical
> variables and unification into the term itself, and replaces non-
> deterministic search with a (deterministic) tree of successful results."
> <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
>
> So they rediscovered OLD resolution? Didn't check the rest of
> the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> They don't know the advantage of DPLL algorithms implemented
> with Backtracking, concerning time versus space tradeoff?

I find it quite interesting actually (thanks for the reference), as
I am trying to learn how to put logical and functional together,
and I find the fact that it is totally deterministic quite exiting
actually... nor I can envision any serious memory cost with
expanding choices in statements.

Julio

Julio wrote
> nor I can envision any serious memory cost

Unless P = NP, there is a serious difference between making
a full expansion tree and just using backtracking in an NP problem.

The difference is:

1) Memory Consumption in NP Problem, using backtracking:
O(f(n)) where f is some polynomial

2) Memory Consumption in NP Problem, using full expansion:
O(2^f(n)) where f is some polynomial

So you are unnecessarily moving
from PSPACE to EXPSPACE.

In computational complexity theory, PSPACE is the set
of all decision problems that can be solved by a Turing
machine using a polynomial amount of space.
https://en.wikipedia.org/wiki/PSPACE

In computational complexity theory, EXPSPACE is the
set of all decision problems solvable by a deterministic
Turing machine in exponential space
https://en.wikipedia.org/wiki/EXPSPACE

Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 15:45:21 UTC+2:
> On Wednesday, 26 April 2023 at 12:47:50 UTC+2, Mostowski Collapse wrote:
> > The convinced me again that they hate logic and
> > logic programming, especially Backtracking. They
> > write nonsense like this:
> >
> > "Choice and determinism. Choice is a fundamental feature
> > of all functional logic languages. In VC, choice is expressed in the
> > syntax of the term (“laid out in space”) rather than, as is more typical,
> > handled by non-deterministic rewrites and backtracking
> > (“laid out in time”). This makes VC completely deterministic,
> > unlike most functional logic languages which are non-deterministic
> > by design (Section 6.1). Inspired by their idea, we present a new
> > rewrite system for functional logic programs that reifies logical
> > variables and unification into the term itself, and replaces non-
> > deterministic search with a (deterministic) tree of successful results."
> > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> >
> > So they rediscovered OLD resolution? Didn't check the rest of
> > the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> > They don't know the advantage of DPLL algorithms implemented
> > with Backtracking, concerning time versus space tradeoff?
> I find it quite interesting actually (thanks for the reference), as
> I am trying to learn how to put logical and functional together,
> and I find the fact that it is totally deterministic quite exiting
> actually... nor I can envision any serious memory cost with
> expanding choices in statements.
>
> Julio

PSPACE = NPSPACE
https://en.wikipedia.org/wiki/Savitch%27s_theorem

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:43:21 UTC+2:
> Julio wrote
> > nor I can envision any serious memory cost
> Unless P = NP, there is a serious difference between making
> a full expansion tree and just using backtracking in an NP problem.
>
> The difference is:
>
> 1) Memory Consumption in NP Problem, using backtracking:
> O(f(n)) where f is some polynomial
>
> 2) Memory Consumption in NP Problem, using full expansion:
> O(2^f(n)) where f is some polynomial
>
> So you are unnecessarily moving
> from PSPACE to EXPSPACE.
>
> In computational complexity theory, PSPACE is the set
> of all decision problems that can be solved by a Turing
> machine using a polynomial amount of space.
> https://en.wikipedia.org/wiki/PSPACE
>
> In computational complexity theory, EXPSPACE is the
> set of all decision problems solvable by a deterministic
> Turing machine in exponential space
> https://en.wikipedia.org/wiki/EXPSPACE
> Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 15:45:21 UTC+2:
> > On Wednesday, 26 April 2023 at 12:47:50 UTC+2, Mostowski Collapse wrote:
> > > The convinced me again that they hate logic and
> > > logic programming, especially Backtracking. They
> > > write nonsense like this:
> > >
> > > "Choice and determinism. Choice is a fundamental feature
> > > of all functional logic languages. In VC, choice is expressed in the
> > > syntax of the term (“laid out in space”) rather than, as is more typical,
> > > handled by non-deterministic rewrites and backtracking
> > > (“laid out in time”). This makes VC completely deterministic,
> > > unlike most functional logic languages which are non-deterministic
> > > by design (Section 6.1). Inspired by their idea, we present a new
> > > rewrite system for functional logic programs that reifies logical
> > > variables and unification into the term itself, and replaces non-
> > > deterministic search with a (deterministic) tree of successful results."
> > > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> > >
> > > So they rediscovered OLD resolution? Didn't check the rest of
> > > the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> > > They don't know the advantage of DPLL algorithms implemented
> > > with Backtracking, concerning time versus space tradeoff?
> > I find it quite interesting actually (thanks for the reference), as
> > I am trying to learn how to put logical and functional together,
> > and I find the fact that it is totally deterministic quite exiting
> > actually... nor I can envision any serious memory cost with
> > expanding choices in statements.
> >
> > Julio

Hint: In complexity theory the word "space" is used
instead of the word "memory". You have different
complexity classes along these two dimensions:

XXX-TIME: Complexity classes looking at the runtime.

XXX-SPACE: Complexity classes looking at the space
requirement, aka memory requirement.

NP is defined as a XXX-TIME complexity, but there
exist some insights that give XXX-SPACE complexity
nevertheless. Functional programming not necessarily

sacrifices these lower bounds, since programming
languages such as Haskell have lazy evaluators, and
can be memory savy. But if a paper explicitly wants

to be memory eating, what can one say else than DOA,
i.e. dead on arrival. Its just a miscarriage. The poor
baby is already dead when it sees the light.

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:46:15 UTC+2:
> PSPACE = NPSPACE
> https://en.wikipedia.org/wiki/Savitch%27s_theorem
> Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:43:21 UTC+2:
> > Julio wrote
> > > nor I can envision any serious memory cost
> > Unless P = NP, there is a serious difference between making
> > a full expansion tree and just using backtracking in an NP problem.
> >
> > The difference is:
> >
> > 1) Memory Consumption in NP Problem, using backtracking:
> > O(f(n)) where f is some polynomial
> >
> > 2) Memory Consumption in NP Problem, using full expansion:
> > O(2^f(n)) where f is some polynomial
> >
> > So you are unnecessarily moving
> > from PSPACE to EXPSPACE.
> >
> > In computational complexity theory, PSPACE is the set
> > of all decision problems that can be solved by a Turing
> > machine using a polynomial amount of space.
> > https://en.wikipedia.org/wiki/PSPACE
> >
> > In computational complexity theory, EXPSPACE is the
> > set of all decision problems solvable by a deterministic
> > Turing machine in exponential space
> > https://en.wikipedia.org/wiki/EXPSPACE
> > Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 15:45:21 UTC+2:
> > > On Wednesday, 26 April 2023 at 12:47:50 UTC+2, Mostowski Collapse wrote:
> > > > The convinced me again that they hate logic and
> > > > logic programming, especially Backtracking. They
> > > > write nonsense like this:
> > > >
> > > > "Choice and determinism. Choice is a fundamental feature
> > > > of all functional logic languages. In VC, choice is expressed in the
> > > > syntax of the term (“laid out in space”) rather than, as is more typical,
> > > > handled by non-deterministic rewrites and backtracking
> > > > (“laid out in time”). This makes VC completely deterministic,
> > > > unlike most functional logic languages which are non-deterministic
> > > > by design (Section 6.1). Inspired by their idea, we present a new
> > > > rewrite system for functional logic programs that reifies logical
> > > > variables and unification into the term itself, and replaces non-
> > > > deterministic search with a (deterministic) tree of successful results."
> > > > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> > > >
> > > > So they rediscovered OLD resolution? Didn't check the rest of
> > > > the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> > > > They don't know the advantage of DPLL algorithms implemented
> > > > with Backtracking, concerning time versus space tradeoff?
> > > I find it quite interesting actually (thanks for the reference), as
> > > I am trying to learn how to put logical and functional together,
> > > and I find the fact that it is totally deterministic quite exiting
> > > actually... nor I can envision any serious memory cost with
> > > expanding choices in statements.
> > >
> > > Julio

On the other hand, it would be quite an interesting
experiment, whether the divide and conquere algorithm
behind Savitch's theorem:

"To test for a k-edge path from s to t, a deterministic algorithm
can iterate through all vertices u, and recursively search for paths
of half the length from s to u and from u to t. This algorithm can
be expressed in pseudocode (in Python syntax) as follows"
https://en.wikipedia.org/wiki/Savitch%27s_theorem

Has some feasible practical impact. Like:

a) Whether there is some impact on rewriting techniques,
what the Verse Paper subscribes to.
b) Whether there is some impact on reolution proving
technique more what Prolog subscribes to.

Don't know enough. Maybe Prolog isn't specialized enough,
and more general, so that already a Prolog text is too
general too be fed into a Savitch solver.

Maybe for some less general cases the approach
could be used. On the other hand the Verse Paper
reminds me to the idea that a logic program has

a finite solution, their all() construct. Not sure whether
this is a sub class enough that admits some clever evaluation
strategies so that the rewriting doesn't explode.

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:53:19 UTC+2:
> Hint: In complexity theory the word "space" is used
> instead of the word "memory". You have different
> complexity classes along these two dimensions:
>
> XXX-TIME: Complexity classes looking at the runtime.
>
> XXX-SPACE: Complexity classes looking at the space
> requirement, aka memory requirement.
>
> NP is defined as a XXX-TIME complexity, but there
> exist some insights that give XXX-SPACE complexity
> nevertheless. Functional programming not necessarily
>
> sacrifices these lower bounds, since programming
> languages such as Haskell have lazy evaluators, and
> can be memory savy. But if a paper explicitly wants
>
> to be memory eating, what can one say else than DOA,
> i.e. dead on arrival. Its just a miscarriage. The poor
> baby is already dead when it sees the light.
> Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:46:15 UTC+2:
> > PSPACE = NPSPACE
> > https://en.wikipedia.org/wiki/Savitch%27s_theorem
> > Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:43:21 UTC+2:
> > > Julio wrote
> > > > nor I can envision any serious memory cost
> > > Unless P = NP, there is a serious difference between making
> > > a full expansion tree and just using backtracking in an NP problem.
> > >
> > > The difference is:
> > >
> > > 1) Memory Consumption in NP Problem, using backtracking:
> > > O(f(n)) where f is some polynomial
> > >
> > > 2) Memory Consumption in NP Problem, using full expansion:
> > > O(2^f(n)) where f is some polynomial
> > >
> > > So you are unnecessarily moving
> > > from PSPACE to EXPSPACE.
> > >
> > > In computational complexity theory, PSPACE is the set
> > > of all decision problems that can be solved by a Turing
> > > machine using a polynomial amount of space.
> > > https://en.wikipedia.org/wiki/PSPACE
> > >
> > > In computational complexity theory, EXPSPACE is the
> > > set of all decision problems solvable by a deterministic
> > > Turing machine in exponential space
> > > https://en.wikipedia.org/wiki/EXPSPACE
> > > Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 15:45:21 UTC+2:
> > > > On Wednesday, 26 April 2023 at 12:47:50 UTC+2, Mostowski Collapse wrote:
> > > > > The convinced me again that they hate logic and
> > > > > logic programming, especially Backtracking. They
> > > > > write nonsense like this:
> > > > >
> > > > > "Choice and determinism. Choice is a fundamental feature
> > > > > of all functional logic languages. In VC, choice is expressed in the
> > > > > syntax of the term (“laid out in space”) rather than, as is more typical,
> > > > > handled by non-deterministic rewrites and backtracking
> > > > > (“laid out in time”). This makes VC completely deterministic,
> > > > > unlike most functional logic languages which are non-deterministic
> > > > > by design (Section 6.1). Inspired by their idea, we present a new
> > > > > rewrite system for functional logic programs that reifies logical
> > > > > variables and unification into the term itself, and replaces non-
> > > > > deterministic search with a (deterministic) tree of successful results."
> > > > > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> > > > >
> > > > > So they rediscovered OLD resolution? Didn't check the rest of
> > > > > the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> > > > > They don't know the advantage of DPLL algorithms implemented
> > > > > with Backtracking, concerning time versus space tradeoff?
> > > > I find it quite interesting actually (thanks for the reference), as
> > > > I am trying to learn how to put logical and functional together,
> > > > and I find the fact that it is totally deterministic quite exiting
> > > > actually... nor I can envision any serious memory cost with
> > > > expanding choices in statements.
> > > >
> > > > Julio

I picked NP as an example, since NP has also the property
that it only produces an finite number of solutions, since
the non-deterninistic head of the turing machin,

has only finite number of choices? And the number of
steps the turing machine does in a trace is bounded by
a polynomial. But I guess there a few more classes

that have a finite number of solutions property as well.
Whenever the SPACE is bounded? On the other
hand Prolog can easily succeeds infinitely many times:

nat(0).
nat(s(X)) :- nat(X).

?- nat(X).
X = 0 ;
X = s(0) ;
X = s(s(0)) ;
X = s(s(s(0))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(s(0)))))
Etc...

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 19:01:12 UTC+2:
> On the other hand, it would be quite an interesting
> experiment, whether the divide and conquere algorithm
> behind Savitch's theorem:
>
> "To test for a k-edge path from s to t, a deterministic algorithm
> can iterate through all vertices u, and recursively search for paths
> of half the length from s to u and from u to t. This algorithm can
> be expressed in pseudocode (in Python syntax) as follows"
> https://en.wikipedia.org/wiki/Savitch%27s_theorem
>
> Has some feasible practical impact. Like:
>
> a) Whether there is some impact on rewriting techniques,
> what the Verse Paper subscribes to.
> b) Whether there is some impact on reolution proving
> technique more what Prolog subscribes to.
>
> Don't know enough. Maybe Prolog isn't specialized enough,
> and more general, so that already a Prolog text is too
> general too be fed into a Savitch solver.
>
> Maybe for some less general cases the approach
> could be used. On the other hand the Verse Paper
> reminds me to the idea that a logic program has
>
> a finite solution, their all() construct. Not sure whether
> this is a sub class enough that admits some clever evaluation
> strategies so that the rewriting doesn't explode.
> Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:53:19 UTC+2:
> > Hint: In complexity theory the word "space" is used
> > instead of the word "memory". You have different
> > complexity classes along these two dimensions:
> >
> > XXX-TIME: Complexity classes looking at the runtime.
> >
> > XXX-SPACE: Complexity classes looking at the space
> > requirement, aka memory requirement.
> >
> > NP is defined as a XXX-TIME complexity, but there
> > exist some insights that give XXX-SPACE complexity
> > nevertheless. Functional programming not necessarily
> >
> > sacrifices these lower bounds, since programming
> > languages such as Haskell have lazy evaluators, and
> > can be memory savy. But if a paper explicitly wants
> >
> > to be memory eating, what can one say else than DOA,
> > i.e. dead on arrival. Its just a miscarriage. The poor
> > baby is already dead when it sees the light.
> > Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:46:15 UTC+2:
> > > PSPACE = NPSPACE
> > > https://en.wikipedia.org/wiki/Savitch%27s_theorem
> > > Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 18:43:21 UTC+2:
> > > > Julio wrote
> > > > > nor I can envision any serious memory cost
> > > > Unless P = NP, there is a serious difference between making
> > > > a full expansion tree and just using backtracking in an NP problem.
> > > >
> > > > The difference is:
> > > >
> > > > 1) Memory Consumption in NP Problem, using backtracking:
> > > > O(f(n)) where f is some polynomial
> > > >
> > > > 2) Memory Consumption in NP Problem, using full expansion:
> > > > O(2^f(n)) where f is some polynomial
> > > >
> > > > So you are unnecessarily moving
> > > > from PSPACE to EXPSPACE.
> > > >
> > > > In computational complexity theory, PSPACE is the set
> > > > of all decision problems that can be solved by a Turing
> > > > machine using a polynomial amount of space.
> > > > https://en.wikipedia.org/wiki/PSPACE
> > > >
> > > > In computational complexity theory, EXPSPACE is the
> > > > set of all decision problems solvable by a deterministic
> > > > Turing machine in exponential space
> > > > https://en.wikipedia.org/wiki/EXPSPACE
> > > > Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 15:45:21 UTC+2:
> > > > > On Wednesday, 26 April 2023 at 12:47:50 UTC+2, Mostowski Collapse wrote:
> > > > > > The convinced me again that they hate logic and
> > > > > > logic programming, especially Backtracking. They
> > > > > > write nonsense like this:
> > > > > >
> > > > > > "Choice and determinism. Choice is a fundamental feature
> > > > > > of all functional logic languages. In VC, choice is expressed in the
> > > > > > syntax of the term (“laid out in space”) rather than, as is more typical,
> > > > > > handled by non-deterministic rewrites and backtracking
> > > > > > (“laid out in time”). This makes VC completely deterministic,
> > > > > > unlike most functional logic languages which are non-deterministic
> > > > > > by design (Section 6.1). Inspired by their idea, we present a new
> > > > > > rewrite system for functional logic programs that reifies logical
> > > > > > variables and unification into the term itself, and replaces non-
> > > > > > deterministic search with a (deterministic) tree of successful results."
> > > > > > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> > > > > >
> > > > > > So they rediscovered OLD resolution? Didn't check the rest of
> > > > > > the paper yet. Looks like a DOA paper, Dead on Arrival Paper?
> > > > > > They don't know the advantage of DPLL algorithms implemented
> > > > > > with Backtracking, concerning time versus space tradeoff?
> > > > > I find it quite interesting actually (thanks for the reference), as
> > > > > I am trying to learn how to put logical and functional together,
> > > > > and I find the fact that it is totally deterministic quite exiting
> > > > > actually... nor I can envision any serious memory cost with
> > > > > expanding choices in statements.
> > > > >
> > > > > Julio

On Wednesday, 26 April 2023 at 18:43:21 UTC+2, Mostowski Collapse wrote:
> Julio wrote
> > > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> > nor I can envision any serious memory cost [with
> > expanding choices in statements.]
>
> Unless P = NP, there is a serious difference between making
> a full expansion tree and just using backtracking in an NP problem.

"Expanding choices in statements", e.g. (A/\(B|C)) becomes
((A/\B)\/(A/\C)): it is not about writing down all possible
solutions in advance... Read the paper.

Julio

Thats good example that shows the misery:

slow :- between(1,1000000,_), fail; true.
fast :- between(1,1,_), fail; true.

?- time((slow,(fast;fast),fail;true)).
% 1,000,005 inferences, 0.047 CPU in 0.044 seconds (107% CPU, 21333440 Lips)
true.

?- time((((slow,fast);(slow,fast)),fail;true)).
% 2,000,004 inferences, 0.078 CPU in 0.090 seconds (87% CPU, 25600051 Lips)
true.

Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 22:46:41 UTC+2:
> On Wednesday, 26 April 2023 at 18:43:21 UTC+2, Mostowski Collapse wrote:
> > Julio wrote
> > > > <https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf>
> > > nor I can envision any serious memory cost [with
> > > expanding choices in statements.]
> >
> > Unless P = NP, there is a serious difference between making
> > a full expansion tree and just using backtracking in an NP problem.
> "Expanding choices in statements", e.g. (A/\(B|C)) becomes
> ((A/\B)\/(A/\C)): it is not about writing down all possible
> solutions in advance... Read the paper.
>
> Julio

On Wednesday, 26 April 2023 at 23:07:07 UTC+2, Mostowski Collapse wrote:

> Thats good example that shows the misery:

A good example of the fact that you can't even read what you link.

Never mind.

Julio

Troll alert.

Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 23:40:26 UTC+2:
> On Wednesday, 26 April 2023 at 23:07:07 UTC+2, Mostowski Collapse wrote:
>
> > Thats good example that shows the misery:
> A good example of the fact that you can't even read what you link.
>
> Never mind.
>
> Julio

The trolling is possible the Type Prop from other
languages, and the rule posted by Julio:

> (A/\(B|C)) becomes ((A/\B)|(A/\C)) Read the paper

Which is nowhere in the paper. There is only a kind
of maplist, non-deterministic which reads:

<v1,..,vn> (v) = ∃x. x = v; (x = 0; v0) | ··· | (x = n; vn)

Which corresponds the Prolog library(lists) nth0.
This would allow to do what is prohibited in a choice
context, namely in a choice context, there is exactly
no possible choices to the left of the hole. So:

A/\(B|C)

needs to be rewritten into, provided one is happy
with a nth0 result, not sure where to put all() etc..:

lambda x ( (x B) | (x C) ) A

But if A is already evaluated before its passed into the
lambda expression, then you have the effect of Prolog A,(B;C).
This is an interesting idea, quite different from the
continuation style ideas for backtracking found elsewhere.

Continuation are though to be on the right hand side,
and thus lambda expressions usually have a formal parameter
for this right hand side. In the above a formal parameter for
a left hand side, the forbidden hole, appears.

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 23:52:55 UTC+2:
> Troll alert.
> Julio Di Egidio schrieb am Mittwoch, 26. April 2023 um 23:40:26 UTC+2:
> > On Wednesday, 26 April 2023 at 23:07:07 UTC+2, Mostowski Collapse wrote:
> >
> > > Thats good example that shows the misery:
> > A good example of the fact that you can't even read what you link.
> >
> > Never mind.
> >
> > Julio

On Thursday, 27 April 2023 at 00:20:28 UTC+2, Mostowski Collapse wrote:
> The trolling is possible the Type Prop from other
> languages, and the rule posted by Julio:
> > (A/\(B|C)) becomes ((A/\B)|(A/\C)) Read the paper

LOL, you insane spamming asshole.

Welcome to my killfile for good.

*Plonk*

Julio

You are not very good in arguing, you lack some
patience to dig to the ground of a problem. Did
greek rethorics get lost on its way to italy?

Julio Di Egidio schrieb am Donnerstag, 27. April 2023 um 02:37:37 UTC+2:
> On Thursday, 27 April 2023 at 00:20:28 UTC+2, Mostowski Collapse wrote:
> > The trolling is possible the Type Prop from other
> > languages, and the rule posted by Julio:
> > > (A/\(B|C)) becomes ((A/\B)|(A/\C)) Read the paper
> LOL, you insane spamming asshole.
>
> Welcome to my killfile for good.
>
> *Plonk*
>
> Julio

Hi everyone, I found a description of what looks like an interesting paper: https://web.archive.org/web/20220914214923/https://www.semanticscholar.org/paper/2-From-Prolog-to-Haskell-and-Back-Schrijvers-Demoen/3e0aff0f1e287b06deb427d56a2696af8228dd61

Unfortunately, I can't find the paper itself anywhere, even through the authors' respective webpages. Does anybody know where it might be? Thank you!

On 9/14/22 14:55, Geoffrey Churchill wrote:
> Hi everyone, I found a description of what looks like an interesting paper: https://web.archive.org/web/20220914214923/https://www.semanticscholar.org/paper/2-From-Prolog-to-Haskell-and-Back-Schrijvers-Demoen/3e0aff0f1e287b06deb427d56a2696af8228dd61
>
> Unfortunately, I can't find the paper itself anywhere, even through the authors' respective webpages. Does anybody know where it might be? Thank you!

https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/draft_eqprolog_iclp08.pdf

On Wednesday, September 21, 2022 at 12:15:02 PM UTC-4, Marc Petit-Huguenin wrote:
> On 9/14/22 14:55, Geoffrey Churchill wrote:
> > Hi everyone, I found a description of what looks like an interesting paper: https://web.archive.org/web/20220914214923/https://www.semanticscholar..org/paper/2-From-Prolog-to-Haskell-and-Back-Schrijvers-Demoen/3e0aff0f1e287b06deb427d56a2696af8228dd61
> >
> > Unfortunately, I can't find the paper itself anywhere, even through the authors' respective webpages. Does anybody know where it might be? Thank you!
> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/draft_eqprolog_iclp08.pdf

Ah thanks so much, and excellent sleuthing... I didn't see any notification from this group for some reason, so sorry for the late response.

It's interesting to think about which transformations might be best applied directly to Prolog source, and which could be better handled after compiling to some target language. Or, if there's a useful sequence of logics/languages between Prolog and a machine-friendly deterministic, imperative language, each of which would be conducive to a different class of transformations (e.g. idempotency of conj and disj might be best applied in Prolog, while constant folding could be applied after dropping to a functional language with deterministic procedural semantics). An optimizing compiler for Prolog could restrict itself to Prolog-specific transformations, and defer to a high-level target language's compiler for the rest.

The Prolog FAQ had a link:

This link says "Browse Open Source Software"
http://wambook.sourceforge.net

But this is now broken. It was a good source for Prolog
implementation, along different functionality levels,
i.e. what the Prolog system can do, a Prolog system

that is based on translating a Prolog text to WAM.
Maybe the FAQ should update the link, or maybe
even include another link, for example this

one is also nice:

"PicoProlog is a minimal subset of Prolog, implemented
by an interpreter written in Pascal. It is described in the
book, An introduction to logic programming through
Prolog, also available from this site."
https://spivey.oriel.ox.ac.uk/corner/PicoProlog

geoffrey.a...@gmail.com schrieb am Samstag, 15. Oktober 2022 um 23:37:07 UTC+2:
> On Wednesday, September 21, 2022 at 12:15:02 PM UTC-4, Marc Petit-Huguenin wrote:
> > On 9/14/22 14:55, Geoffrey Churchill wrote:
> > > Hi everyone, I found a description of what looks like an interesting paper: https://web.archive.org/web/20220914214923/https://www.semanticscholar.org/paper/2-From-Prolog-to-Haskell-and-Back-Schrijvers-Demoen/3e0aff0f1e287b06deb427d56a2696af8228dd61
> > >
> > > Unfortunately, I can't find the paper itself anywhere, even through the authors' respective webpages. Does anybody know where it might be? Thank you!
> > https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/draft_eqprolog_iclp08.pdf
> Ah thanks so much, and excellent sleuthing... I didn't see any notification from this group for some reason, so sorry for the late response.
>
> It's interesting to think about which transformations might be best applied directly to Prolog source, and which could be better handled after compiling to some target language. Or, if there's a useful sequence of logics/languages between Prolog and a machine-friendly deterministic, imperative language, each of which would be conducive to a different class of transformations (e.g. idempotency of conj and disj might be best applied in Prolog, while constant folding could be applied after dropping to a functional language with deterministic procedural semantics). An optimizing compiler for Prolog could restrict itself to Prolog-specific transformations, and defer to a high-level target language's compiler for the rest.

Since it wants Pascal, some discussion here to compile it:
https://stackoverflow.com/q/29907432/17524790

Mostowski Collapse schrieb am Dienstag, 18. Oktober 2022 um 15:49:07 UTC+2:
> The Prolog FAQ had a link:
>
> This link says "Browse Open Source Software"
> http://wambook.sourceforge.net
>
> But this is now broken. It was a good source for Prolog
> implementation, along different functionality levels,
> i.e. what the Prolog system can do, a Prolog system
>
> that is based on translating a Prolog text to WAM.
> Maybe the FAQ should update the link, or maybe
> even include another link, for example this
>
> one is also nice:
>
> "PicoProlog is a minimal subset of Prolog, implemented
> by an interpreter written in Pascal. It is described in the
> book, An introduction to logic programming through
> Prolog, also available from this site."
> https://spivey.oriel.ox.ac.uk/corner/PicoProlog
> geoffrey.a...@gmail.com schrieb am Samstag, 15. Oktober 2022 um 23:37:07 UTC+2:
> > On Wednesday, September 21, 2022 at 12:15:02 PM UTC-4, Marc Petit-Huguenin wrote:
> > > On 9/14/22 14:55, Geoffrey Churchill wrote:
> > > > Hi everyone, I found a description of what looks like an interesting paper: https://web.archive.org/web/20220914214923/https://www.semanticscholar.org/paper/2-From-Prolog-to-Haskell-and-Back-Schrijvers-Demoen/3e0aff0f1e287b06deb427d56a2696af8228dd61
> > > >
> > > > Unfortunately, I can't find the paper itself anywhere, even through the authors' respective webpages. Does anybody know where it might be? Thank you!
> > > https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/draft_eqprolog_iclp08.pdf
> > Ah thanks so much, and excellent sleuthing... I didn't see any notification from this group for some reason, so sorry for the late response.
> >
> > It's interesting to think about which transformations might be best applied directly to Prolog source, and which could be better handled after compiling to some target language. Or, if there's a useful sequence of logics/languages between Prolog and a machine-friendly deterministic, imperative language, each of which would be conducive to a different class of transformations (e.g. idempotency of conj and disj might be best applied in Prolog, while constant folding could be applied after dropping to a functional language with deterministic procedural semantics). An optimizing compiler for Prolog could restrict itself to Prolog-specific transformations, and defer to a high-level target language's compiler for the rest.

But maybe these discussions are not needed, the
website itself has a few build instructions:

a) Pascal-to-C translator
b) Using the Free Pascal Compiler
https://spivey.oriel.ox.ac.uk/corner/PicoProlog

Mostowski Collapse schrieb am Dienstag, 18. Oktober 2022 um 15:56:26 UTC+2:
> Since it wants Pascal, some discussion here to compile it:
> https://stackoverflow.com/q/29907432/17524790
> Mostowski Collapse schrieb am Dienstag, 18. Oktober 2022 um 15:49:07 UTC+2:
> > The Prolog FAQ had a link:
> >
> > This link says "Browse Open Source Software"
> > http://wambook.sourceforge.net
> >
> > But this is now broken. It was a good source for Prolog
> > implementation, along different functionality levels,
> > i.e. what the Prolog system can do, a Prolog system
> >
> > that is based on translating a Prolog text to WAM.
> > Maybe the FAQ should update the link, or maybe
> > even include another link, for example this
> >
> > one is also nice:
> >
> > "PicoProlog is a minimal subset of Prolog, implemented
> > by an interpreter written in Pascal. It is described in the
> > book, An introduction to logic programming through
> > Prolog, also available from this site."
> > https://spivey.oriel.ox.ac.uk/corner/PicoProlog
> > geoffrey.a...@gmail.com schrieb am Samstag, 15. Oktober 2022 um 23:37:07 UTC+2:
> > > On Wednesday, September 21, 2022 at 12:15:02 PM UTC-4, Marc Petit-Huguenin wrote:
> > > > On 9/14/22 14:55, Geoffrey Churchill wrote:
> > > > > Hi everyone, I found a description of what looks like an interesting paper: https://web.archive.org/web/20220914214923/https://www.semanticscholar.org/paper/2-From-Prolog-to-Haskell-and-Back-Schrijvers-Demoen/3e0aff0f1e287b06deb427d56a2696af8228dd61
> > > > >
> > > > > Unfortunately, I can't find the paper itself anywhere, even through the authors' respective webpages. Does anybody know where it might be? Thank you!
> > > > https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/draft_eqprolog_iclp08.pdf
> > > Ah thanks so much, and excellent sleuthing... I didn't see any notification from this group for some reason, so sorry for the late response.
> > >
> > > It's interesting to think about which transformations might be best applied directly to Prolog source, and which could be better handled after compiling to some target language. Or, if there's a useful sequence of logics/languages between Prolog and a machine-friendly deterministic, imperative language, each of which would be conducive to a different class of transformations (e.g. idempotency of conj and disj might be best applied in Prolog, while constant folding could be applied after dropping to a functional language with deterministic procedural semantics). An optimizing compiler for Prolog could restrict itself to Prolog-specific transformations, and defer to a high-level target language's compiler for the rest.