Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.prolog > #15174
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Newsgroups | comp.lang.prolog, comp.theory, sci.logic, sci.math |
| Subject | Re: A new foundation for correct reasoning |
| Followup-To | comp.lang.prolog |
| Date | 2025-12-16 11:44 +0200 |
| Organization | A noiseless patient Spider |
| Message-ID | <10hr9m8$2i2de$1@dont-email.me> (permalink) |
| References | (26 earlier) <10hju2h$4hat$1@dont-email.me> <10hm25a$tpc7$1@dont-email.me> <10hngct$1gbn9$1@dont-email.me> <10hoive$1p2m3$2@dont-email.me> <10hp4eo$1uh6i$2@dont-email.me> |
Cross-posted to 4 groups.
Followups directed to: comp.lang.prolog
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. >>>>>>>>>>> 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 >>>>>>> derivation is to a truth value. >>>>>> >>>>> >>>>> You just don't seem to understand: >>>>> ?- G = not(provable(F, G)). >>>>> G = not(provable(F, G)). >>>>> ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>> false. >>>>> >>>>> The first statement creates a cyclic term, also called >>>>> a rational tree. The second executes logically sound >>>>> unification and thus fails. >>>>> https://www.swi-prolog.org/pldoc/man? >>>>> predicate=unify_with_occurs_check/2 >>>> >>>> Saying the same as I said does not support a claim of non- >>>> understanding. >>> >>> It finally resolves the Liar Paradox >>> as not a truth bearer or proposition. >> >> In other words you admit you were lying about me. > > I have no idea what you are referring to. It makes as much sense as "in other words" in your messages. -- Mikko
Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-05 11:43 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-06 11:30 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-06 06:50 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-07 13:02 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-08 13:49 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-08 11:13 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-08 13:09 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-10 12:04 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-10 08:10 -0600
Re: A new foundation for correct reasoning Python <python@cccp.invalid> - 2025-12-10 15:01 +0000
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-10 18:10 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-10 14:01 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-11 10:42 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-11 08:17 -0600
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-11 23:28 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-11 17:49 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-11 19:52 -0500
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-12 10:50 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-12 08:19 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-12 09:24 -0500
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-14 19:03 +0000
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-13 12:19 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-13 08:43 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-13 13:36 -0500
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-14 12:05 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 17:14 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 19:13 -0500
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 18:46 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 19:53 -0500
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 19:08 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 20:46 -0500
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 20:05 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 21:23 -0500
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 20:09 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 21:27 -0500
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 21:22 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-15 07:33 -0500
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-15 11:04 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-15 08:03 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-16 11:44 +0200
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-16 11:48 +0200
csiph-web