Stream: Beginner Questions

Topic: How to inspect the domain and range of a function?

Alex Weisberger (Dec 05 2021 at 23:55):

I have a function that has a particular set of mappings that I want to inspect. It's small enough where printing out the entire domain and range would be manageable. However, when I execute:

value "domain f"

I get an output looking like this:

"domain
  (λu. if u = ⦇x = 8, y = 5⦈ then 1
        else if u = ⦇x = 7, y = 5⦈ then 1
             else if u = ⦇x = 6, y = 5⦈ then 1
                  else if u = ⦇x = 5, y = 5⦈ then 1
                       else if u = ⦇x = 8, y = 0⦈ then 1
...

And when I execute:

value "range f"

I get:

exception Match raised (line 244 of "generated code")

I thought domain and range would just return the obvious sets. Any advice here?

Alex Weisberger (Dec 05 2021 at 23:57):

In my case, I'm actually using a function like a hash table, i.e. the function has a specific set of "keys" and "values" that I'm interested in observing. Moreso for debug purposes. That may be useful information for this.

Alex Weisberger (Dec 06 2021 at 00:26):

Possibly other useful information - this function is a mapping from points to nat, i.e.:

record point =
  x :: nat
  y :: nat

definition f :: "point => nat"

And I'm trying to collect points which have a count of more than 1:

{p. (f p) > 1 }

This yields this error:

Wellsortedness error:
Type point not of sort enum
No type arity point_ext :: enum

Simon Roßkopf (Dec 06 2021 at 14:18):

As all functions in Isabelle/HOL are total, talking about the domain of a function f :: 'a => 'bmeans talking about UNIV :: 'a set. Therefore there is no constant domain defined by the library (Note that domain is printed blue in the output window. range f is then defined simply as the image of UNIVunder f. If you need partiality, you need to model this explicitly, for example with a function f' :: 'a => 'b option". To get domain and range of such partial functions use domand randefined in Map.thy` (Included in Main).

For your first output: domainis just a free variable, and therefore Isabelle cannot proceed with the evaluation.

The value command works by invoking the code generator and running the generated ML code. If it gives an error, most of the times that means what you supplied is not executable or at least Isabelle does not know how.

For value "range f" the generated code tries to compute the range by taking the image of UNIV :: point under fbut there is only a code equation for finite sets, therefore it fails. Maybe there is a more clever way to find range f, but Isabelle does no magic :(.
You can take a look at (something probably similar to) the generated code:

definition "R = range (\<lambda> x::bool . True::bool)"
export_code "R" in SML

For your last example, the 'obvious' way of computing the set is, once again, to compute f p > 1 for all points p. To do this the code generator would like to enumerate all values of the type. This would be provided by the class enum for finite types. As your point type contains infinite values it does not instantiate enum and the code generator cannot proceed.

Alex Weisberger (Dec 06 2021 at 18:41):

I see, that all makes sense. For what I'm trying to do, I think an association list might make more sense. It was just convenient to use a function to start.

Last updated: Jul 15 2022 at 23:21 UTC