Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] monadic function definition


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 01:04 UTC