From Newsgroup: comp.lang.prolog
On 12/15/2025 3:04 AM, Mikko wrote:
On 15/12/2025 01:14, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
On 12/13/2025 4:19 AM, Mikko wrote:
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:
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: >>>>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
-a-a?- G = not(provable(F, G)).
and
-a-a?- 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(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 rCLinfinite termrCY 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 >>>>>>>> -a>> 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. >>>>>>>
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.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
In other words you admit you were lying about me.
I have no idea what you are referring to.
--
Copyright 2025 Olcott<br><br>
My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable.<br><br>
This required establishing a new foundation<br>
--- Synchronet 3.21b-Linux NewsLink 1.2