Email Gateway (Aug 19 2022 at 15:21): Email Gateway (Aug 19 2022 at 15:21):From: Gergely Buday <gbuday@gmail.com>
Hi,
I have found
partial_function (option)
collatz :: "nat ⇒ nat list option"
where
"collatz n =
(if n ≤ 1 then Some [n]
else if even n
then do { ns ← collatz (n div 2); Some (n # ns) }
else do { ns ← collatz (3 * n + 1); Some (n # ns)})"
in src/HOL/Ex/Fundefs.thy
Where can I find a description of such monadic definitions?
I did not find it in the Isar reference and what I have found was the
early history of it:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-May/msg00055.html
Email Gateway (Aug 19 2022 at 15:21):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Gergely,
Definitions of recursive functions in a monad with execptions (via partial_function) is
described in Alex Krauss' paper at PAR 2010 available from
http://www4.in.tum.de/~krauss/
Do-notation has been presented at the Isabelle Developer Workshop in 2010 by Christian
Sternagel. His slides are available at:
http://isabelle.in.tum.de/nominal/activities/idw10/idw.html
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:21):From: Christian Sternagel <c.sternagel@gmail.com>
Hi Gergely,
note that do-notation itself is just syntactic sugar (as, e.g., also in
Haskell). So actually there is nothing important about it ;), it just
makes some terms "easier" or maybe more concise to write down.
And maybe obvious, but I'll say it anyway: "partial_function" and
do-notation are completely orthogonal.
cheers
chris
Email Gateway (Aug 19 2022 at 15:21):From: Christian Sternagel <c.sternagel@gmail.com>
Sorry, I wanted to point at
http://isabelle.in.tum.de/website-Isabelle2014-RC3/dist/library/HOL/HOL-Library/Monad_Syntax.html
in my last email, but forgot it. There you can see the actual
translation (keyword "translations"), which tells you everything there
is to know about do-notation (using itself the more basic adhoc
overloading mechanism).
cheers
chris
Email Gateway (Aug 19 2022 at 15:22):From: Gergely Buday <gbuday@gmail.com>
Christian Sternagel wrote:
And maybe obvious, but I'll say it anyway: "partial_function" and
do-notation are completely orthogonal.
Now it is obvious :-)
Where can I find some description of the partial_function definition
mechanism? There is a page in the Isar reference manual but that is
not very much detailed.
Email Gateway (Aug 19 2022 at 15:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gergely,
As I wrote in my last post, Alex Krauss' paper about partial_function describes it.
Another application can be found in Johannes' and my ITP paper this year:
http://www.infsec.ethz.ch/people/andreloc/publications/lochbihler14itp.pdf
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:31):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Gergely,
there also is the AFP-entry Partial-Function-MR which allows you to define
sets of mutual recursive partial functions (which is not possible using the
original partial-function command). In the entry you also find further
examples of partial functions, including Collatz and a potentially
non-terminating evaluator for (a kind of) mu-recursive expressions.
Best,
René
Last updated: Nov 21 2024 at 12:39 UTC