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