A Challenge for Fixpoint Lovers (Was: Biene Maya)

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?

>