Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] formalising abstract machines

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

• Gergely

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

• Gergely
  

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.

• Gergely

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é

Email Gateway (Aug 19 2022 at 13:24):

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

Tobias

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: Nov 21 2024 at 12:39 UTC