XPost: comp.lang.prolog, comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   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   
   >>>>>>>>>>>>>>>>>>>   ?- 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(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)   
   >>>>>>>>>>   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)