Sujet : Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT
De : polcott333 (at) *nospam* gmail.com (olcott)
Groupes : sci.logic comp.theoryDate : 29. May 2024, 15:00:44
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <v37ced$15rjf$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
User-Agent : Mozilla Thunderbird
On 5/29/2024 6:31 AM, Richard Damon wrote:
On 5/28/24 11:54 PM, olcott wrote:
On 5/28/2024 10:38 PM, Richard Damon wrote:
On 5/28/24 10:39 PM, olcott wrote:
On 5/28/2024 9:04 PM, Richard Damon wrote:
On 5/28/24 10:59 AM, olcott wrote:
On 5/28/2024 1:59 AM, Mikko wrote:
On 2024-05-27 14:34:14 +0000, olcott said:
>
?- LP = not(true(LP)).
LP = not(true(LP)).
>
?- unify_with_occurs_check(LP, not(true(LP))).
false.
>
In other words Prolog has detected a cycle in the directed graph of the
evaluation sequence of the structure of the Liar Paradox. Experts seem
to think that Prolog is taking "not" and "true" as meaningless and is
only evaluating the structure of the expression.
>
The words "not" and "true" of Prolog are meaningful in some contexts
but not above. The word "true" is meaningful only when it has no arguments.
>
>
That Prolog construes any expression having the same structure as the
Liar Paradox as having a cycle in the directed graph of its evaluation
sequence already completely proves my point. In other words Prolog
is saying that there is something wrong with the expression and it must
be rejected.
>
But Prolog doesn't support powerful enough logic to handle the system like Tarski and Godel are talking about.
>
The fact that Prolog just rejects it shows that.
>
>
Your ignorance is no excuse.
>
What ignorance?
>
>
The fact that you assert that you know the underlying details of
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
without even glancing at the documentation and write-up in Clocksin and
Mellish seems to be willful ignorance.
What makes you think that? I understand how Prolog works, and why it only models relatively simple logic systems, because it just can't handle the higher order logical primitives. It can't even handle full first order logic.
Your explanation of
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2was ridiculous.
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 tills 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.
-- Copyright 2024 Olcott "Talent hits a target no one else can hit; Geniushits a target no one else can see." Arthur Schopenhauer