Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] The partial_function command

Email Gateway (Apr 17 2023 at 10:46):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

I am a fan of the partial_function command, but I noticed two small
technical shortcomings:

1. Despite working with chain-complete partial orders, it can only
   define functions that return a CCPO, not values of a CCPO. If you
   try to do something like

partial_function (option) foo :: "'a option" where "foo = foo"

you simply get: exception Empty raised (line 357 of "library.ML")

You might think using partial_function to define a constant is silly,
but there are settings where it makes sense, e.g. probabilistic ones:

partial_function (spmf) foo :: "nat spmf"
  where "foo = do {b ← coin_spmf; if b then return_spmf 0 else map_spmf
Suc foo}"

Of course, the problem can be avoided by simply adding a dummy parameter
of type unit.

So is there any reason for why this is not supported? If one wanted to
support it, would one have to implement the "unit abstraction hack" or
is there a more direct way?

2. The internal definition is not only not exposed to the user level
   (i.e. "thm foo_def" does not work) but there also seems to be no way to
   access it from ML. The only thing that is returned is the term itself
   (foo) and the recurrence (foo.simps). This makes it hard (if not
   impossible) to use partial_function as a component in other tools.

Of course one could always write down the fixed point explicitly, but
the partial_function command provides nice automation for e.g.
monotonicity proofs that one would have to do manually.

Cheers,

Manuel

Email Gateway (Apr 17 2023 at 11:07):

From: Peter Gammie <peteg42@gmail.com>
Manuel,

On 17 Apr 2023, at 20:46, Manuel Eberl <manuel@pruvisto.org> wrote:

I am a fan of the partial_function command, but I noticed two small technical shortcomings:

1. Despite working with chain-complete partial orders, it can only define functions that return a CCPO, not values of a CCPO. If you try to do something like

partial_function (option) foo :: "'a option" where "foo = foo"

you simply get: exception Empty raised (line 357 of "library.ML")

You might think using partial_function to define a constant is silly, but there are settings where it makes sense, e.g. probabilistic ones:

partial_function (spmf) foo :: "nat spmf"
where "foo = do {b ← coin_spmf; if b then return_spmf 0 else map_spmf Suc foo}"

Of course, the problem can be avoided by simply adding a dummy parameter of type unit.

So is there any reason for why this is not supported? If one wanted to support it, would one have to implement the "unit abstraction hack" or is there a more direct way?

I’d like to see that too but it strikes me as not too much bother to just use the fixed-point combinator directly in these cases.

2. The internal definition is not only not exposed to the user level (i.e. "thm foo_def" does not work) but there also seems to be no way to access it from ML. The only thing that is returned is the term itself (foo) and the recurrence (foo.simps). This makes it hard (if not impossible) to use partial_function as a component in other tools.

Try

context
notes [[function_internals]]
begin

partial_function (spmf) ….
(* put a valid def here *)

print_theorems

end

(see e.g. CryptHOL in the AFP)

I tend to feel that partial_function should always yield a def.

Of course one could always write down the fixed point explicitly, but the partial_function command provides nice automation for e.g. monotonicity proofs that one would have to do manually.

Is there really much gained for recursively-defined CAFs (Haskell terminology)? No parameters, no interesting monotonicity.

regards,
Peter

Email Gateway (Apr 17 2023 at 11:12):

From: Manuel Eberl <manuel@pruvisto.org>

context
notes [[function_internals]]
begin

Aha, good to know! Thanks. I wasn't aware that worked for
partial_function as well.

I tend to feel that partial_function should always yield a def.
I feel so, too. Especially in ML. Calling a command and then making a
string and accessing a generated theorem by name seems hacky to me.

Is there really much gained for recursively-defined CAFs (Haskell terminology)? No parameters, no interesting monotonicity.

Honestly I haven't given that much thought. For me it's mainly a matter
of uniformity: if you want to build some automation on top of
partial_function (which I have very vague mid-term plans to do) it's
annoying if you have to add a case distinction like that.

Manuel

Last updated: Apr 20 2024 at 04:19 UTC