Georgy Dunaev (Jul 09 2024 at 17:31): Georgy Dunaev (Jul 09 2024 at 17:31):Good day! I have the following idea of how it is possible to interpret Isabelle's theorems. Of course, most of the computable functions are ending with an exception, or stuck in a loop forever. But, IN PRINCIPLE, since "busy-beaver"-related ideas, Isabelle's metalogic is indeed an LCF for such functions. (If the function stucks in a loop, the it means that it's type is indeed "valid"). I would like to open the discussion of the following short program. Such semantic is both ridiculous and natural at the same time. It doesn't collapses notions of Formulas and Propositions just in bool, they indeed have different meaning.
The file : lcf.ML
It is related very much to Paulson's article https://arxiv.org/pdf/cs/9301105 , but it is different.
Mathias Fleury (Jul 09 2024 at 17:39):Isabelle already supports partial functions that are not required to terminate
partial_function (tailrec) f where
‹f n = f (Suc (Suc n))›
Mathias Fleury said:
Isabelle already supports partial functions that are not required to terminate
partial_function (tailrec) f where ‹f n = f (Suc (Suc n))›
Thanks for mentioning, but it is unrelated. (I am talking about a semantics for a metatheory.) But it is also nice, because it will allow to prove some statements about such semantics within ISabelle itself, if it will be desirable. (And many other things.)
Georgy Dunaev (Jul 09 2024 at 17:51):The reason behind is that I don't like the idea of "collapsing of interpretations", i.e. interpreting different symbols with the same set, e.g. i don't want to "collapse" (==> and -->), (/\ and "forall"), ("form"/"o" and "prop" as "bool"), ("i" and "term") .
Georgy Dunaev (Jul 09 2024 at 17:53):Also LCF means that there should be some computable functions. :) So I defined them. (within the boundaries of the compiler)
Last updated: Dec 21 2024 at 16:20 UTC