olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable(
F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable
(F, G))" can be proven for some F and some G that do not contain cycles.
The answer is that in the proof system of Prolog it cannot be.
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable(
F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable
(F, G))" can be proven for some F and some G that do not contain cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable( >>> F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable >>> (F, G))" can be proven for some F and some G that do not contain cycles. >>> The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
When "G = not(provable(F, G))." is used as a Prolog goal the
applied semantics is what Prolog lauguage definition specifies.
Does "semantically sound" mean something in that context?
At least your Prolog interpretation finds it meaningful. It determines
that the excution of that goal succeeds and assigns a value G but not
to F.
On 12/6/2025 3:30 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
When "G = not(provable(F, G))." is used as a Prolog goal the
applied semantics is what Prolog lauguage definition specifies.
Does "semantically sound" mean something in that context?
At least your Prolog interpretation finds it meaningful. It determines
that the excution of that goal succeeds and assigns a value G but not
to F.
Is this sentence true or false:
"This sentence is not true"
It is not semantically sound.
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable(
F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable
(F, G))" can be proven for some F and some G that do not contain cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable( >>> F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable >>> (F, G))" can be proven for some F and some G that do not contain cycles. >>> The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
olcott kirjoitti 6.12.2025 klo 14.50:
On 12/6/2025 3:30 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
When "G = not(provable(F, G))." is used as a Prolog goal the
applied semantics is what Prolog lauguage definition specifies.
Does "semantically sound" mean something in that context?
At least your Prolog interpretation finds it meaningful. It determines
that the excution of that goal succeeds and assigns a value G but not
to F.
Is this sentence true or false:
"This sentence is not true"
It is not semantically sound.
Formal systems we usually use have no expression for "this".
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)...
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate unify_with_occurs_check/2 is used explicitly instead of the normal unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable. END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
On 10/12/2025 14:10, olcott wrote:
BEGIN:(Clocksin & Mellish 2003:254)...
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
You're a veritable treasure-trove.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:% This sentence cannot be proven in F
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter >>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means. >>>>>>
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it >>>>>> can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate unify_with_occurs_check/2 is used explicitly instead of the normal unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable. END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
olcott kirjoitti 10.12.2025 klo 16.10:
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:% This sentence cannot be proven in F
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter >>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means. >>>>>>>
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that >>>>>>> it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain >>>>>>> cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
As I say non-terminating, thus never resolves to a truth value.Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
olcott kirjoitti 10.12.2025 klo 16.10:
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As I say non-terminating, thus never resolves to a truth value.
olcott kirjoitti 10.12.2025 klo 16.10:
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
On 11/12/2025 14:17, olcott wrote:
As I say non-terminating, thus never resolves to a truth value.
$ export S='G=foo(G).'; gprolog <<<"$S"; swipl <<<"$S"
GNU Prolog 1.4.5 (64 bits)
Compiled Feb 23 2020, 20:14:50 with gcc
By Daniel Diaz
Copyright (C) 1999-2020 Daniel Diaz
| ?-
cannot display cyclic term for G
yes
| ?-
Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
G = foo(G).
% halt
On 12/11/2025 5:28 PM, Tristan Wibberley wrote:
olcott kirjoitti 10.12.2025 klo 16.10:
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
On 11/12/2025 14:17, olcott wrote:
As I say non-terminating, thus never resolves to a truth value.
$ export S='G=foo(G).'; gprolog <<<"$S"; swipl <<<"$S"
GNU Prolog 1.4.5 (64 bits)
Compiled Feb 23 2020, 20:14:50 with gcc
By Daniel Diaz
Copyright (C) 1999-2020 Daniel Diaz
| ?-
cannot display cyclic term for G
yes
| ?-
Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
G = foo(G).
% halt
Run SWI-Prolog
paste "G = not(provable(F, G))."
at the ?- prompt ending up this:
?- G = not(provable(F, G)).
Then you hit return and get this:
G = not(provable(F, G)).
Then you past this: "unify_with_occurs_check(G, not(provable(F, G)))."
at the next ?- prompt and get this
?- unify_with_occurs_check(G, not(provable(F, G))).
You hit return and get this:
false
*It all ends up looking like this*
*It all ends up looking like this*
*It all ends up looking like this*
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:% This sentence cannot be proven in F
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means. >>>>>>>>
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that >>>>>>>> it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain >>>>>>>> cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
As I say non-terminating, thus never resolves to a truth value.Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that >>>>>>>>> it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not
contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>> that it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not
contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>> that it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not
contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>>> that it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G)) >>>>>>> to a truth value true. When doing so it evaluated each side of = >>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated >>>>>> subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that >>>>>> wherever an occurs check might be applicable the built-in predicate >>>>>> unify_with_occurs_check/2 is used explicitly instead of the normal >>>>>> unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable. >>>>>> END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
Not true. Prolog also has term expressions that can be used in facts
and rules. In particular, in the goal G = not(provable(F, G)) the
symbol G is a term expression and provable(F, G) is another term
expression. A goal is evaluated to a truth value but if that truth
value is true the values of variables (if there are any) are also
evalueted to values that are not truth values. In the example
?- G = not(provable(F, G)).
the answer
G = not(provable(F, G)).
mans that the Prolog implementation evaluated the query to true and
the variable G to the expression not(provable(F, G)). The quoted
text says that another Prolog implementation may interprethe the
same query differently.
The quoted text does not stay unify_with_occurs_check/2 would reject
anything as "semntically unsound". First of all, it nas no consequences unless it is used. Secondly, if the result of unification would be
that at a cycle be created then it simpy evaluates to false just
like unify_with_occurs_check(1, 2) evaluates to false.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,090 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 158:12:41 |
| Calls: | 13,922 |
| Files: | 187,021 |
| D/L today: |
221 files (58,560K bytes) |
| Messages: | 2,457,273 |