XPost: comp.theory, sci.logic, sci.math
From: 643-408-1753@kylheku.com
On 2025-11-19, olcott wrote:
> On 11/19/2025 12:51 PM, Tristan Wibberley wrote:
>> On 19/11/2025 01:36, olcott wrote:
>>> On 11/18/2025 7:03 PM, Tristan Wibberley wrote:
>>>> On 17/11/2025 22:59, olcott wrote:
>>>>> On 11/17/2025 4:45 PM, Tristan Wibberley wrote:
>>>>>> On 17/11/2025 22:15, Alan Mackenzie wrote:
>>>>>>
>>>>>>> There is no proper academic conversation to be had over 2 + 2 = 4.
>>>>>>> It is
>>>>>>> firm, unassailable knowledge, unchallengeable. The Halting Theorem
>>>>>>> is of
>>>>>>> the same status, proven using the same methodology from the same
>>>>>>> fundamentals.
>>>>>>
>>>>>>
>>>>>> It's a completely different league from 2 + 2 = 4.
>>>>>> It's closer to x = 1/2 + x/2 but it's still conceptually /much/ harder
>>>>>> than that.
>>>>>> It's more like the problem of whether a fixed point exists or not, but
>>>>>> it's for the fixed point of a limit of a particular, conceptually
>>>>>> weird,
>>>>>> sequence of functions.
>>>>>>
>>>>>> It really is quite peculiar.
>>>>>>
>>>>>
>>>>> Ultimately it is essentially the Liar Paradox in disguise.
>>>>>
>>>>> The Liar Paradox formalized in the Prolog Programming language
>>>>>
>>>>> This sentence is not true.
>>>>> It is not true about what?
>>>>> It is not true about being not true.
>>>>> It is not true about being not true about what?
>>>>> It is not true about being not true about being not true.
>>>>> Oh I see you are stuck in a loop!
>>>>>
>>>>> This is formalized in the Prolog programming language below.
>>>>>
>>>>> ?- LP = not(true(LP)).
>>>>> LP = not(true(LP)).
>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>> false.
>>>>
>>>> true/0
>>>> use \+/1 rather than not/1
>>>>
>>>>
>>>>> Failing an occurs check seems to mean that the
>>>>> resolution of an expression remains stuck in an
>>>> ^^^^^^^^^^
>>>>> infinite loop.
>>>>
>>>> You mean "judgement" ?
>>>
>>> I mean like this thingy:
>>>
>>> void Infinite_Loop()
>>> {
>>> HERE: goto HERE;
>>> return;
>>> }
>>
>> Ah the terminological problem of what to call something like a
>> "normalisation" process when it might be that no normal form exists.
>>
>> In the pure functional world your C characterisation is typically called
>> "a computation" but I'm not sure where the boundary lies or whether you
>> really mean "judgement" or "evaluation". In the C world "evaluation" of
>> "Infinite_Loop()" is a real thing that exists, even if the expression
>> has no value or any normal form in any conventionally reasonable
>> formalisation and the mapping of your original terms to Infinite_Loop is
>> just one choice for how to judge.
>>
>
> When you fully understand every nuance of my terms
> then you understand that when the directed graph
> of the evaluation sequence of a formal expression
> contains a cycle that this proves that this expression
> is semantically unsound because the evaluation of
> this expression does have an actual infinite loop
> just like this one.
Your three pages full of nothng, titled Minimal Type Theory,
don't contain anything original.
Programming language expression trees are directed graphs
already.
Long before you wrote that, it was possible to write the
Liar Paradox using Lisp, whose data notation supports a way of
introducing cycles into the graph:
#1=(not #1#)
That little expression is all it takes to show that the
self reference is not evaluatable.
Furthermore, in Lisp, we can readily model the equivalent
of "This sentence of has five words"; we can translate
it to a three-element expression which says "this expression
has three elements":
#1=(eql 3 (length '#1#)) ;; yields T
#1# refers back to the entire expression '#1# means (quote #1#):
it quotes it, creating an expression referring to the syntax
itself, rather than its value. (This is significant.)
Then length is applied to that syntax itself, producing 3,
which is EQL to 3, resulting in true.
Showing it more formally in Lisp this way shows the reason
that a paradox is avoided here. The key is that we had to
use the quote operator.
When a sentence talks about itself quoted, it is different
than when the sentence refers to its value.
A sentence could refer to the value of its quoted self with EVAL; then
that would be back to the liar paradox, like this:
#1=(not (eval '#1#))
But when the sentence grasps itself quoted, it doesn't have to evaluate.
Examining certain properties of itself other than its value does not
lead to infinite regress; for instance the number of terms in the
expression can be safely counted with LENGTH.
---
By the way, on a related note: under the CLISP implementation of
Common Lisp (and perhaps others) we can use STEP to simulate the
Liar paradox step by step and see the backtrace. CLISP's
implementation of STEP does not perform a full macro-expanson;
it expands incrementally so it is able to get into it:
We turn on printing of the Circle Notation, so we can print
the self-referential code:
[1]> (setf *print-circle* t)
T
Validate that printing it is now possible without stack overflow/reset:
[2]> (quote #1=(not #1#))
#1=(NOT #1#)
Now begin stepping:
[3]> (step #1=(not #1#))
step 1 --> #1=(NOT #1#)
Step 1 [4]> :s
step 2 --> #1=(NOT #1#)
Step 2 [5]> :s
step 3 --> #1=(NOT #1#)
Show the backtrace at this point: 14 frames are printed
Step 3 [6]> :bt
<1/214> # 3
<2/207> #
<3/201> #
<4/192> # 2
<5/189> #
<6/185> # 2
<7/171> #
<8/169> #
<9/135> #
[128] EVAL frame for form #1=(NOT #1#)
[124] EVAL frame for form #1=(NOT #1#)
<10/114> #
<11/100> #
[93] EVAL frame for form #1=(NOT #1#)
[89] EVAL frame for form #1=(NOT #1#)
<12/79> #
<13/65> #
[58] EVAL frame for form #1=(NOT #1#)
<14/39> #
[37] EVAL frame for form (LET* ((SYSTEM::*STEP-LEVEL* 0) (SYST
M::*STEP-QUIT* MOST-POSITIVE-FIXNUM) (SYSTEM::*STEP-WATCH* NIL) (*EVALHOOK*
#'SYSTEM::STEP-HOOK-FN)) #1=(NOT #1#))
Printed 14 frames
Step one more:
Step 3 [6]> :s
step 4 --> #1=(NOT #1#)
Backtrace again, now there are 16 frames:
Step 4 [7]> :bt
<1/249> # 3
[continued in next message]
--- SoupGate-Win32 v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
