Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #14127

A Challenge for Fixpoint Lovers (Was: Biene Maya)

Show all headers | View raw

Here is a challenge that might appeal
to all fixpoint lovers and non-classical
logic lovers. Althought I expect them

to be a rather rare species. Take the
Clark completion and the 3-valued semantics.
Then this logic program:

foo(n)
foo(s(X)) :- foo(X).

bar(n).
bar(s(X)) :- bar(X).
bar(w) :- \+ (foo(X), \+ bar(X)).

Here the quizz that makes up the challenge:

- Whats the least fixpoint of bar/1,
   giving bar a domain that makes
   bar bivalent?

- Does bar/1 have finite derivations, i.e.
   terminates, for each element taken
   from that domain?

Have Fun!

The exercise is inspired by this quote and paper:

"The finite stages (JnP)n<w have a computational meaning."
The theoretical foundations of LPTP
Robert F. Stärk - 1998
https://www.sciencedirect.com/science/article/pii/S0743106697100139

Mild Shock schrieb:
> 
> Karel Gott - Rot und schwarz
> https://www.youtube.com/watch?v=R3qAGDchWWM
> 
> So whats the fallacy in Robert Staerks modality?
> It has to do with the difference between computation
> and derivation, don't confuse the two!
> 
> What also helps nowadays, don't take a philosopher
> on board who is totally clueless about non-classical
> logics. I don't want to say names, but being that
> 
> ignorant is quite a feat. So how did Robert Staerk
> start? Well he possibly had first the problem
> that this here simple logic program:
> 
> p :- \+ p.
> 
> when classically translated is unsatisfiable, and
> therefore in classical logic, leads to Ex Falso
> Quodlibet. So they went with non-classical logic,
> 
> but a cheap one, i.e. 3-valued logic, so that
> we have these two modalities:
> 
> p_s : p succeeds
> p_f : p fails
> 
> The fallacy is now to think a total computable
> function is the same as BIVALENCE, expressed here,
> using the further modality in the game:
> 
> p_t -> p_s v p_f
> 
> non-constructive logics would immediately see
> that p_s v p_f is problematic, since the above
> intoduces a disjunction, without a disjunction
> 
> property. Now there is possibly the surprise
> with this overall fixpoint juggling we might
> have derivations that say p_t, but not in this sense:
> 
> p_t : p terminates
> 
> Just try an example with a non-continous fixpoint
> operator, derived from a Clark completion. I don't
> see in the slides that it is excluded?
> 
> Might even try to provide a concrete example myself...
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Although the work itself might be solid work.
>> the appeal to fixpoints should already ring a
>> bell. What I wish from a logic framework and
>>
>> what would attract me is:
>> - includes the concept of a model finder,
>>    to show things unprovable.
>> - indeally a model finder, that can also
>>    find functions as counter models.
>> - allows to express things in non-classical
>>    logic and can make good use of non-classical logic.
>> - allows to express things in constructive
>>    function spaces and can make good use of constructive function spaces.
>>
>> Currently with fixpoints and classical logic,
>> the approach is not enough advanced, doesn't
>> utilize what type theory could offer.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> I remember Robert Stärk's disappearing from
>>> academic life at ETH Zurich all of a sudden.
>>> Did Ulrich Neumerkel now also disappeared not
>>>
>>> because the Scryer Prolog disaster, but after
>>> he figured out that failure slices are not hip
>>> enought? What could be more hip, are the modalities
>>>
>>> of Robert Stärk's logic more hip now and even useful?
>>>
>>> Automated Theorem Proving for Prolog Verification
>>> Fred Mesnard etc.. May 2024
>>> https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf 
>>>
>>>
>>> Disclaimer: I am not deep into this theory,
>>> it has some ingredients that were floating around
>>> the 80's / 80's, not only in the millieau of ETH Zurich,
>>>
>>> but also in the vincinity of Gehard Jaeger, Bern.
>>> There are many alternative formalizations that
>>> can express termination etc.. But maybe LPTP is
>>>
>>> especially suited for Prolog?
>>
> 

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:13 +0200
  Alan Kay's Dynabook fueled by Prolog? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:20 +0200
    ZebralLogic for evaluating LLMs (Was: Alan Kay's Dynabook fueled by Prolog?) Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:24 +0200
  Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-01 19:21 +0200
    Biene Maya (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-01 22:26 +0200
      A Challenge for Fixpoint Lovers (Was: Biene Maya) Mild Shock <janburse@fastmail.fm> - 2024-08-02 08:03 +0200
  Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-09 14:42 +0200
    Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 12:25 +0200
      Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 12:59 +0200
        Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:03 +0200
          Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:14 +0200
            Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:19 +0200
              Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:32 +0200
                Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:41 +0200
                Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:46 +0200
    The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:03 +0200
      Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:05 +0200
        Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:19 +0200
          Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 14:03 +0200
    How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-13 15:48 +0200
      Re: How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-13 15:49 +0200
  Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-13 09:08 +0200

csiph-web