René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Feedback from Yves Bertot","articleBody":"\"  - In QED-at-large, you seem to state that Isabelle/HOL does not\r\nsupport partial functions.  In a recent assignment where I tried to\r\nunderstand the support of inductive predicates in both HOL based and\r\ntype-theory-based provers, I noted some work by Krauss \"Partial and\r\nNested Recursive Function Definitions in Higher-order Logic\" which\r\ncontradicts this assertion.  Here is a very short summary:\r\n\r\n   * you can describe a recursive function, potentially non-terminating,\r\nas a function that returns an arbitrary value when not terminating.\r\n\r\n   * All theorems about the behavior of this function are prefixed by\r\nthe condition that the input must be in the domain of definition.\r\n\r\n  * The domain definition itself can be described as an inductive predicate.\r\n\r\n  * In practice, the function is first described as an inductive\r\nrelation: R_f(x, y) that holds exactly when f(x) terminates and f(x) =\r\ny.  The HOL logic in Isabelle contains the \"Hilbert\" choice operator,\r\nwhich makes it possible to construct the final value f(x) from the\r\nrelation R_f.\r\n\r\nIt is probably too late to correct the paper, but it is useful to know\r\nthat Isabelle has a powerful tool to handle potentially non-terminating\r\nrecursive functions in a comfortable way (in some sense, it is more\r\ncomfortable that what is available in plain Coq, because you can write\r\nf(x) even before you have proved that recursion terminates on x).\"","author":{"url":"https://github.com/tlringer","@type":"Person","name":"tlringer"},"datePublished":"2020-09-25T16:59:03.000Z","interactionStatistic":{"@type":"InteractionCounter","interactionType":"https://schema.org/CommentAction","userInteractionCount":0},"url":"https://github.com/8/proofengineering.github.io/issues/8"}