XPost: comp.lang.prolog, comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   On 15/12/2025 16:03, olcott wrote:   
   > 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.   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)