Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] formalising abstract machines


view this post on Zulip Email Gateway (Aug 19 2022 at 13:22):

From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,

I am formalising an abstract machine. For being able to prove pattern completeness, I defined the function to evalute to

value option

and added a last clause that returns None if all the other patterns fail.

But it is not clear how this interplays with

abstract_machine_dom arguments => (abstract_machine arguments) meets specification

type theorems. Would it be better to simply make an infinite recursive call as a last pattern?

| abstract_machine arguments = abstract_machine arguments

letting it not to terminate at all?

What is the standard way of defining an interpreter and its partial correctness in Isabelle?

Cheers

view this post on Zulip Email Gateway (Aug 19 2022 at 13:22):

From: Tobias Nipkow <nipkow@in.tum.de>
On 28/01/2014 12:10, Buday Gergely wrote:

Hi,

I am formalising an abstract machine. For being able to prove pattern completeness, I defined the function to evalute to

value option

and added a last clause that returns None if all the other patterns fail.

But it is not clear how this interplays with

abstract_machine_dom arguments => (abstract_machine arguments) meets specification

type theorems.

If you have a dom predicate, you don't need the option type because the
predicate should guaratee you never get into an underdefined situation.
Conversely, with option you can formulate your theorem like this:

abstract_machine arguments = Some result ==> results meets spec

Would it be better to simply make an infinite recursive call as a last pattern?

| abstract_machine arguments = abstract_machine arguments

letting it not to terminate at all?

You would not be able to define this with "fun" and would need to use
"partial_function (option)". However, you should only do this if it is a genuine
case of nontermination and not failed pattern-matching turned into artificial
nontermination.

Tobias

What is the standard way of defining an interpreter and its partial correctness in Isabelle?

Cheers

view this post on Zulip Email Gateway (Aug 19 2022 at 13:24):

From: Buday Gergely <gbuday@karolyrobert.hu>
Where can I find documentation on this partial_function (option) keyword? I did not find it in the function definition paper -- I have found its definition in an ML file but that was not very helpful.

view this post on Zulip Email Gateway (Aug 19 2022 at 13:24):

From: René Thiemann <rene.thiemann@uibk.ac.at>

Where can I find documentation on this partial_function (option) keyword? I did not find it in the function definition paper -- I have found its definition in an ML file but that was not very helpful.

I don't know whether this is the most recent reference, but it is described in:

A. Krauss. Recursive definitions of monadic functions. In Proc. PAR ’10, volume 43
of EPTCS, pages 1–13, 2010.

(available at http://arxiv.org/pdf/1012.4895v1.pdf)

To see its use in practice, you may also have a look at the IsaFoR/CeTA formalization
(http://cl-informatik.uibk.ac.at/software/ceta/)
which contains at least 18 definitions via partial function, where also a user-defined
monad is utilized.

Cheers,
René

view this post on Zulip Email Gateway (Aug 19 2022 at 13:24):

From: Tobias Nipkow <nipkow@in.tum.de>
There are two examples in ex/Fundefs.thy.

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 13:25):

From: Dmitriy Traytel <traytel@in.tum.de>
There is also a page about it in the Isar reference manual:

Isabelle2013-2 doc isar-ref

Section 11.2.2

Dmitriy


Last updated: Mar 28 2024 at 20:16 UTC