Re: [isabelle] domain of function

There is of course a third (Z) option: modelling partial functions as deterministic relations, ie ('a * 'b) set. This is similar to the 'a => 'b option model in most respects, but is slightly more natural when defining finite functions and has the advantage of inheriting a lot of
machinery from the relational super-type.

You can reduce this model (and those mentioned by Clemens) to the arbitrary-off-domain model by defining an application operator, in this case

f.x = (THE y. (x, y) : f),

but you now have the advantage of an explicit record of the domain.

On 19/02/2007, at 9:29 PM, Clemens Ballarin wrote:

Dear Hidetsune,

unfortunately, modelling partial functions with arbitrary is rather counter-intuitive and weak. Since arbitrary is an (unspecified) element from the underlying type, it is not possible to determine the domain of such a function. The function could be undefined at point x, or it could map x to a value that coincides with the (unspecified) value of arbitrary.

If you want to deal with partial functions seriously, you will have to make the domain explicit. I can think of two ways of dealing with this. You can either make the function a pair (f, A) where A is the domain of f. Or you let f be of type 'a => 'b option, and x is in the domain of f iff f x = None. Both are precise but not convenient to deal with, I'm afraid.


Dr Brendan Mahony
Information Networks Division                   ph +61 8 8259 6046
Defence Science and Technology Organisation     fx +61 8 8259 5589
Edinburgh, South Australia      Brendan.Mahony at

Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.