Deutsch English Français Italiano |
<v8hsr2$m6t2$1@solani.org> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!feeds.phibee-telecom.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock <janburse@fastmail.fm> Newsgroups: comp.lang.prolog Subject: A Challenge for Fixpoint Lovers (Was: Biene Maya) Date: Fri, 2 Aug 2024 08:03:14 +0200 Message-ID: <v8hsr2$m6t2$1@solani.org> References: <v8gc6e$l44p$1@solani.org> <v8gg7a$liqo$1@solani.org> <v8gr23$lcke$1@solani.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 2 Aug 2024 06:03:14 -0000 (UTC) Injection-Info: solani.org; logging-data="727970"; mail-complaints-to="abuse@news.solani.org" User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.18.2 Cancel-Lock: sha1:qcJn4cdDf2qQsJxxnuf4VHZzLBU= In-Reply-To: <v8gr23$lcke$1@solani.org> X-User-ID: eJwFwQkBACAIA8BKyrNhHBDpH8E7V2xcGhzm4xNCMV/KLS9gzAydWuppJXOSVdXMI1XrOAXB6S15X8Pa7gcyvhVf Bytes: 5269 Lines: 138 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? >> >