LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
On 2022-04-30 07:02:23 +0000, olcott said:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
This is correct but to fail would also be correct.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
unify_with_occurs_check must fail if the unified data structure
would contain loops.
Mikko
I just want to add some small note.
This "not(true(_))" thing is misleading.
Please note that it is *not* a negation.
Functionally it is equivalent to:
X = foo(bar(X)).
On 4/30/22 11:31, Mikko wrote:
On 2022-04-30 07:02:23 +0000, olcott said:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
This is correct but to fail would also be correct.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
unify_with_occurs_check must fail if the unified data structure
would contain loops.
Mikko
On 2022-04-30 07:02:23 +0000, olcott said:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
This is correct but to fail would also be correct.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
unify_with_occurs_check must fail if the unified data structure
would contain loops.
Mikko
On 4/30/2022 4:31 AM, Mikko wrote:
On 2022-04-30 07:02:23 +0000, olcott said:
LP := ~True(LP) is translated to Prolog:
?- LP = not(true(LP)).
LP = not(true(LP)).
This is correct but to fail would also be correct.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
unify_with_occurs_check must fail if the unified data structure
would contain loops.
Mikko
The above is the actual execution of actual Prolog code using
(SWI-Prolog (threaded, 64 bits, version 7.6.4).
According to Clocksin & Mellish it is not a mere loop, it is an
"infinite term" thus infinitely recursive definition.
I am trying to validate whether or not my Prolog code encodes the Liar Paradox.
I just want to add some small note.
This "not(true(_))" thing is misleading.
Please note that it is *not* a negation.
Functionally it is equivalent to:
X = foo(bar(X)).
Not in this case, it is very obvious that no theorem prover can
possibly prove any infinite expression.
negation, not, \+
The concept of logical negation in Prolog is problematical, in the
sense that the only method that Prolog can use to tell if a proposition
is false is to try to prove it (from the facts and rules that it has
been told about), and then if this attempt fails, it concludes that the proposition is false. This is referred to as negation as failure.
The whole purpose of this thread is to find out exactly how to encode: "This sentence is not true" in Prolog when we assume that True is
exactly the same thing as Provable in Prolog.
"This sentence is not provable" can be naïvely encoded:
g :- \+ g.
Then you can ask Prolog if this sentence is true:
?- g.
On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
The whole purpose of this thread is to find out exactly how to encode:
"This sentence is not true" in Prolog when we assume that True is
exactly the same thing as Provable in Prolog.
As long as it's equal to "<whatever> is not provable",
that's just any proposition <whatever> that fails, e.g.
g :- fail. As to how to rather encode self-referentiality,
and to begin with one needs first-order, that's something
to think about... just I am not sure how you do without
the whole Goedel construction unless by using Prolog
and maybe its meta-programming in some clever way.
"This sentence is not provable" can be naïvely encoded:
g :- \+ g.
Then you can ask Prolog if this sentence is true:
?- g.
Prolog won't give any answer, it'll just crash. You (think you)
know what the answer is, but in fact it's the same answer
you'd get with g :- g.
Julio
On 5/2/2022 9:59 AM, Julio Di Egidio wrote:
On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
The whole purpose of this thread is to find out exactly how to encode: >>> "This sentence is not true" in Prolog when we assume that True is
exactly the same thing as Provable in Prolog.
As long as it's equal to "<whatever> is not provable",
that's just any proposition <whatever> that fails, e.g.
g :- fail. As to how to rather encode self-referentiality,
and to begin with one needs first-order, that's something
to think about... just I am not sure how you do without
the whole Goedel construction unless by using Prolog
and maybe its meta-programming in some clever way.
"This sentence is not provable" can be naïvely encoded:
g :- \+ g.
Then you can ask Prolog if this sentence is true:
?- g.
Prolog won't give any answer, it'll just crash. You (think you)
know what the answer is, but in fact it's the same answer
you'd get with g :- g.
That is exactly what I expected.
Does it crash because it ran out of memory?
unify_with_occurs_check is supposed to determine in
advance that unification will crash. Can it be applied to
the above?
Do we have any Prolog that shows in advance that the
above expressions would crash?
On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
"This sentence is not provable" can be naïvely encoded:
g :- \+ g.
Then you can ask Prolog if this sentence is true:
?- g.
Prolog won't give any answer, it'll just crash. You (think you)
know what the answer is, but in fact it's the same answer
you'd get with g :- g.
Julio
On 5/2/22 18:04, olcott wrote:
Is there any Prolog that can detect that the above will not terminate prior to executing it?
As I have said previously, my example is naïve.
Maybe if you will think
hard enough you can make it detect such conditions, probably by writing meta-interpreter of some sort, and terminate. Personally, I don't think
that using Prolog can be accepted as a "rigorous proof" of anything.
On Monday, 2 May 2022 at 17:45:26 UTC+2, olcott wrote:
On 5/2/2022 9:59 AM, Julio Di Egidio wrote:
On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
The whole purpose of this thread is to find out exactly how to encode: >>>>> "This sentence is not true" in Prolog when we assume that True is
exactly the same thing as Provable in Prolog.
As long as it's equal to "<whatever> is not provable",
that's just any proposition <whatever> that fails, e.g.
g :- fail. As to how to rather encode self-referentiality,
and to begin with one needs first-order, that's something
to think about... just I am not sure how you do without
the whole Goedel construction unless by using Prolog
and maybe its meta-programming in some clever way.
"This sentence is not provable" can be naïvely encoded:
g :- \+ g.
Then you can ask Prolog if this sentence is true:
?- g.
Prolog won't give any answer, it'll just crash. You (think you)
know what the answer is, but in fact it's the same answer
you'd get with g :- g.
That is exactly what I expected.
g:-\+g as g:-g are literally and simply infinite loops: neither
captures anything deep about anything. Aka plain and
simple divergent computation.
Does it crash because it ran out of memory?
Yes, but even if it didn't, it'd be you at some point who would
have to switch it off. And still that wouldn't be a proof of
anything.
unify_with_occurs_check is supposed to determine in
advance that unification will crash. Can it be applied to
the above?
So far you aren't using unification at all: you need to go
first order, i.e. predicates with (variable) arguments.
Do we have any Prolog that shows in advance that the
above expressions would crash?
Would "not terminate", "crash" is quite broader... and no,
not in general: i.e. not until you solve the halting problem.
Julio
On 5/2/22 18:51, Julio Di Egidio wrote:
On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
On 5/2/22 18:04, olcott wrote:
Is there any Prolog that can detect that the above will not terminate >>> prior to executing it?
As I have said previously, my example is naïve.
And as I have pointed out to you, your "solution" solves nothing at all.The request from topic poster was — how would I represent sentence "This sentence is not provable". I came up with some small example
Maybe if you will think
hard enough you can make it detect such conditions, probably by writing >> meta-interpreter of some sort, and terminate. Personally, I don't think >> that using Prolog can be accepted as a "rigorous proof" of anything.
That's just nonsense: Prolog is a formal language no less than any other. Plus you too must think you have a solution to the halting problem...
No, I don't have a solution for a halting problem, I'm not a freak, but
also solving termination for _some_ specially designed simple programs doesn't require halting problem. It's some first grader stuff, c'mon.
On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
On 5/2/22 18:04, olcott wrote:
Is there any Prolog that can detect that the above will not terminate
prior to executing it?
As I have said previously, my example is naïve.
And as I have pointed out to you, your "solution" solves nothing at all.
Maybe if you will think
hard enough you can make it detect such conditions, probably by writing
meta-interpreter of some sort, and terminate. Personally, I don't think
that using Prolog can be accepted as a "rigorous proof" of anything.
That's just nonsense: Prolog is a formal language no less than any other. Plus you too must think you have a solution to the halting problem...
On 5/2/22 18:51, Julio Di Egidio wrote:
On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
On 5/2/22 18:04, olcott wrote:
Is there any Prolog that can detect that the above will not terminate
prior to executing it?
As I have said previously, my example is naïve.
And as I have pointed out to you, your "solution" solves nothing at all.
The request from topic poster was — how would I represent sentence "This sentence is not provable". I came up with some small example of "not
provable sentence" which happens to be a simple infinite loop. I did
*not* claim that it captures anything deep and solves halting problem,
that would've been absurd. If you have any better idea please write it.
Maybe if you will think
hard enough you can make it detect such conditions, probably by writing
meta-interpreter of some sort, and terminate. Personally, I don't think
that using Prolog can be accepted as a "rigorous proof" of anything.
That's just nonsense: Prolog is a formal language no less than any other.
Plus you too must think you have a solution to the halting problem...
No, I don't have a solution for a halting problem, I'm not a freak, but
also solving termination for _some_ specially designed simple programs doesn't require halting problem. It's some first grader stuff, c'mon.
Like this random example from my head (in C++):
int sum = 0;
for (int i = 5; i > 0; i--)
sum += i;
Can be proved to always terminate, because loop's variant `i` has lower bound, has total ordering and it's value decreases on each iteration. In
some cases you can automatically detect such loop variants, and
automatically prove termination of _some_ loops.
What do you think of this version:
?- LP = not(LP).
LP = not(LP).
On 5/2/22 18:51, Julio Di Egidio wrote:
On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
On 5/2/22 18:04, olcott wrote:
Is there any Prolog that can detect that the above will not terminate
prior to executing it?
As I have said previously, my example is naïve.
And as I have pointed out to you, your "solution" solves nothing at all.
The request from topic poster was — how would I represent sentence "This sentence is not provable". I came up with some small example of "not
provable sentence"
which happens to be a simple infinite loop. I did
*not* claim that it captures anything deep and solves halting problem,
that would've been absurd. If you have any better idea please write it.
Maybe if you will think
hard enough you can make it detect such conditions, probably by writing
meta-interpreter of some sort, and terminate. Personally, I don't think
that using Prolog can be accepted as a "rigorous proof" of anything.
That's just nonsense: Prolog is a formal language no less than any other.
Plus you too must think you have a solution to the halting problem...
No, I don't have a solution for a halting problem, I'm not a freak, but
also solving termination for _some_ specially designed simple programs doesn't require halting problem. It's some first grader stuff, c'mon.
Like this random example from my head (in C++):
int sum = 0;
for (int i = 5; i > 0; i--)
sum += i;
Can be proved to always terminate, because loop's variant `i` has lower bound, has total ordering and it's value decreases on each iteration. In
some cases you can automatically detect such loop variants, and
automatically prove termination of _some_ loops.
On 5/2/22 21:24, olcott wrote:
What do you think of this version:
?- LP = not(LP).
LP = not(LP).
In this expression, `not` is treated as a term — a symbol without any meaning, just text "not", and not the _negation_.
If you want to check if a variable can be different from itself you can
try this:
?- dif(X, X).
But, remember that dif/2 isn't available in all Prolog implementations.
On Monday, 2 May 2022 at 19:39:01 UTC+2, Aleksy Grabowski wrote:
On 5/2/22 18:51, Julio Di Egidio wrote:
On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:The request from topic poster was — how would I represent sentence "This >> sentence is not provable". I came up with some small example
On 5/2/22 18:04, olcott wrote:
Is there any Prolog that can detect that the above will not terminate >>>>> prior to executing it?
As I have said previously, my example is naïve.
And as I have pointed out to you, your "solution" solves nothing at all.
No, you didn't, and I have said why twice by now.
Maybe if you will think
hard enough you can make it detect such conditions, probably by writing >>>> meta-interpreter of some sort, and terminate. Personally, I don't think >>>> that using Prolog can be accepted as a "rigorous proof" of anything.
That's just nonsense: Prolog is a formal language no less than any other. >>> Plus you too must think you have a solution to the halting problem...
No, I don't have a solution for a halting problem, I'm not a freak, but
also solving termination for _some_ specially designed simple programs
doesn't require halting problem. It's some first grader stuff, c'mon.
You bring it up: and it is in fact irrelevant here, as long as the
original question is the question you noticed it is.
Anyway, discussing with Olcott's interlocutors is always even
worse than discussing with Olcott himself...
(EOD.)
Julio
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
Predicate not/1
not(:Goal)
True if Goal cannot be proven. Retained for compatibility only. New code should use \+/1.
https://www.swi-prolog.org/pldoc/man?predicate=not/1
SWI Prolog does not accept this, did I say it incorrectly?
?- g :- \+ g.
?- g.
?- g :- \+ g.
On 5/2/22 22:10, olcott wrote:
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
Predicate not/1
not(:Goal)
True if Goal cannot be proven. Retained for compatibility only. New
code should use \+/1.
https://www.swi-prolog.org/pldoc/man?predicate=not/1
SWI Prolog does not accept this, did I say it incorrectly?
?- g :- \+ g.
?- g.
You have said it incorrectly. Prolog program has two different parts: knowledge base and a query.
Knowledge base is usually loaded from the text file before starting
Prolog runtime.
Query can be asked using interactive prompt.
The general distinction is that knowledge base should contain everything
that is known, and query is used to ask questions to that database.
?- g :- \+ g.
This expression asks a question (note question mark), which isn't
correct, it should be stated as a fact.
Quick and dirty way to add facts dynamically is to use very special `assertz/1` predicate. Like this:
?- assertz( (g :- \+ g) ).
true.
Then you can normally ask a question:
?- g.
This question causes infinite loop, so you will never see an answer,
which is correct.
There are couple of strategies to detect infinite recursion in some very limited number of predicates, but they are quite advanced and probably
we don't want to go there.
On 5/2/22 22:58, olcott wrote:
This one seems to work:
?- LP = \+(true(LP)).
LP = (\+true(LP)).
?- unify_with_occurs_check(LP, \+(true(LP))).
false.
Sadly you aren't using Prolog correctly. You still have to *execute* predicates, because right now they don't mean anything. You can try to
enable predicate tracer and see for yourself that neither \+ nor `true`
is ever executed.
To enable tracer issue following command in the prompt:
?- trace.
true.
Then you can run your queries again. Then don't forget to disable
tracer, by issuing command:
?- notrace.
true.
Also, Prolog doesn't define true/1 predicate it defines only true/0
without any arguments. First of all you need to define it:
?- assertz( (true(X) :- call(X)) ).
Then still you need to execute your goals by using special call/1
predicate.
?- LP = \+(true(LP)), call(LP).
With occurs check you will see that it will fail even sooner, and it
wont be even executed.
That is why I updated it to this:
?- LP = \+(LP).
LP = (\+LP).
?- unify_with_occurs_check(LP, \+(LP)).
false.
On 5/2/2022 3:37 PM, Aleksy Grabowski wrote:
On 5/2/22 22:10, olcott wrote:
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
Predicate not/1
not(:Goal)
True if Goal cannot be proven. Retained for compatibility only. New
code should use \+/1.
https://www.swi-prolog.org/pldoc/man?predicate=not/1
SWI Prolog does not accept this, did I say it incorrectly?
?- g :- \+ g.
?- g.
You have said it incorrectly. Prolog program has two different parts:
knowledge base and a query.
Knowledge base is usually loaded from the text file before starting
Prolog runtime.
Query can be asked using interactive prompt.
The general distinction is that knowledge base should contain
everything that is known, and query is used to ask questions to that
database.
?- g :- \+ g.
This expression asks a question (note question mark), which isn't
correct, it should be stated as a fact.
Quick and dirty way to add facts dynamically is to use very special
`assertz/1` predicate. Like this:
?- assertz( (g :- \+ g) ).
true.
Then you can normally ask a question:
?- g.
This question causes infinite loop, so you will never see an answer,
which is correct.
I do see that it is rejected by SWI Prolog:
?- assertz( (g :- \+ g) ).
true.
?- g.
ERROR: Out of local stack
?-
There are couple of strategies to detect infinite recursion in some
very limited number of predicates, but they are quite advanced and
probably we don't want to go there.
This one seems to work:
?- LP = \+(true(LP)).
LP = (\+true(LP)).
?- unify_with_occurs_check(LP, \+(true(LP))).
false.
On Tuesday, 3 May 2022 at 00:38:57 UTC+2, Richard Damon wrote:
IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and
in particular, it is very limited in the mathematics it can handle.
I am pretty sure that Prolog is NOT up to handling the logic needed to handle the mathematics needed to express Godel's G, or the Halting Problem.
Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
have only proven that your limited logic system can't reach them in expressibility.
Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form is
a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use Coq
theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.
Prolog is a Turing-complete language, duh.
When Dunning-Kruger is a compliment...
Get the fuck out of comp.lang.prolog.
*Plonk*
Julio
Prolog *by itself* is a very bad theorem prover and it is very limited framework for formal logic, because it implements only Horn clauses.
However it is a very good programming language and you can implement
any theorem prover in it, like you can implement any theorem prover
in C++ or Java.
On 5/3/22 01:00, Julio Di Egidio wrote:
Prolog is a Turing-complete language, duh.
When Dunning-Kruger is a compliment...
Get the fuck out of comp.lang.prolog.
*Plonk*
JulioI've already wrote it in one of my previous posts, I just didn't want to repeat myself:
Prolog *by itself* is a very bad theorem prover and it is very limited framework for formal logic, because it implements only Horn clauses. However it is a very good programming language and you can implement
any theorem prover in it, like you can implement any theorem prover
in C++ or Java.
I probably have found your profile on the internet and I conclude that
your arrogance directly stems from your lack of any formal education.
You didn't graduate from any high school and that's why you want to show everybody your perceived superiority.
I'll just ignore you for the time being.
Aleksy Grabowski <hur...@gmail.com> writes:
IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your
logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.
I am pretty sure that Prolog is NOT up to handling the logic needed to
handle the mathematics needed to express Godel's G, or the Halting Problem.
Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
have only proven that your limited logic system can't reach them in expressibility.
Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use Coq theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).
On 5/2/22 23:42, olcott wrote:
That is why I updated it to this:
?- LP = \+(LP).
LP = (\+LP).
?- unify_with_occurs_check(LP, \+(LP)).
false.
This still is incorrect.
First of all, enable tracing:
?- trace.
true.
Then *execute* the predicates that you are trying to use:
[trace] ?- LP = \+(LP), call(LP).
Call: (11) _6566=(\+_6566) ? creep
Exit: (11) (\+ \+ \+ \+ \+ \+ \+ \+ \+ ...)=(\+ \+ \+ \+ \+ \+ \+ \+ \+ ...) ? creep
ERROR: Cannot represent due to `cyclic_term'
ERROR: In:
ERROR: [10] '<meta-call>'(user:user: ...)
ERROR: [9] toplevel_call(user:user: ...)
Which will throw an exception, because Prolog can't deal with it.
If you will try to unify without occurs check:
[trace] ?- unify_with_occurs_check(LP, \+(LP)), call(LP).
Call: (11) unify_with_occurs_check(_1010, \+_1010) ? creep
Fail: (11) unify_with_occurs_check(_1010, \+_1010) ? creep
false.
Then you will see, that your operator \+ isn't even mentioned, as it
wasn't executed by the Prolog system, because unification with occurs
check doesn't work for self referential terms. The whole reason of
occurs check is to reject such terms, this is why this check was added
in the first place.
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polc...@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hur...@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying to tell >>>> to topic poster in one of my previous posts. Prolog in it's bare form >>>> is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use Coq >>>> theorem prover, I've never used it by myself, but it looks like one of >>>> the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper proof assistant, Coq.
It is OK that you are not a math guy.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 491 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 147:11:50 |
| Calls: | 9,694 |
| Calls today: | 4 |
| Files: | 13,732 |
| Messages: | 6,178,671 |