Hi,
This is nothing for Bart Demoen, Physics PhD,
academic fraud. The ideal choice point can
be formulated as a logical formula, involving
an existential quantifier. Assume we have
a query and already these answers, and the
Prolog system is prompting the interactive user:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
A mathematical oracle that could indicate whether
it is even necessary to prompt the user could be:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
It doesn't match 100% Prolog since Prolog might
give duplicate answers or non-ground answers,
but assume for the moment the query q(X),
produces only distinct and ground results.
Nice existential FOL formula we have in the above.
Bye
Mild Shock schrieb:
Henri Poincaré believed that mathematical
and scientific creativity came from a deep,
unconscious intuition that could not be
captured by mechanical reasoning or formal
systems. He famously wrote about how insights
came not from plodding logic but from sudden
illuminations — leaps of creative synthesis.
But now we have generative AI — models like GPT — that:
- produce poetry, proofs, stories, and code,
- combine ideas in novel ways,
- and do so by processing patterns in massive
datasets, without conscious understanding.
And that does seem to contradict Poincaré's belief
that true invention cannot come from automation.
Mild Shock schrieb:
Hi,
But I shouldn't waste too much time.
One shouldn't punish people for just
being plain stupid.
Like for example this clueless french
philosopher who had a lot of troubles
with non-classical logic.
His brain tried to eliminate non-classical
logic, it was keen on avoiding non-classical
logic. A typical species of a human with
an extremly small brain, again working
in the wrong place!
Bye
P.S.: Maybe this a Poincaré thingy? Poincaré
was a strong critic of logicism (as championed
by Frege and Russell) and of Hilbert’s
formalist program.
But, he did not formally use or promote systems
like intuitionistic logic, modal logic, or
relevance logic. His logical framework remained
within the bounds of classical logic,
though he was skeptical of excessive formalism.
He thought formal systems could miss the creative
and synthetic nature of mathematical
invention.
Hi,
Now what does a Prolog system do? Well when
it prompts the end-user it has somewhere
a list of the current query choice points:
CPs = [CP1, CP2, .., CPn]
This is implementation specific, what choice
points a system creates, also the ISO core standard
shows a machine in its more procedural explanation,
that depicts something that has also somewhere
choice points. Since it is implementation specific
a Prolog System A and Prolog System B might
use different choice points:
System A:
CPs = [CP1, CP2, .., CPn]
System B:
CP's = [CP'1, CP'2, .., CP'n]
We say a System B could eliminate a choice point CP,
relative to a System A, if we have:
System A:
CP ∈ CPs
System B:
CP ∉ CPs
So System B might have an advantage over System A,
since it will not backtrack over CP.
When it comes to answer substitution display,
it is now very common, that a Prolog system checks
its own choice points, and when it finds that
CP = []
It knows that the query left no choice points,
either because there were never any, because
there was no branching in the executed code, or
because a cut removed branching, or because
they were eliminated somehow. Like through
some index analysis.
Bye
Mild Shock schrieb:
Hi,
This is nothing for Bart Demoen, Physics PhD,
academic fraud. The ideal choice point can
be formulated as a logical formula, involving
an existential quantifier. Assume we have
a query and already these answers, and the
Prolog system is prompting the interactive user:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
A mathematical oracle that could indicate whether
it is even necessary to prompt the user could be:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
It doesn't match 100% Prolog since Prolog might
give duplicate answers or non-ground answers,
but assume for the moment the query q(X),
produces only distinct and ground results.
Nice existential FOL formula we have in the above.
Bye
Mild Shock schrieb:
Henri Poincaré believed that mathematical
and scientific creativity came from a deep,
unconscious intuition that could not be
captured by mechanical reasoning or formal
systems. He famously wrote about how insights
came not from plodding logic but from sudden
illuminations — leaps of creative synthesis.
But now we have generative AI — models like GPT — that:
- produce poetry, proofs, stories, and code,
- combine ideas in novel ways,
- and do so by processing patterns in massive
datasets, without conscious understanding.
And that does seem to contradict Poincaré's belief
that true invention cannot come from automation.
Mild Shock schrieb:
Hi,
But I shouldn't waste too much time.
One shouldn't punish people for just
being plain stupid.
Like for example this clueless french
philosopher who had a lot of troubles
with non-classical logic.
His brain tried to eliminate non-classical
logic, it was keen on avoiding non-classical
logic. A typical species of a human with
an extremly small brain, again working
in the wrong place!
Bye
P.S.: Maybe this a Poincaré thingy? Poincaré
was a strong critic of logicism (as championed
by Frege and Russell) and of Hilbert’s
formalist program.
But, he did not formally use or promote systems
like intuitionistic logic, modal logic, or
relevance logic. His logical framework remained
within the bounds of classical logic,
though he was skeptical of excessive formalism.
He thought formal systems could miss the creative
and synthetic nature of mathematical
invention.
Hi,
Now one might ask, if we have a Prolog system
that anyway juggles with choice points, why
would we need a logical formula for choice points?
Well there is a funny correctness criteria,
for example in the top-level, if the top-level
doesn't prompt the end user anymore in such a scenario:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
So the end user is not prompted because the
Prolog system founds CP = []. This is licensed
by this correctness statement for any choice
point elimination:
CP = [] => ~∃X ( p(X) & X =\= a1 & ... & X =\= ak)
Have Fun!
Bye
Mild Shock schrieb:
Hi,
Now what does a Prolog system do? Well when
it prompts the end-user it has somewhere
a list of the current query choice points:
CPs = [CP1, CP2, .., CPn]
This is implementation specific, what choice
points a system creates, also the ISO core standard
shows a machine in its more procedural explanation,
that depicts something that has also somewhere
choice points. Since it is implementation specific
a Prolog System A and Prolog System B might
use different choice points:
System A:
CPs = [CP1, CP2, .., CPn]
System B:
CP's = [CP'1, CP'2, .., CP'n]
We say a System B could eliminate a choice point CP,
relative to a System A, if we have:
System A:
CP ∈ CPs
System B:
CP ∉ CPs
So System B might have an advantage over System A,
since it will not backtrack over CP.
When it comes to answer substitution display,
it is now very common, that a Prolog system checks
its own choice points, and when it finds that
CP = []
It knows that the query left no choice points,
either because there were never any, because
there was no branching in the executed code, or
because a cut removed branching, or because
they were eliminated somehow. Like through
some index analysis.
Bye
Mild Shock schrieb:
Hi,
This is nothing for Bart Demoen, Physics PhD,
academic fraud. The ideal choice point can
be formulated as a logical formula, involving
an existential quantifier. Assume we have
a query and already these answers, and the
Prolog system is prompting the interactive user:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
A mathematical oracle that could indicate whether
it is even necessary to prompt the user could be:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
It doesn't match 100% Prolog since Prolog might
give duplicate answers or non-ground answers,
but assume for the moment the query q(X),
produces only distinct and ground results.
Nice existential FOL formula we have in the above.
Bye
Mild Shock schrieb:
Henri Poincaré believed that mathematical
and scientific creativity came from a deep,
unconscious intuition that could not be
captured by mechanical reasoning or formal
systems. He famously wrote about how insights
came not from plodding logic but from sudden
illuminations — leaps of creative synthesis.
But now we have generative AI — models like GPT — that:
- produce poetry, proofs, stories, and code,
- combine ideas in novel ways,
- and do so by processing patterns in massive
datasets, without conscious understanding.
And that does seem to contradict Poincaré's belief
that true invention cannot come from automation.
Mild Shock schrieb:
Hi,
But I shouldn't waste too much time.
One shouldn't punish people for just
being plain stupid.
Like for example this clueless french
philosopher who had a lot of troubles
with non-classical logic.
His brain tried to eliminate non-classical
logic, it was keen on avoiding non-classical
logic. A typical species of a human with
an extremly small brain, again working
in the wrong place!
Bye
P.S.: Maybe this a Poincaré thingy? Poincaré
was a strong critic of logicism (as championed
by Frege and Russell) and of Hilbert’s
formalist program.
But, he did not formally use or promote systems
like intuitionistic logic, modal logic, or
relevance logic. His logical framework remained
within the bounds of classical logic,
though he was skeptical of excessive formalism.
He thought formal systems could miss the creative
and synthetic nature of mathematical
invention.
Hi,
Today I had an idea, of some semi-deep Prolog
argument indexing. Just because choice point
elimination is so important and has so many
benefits for performance and the end user
experience, like also debugging. And because it is
tied to indexing. An index and the resulting clause
list, which can be always checked for having reached
its end. This gives a look-ahead information to the
Prolog system which answers this oracle, concering
clause instantiation:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
So the idea of semi-deep Prolog argument indexing
would be a hybrid between Scryer Prolog and
SWI-Prolog taking the best of both worls.
It would adopt skip indexes from Scryer Prolog
and deep indexing of SWI-Prolog, but deep indexing
through a Key computation trick. The Key computation
trick is quickly explained.
Normal Key Computations:
p(a, ..) ~~> Computed Key: a/0 or sometimes a alone
p(b(x,y), ..) ~~> Computed Key: b/2 or sometimes b alone
Etc..
Semi Deep Key Computation:
p(a, ..) ~~> Computed Key: 'a'
p([a, ..], ..) ~~> Computed Key: '.a'
Ect..
Got it?
The Scryer Prolog skip index is needed because
in a DCG the interesting arguments are usually
not the first argument.
Bye
Mild Shock schrieb:
Hi,
Now one might ask, if we have a Prolog system
that anyway juggles with choice points, why
would we need a logical formula for choice points?
Well there is a funny correctness criteria,
for example in the top-level, if the top-level
doesn't prompt the end user anymore in such a scenario:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
So the end user is not prompted because the
Prolog system founds CP = []. This is licensed
by this correctness statement for any choice
point elimination:
CP = [] => ~∃X ( p(X) & X =\= a1 & ... & X =\= ak)
Have Fun!
Bye
Mild Shock schrieb:
Hi,
Now what does a Prolog system do? Well when
it prompts the end-user it has somewhere
a list of the current query choice points:
CPs = [CP1, CP2, .., CPn]
This is implementation specific, what choice
points a system creates, also the ISO core standard
shows a machine in its more procedural explanation,
that depicts something that has also somewhere
choice points. Since it is implementation specific
a Prolog System A and Prolog System B might
use different choice points:
System A:
CPs = [CP1, CP2, .., CPn]
System B:
CP's = [CP'1, CP'2, .., CP'n]
We say a System B could eliminate a choice point CP,
relative to a System A, if we have:
System A:
CP ∈ CPs
System B:
CP ∉ CPs
So System B might have an advantage over System A,
since it will not backtrack over CP.
When it comes to answer substitution display,
it is now very common, that a Prolog system checks
its own choice points, and when it finds that
CP = []
It knows that the query left no choice points,
either because there were never any, because
there was no branching in the executed code, or
because a cut removed branching, or because
they were eliminated somehow. Like through
some index analysis.
Bye
Mild Shock schrieb:
Hi,
This is nothing for Bart Demoen, Physics PhD,
academic fraud. The ideal choice point can
be formulated as a logical formula, involving
an existential quantifier. Assume we have
a query and already these answers, and the
Prolog system is prompting the interactive user:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
A mathematical oracle that could indicate whether
it is even necessary to prompt the user could be:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
It doesn't match 100% Prolog since Prolog might
give duplicate answers or non-ground answers,
but assume for the moment the query q(X),
produces only distinct and ground results.
Nice existential FOL formula we have in the above.
Bye
Mild Shock schrieb:
Henri Poincaré believed that mathematical
and scientific creativity came from a deep,
unconscious intuition that could not be
captured by mechanical reasoning or formal
systems. He famously wrote about how insights
came not from plodding logic but from sudden
illuminations — leaps of creative synthesis.
But now we have generative AI — models like GPT — that:
- produce poetry, proofs, stories, and code,
- combine ideas in novel ways,
- and do so by processing patterns in massive
datasets, without conscious understanding.
And that does seem to contradict Poincaré's belief
that true invention cannot come from automation.
Mild Shock schrieb:
Hi,
But I shouldn't waste too much time.
One shouldn't punish people for just
being plain stupid.
Like for example this clueless french
philosopher who had a lot of troubles
with non-classical logic.
His brain tried to eliminate non-classical
logic, it was keen on avoiding non-classical
logic. A typical species of a human with
an extremly small brain, again working
in the wrong place!
Bye
P.S.: Maybe this a Poincaré thingy? Poincaré
was a strong critic of logicism (as championed
by Frege and Russell) and of Hilbert’s
formalist program.
But, he did not formally use or promote systems
like intuitionistic logic, modal logic, or
relevance logic. His logical framework remained
within the bounds of classical logic,
though he was skeptical of excessive formalism.
He thought formal systems could miss the creative
and synthetic nature of mathematical
invention.
Hi,
Lets say these semi-deep Prolog argument indexing
will really work. Then I could rollback some
uses of ROKs trick in my DCG based code base,
where I massaged the DCG to have a terminal in
the first argument, and DCG was somehow degraded
in only doing the concatenative stuff, through its
monad rewriting. This would lead to elegant code.
But it will not perform on a couple of Prolog systems,
that don't have deep indexing. I suspect the more
elegant code will not perform on these Prolog system:
- GNU Prolog
- Scryer Prolog
- Trealla Prolog
-
I didn't check ECLiPSe Prolog towards deep indexing,
and also I didn't check Ciao Prolog towards deep
indexing yet. It will show good performance:
- SWI-Prolog
- Dogelog Player (if I add semi-deep and skip there)
- Jekejeke Runtime (if I add semi-deep there, it has already skip)
-
Bye
Mild Shock schrieb:
Hi,
Today I had an idea, of some semi-deep Prolog
argument indexing. Just because choice point
elimination is so important and has so many
benefits for performance and the end user
experience, like also debugging. And because it is
tied to indexing. An index and the resulting clause
list, which can be always checked for having reached
its end. This gives a look-ahead information to the
Prolog system which answers this oracle, concering
clause instantiation:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
So the idea of semi-deep Prolog argument indexing
would be a hybrid between Scryer Prolog and
SWI-Prolog taking the best of both worls.
It would adopt skip indexes from Scryer Prolog
and deep indexing of SWI-Prolog, but deep indexing
through a Key computation trick. The Key computation
trick is quickly explained.
Normal Key Computations:
p(a, ..) ~~> Computed Key: a/0 or sometimes a alone
p(b(x,y), ..) ~~> Computed Key: b/2 or sometimes b alone
Etc..
Semi Deep Key Computation:
p(a, ..) ~~> Computed Key: 'a'
p([a, ..], ..) ~~> Computed Key: '.a'
Ect..
Got it?
The Scryer Prolog skip index is needed because
in a DCG the interesting arguments are usually
not the first argument.
Bye
Mild Shock schrieb:
Hi,
Now one might ask, if we have a Prolog system
that anyway juggles with choice points, why
would we need a logical formula for choice points?
Well there is a funny correctness criteria,
for example in the top-level, if the top-level
doesn't prompt the end user anymore in such a scenario:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
So the end user is not prompted because the
Prolog system founds CP = []. This is licensed
by this correctness statement for any choice
point elimination:
CP = [] => ~∃X ( p(X) & X =\= a1 & ... & X =\= ak)
Have Fun!
Bye
Mild Shock schrieb:
Hi,
Now what does a Prolog system do? Well when
it prompts the end-user it has somewhere
a list of the current query choice points:
CPs = [CP1, CP2, .., CPn]
This is implementation specific, what choice
points a system creates, also the ISO core standard
shows a machine in its more procedural explanation,
that depicts something that has also somewhere
choice points. Since it is implementation specific
a Prolog System A and Prolog System B might
use different choice points:
System A:
CPs = [CP1, CP2, .., CPn]
System B:
CP's = [CP'1, CP'2, .., CP'n]
We say a System B could eliminate a choice point CP,
relative to a System A, if we have:
System A:
CP ∈ CPs
System B:
CP ∉ CPs
So System B might have an advantage over System A,
since it will not backtrack over CP.
When it comes to answer substitution display,
it is now very common, that a Prolog system checks
its own choice points, and when it finds that
CP = []
It knows that the query left no choice points,
either because there were never any, because
there was no branching in the executed code, or
because a cut removed branching, or because
they were eliminated somehow. Like through
some index analysis.
Bye
Mild Shock schrieb:
Hi,
This is nothing for Bart Demoen, Physics PhD,
academic fraud. The ideal choice point can
be formulated as a logical formula, involving
an existential quantifier. Assume we have
a query and already these answers, and the
Prolog system is prompting the interactive user:
?- p(X).
X = a1 ;
X = a2 ;
...
X = ak-1 ;
X = ak
A mathematical oracle that could indicate whether
it is even necessary to prompt the user could be:
∃X ( p(X) & X =\= a1 & ... & X =\= ak)
It doesn't match 100% Prolog since Prolog might
give duplicate answers or non-ground answers,
but assume for the moment the query q(X),
produces only distinct and ground results.
Nice existential FOL formula we have in the above.
Bye
Mild Shock schrieb:
Henri Poincaré believed that mathematical
and scientific creativity came from a deep,
unconscious intuition that could not be
captured by mechanical reasoning or formal
systems. He famously wrote about how insights
came not from plodding logic but from sudden
illuminations — leaps of creative synthesis.
But now we have generative AI — models like GPT — that:
- produce poetry, proofs, stories, and code,
- combine ideas in novel ways,
- and do so by processing patterns in massive
datasets, without conscious understanding.
And that does seem to contradict Poincaré's belief
that true invention cannot come from automation.
Mild Shock schrieb:
Hi,
But I shouldn't waste too much time.
One shouldn't punish people for just
being plain stupid.
Like for example this clueless french
philosopher who had a lot of troubles
with non-classical logic.
His brain tried to eliminate non-classical
logic, it was keen on avoiding non-classical
logic. A typical species of a human with
an extremly small brain, again working
in the wrong place!
Bye
P.S.: Maybe this a Poincaré thingy? Poincaré
was a strong critic of logicism (as championed
by Frege and Russell) and of Hilbert’s
formalist program.
But, he did not formally use or promote systems
like intuitionistic logic, modal logic, or
relevance logic. His logical framework remained
within the bounds of classical logic,
though he was skeptical of excessive formalism.
He thought formal systems could miss the creative
and synthetic nature of mathematical
invention.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 716 |
| Nodes: | 16 (3 / 13) |
| Uptime: | 53:17:36 |
| Calls: | 12,116 |
| Calls today: | 7 |
| Files: | 15,010 |
| Messages: | 6,518,604 |
| Posted today: | 2 |