Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.prolog > #12766 > unrolled thread
| Started by | olcott <NoOne@NoWhere.com> |
|---|---|
| First post | 2022-04-30 02:02 -0500 |
| Last post | 2022-05-01 11:21 -0600 |
| Articles | 20 on this page of 173 — 11 participants |
Back to article view | Back to comp.lang.prolog
Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 02:02 -0500
Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-04-30 12:31 +0300
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-04-30 20:15 +0200
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 16:08 -0500
Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:26 +0300
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:00 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 13:49 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 08:09 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 15:35 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 08:55 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 16:28 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 10:24 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 17:44 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 11:04 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 18:38 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 11:49 -0500
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 09:51 -0700
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 19:38 +0200
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 11:04 -0700
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:22 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:14 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:24 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 21:43 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 15:10 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 22:37 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 15:58 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 16:30 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 23:33 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 16:42 -0500
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-03 00:13 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:35 -0500
Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-02 11:28 -0600
Re: Is this correct Prolog? Mr Flibble <flibble@reddwarf.jmc> - 2022-05-02 19:41 +0100
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:26 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:32 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 18:28 -0400
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-03 00:41 +0200
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 16:00 -0700
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-03 01:39 +0200
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 17:26 -0700
Re: Is this correct Prolog? Ben <ben.usenet@bsb.me.uk> - 2022-05-03 00:43 +0100
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 17:20 -0700
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:57 -0500
Re: Is this correct Prolog? Ben <ben.usenet@bsb.me.uk> - 2022-05-03 03:21 +0100
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 22:01 -0500
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-03 01:18 -0700
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-03 08:05 -0400
Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-04 21:30 -0500
Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-04 22:46 -0400
Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-04 22:02 -0500
Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-05 07:41 -0400
Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-05 12:57 -0500
Re: Is this correct Prolog? [ Tarski ] André G. Isaak <agisaak@gm.invalid> - 2022-05-05 12:06 -0600
Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-05 16:23 -0500
Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-05 22:24 -0400
Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-05 21:37 -0500
Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-06 07:43 -0400
Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-06 15:29 -0500
Re: Is this correct Prolog? Ben <ben.usenet@bsb.me.uk> - 2022-05-03 15:59 +0100
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 09:18 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 11:08 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 10:52 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 12:05 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 11:17 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 12:33 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 12:23 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 13:59 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 14:03 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 22:24 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 21:54 -0600
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-04 07:27 -0400
Re: Is this correct Prolog? [ André didn't lie after all ] olcott <polcott2@gmail.com> - 2022-05-03 12:08 -0500
Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-03 12:33 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 14:12 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 13:22 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 21:53 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-03 23:12 -0400
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 22:53 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 22:06 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-04 01:17 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-04 08:02 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-04 14:01 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-04 19:48 -0400
Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-03 15:58 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 17:13 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:11 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:35 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 20:47 -0400
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 07:59 -0700
Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 17:15 +0200
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 10:45 -0500
Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 09:02 -0700
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 11:26 -0500
Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:24 +0300
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 05:58 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 07:12 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:45 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:07 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 07:15 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:49 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 15:48 -0500
Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:38 +0300
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:06 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 07:26 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:54 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:11 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 07:19 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 14:00 -0400
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 21:08 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 20:42 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 22:00 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 21:21 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 22:38 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 21:56 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 23:11 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 22:15 -0500
Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-04-30 23:24 -0600
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:35 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:16 -0400
Re: Is this correct Prolog? Mr Flibble <flibble@reddwarf.jmc> - 2022-05-01 13:19 +0100
Re: Is this correct Prolog? polcott <polcott2@gmail.com> - 2022-05-01 07:51 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:19 -0400
Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-01 11:22 -0600
Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:45 +0300
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:28 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:01 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 07:09 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:16 -0400
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 07:18 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:50 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:26 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 20:47 -0500
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 23:49 -0500
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 11:08 -0500
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 13:28 -0500
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 14:00 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 15:19 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 14:32 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 13:44 -0600
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 14:48 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 16:01 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 15:42 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 14:51 -0600
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 17:04 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 18:08 -0400
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 17:39 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 19:18 -0400
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 17:26 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 19:58 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 21:32 -0400
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 20:53 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 22:14 -0400
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 21:18 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 20:37 -0600
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 22:47 -0400
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 22:04 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 22:10 -0600
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 07:10 -0400
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 08:19 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 18:38 -0400
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 16:37 -0600
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 17:44 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 17:15 -0600
Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <NoOne@NoWhere.com> - 2022-05-01 18:33 -0500
Re: Is this correct Prolog? [ André is proven to be a liar ] André G. Isaak <agisaak@gm.invalid> - 2022-05-01 17:44 -0600
Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <NoOne@NoWhere.com> - 2022-05-01 18:53 -0500
Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <polcott2@gmail.com> - 2022-05-01 18:15 -0500
Re: Is this correct Prolog? [ André is proven to be a liar ] Richard Damon <Richard@Damon-Family.org> - 2022-05-01 19:21 -0400
Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <polcott2@gmail.com> - 2022-05-01 19:56 -0500
Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 17:05 -0500
Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 16:55 -0400
Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 11:57 -0500
Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 11:21 -0600
Page 6 of 9 — ← Prev page 1 2 3 4 5 [6] 7 8 9 Next page →
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-04-30 15:48 -0500 |
| Message-ID | <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #12767 |
On 4/30/2022 4:31 AM, Mikko wrote: > On 2022-04-30 07:02:23 +0000, olcott said: > >> LP := ~True(LP) is translated to Prolog: >> >> ?- LP = not(true(LP)). >> LP = not(true(LP)). > > This is correct but to fail would also be correct. > >> ?- unify_with_occurs_check(LP, not(true(LP))). >> false. > > unify_with_occurs_check must fail if the unified data structure > would contain loops. > > Mikko > The above is the actual execution of actual Prolog code using (SWI-Prolog (threaded, 64 bits, version 7.6.4). According to Clocksin & Mellish it is not a mere loop, it is an "infinite term" thus infinitely recursive definition. I am trying to validate whether or not my Prolog code encodes the Liar Paradox. I believe that it does and it also shows exactly how the Liar Paradox is erroneous. From all of my analysis and research this expression correctly formalizes the Liar Paradox: LP := ~True(LP) -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2022-05-01 12:38 +0300 |
| Message-ID | <t4lkei$acm$1@dont-email.me> |
| In reply to | #12773 |
On 2022-04-30 20:48:47 +0000, olcott said: > On 4/30/2022 4:31 AM, Mikko wrote: >> On 2022-04-30 07:02:23 +0000, olcott said: >> >>> LP := ~True(LP) is translated to Prolog: >>> >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >> >> This is correct but to fail would also be correct. >> >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >> >> unify_with_occurs_check must fail if the unified data structure >> would contain loops. >> >> Mikko >> > > The above is the actual execution of actual Prolog code using > (SWI-Prolog (threaded, 64 bits, version 7.6.4). Another Prolog implementation might interprete LP = not(true(LP)) differently and still conform to the prolog standard. > According to Clocksin & Mellish it is not a mere loop, it is an > "infinite term" thus infinitely recursive definition. When discussing data structures, "infinite" and "loop" mean the same. The data structure is infinitely deep but contains only finitely many distinct objects and occupies only a finite amount of memory. > I am trying to validate whether or not my Prolog code encodes the Liar Paradox. That cannot be inferred from Prolog rules. Prolog defines some encodings like how to encode numbers with characters of Prolog character set but for more complex things you must make your own encoding rules. Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-05-01 06:06 -0500 |
| Message-ID | <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com> |
| In reply to | #12788 |
On 5/1/2022 4:38 AM, Mikko wrote: > On 2022-04-30 20:48:47 +0000, olcott said: > >> On 4/30/2022 4:31 AM, Mikko wrote: >>> On 2022-04-30 07:02:23 +0000, olcott said: >>> >>>> LP := ~True(LP) is translated to Prolog: >>>> >>>> ?- LP = not(true(LP)). >>>> LP = not(true(LP)). >>> >>> This is correct but to fail would also be correct. >>> >>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>> false. >>> >>> unify_with_occurs_check must fail if the unified data structure >>> would contain loops. >>> >>> Mikko >>> >> >> The above is the actual execution of actual Prolog code using >> (SWI-Prolog (threaded, 64 bits, version 7.6.4). > > Another Prolog implementation might interprete LP = not(true(LP)) > differently > and still conform to the prolog standard. > >> According to Clocksin & Mellish it is not a mere loop, it is an >> "infinite term" thus infinitely recursive definition. > > When discussing data structures, "infinite" and "loop" mean the same. > The data structure is infinitely deep but contains only finitely many > distinct objects and occupies only a finite amount of memory. > That is incorrect. any structure that is infinitely deep would take all of the memory that is available yet specifies an infinite amount of memory. >> I am trying to validate whether or not my Prolog code encodes the Liar >> Paradox. > > That cannot be inferred from Prolog rules. Prolog defines some encodings > like how to encode numbers with characters of Prolog character set but for > more complex things you must make your own encoding rules. > > Mikko > This says that G is logically equivalent to its own unprovability in F G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-05-01 07:26 -0400 |
| Message-ID | <u7ubK.20174$HLy4.14606@fx38.iad> |
| In reply to | #12792 |
On 5/1/22 7:06 AM, olcott wrote: > On 5/1/2022 4:38 AM, Mikko wrote: >> On 2022-04-30 20:48:47 +0000, olcott said: >> >>> On 4/30/2022 4:31 AM, Mikko wrote: >>>> On 2022-04-30 07:02:23 +0000, olcott said: >>>> >>>>> LP := ~True(LP) is translated to Prolog: >>>>> >>>>> ?- LP = not(true(LP)). >>>>> LP = not(true(LP)). >>>> >>>> This is correct but to fail would also be correct. >>>> >>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>> false. >>>> >>>> unify_with_occurs_check must fail if the unified data structure >>>> would contain loops. >>>> >>>> Mikko >>>> >>> >>> The above is the actual execution of actual Prolog code using >>> (SWI-Prolog (threaded, 64 bits, version 7.6.4). >> >> Another Prolog implementation might interprete LP = not(true(LP)) >> differently >> and still conform to the prolog standard. >> >>> According to Clocksin & Mellish it is not a mere loop, it is an >>> "infinite term" thus infinitely recursive definition. >> >> When discussing data structures, "infinite" and "loop" mean the same. >> The data structure is infinitely deep but contains only finitely many >> distinct objects and occupies only a finite amount of memory. >> > > That is incorrect. any structure that is infinitely deep would take all > of the memory that is available yet specifies an infinite amount of memory. Nope, a tree that one branch points into itself higher up represents a tree with infinite depth, but only needs a finite amount of memory. Building such a structure may require the ability to forward declare something or reference something not yet defined. Some infinities have finite representation. You don't seem able to understand that. Yes, some naive ways of expanding them fail, but the answer to that is you just don't do that, but need to use a less naive method. > >>> I am trying to validate whether or not my Prolog code encodes the >>> Liar Paradox. >> >> That cannot be inferred from Prolog rules. Prolog defines some encodings >> like how to encode numbers with characters of Prolog character set but >> for >> more complex things you must make your own encoding rules. >> >> Mikko >> > > This says that G is logically equivalent to its own unprovability in F > G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog. > >
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-05-01 06:54 -0500 |
| Message-ID | <i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #12795 |
On 5/1/2022 6:26 AM, Richard Damon wrote: > On 5/1/22 7:06 AM, olcott wrote: >> On 5/1/2022 4:38 AM, Mikko wrote: >>> On 2022-04-30 20:48:47 +0000, olcott said: >>> >>>> On 4/30/2022 4:31 AM, Mikko wrote: >>>>> On 2022-04-30 07:02:23 +0000, olcott said: >>>>> >>>>>> LP := ~True(LP) is translated to Prolog: >>>>>> >>>>>> ?- LP = not(true(LP)). >>>>>> LP = not(true(LP)). >>>>> >>>>> This is correct but to fail would also be correct. >>>>> >>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>> false. >>>>> >>>>> unify_with_occurs_check must fail if the unified data structure >>>>> would contain loops. >>>>> >>>>> Mikko >>>>> >>>> >>>> The above is the actual execution of actual Prolog code using >>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4). >>> >>> Another Prolog implementation might interprete LP = not(true(LP)) >>> differently >>> and still conform to the prolog standard. >>> >>>> According to Clocksin & Mellish it is not a mere loop, it is an >>>> "infinite term" thus infinitely recursive definition. >>> >>> When discussing data structures, "infinite" and "loop" mean the same. >>> The data structure is infinitely deep but contains only finitely many >>> distinct objects and occupies only a finite amount of memory. >>> >> >> That is incorrect. any structure that is infinitely deep would take >> all of the memory that is available yet specifies an infinite amount >> of memory. > > Nope, a tree that one branch points into itself higher up represents a > tree with infinite depth, but only needs a finite amount of memory. > Building such a structure may require the ability to forward declare > something or reference something not yet defined. > That is counter-factual. unify_with_occurs_check determines that it would require infinite memory and then aborts its evaluation. foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) "..." indicates infinite depth, thus infinite string length. > Some infinities have finite representation. You don't seem able to > understand that. > > Yes, some naive ways of expanding them fail, but the answer to that is > you just don't do that, but need to use a less naive method. > > >> >>>> I am trying to validate whether or not my Prolog code encodes the >>>> Liar Paradox. >>> >>> That cannot be inferred from Prolog rules. Prolog defines some encodings >>> like how to encode numbers with characters of Prolog character set >>> but for >>> more complex things you must make your own encoding rules. >>> >>> Mikko >>> >> >> This says that G is logically equivalent to its own unprovability in F >> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog. >> >> > -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-05-01 08:11 -0400 |
| Message-ID | <9OubK.452731$iK66.239461@fx46.iad> |
| In reply to | #12800 |
On 5/1/22 7:54 AM, olcott wrote: > On 5/1/2022 6:26 AM, Richard Damon wrote: >> On 5/1/22 7:06 AM, olcott wrote: >>> On 5/1/2022 4:38 AM, Mikko wrote: >>>> On 2022-04-30 20:48:47 +0000, olcott said: >>>> >>>>> On 4/30/2022 4:31 AM, Mikko wrote: >>>>>> On 2022-04-30 07:02:23 +0000, olcott said: >>>>>> >>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>> >>>>>>> ?- LP = not(true(LP)). >>>>>>> LP = not(true(LP)). >>>>>> >>>>>> This is correct but to fail would also be correct. >>>>>> >>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>> false. >>>>>> >>>>>> unify_with_occurs_check must fail if the unified data structure >>>>>> would contain loops. >>>>>> >>>>>> Mikko >>>>>> >>>>> >>>>> The above is the actual execution of actual Prolog code using >>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4). >>>> >>>> Another Prolog implementation might interprete LP = not(true(LP)) >>>> differently >>>> and still conform to the prolog standard. >>>> >>>>> According to Clocksin & Mellish it is not a mere loop, it is an >>>>> "infinite term" thus infinitely recursive definition. >>>> >>>> When discussing data structures, "infinite" and "loop" mean the same. >>>> The data structure is infinitely deep but contains only finitely many >>>> distinct objects and occupies only a finite amount of memory. >>>> >>> >>> That is incorrect. any structure that is infinitely deep would take >>> all of the memory that is available yet specifies an infinite amount >>> of memory. >> >> Nope, a tree that one branch points into itself higher up represents a >> tree with infinite depth, but only needs a finite amount of memory. >> Building such a structure may require the ability to forward declare >> something or reference something not yet defined. >> > > That is counter-factual. unify_with_occurs_check determines that it > would require infinite memory and then aborts its evaluation. You misunderstand what it says. It says that it can't figure how to express the statement without a cycle. That is different then taking infinite memory. It only possibly implies infinite memory in a naive expansion, which isn't the only method. As was pointed out, the recursive factorial definition, if naively expanded, becomes unbounded in size, but the recursive factorial definition, to a logic system that understands recursion, is usable and has meaning. So all you have shown is that these forms CAN cause failure to some forms of naive logic. You are just stuck in your own false thinking, and have convinced youself of a lie. > > foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) > "..." indicates infinite depth, thus infinite string length. > >> Some infinities have finite representation. You don't seem able to >> understand that. >> >> Yes, some naive ways of expanding them fail, but the answer to that is >> you just don't do that, but need to use a less naive method. >> > >> >>> >>>>> I am trying to validate whether or not my Prolog code encodes the >>>>> Liar Paradox. >>>> >>>> That cannot be inferred from Prolog rules. Prolog defines some >>>> encodings >>>> like how to encode numbers with characters of Prolog character set >>>> but for >>>> more complex things you must make your own encoding rules. >>>> >>>> Mikko >>>> >>> >>> This says that G is logically equivalent to its own unprovability in F >>> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog. >>> >>> >> > >
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-05-01 07:19 -0500 |
| Message-ID | <rsqdnZ_T5YtG5_P_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #12804 |
On 5/1/2022 7:11 AM, Richard Damon wrote: > On 5/1/22 7:54 AM, olcott wrote: >> On 5/1/2022 6:26 AM, Richard Damon wrote: >>> On 5/1/22 7:06 AM, olcott wrote: >>>> On 5/1/2022 4:38 AM, Mikko wrote: >>>>> On 2022-04-30 20:48:47 +0000, olcott said: >>>>> >>>>>> On 4/30/2022 4:31 AM, Mikko wrote: >>>>>>> On 2022-04-30 07:02:23 +0000, olcott said: >>>>>>> >>>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>>> >>>>>>>> ?- LP = not(true(LP)). >>>>>>>> LP = not(true(LP)). >>>>>>> >>>>>>> This is correct but to fail would also be correct. >>>>>>> >>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>> false. >>>>>>> >>>>>>> unify_with_occurs_check must fail if the unified data structure >>>>>>> would contain loops. >>>>>>> >>>>>>> Mikko >>>>>>> >>>>>> >>>>>> The above is the actual execution of actual Prolog code using >>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4). >>>>> >>>>> Another Prolog implementation might interprete LP = not(true(LP)) >>>>> differently >>>>> and still conform to the prolog standard. >>>>> >>>>>> According to Clocksin & Mellish it is not a mere loop, it is an >>>>>> "infinite term" thus infinitely recursive definition. >>>>> >>>>> When discussing data structures, "infinite" and "loop" mean the same. >>>>> The data structure is infinitely deep but contains only finitely many >>>>> distinct objects and occupies only a finite amount of memory. >>>>> >>>> >>>> That is incorrect. any structure that is infinitely deep would take >>>> all of the memory that is available yet specifies an infinite amount >>>> of memory. >>> >>> Nope, a tree that one branch points into itself higher up represents >>> a tree with infinite depth, but only needs a finite amount of memory. >>> Building such a structure may require the ability to forward declare >>> something or reference something not yet defined. >>> >> >> That is counter-factual. unify_with_occurs_check determines that it >> would require infinite memory and then aborts its evaluation. > > You misunderstand what it says. It says that it can't figure how to > express the statement without a cycle. The expression inherently has an infinite cycle, making it erroneous. > That is different then taking > infinite memory. It only possibly implies infinite memory in a naive > expansion, which isn't the only method. > > As was pointed out, the recursive factorial definition, if naively > expanded, becomes unbounded in size, but the recursive factorial > definition, to a logic system that understands recursion, is usable and > has meaning. > Does not have an infinite cycle. It always begins with a finite integer that specifies the finite number of cycles. > So all you have shown is that these forms CAN cause failure to some > forms of naive logic. > An infinite cycle is the same thing as an infinite loop inherently incorrect. > You are just stuck in your own false thinking, and have convinced > youself of a lie. > You are simply ignoring key details. You are pretending that a finite thing is an infinite thing. > >> >> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) >> "..." indicates infinite depth, thus infinite string length. >> >>> Some infinities have finite representation. You don't seem able to >>> understand that. >>> >>> Yes, some naive ways of expanding them fail, but the answer to that >>> is you just don't do that, but need to use a less naive method. >>> >> >>> >>>> >>>>>> I am trying to validate whether or not my Prolog code encodes the >>>>>> Liar Paradox. >>>>> >>>>> That cannot be inferred from Prolog rules. Prolog defines some >>>>> encodings >>>>> like how to encode numbers with characters of Prolog character set >>>>> but for >>>>> more complex things you must make your own encoding rules. >>>>> >>>>> Mikko >>>>> >>>> >>>> This says that G is logically equivalent to its own unprovability in F >>>> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog. >>>> >>>> >>> >> >> > -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-05-01 14:00 -0400 |
| Message-ID | <lVzbK.816079$oF2.372227@fx10.iad> |
| In reply to | #12807 |
On 5/1/22 8:19 AM, olcott wrote: > On 5/1/2022 7:11 AM, Richard Damon wrote: >> On 5/1/22 7:54 AM, olcott wrote: >>> On 5/1/2022 6:26 AM, Richard Damon wrote: >>>> On 5/1/22 7:06 AM, olcott wrote: >>>>> On 5/1/2022 4:38 AM, Mikko wrote: >>>>>> On 2022-04-30 20:48:47 +0000, olcott said: >>>>>> >>>>>>> On 4/30/2022 4:31 AM, Mikko wrote: >>>>>>>> On 2022-04-30 07:02:23 +0000, olcott said: >>>>>>>> >>>>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>>>> >>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>> LP = not(true(LP)). >>>>>>>> >>>>>>>> This is correct but to fail would also be correct. >>>>>>>> >>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>> false. >>>>>>>> >>>>>>>> unify_with_occurs_check must fail if the unified data structure >>>>>>>> would contain loops. >>>>>>>> >>>>>>>> Mikko >>>>>>>> >>>>>>> >>>>>>> The above is the actual execution of actual Prolog code using >>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4). >>>>>> >>>>>> Another Prolog implementation might interprete LP = not(true(LP)) >>>>>> differently >>>>>> and still conform to the prolog standard. >>>>>> >>>>>>> According to Clocksin & Mellish it is not a mere loop, it is an >>>>>>> "infinite term" thus infinitely recursive definition. >>>>>> >>>>>> When discussing data structures, "infinite" and "loop" mean the same. >>>>>> The data structure is infinitely deep but contains only finitely many >>>>>> distinct objects and occupies only a finite amount of memory. >>>>>> >>>>> >>>>> That is incorrect. any structure that is infinitely deep would take >>>>> all of the memory that is available yet specifies an infinite >>>>> amount of memory. >>>> >>>> Nope, a tree that one branch points into itself higher up represents >>>> a tree with infinite depth, but only needs a finite amount of >>>> memory. Building such a structure may require the ability to forward >>>> declare something or reference something not yet defined. >>>> >>> >>> That is counter-factual. unify_with_occurs_check determines that it >>> would require infinite memory and then aborts its evaluation. >> >> You misunderstand what it says. It says that it can't figure how to >> express the statement without a cycle. > > The expression inherently has an infinite cycle, making it erroneous. Maybe it just says that PROLOG can't express the statement without an infinite cycle due to the limitiations in Prologs logic system? Better logic systems can handle and work with statements that are self-referential or recursive. Your reliance on Prolog just limits the fields you can discuss. Like I think Prolog isn't able to express all the properties of the Natural Numbers, which means that it BY DEFINITION isn't capable of handling a full incompleteness prooof. > >> That is different then taking infinite memory. It only possibly >> implies infinite memory in a naive expansion, which isn't the only >> method. >> >> As was pointed out, the recursive factorial definition, if naively >> expanded, becomes unbounded in size, but the recursive factorial >> definition, to a logic system that understands recursion, is usable >> and has meaning. >> > > Does not have an infinite cycle. It always begins with a finite integer > that specifies the finite number of cycles. Nope. I can write Fact(n), where n is an unknow integer and do logic with it. Just like H(H^,H^) has a finite expansion if H will answer the question, and thus does not have infinite recursion, and thus H^(H^) does not either as it is a finite extension of the expansion of H(H^,H^). Only your failure to inplement that limit makes it infinite, which just proves that such an H never answers. > >> So all you have shown is that these forms CAN cause failure to some >> forms of naive logic. >> > > An infinite cycle is the same thing as an infinite loop inherently > incorrect. > Yes, but a finite loop can expand infinitely if not done correctly or naively. The fact that one method expanse something infinitely doesn't mean the expression is in fact an infinte loop. >> You are just stuck in your own false thinking, and have convinced >> youself of a lie. >> > > You are simply ignoring key details. You are pretending that a finite > thing is an infinite thing. Yes, any expansion of fact for a KNOWN n will be finite, but if n is not known, generates what appears to be an infinite expansion that will colapse to finite once a value is known. Tell me how many cycles your logic is going to expand fact, and I will give you an n that it didn't handle. > >> >>> >>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) >>> "..." indicates infinite depth, thus infinite string length. >>> >>>> Some infinities have finite representation. You don't seem able to >>>> understand that. >>>> >>>> Yes, some naive ways of expanding them fail, but the answer to that >>>> is you just don't do that, but need to use a less naive method. >>>> >>> >>>> >>>>> >>>>>>> I am trying to validate whether or not my Prolog code encodes the >>>>>>> Liar Paradox. >>>>>> >>>>>> That cannot be inferred from Prolog rules. Prolog defines some >>>>>> encodings >>>>>> like how to encode numbers with characters of Prolog character set >>>>>> but for >>>>>> more complex things you must make your own encoding rules. >>>>>> >>>>>> Mikko >>>>>> >>>>> >>>>> This says that G is logically equivalent to its own unprovability in F >>>>> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog. >>>>> >>>>> >>>> >>> >>> >> > >
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-04-30 21:08 -0400 |
| Message-ID | <I4lbK.452483$t2Bb.96330@fx98.iad> |
| In reply to | #12766 |
On 4/30/22 3:02 AM, olcott wrote: > LP := ~True(LP) is translated to Prolog: > > ?- LP = not(true(LP)). > LP = not(true(LP)). > > ?- unify_with_occurs_check(LP, not(true(LP))). > false. > > (SWI-Prolog (threaded, 64 bits, version 7.6.4) > > https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence > > > Since it isn't giving you a "syntax error", it is probably correct Prolog. Not sure if your interpretation of the results is correct. All that false means is that the statement LP = not(true(LP)) is recursive and that Prolog can't actually evaluate it due to its limited logic rules. I will condition this answer on the fact that I am not a prolog specialist, but just reading the manual and providing basic understanding, which I am not sure of your ability to do so.
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-04-30 20:42 -0500 |
| Message-ID | <3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #12775 |
On 4/30/2022 8:08 PM, Richard Damon wrote: > On 4/30/22 3:02 AM, olcott wrote: >> LP := ~True(LP) is translated to Prolog: >> >> ?- LP = not(true(LP)). >> LP = not(true(LP)). >> >> ?- unify_with_occurs_check(LP, not(true(LP))). >> false. >> >> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >> >> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >> >> >> > > Since it isn't giving you a "syntax error", it is probably correct > Prolog. Not sure if your interpretation of the results is correct. > > All that false means is that the statement > > > LP = not(true(LP)) > > is recursive and that Prolog can't actually evaluate it due to its > limited logic rules. > That is not what Clocksin & Mellish says. They say it is an erroneous "infinite term" meaning that it specifies infinitely nested definition like this: LP := ~True(LP) specifies: ~True(~True(~True(L~True(L~True(...)) The ellipses "..." mean "on and on forever" One half a page of the Clocksin & Mellish text is quoted on page (3) of my paper: https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence > I will condition this answer on the fact that I am not a prolog > specialist, but just reading the manual and providing basic > understanding, which I am not sure of your ability to do so. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-04-30 22:00 -0400 |
| Message-ID | <AQlbK.11129$lX6b.2320@fx33.iad> |
| In reply to | #12776 |
On 4/30/22 9:42 PM, olcott wrote: > On 4/30/2022 8:08 PM, Richard Damon wrote: >> On 4/30/22 3:02 AM, olcott wrote: >>> LP := ~True(LP) is translated to Prolog: >>> >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >>> >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >>> >>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>> >>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>> >>> >>> >> >> Since it isn't giving you a "syntax error", it is probably correct >> Prolog. Not sure if your interpretation of the results is correct. >> >> All that false means is that the statement >> >> >> LP = not(true(LP)) >> >> is recursive and that Prolog can't actually evaluate it due to its >> limited logic rules. >> > > That is not what Clocksin & Mellish says. They say it is an erroneous > "infinite term" meaning that it specifies infinitely nested definition > like this: No, that IS what they say, that this sort of recursion fails the test of Unification, not that it is has no possible logical meaning. Prolog represents a somewhat basic form of logic, useful for many cases, but not encompassing all possible reasoning systems. Maybe it can handle every one that YOU can understand, but it can't handle many higher order logical structures. Note, for instance, at least some ways of writing factorial for an unknown value can lead to an infinite expansion, but the factorial is well defined for all positive integers. The fact that a "prolog like" expansion operator might not be able to handle the definition, doesn't mean it doesn't have meaning. > > LP := ~True(LP) specifies: > ~True(~True(~True(L~True(L~True(...)) > The ellipses "..." mean "on and on forever" > > One half a page of the Clocksin & Mellish text is quoted on page (3) of > my paper: > > https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence > > >> I will condition this answer on the fact that I am not a prolog >> specialist, but just reading the manual and providing basic >> understanding, which I am not sure of your ability to do so. > >
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-04-30 21:21 -0500 |
| Message-ID | <39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com> |
| In reply to | #12778 |
On 4/30/2022 9:00 PM, Richard Damon wrote: > On 4/30/22 9:42 PM, olcott wrote: >> On 4/30/2022 8:08 PM, Richard Damon wrote: >>> On 4/30/22 3:02 AM, olcott wrote: >>>> LP := ~True(LP) is translated to Prolog: >>>> >>>> ?- LP = not(true(LP)). >>>> LP = not(true(LP)). >>>> >>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>> false. >>>> >>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>> >>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>> >>>> >>>> >>> >>> Since it isn't giving you a "syntax error", it is probably correct >>> Prolog. Not sure if your interpretation of the results is correct. >>> >>> All that false means is that the statement >>> >>> >>> LP = not(true(LP)) >>> >>> is recursive and that Prolog can't actually evaluate it due to its >>> limited logic rules. >>> >> >> That is not what Clocksin & Mellish says. They say it is an erroneous >> "infinite term" meaning that it specifies infinitely nested definition >> like this: > > No, that IS what they say, that this sort of recursion fails the test of > Unification, not that it is has no possible logical meaning. > > Prolog represents a somewhat basic form of logic, useful for many cases, > but not encompassing all possible reasoning systems. > > Maybe it can handle every one that YOU can understand, but it can't > handle many higher order logical structures. > > Note, for instance, at least some ways of writing factorial for an > unknown value can lead to an infinite expansion, but the factorial is > well defined for all positive integers. The fact that a "prolog like" > expansion operator might not be able to handle the definition, doesn't > mean it doesn't have meaning. > It is really dumb that you continue to take wild guesses again the verified facts. Please read the Clocksin & Mellish (on page 3 of my paper) text and eliminate your ignorance. >> >> LP := ~True(LP) specifies: >> ~True(~True(~True(L~True(L~True(...)) >> The ellipses "..." mean "on and on forever" >> >> One half a page of the Clocksin & Mellish text is quoted on page (3) >> of my paper: >> >> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >> >> >>> I will condition this answer on the fact that I am not a prolog >>> specialist, but just reading the manual and providing basic >>> understanding, which I am not sure of your ability to do so. >> >> > -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-04-30 22:38 -0400 |
| Message-ID | <uombK.379436$Gojc.287190@fx99.iad> |
| In reply to | #12779 |
On 4/30/22 10:21 PM, olcott wrote: > On 4/30/2022 9:00 PM, Richard Damon wrote: >> On 4/30/22 9:42 PM, olcott wrote: >>> On 4/30/2022 8:08 PM, Richard Damon wrote: >>>> On 4/30/22 3:02 AM, olcott wrote: >>>>> LP := ~True(LP) is translated to Prolog: >>>>> >>>>> ?- LP = not(true(LP)). >>>>> LP = not(true(LP)). >>>>> >>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>> false. >>>>> >>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>>> >>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>>> >>>>> >>>>> >>>> >>>> Since it isn't giving you a "syntax error", it is probably correct >>>> Prolog. Not sure if your interpretation of the results is correct. >>>> >>>> All that false means is that the statement >>>> >>>> >>>> LP = not(true(LP)) >>>> >>>> is recursive and that Prolog can't actually evaluate it due to its >>>> limited logic rules. >>>> >>> >>> That is not what Clocksin & Mellish says. They say it is an erroneous >>> "infinite term" meaning that it specifies infinitely nested >>> definition like this: >> >> No, that IS what they say, that this sort of recursion fails the test >> of Unification, not that it is has no possible logical meaning. >> >> Prolog represents a somewhat basic form of logic, useful for many >> cases, but not encompassing all possible reasoning systems. >> >> Maybe it can handle every one that YOU can understand, but it can't >> handle many higher order logical structures. >> >> Note, for instance, at least some ways of writing factorial for an >> unknown value can lead to an infinite expansion, but the factorial is >> well defined for all positive integers. The fact that a "prolog like" >> expansion operator might not be able to handle the definition, doesn't >> mean it doesn't have meaning. >> > > It is really dumb that you continue to take wild guesses again the > verified facts. > > Please read the Clocksin & Mellish (on page 3 of my paper) text and > eliminate your ignorance. > I did. You just don't seem to understand what I am saying because it is above your head. Prolog is NOT the defining authority for what is a valid logical statement, but a system of programming to handle a subset of those statements (a useful subset, but a subset). The fact that Prolog doesn't allow something doesn't mean it doesn't have a logical meaning, only that it doesn't have a logical meaning in Prolog. The inability of Prolog to "Unify" the expression, does not mean the expression doesn't have logical meaning, just that PROLOG can't derive meaning from the expression. The Halting Problem and the incompleteness proofs never claims that they is designed for the subset of logic that is Prolog, and in fact they may be implicitly denying that, as I don't think Prolog handles enough complexity of logic to reach the threshold needed to express "G" in Godel's proof. (Your need to "simplify" it, is indicative of this, and shows you don't understand the actual proof). This means that the fact that Prolog rejects unification of the statements doesn't actually say that much, just that the statement isn't of the type that Prolog can fully process.
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-04-30 21:56 -0500 |
| Message-ID | <pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com> |
| In reply to | #12780 |
On 4/30/2022 9:38 PM, Richard Damon wrote: > On 4/30/22 10:21 PM, olcott wrote: >> On 4/30/2022 9:00 PM, Richard Damon wrote: >>> On 4/30/22 9:42 PM, olcott wrote: >>>> On 4/30/2022 8:08 PM, Richard Damon wrote: >>>>> On 4/30/22 3:02 AM, olcott wrote: >>>>>> LP := ~True(LP) is translated to Prolog: >>>>>> >>>>>> ?- LP = not(true(LP)). >>>>>> LP = not(true(LP)). >>>>>> >>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>> false. >>>>>> >>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>>>> >>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>>>> >>>>>> >>>>>> >>>>> >>>>> Since it isn't giving you a "syntax error", it is probably correct >>>>> Prolog. Not sure if your interpretation of the results is correct. >>>>> >>>>> All that false means is that the statement >>>>> >>>>> >>>>> LP = not(true(LP)) >>>>> >>>>> is recursive and that Prolog can't actually evaluate it due to its >>>>> limited logic rules. >>>>> >>>> >>>> That is not what Clocksin & Mellish says. They say it is an >>>> erroneous "infinite term" meaning that it specifies infinitely >>>> nested definition like this: >>> >>> No, that IS what they say, that this sort of recursion fails the test >>> of Unification, not that it is has no possible logical meaning. >>> >>> Prolog represents a somewhat basic form of logic, useful for many >>> cases, but not encompassing all possible reasoning systems. >>> >>> Maybe it can handle every one that YOU can understand, but it can't >>> handle many higher order logical structures. >>> >>> Note, for instance, at least some ways of writing factorial for an >>> unknown value can lead to an infinite expansion, but the factorial is >>> well defined for all positive integers. The fact that a "prolog like" >>> expansion operator might not be able to handle the definition, >>> doesn't mean it doesn't have meaning. >>> >> >> It is really dumb that you continue to take wild guesses again the >> verified facts. >> >> Please read the Clocksin & Mellish (on page 3 of my paper) text and >> eliminate your ignorance. >> > > I did. You just don't seem to understand what I am saying because it is > above your head. > > Prolog is NOT the defining authority for what is a valid logical > statement, but a system of programming to handle a subset of those > statements (a useful subset, but a subset). > > The fact that Prolog doesn't allow something doesn't mean it doesn't > have a logical meaning, only that it doesn't have a logical meaning in > Prolog. In this case it does. I have spent thousands of hours on the semantic error of infinitely recursive definition and written a dozen papers on it. Glancing at one of two of the words of Clocksin & Mellish does not count as reading it. 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. END:(Clocksin & Mellish 2003:254) foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))))) -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-04-30 23:11 -0400 |
| Message-ID | <VTmbK.655548$mF2.416033@fx11.iad> |
| In reply to | #12781 |
On 4/30/22 10:56 PM, olcott wrote: > On 4/30/2022 9:38 PM, Richard Damon wrote: >> On 4/30/22 10:21 PM, olcott wrote: >>> On 4/30/2022 9:00 PM, Richard Damon wrote: >>>> On 4/30/22 9:42 PM, olcott wrote: >>>>> On 4/30/2022 8:08 PM, Richard Damon wrote: >>>>>> On 4/30/22 3:02 AM, olcott wrote: >>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>> >>>>>>> ?- LP = not(true(LP)). >>>>>>> LP = not(true(LP)). >>>>>>> >>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>> false. >>>>>>> >>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>>>>> >>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> Since it isn't giving you a "syntax error", it is probably correct >>>>>> Prolog. Not sure if your interpretation of the results is correct. >>>>>> >>>>>> All that false means is that the statement >>>>>> >>>>>> >>>>>> LP = not(true(LP)) >>>>>> >>>>>> is recursive and that Prolog can't actually evaluate it due to its >>>>>> limited logic rules. >>>>>> >>>>> >>>>> That is not what Clocksin & Mellish says. They say it is an >>>>> erroneous "infinite term" meaning that it specifies infinitely >>>>> nested definition like this: >>>> >>>> No, that IS what they say, that this sort of recursion fails the >>>> test of Unification, not that it is has no possible logical meaning. >>>> >>>> Prolog represents a somewhat basic form of logic, useful for many >>>> cases, but not encompassing all possible reasoning systems. >>>> >>>> Maybe it can handle every one that YOU can understand, but it can't >>>> handle many higher order logical structures. >>>> >>>> Note, for instance, at least some ways of writing factorial for an >>>> unknown value can lead to an infinite expansion, but the factorial >>>> is well defined for all positive integers. The fact that a "prolog >>>> like" expansion operator might not be able to handle the definition, >>>> doesn't mean it doesn't have meaning. >>>> >>> >>> It is really dumb that you continue to take wild guesses again the >>> verified facts. >>> >>> Please read the Clocksin & Mellish (on page 3 of my paper) text and >>> eliminate your ignorance. >>> >> >> I did. You just don't seem to understand what I am saying because it >> is above your head. >> >> Prolog is NOT the defining authority for what is a valid logical >> statement, but a system of programming to handle a subset of those >> statements (a useful subset, but a subset). >> >> The fact that Prolog doesn't allow something doesn't mean it doesn't >> have a logical meaning, only that it doesn't have a logical meaning in >> Prolog. > In this case it does. I have spent thousands of hours on the semantic > error of infinitely recursive definition and written a dozen papers on > it. Glancing at one of two of the words of Clocksin & Mellish does not > count as reading it. And it appears that you don't understand it, because you still make category errors when trying to talk about it. > > 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. > END:(Clocksin & Mellish 2003:254) > > foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))))) > Right. but some infinite structures might actually have meaning. The fact that Prolog uses certain limited method to figure out meaning doesn't mean that other methods can't find the meaning. Just like: Fact(n) := (N == 1) ? 1 : N*Fact(n-1); if naively expanded has an infinite expansion. But, based on mathematical knowledge, and can actually be proven from the definition, something like Fact(n+1)/fact(n), even for an unknown n, can be reduced without the need to actually expend infinite operations. Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't abort its simulation, then for THAT H^, we have that H^(H^) is non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a counter example When you program H to abort its simulation of H^ at some point, and build your H^ on that H, then H(H^,H^), will return the non-halting answer, and H^(H^) when PROPERLY run or simulated halts, because H has the same "cut off" logic at the factorial above. The naive expansion thinks it is infinite, but the correct expansion sees the cut off and sees that it is actually finite.
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-04-30 22:15 -0500 |
| Message-ID | <Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> |
| In reply to | #12782 |
On 4/30/2022 10:11 PM, Richard Damon wrote: > On 4/30/22 10:56 PM, olcott wrote: >> On 4/30/2022 9:38 PM, Richard Damon wrote: >>> On 4/30/22 10:21 PM, olcott wrote: >>>> On 4/30/2022 9:00 PM, Richard Damon wrote: >>>>> On 4/30/22 9:42 PM, olcott wrote: >>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote: >>>>>>> On 4/30/22 3:02 AM, olcott wrote: >>>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>>> >>>>>>>> ?- LP = not(true(LP)). >>>>>>>> LP = not(true(LP)). >>>>>>>> >>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>> false. >>>>>>>> >>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>>>>>> >>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> Since it isn't giving you a "syntax error", it is probably >>>>>>> correct Prolog. Not sure if your interpretation of the results is >>>>>>> correct. >>>>>>> >>>>>>> All that false means is that the statement >>>>>>> >>>>>>> >>>>>>> LP = not(true(LP)) >>>>>>> >>>>>>> is recursive and that Prolog can't actually evaluate it due to >>>>>>> its limited logic rules. >>>>>>> >>>>>> >>>>>> That is not what Clocksin & Mellish says. They say it is an >>>>>> erroneous "infinite term" meaning that it specifies infinitely >>>>>> nested definition like this: >>>>> >>>>> No, that IS what they say, that this sort of recursion fails the >>>>> test of Unification, not that it is has no possible logical meaning. >>>>> >>>>> Prolog represents a somewhat basic form of logic, useful for many >>>>> cases, but not encompassing all possible reasoning systems. >>>>> >>>>> Maybe it can handle every one that YOU can understand, but it can't >>>>> handle many higher order logical structures. >>>>> >>>>> Note, for instance, at least some ways of writing factorial for an >>>>> unknown value can lead to an infinite expansion, but the factorial >>>>> is well defined for all positive integers. The fact that a "prolog >>>>> like" expansion operator might not be able to handle the >>>>> definition, doesn't mean it doesn't have meaning. >>>>> >>>> >>>> It is really dumb that you continue to take wild guesses again the >>>> verified facts. >>>> >>>> Please read the Clocksin & Mellish (on page 3 of my paper) text and >>>> eliminate your ignorance. >>>> >>> >>> I did. You just don't seem to understand what I am saying because it >>> is above your head. >>> >>> Prolog is NOT the defining authority for what is a valid logical >>> statement, but a system of programming to handle a subset of those >>> statements (a useful subset, but a subset). >>> >>> The fact that Prolog doesn't allow something doesn't mean it doesn't >>> have a logical meaning, only that it doesn't have a logical meaning >>> in Prolog. >> In this case it does. I have spent thousands of hours on the semantic >> error of infinitely recursive definition and written a dozen papers on >> it. Glancing at one of two of the words of Clocksin & Mellish does not >> count as reading it. > > And it appears that you don't understand it, because you still make > category errors when trying to talk about it. > >> >> 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. >> END:(Clocksin & Mellish 2003:254) >> >> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))))) >> > > Right. but some infinite structures might actually have meaning. Not in this case, it is very obvious that no theorem prover can possibly prove any infinite expression. It is the same thing as a program that is stuck in an infinite loop. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Jeff Barnett <jbb@notatt.com> |
|---|---|
| Date | 2022-04-30 23:24 -0600 |
| Message-ID | <t4l5hq$8bi$1@dont-email.me> |
| In reply to | #12783 |
On 4/30/2022 9:15 PM, olcott wrote:
> On 4/30/2022 10:11 PM, Richard Damon wrote:
>> On 4/30/22 10:56 PM, olcott wrote:
>>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>>> On 4/30/22 10:21 PM, olcott wrote:
>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>
>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>
>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>> false.
>>>>>>>>>
>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>
>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>
>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>> is correct.
>>>>>>>>
>>>>>>>> All that false means is that the statement
>>>>>>>>
>>>>>>>>
>>>>>>>> LP = not(true(LP))
>>>>>>>>
>>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>>> its limited logic rules.
>>>>>>>>
>>>>>>>
>>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>>> nested definition like this:
>>>>>>
>>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>>
>>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>>
>>>>>> Maybe it can handle every one that YOU can understand, but it
>>>>>> can't handle many higher order logical structures.
>>>>>>
>>>>>> Note, for instance, at least some ways of writing factorial for an
>>>>>> unknown value can lead to an infinite expansion, but the factorial
>>>>>> is well defined for all positive integers. The fact that a "prolog
>>>>>> like" expansion operator might not be able to handle the
>>>>>> definition, doesn't mean it doesn't have meaning.
>>>>>>
>>>>>
>>>>> It is really dumb that you continue to take wild guesses again the
>>>>> verified facts.
>>>>>
>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text and
>>>>> eliminate your ignorance.
>>>>>
>>>>
>>>> I did. You just don't seem to understand what I am saying because it
>>>> is above your head.
>>>>
>>>> Prolog is NOT the defining authority for what is a valid logical
>>>> statement, but a system of programming to handle a subset of those
>>>> statements (a useful subset, but a subset).
>>>>
>>>> The fact that Prolog doesn't allow something doesn't mean it doesn't
>>>> have a logical meaning, only that it doesn't have a logical meaning
>>>> in Prolog.
>>> In this case it does. I have spent thousands of hours on the semantic
>>> error of infinitely recursive definition and written a dozen papers
>>> on it. Glancing at one of two of the words of Clocksin & Mellish does
>>> not count as reading it.
>>
>> And it appears that you don't understand it, because you still make
>> category errors when trying to talk about it.
>>
>>>
>>> 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.
>>> END:(Clocksin & Mellish 2003:254)
>>>
>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>>
>>
>> Right. but some infinite structures might actually have meaning.
> Not in this case, it is very obvious that no theorem prover can possibly
> prove any infinite expression. It is the same thing as a program that is
> stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
Just like:
Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
if naively expanded has an infinite expansion.
But, based on mathematical knowledge, and can actually be proven from
the definition, something like Fact(n+1)/fact(n), even for an unknown n,
can be reduced without the need to actually expend infinite operations.
Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't
abort its simulation, then for THAT H^, we have that H^(H^) is
non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a
counter example
When you program H to abort its simulation of H^ at some point, and
build your H^ on that H, then H(H^,H^), will return the non-halting
answer, and H^(H^) when PROPERLY run or simulated halts, because H has
the same "cut off" logic at the factorial above.
The naive expansion thinks it is infinite, but the correct expansion
sees the cut off and sees that it is actually finite.
----------------------------------------------------------------------
A good symbolic manipulation system or a theorem prover with appropriate
axioms and rules of inference could surely handle forms such as
Fact(n+1)/fact(n) without breathing hard. It is only you, an ignorant
fool, who seems to think that the unthinking infinite unrolling of a
form must occur. Only you would think that a solver system would
completely unroll a form before analyzing it and applying
transformations to it.
Son, it don't work that way (unless you are defining and making a mess
trying to write the system yourself). Systems usually have rules that
make small incremental transformations and usually search breadth first
with perhaps a limited amount of depth first interludes. If they don't
use a breadth first strategy, they will not be able to claim the
completeness property. (See resolution theorem prover literature for
some explanation. You wont understand it but you can cite as if you did!)
Richard was trying to explain this to you in the snipped portion I
recited just above. Question for Peter holding his pecker: How do you
always and I mean always manage to delete the part of a message you
respond too that addresses the point you now try to make?
A typically subsequence you might see in the trace: would include in
order but not necessarily consecutively:
Fact(n+1)/Fact(n)
(n+1)*Fact(n)/Fact(n)
(n+1)
Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found
too. In some circumstances, these other terms might be helpful. A
theorem prover or manipulator does all of this, breadth first, hoping to
blindly stumble on a solution. You can provide heuristics that might
speed up the process but no advice short of an oracle will get you even
one more result. (Another manifestation of HP.) It's the slow grinding
through the possibilities that guarantees that if a result can be found,
it will be found. And all the theory that you don't understand says
that's the best you can do.
Ben and I disagree on reasons for your type of total dishonesty. He
thinks that you are so self deluded that you actual believe what you are
saying; that you are so self deluded that the dishonest utterances are
just your subconscious protecting your already damaged ego. To that, I
say phooey; you are just a long term troll who lies a lot about math,
about your history and health, and about your accomplishments.
I don't believe that you will read this before you start to respond but
that's okay. Understanding is not required. Neither is respect in
either direction.
--
Jeff Barnett
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-05-01 06:35 -0500 |
| Message-ID | <_v2dnUiL-Yjh7fP_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #12785 |
On 5/1/2022 12:24 AM, Jeff Barnett wrote: > On 4/30/2022 9:15 PM, olcott wrote: >> On 4/30/2022 10:11 PM, Richard Damon wrote: >>> On 4/30/22 10:56 PM, olcott wrote: >>>> On 4/30/2022 9:38 PM, Richard Damon wrote: >>>>> On 4/30/22 10:21 PM, olcott wrote: >>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote: >>>>>>> On 4/30/22 9:42 PM, olcott wrote: >>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote: >>>>>>>>> On 4/30/22 3:02 AM, olcott wrote: >>>>>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>>>>> >>>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>>> LP = not(true(LP)). >>>>>>>>>> >>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>> false. >>>>>>>>>> >>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>>>>>>>> >>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> Since it isn't giving you a "syntax error", it is probably >>>>>>>>> correct Prolog. Not sure if your interpretation of the results >>>>>>>>> is correct. >>>>>>>>> >>>>>>>>> All that false means is that the statement >>>>>>>>> >>>>>>>>> >>>>>>>>> LP = not(true(LP)) >>>>>>>>> >>>>>>>>> is recursive and that Prolog can't actually evaluate it due to >>>>>>>>> its limited logic rules. >>>>>>>>> >>>>>>>> >>>>>>>> That is not what Clocksin & Mellish says. They say it is an >>>>>>>> erroneous "infinite term" meaning that it specifies infinitely >>>>>>>> nested definition like this: >>>>>>> >>>>>>> No, that IS what they say, that this sort of recursion fails the >>>>>>> test of Unification, not that it is has no possible logical meaning. >>>>>>> >>>>>>> Prolog represents a somewhat basic form of logic, useful for many >>>>>>> cases, but not encompassing all possible reasoning systems. >>>>>>> >>>>>>> Maybe it can handle every one that YOU can understand, but it >>>>>>> can't handle many higher order logical structures. >>>>>>> >>>>>>> Note, for instance, at least some ways of writing factorial for >>>>>>> an unknown value can lead to an infinite expansion, but the >>>>>>> factorial is well defined for all positive integers. The fact >>>>>>> that a "prolog like" expansion operator might not be able to >>>>>>> handle the definition, doesn't mean it doesn't have meaning. >>>>>>> >>>>>> >>>>>> It is really dumb that you continue to take wild guesses again the >>>>>> verified facts. >>>>>> >>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text >>>>>> and eliminate your ignorance. >>>>>> >>>>> >>>>> I did. You just don't seem to understand what I am saying because >>>>> it is above your head. >>>>> >>>>> Prolog is NOT the defining authority for what is a valid logical >>>>> statement, but a system of programming to handle a subset of those >>>>> statements (a useful subset, but a subset). >>>>> >>>>> The fact that Prolog doesn't allow something doesn't mean it >>>>> doesn't have a logical meaning, only that it doesn't have a logical >>>>> meaning in Prolog. >>>> In this case it does. I have spent thousands of hours on the >>>> semantic error of infinitely recursive definition and written a >>>> dozen papers on it. Glancing at one of two of the words of Clocksin >>>> & Mellish does not count as reading it. >>> >>> And it appears that you don't understand it, because you still make >>> category errors when trying to talk about it. >>> >>>> >>>> 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. >>>> END:(Clocksin & Mellish 2003:254) >>>> >>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))))) >>>> >>> >>> Right. but some infinite structures might actually have meaning. >> Not in this case, it is very obvious that no theorem prover can >> possibly prove any infinite expression. It is the same thing as a >> program that is stuck in an infinite loop. > > Richard wrote and the asshole (PO) snipped > ------------------------------------------ > Right. but some infinite structures might actually have meaning. The > fact that Prolog uses certain limited method to figure out meaning > doesn't mean that other methods can't find the meaning. > The question is not whether some infinite structures have meaning that is the dishonest dodge of the strawman error. The question is whether on not the expression at hand has meaning or is simply semantically incoherent. I just posted all of the Clocksin & Mellish text in my prior post to make this more clear. This example expanded from Clocksin & Mellish conclusively proves that some expressions of language are incorrect: foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) > Just like: > > Fact(n) := (N == 1) ? 1 : N*Fact(n-1); > > if naively expanded has an infinite expansion. > > But, based on mathematical knowledge, and can actually be proven from > the definition, something like Fact(n+1)/fact(n), even for an unknown n, > can be reduced without the need to actually expend infinite operations. > > Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't > abort its simulation, then for THAT H^, we have that H^(H^) is > non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a > counter example > > When you program H to abort its simulation of H^ at some point, and > build your H^ on that H, then H(H^,H^), will return the non-halting > answer, and H^(H^) when PROPERLY run or simulated halts, because H has > the same "cut off" logic at the factorial above. > > The naive expansion thinks it is infinite, but the correct expansion > sees the cut off and sees that it is actually finite. > ---------------------------------------------------------------------- > > A good symbolic manipulation system or a theorem prover with appropriate > axioms and rules of inference could surely handle forms such as > Fact(n+1)/fact(n) without breathing hard. It is only you, an ignorant > fool, who seems to think that the unthinking infinite unrolling of a > form must occur. Only you would think that a solver system would > completely unroll a form before analyzing it and applying > transformations to it. > > Son, it don't work that way (unless you are defining and making a mess > trying to write the system yourself). Systems usually have rules that > make small incremental transformations and usually search breadth first > with perhaps a limited amount of depth first interludes. If they don't > use a breadth first strategy, they will not be able to claim the > completeness property. (See resolution theorem prover literature for > some explanation. You wont understand it but you can cite as if you did!) > > Richard was trying to explain this to you in the snipped portion I > recited just above. Question for Peter holding his pecker: How do you > always and I mean always manage to delete the part of a message you > respond too that addresses the point you now try to make? > > A typically subsequence you might see in the trace: would include in > order but not necessarily consecutively: > Fact(n+1)/Fact(n) > (n+1)*Fact(n)/Fact(n) > (n+1) > Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found > too. In some circumstances, these other terms might be helpful. A > theorem prover or manipulator does all of this, breadth first, hoping to > blindly stumble on a solution. You can provide heuristics that might > speed up the process but no advice short of an oracle will get you even > one more result. (Another manifestation of HP.) It's the slow grinding > through the possibilities that guarantees that if a result can be found, > it will be found. And all the theory that you don't understand says > that's the best you can do. > > Ben and I disagree on reasons for your type of total dishonesty. He > thinks that you are so self deluded that you actual believe what you are > saying; that you are so self deluded that the dishonest utterances are > just your subconscious protecting your already damaged ego. To that, I > say phooey; you are just a long term troll who lies a lot about math, > about your history and health, and about your accomplishments. > > I don't believe that you will read this before you start to respond but > that's okay. Understanding is not required. Neither is respect in either > direction. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-05-01 13:16 -0400 |
| Message-ID | <tfzbK.388022$f2a5.287279@fx48.iad> |
| In reply to | #12797 |
On 5/1/22 7:35 AM, olcott wrote: > On 5/1/2022 12:24 AM, Jeff Barnett wrote: >> On 4/30/2022 9:15 PM, olcott wrote: >>> On 4/30/2022 10:11 PM, Richard Damon wrote: >>>> On 4/30/22 10:56 PM, olcott wrote: >>>>> On 4/30/2022 9:38 PM, Richard Damon wrote: >>>>>> On 4/30/22 10:21 PM, olcott wrote: >>>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote: >>>>>>>> On 4/30/22 9:42 PM, olcott wrote: >>>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote: >>>>>>>>>> On 4/30/22 3:02 AM, olcott wrote: >>>>>>>>>>> LP := ~True(LP) is translated to Prolog: >>>>>>>>>>> >>>>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>>>> LP = not(true(LP)). >>>>>>>>>>> >>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>> false. >>>>>>>>>>> >>>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) >>>>>>>>>>> >>>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Since it isn't giving you a "syntax error", it is probably >>>>>>>>>> correct Prolog. Not sure if your interpretation of the results >>>>>>>>>> is correct. >>>>>>>>>> >>>>>>>>>> All that false means is that the statement >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> LP = not(true(LP)) >>>>>>>>>> >>>>>>>>>> is recursive and that Prolog can't actually evaluate it due to >>>>>>>>>> its limited logic rules. >>>>>>>>>> >>>>>>>>> >>>>>>>>> That is not what Clocksin & Mellish says. They say it is an >>>>>>>>> erroneous "infinite term" meaning that it specifies infinitely >>>>>>>>> nested definition like this: >>>>>>>> >>>>>>>> No, that IS what they say, that this sort of recursion fails the >>>>>>>> test of Unification, not that it is has no possible logical >>>>>>>> meaning. >>>>>>>> >>>>>>>> Prolog represents a somewhat basic form of logic, useful for >>>>>>>> many cases, but not encompassing all possible reasoning systems. >>>>>>>> >>>>>>>> Maybe it can handle every one that YOU can understand, but it >>>>>>>> can't handle many higher order logical structures. >>>>>>>> >>>>>>>> Note, for instance, at least some ways of writing factorial for >>>>>>>> an unknown value can lead to an infinite expansion, but the >>>>>>>> factorial is well defined for all positive integers. The fact >>>>>>>> that a "prolog like" expansion operator might not be able to >>>>>>>> handle the definition, doesn't mean it doesn't have meaning. >>>>>>>> >>>>>>> >>>>>>> It is really dumb that you continue to take wild guesses again >>>>>>> the verified facts. >>>>>>> >>>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text >>>>>>> and eliminate your ignorance. >>>>>>> >>>>>> >>>>>> I did. You just don't seem to understand what I am saying because >>>>>> it is above your head. >>>>>> >>>>>> Prolog is NOT the defining authority for what is a valid logical >>>>>> statement, but a system of programming to handle a subset of those >>>>>> statements (a useful subset, but a subset). >>>>>> >>>>>> The fact that Prolog doesn't allow something doesn't mean it >>>>>> doesn't have a logical meaning, only that it doesn't have a >>>>>> logical meaning in Prolog. >>>>> In this case it does. I have spent thousands of hours on the >>>>> semantic error of infinitely recursive definition and written a >>>>> dozen papers on it. Glancing at one of two of the words of Clocksin >>>>> & Mellish does not count as reading it. >>>> >>>> And it appears that you don't understand it, because you still make >>>> category errors when trying to talk about it. >>>> >>>>> >>>>> 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. >>>>> END:(Clocksin & Mellish 2003:254) >>>>> >>>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))))) >>>>> >>>> >>>> Right. but some infinite structures might actually have meaning. >>> Not in this case, it is very obvious that no theorem prover can >>> possibly prove any infinite expression. It is the same thing as a >>> program that is stuck in an infinite loop. >> >> Richard wrote and the asshole (PO) snipped >> ------------------------------------------ >> Right. but some infinite structures might actually have meaning. The >> fact that Prolog uses certain limited method to figure out meaning >> doesn't mean that other methods can't find the meaning. >> > > The question is not whether some infinite structures have meaning that > is the dishonest dodge of the strawman error. > > The question is whether on not the expression at hand has meaning or is > simply semantically incoherent. I just posted all of the Clocksin & > Mellish text in my prior post to make this more clear. > > > This example expanded from Clocksin & Mellish conclusively proves that > some expressions of language are incorrect: > > foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) No, not "incorrect", just "can't be handled by Prolog". If foo is my fact() function, it is definitely "defined". > >> Just like: >> >> Fact(n) := (N == 1) ? 1 : N*Fact(n-1); >> >> if naively expanded has an infinite expansion. >> >> But, based on mathematical knowledge, and can actually be proven from >> the definition, something like Fact(n+1)/fact(n), even for an unknown >> n, can be reduced without the need to actually expend infinite >> operations. >> >> Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't >> abort its simulation, then for THAT H^, we have that H^(H^) is >> non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be >> a counter example >> >> When you program H to abort its simulation of H^ at some point, and >> build your H^ on that H, then H(H^,H^), will return the non-halting >> answer, and H^(H^) when PROPERLY run or simulated halts, because H has >> the same "cut off" logic at the factorial above. >> >> The naive expansion thinks it is infinite, but the correct expansion >> sees the cut off and sees that it is actually finite. >> ---------------------------------------------------------------------- >> >> A good symbolic manipulation system or a theorem prover with >> appropriate axioms and rules of inference could surely handle forms >> such as Fact(n+1)/fact(n) without breathing hard. It is only you, an >> ignorant fool, who seems to think that the unthinking infinite >> unrolling of a form must occur. Only you would think that a solver >> system would completely unroll a form before analyzing it and applying >> transformations to it. >> >> Son, it don't work that way (unless you are defining and making a mess >> trying to write the system yourself). Systems usually have rules that >> make small incremental transformations and usually search breadth >> first with perhaps a limited amount of depth first interludes. If they >> don't use a breadth first strategy, they will not be able to claim the >> completeness property. (See resolution theorem prover literature for >> some explanation. You wont understand it but you can cite as if you did!) >> >> Richard was trying to explain this to you in the snipped portion I >> recited just above. Question for Peter holding his pecker: How do you >> always and I mean always manage to delete the part of a message you >> respond too that addresses the point you now try to make? >> >> A typically subsequence you might see in the trace: would include in >> order but not necessarily consecutively: >> Fact(n+1)/Fact(n) >> (n+1)*Fact(n)/Fact(n) >> (n+1) >> Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found >> too. In some circumstances, these other terms might be helpful. A >> theorem prover or manipulator does all of this, breadth first, hoping >> to blindly stumble on a solution. You can provide heuristics that >> might speed up the process but no advice short of an oracle will get >> you even one more result. (Another manifestation of HP.) It's the slow >> grinding through the possibilities that guarantees that if a result >> can be found, it will be found. And all the theory that you don't >> understand says that's the best you can do. >> >> Ben and I disagree on reasons for your type of total dishonesty. He >> thinks that you are so self deluded that you actual believe what you >> are saying; that you are so self deluded that the dishonest utterances >> are just your subconscious protecting your already damaged ego. To >> that, I say phooey; you are just a long term troll who lies a lot >> about math, about your history and health, and about your >> accomplishments. >> >> I don't believe that you will read this before you start to respond >> but that's okay. Understanding is not required. Neither is respect in >> either direction. > >
[toc] | [prev] | [next] | [standalone]
| From | Mr Flibble <flibble@reddwarf.jmc> |
|---|---|
| Date | 2022-05-01 13:19 +0100 |
| Message-ID | <20220501131951.00000889@reddwarf.jmc> |
| In reply to | #12785 |
On Sat, 30 Apr 2022 23:24:05 -0600 Jeff Barnett <jbb@notatt.com> wrote: > On 4/30/2022 9:15 PM, olcott wrote: > > On 4/30/2022 10:11 PM, Richard Damon wrote: > >> On 4/30/22 10:56 PM, olcott wrote: > >>> On 4/30/2022 9:38 PM, Richard Damon wrote: > >>>> On 4/30/22 10:21 PM, olcott wrote: > >>>>> On 4/30/2022 9:00 PM, Richard Damon wrote: > >>>>>> On 4/30/22 9:42 PM, olcott wrote: > >>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote: > >>>>>>>> On 4/30/22 3:02 AM, olcott wrote: > >>>>>>>>> LP := ~True(LP) is translated to Prolog: > >>>>>>>>> > >>>>>>>>> ?- LP = not(true(LP)). > >>>>>>>>> LP = not(true(LP)). > >>>>>>>>> > >>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). > >>>>>>>>> false. > >>>>>>>>> > >>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4) > >>>>>>>>> > >>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence > >>>>>>>>> > >>>>>>>>> > >>>>>>>>> > >>>>>>>> > >>>>>>>> Since it isn't giving you a "syntax error", it is probably > >>>>>>>> correct Prolog. Not sure if your interpretation of the > >>>>>>>> results is correct. > >>>>>>>> > >>>>>>>> All that false means is that the statement > >>>>>>>> > >>>>>>>> > >>>>>>>> LP = not(true(LP)) > >>>>>>>> > >>>>>>>> is recursive and that Prolog can't actually evaluate it due > >>>>>>>> to its limited logic rules. > >>>>>>>> > >>>>>>> > >>>>>>> That is not what Clocksin & Mellish says. They say it is an > >>>>>>> erroneous "infinite term" meaning that it specifies > >>>>>>> infinitely nested definition like this: > >>>>>> > >>>>>> No, that IS what they say, that this sort of recursion fails > >>>>>> the test of Unification, not that it is has no possible > >>>>>> logical meaning. > >>>>>> > >>>>>> Prolog represents a somewhat basic form of logic, useful for > >>>>>> many cases, but not encompassing all possible reasoning > >>>>>> systems. > >>>>>> > >>>>>> Maybe it can handle every one that YOU can understand, but it > >>>>>> can't handle many higher order logical structures. > >>>>>> > >>>>>> Note, for instance, at least some ways of writing factorial > >>>>>> for an unknown value can lead to an infinite expansion, but > >>>>>> the factorial is well defined for all positive integers. The > >>>>>> fact that a "prolog like" expansion operator might not be able > >>>>>> to handle the definition, doesn't mean it doesn't have meaning. > >>>>>> > >>>>> > >>>>> It is really dumb that you continue to take wild guesses again > >>>>> the verified facts. > >>>>> > >>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text > >>>>> and eliminate your ignorance. > >>>>> > >>>> > >>>> I did. You just don't seem to understand what I am saying > >>>> because it is above your head. > >>>> > >>>> Prolog is NOT the defining authority for what is a valid logical > >>>> statement, but a system of programming to handle a subset of > >>>> those statements (a useful subset, but a subset). > >>>> > >>>> The fact that Prolog doesn't allow something doesn't mean it > >>>> doesn't have a logical meaning, only that it doesn't have a > >>>> logical meaning in Prolog. > >>> In this case it does. I have spent thousands of hours on the > >>> semantic error of infinitely recursive definition and written a > >>> dozen papers on it. Glancing at one of two of the words of > >>> Clocksin & Mellish does not count as reading it. > >> > >> And it appears that you don't understand it, because you still > >> make category errors when trying to talk about it. > >> > >>> > >>> 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. > >>> END:(Clocksin & Mellish 2003:254) > >>> > >>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))))) > >>> > >> > >> Right. but some infinite structures might actually have meaning. > > Not in this case, it is very obvious that no theorem prover can > > possibly prove any infinite expression. It is the same thing as a > > program that is stuck in an infinite loop. > > Richard wrote and the asshole (PO) snipped > ------------------------------------------ > Right. but some infinite structures might actually have meaning. The > fact that Prolog uses certain limited method to figure out meaning > doesn't mean that other methods can't find the meaning. > > Just like: > > Fact(n) := (N == 1) ? 1 : N*Fact(n-1); Are you mental? That definition isn't infinitely recursive as it terminates when N equals 1 given a set of constraints on N (positive integer greater or equal to 1). /Flibble
[toc] | [prev] | [next] | [standalone]
Page 6 of 9 — ← Prev page 1 2 3 4 5 [6] 7 8 9 Next page →
Back to top | Article view | comp.lang.prolog
csiph-web