Robert Soeldner (Nov 14 2021 at 11:01): Robert Soeldner (Nov 14 2021 at 11:01):In my theory, I work with partial functions. To prevent writing the in some code (readability), I experimented with using defines to make use of total and partial functions.
This approach worked quite well, but now I encountered a problem when trying to specialize a locale. The following example shows such a case:
abbreviation totalize :: "('a ⇀ 'b) ⇒ 'a ⇒ 'b" where
"totalize f a ≡ the (f a)"
locale A =
fixes a :: "'a set"
assumes "finite a"
locale B =
A: A a +
B: A b for a :: "'a set" and b :: "'b set" +
fixes
f :: "'a ⇀ 'b" and
f' :: "'a ⇒ 'b"
defines
f_def: "f' ≡ totalize f"
locale C = B a b "λe. if e ∈ a then Some e else None" id
for a b
Here, locale C is rejected with the following error message:
Bad head of lhs: existing constant "id"
The error(s) above occurred in definition:
"id ≡ λaa. totalize (If (aa ∈ a) (Some aa)) None"
The same "problem"\limitation was reported in 2015 https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-August/msg00030.html
Is there any known workaround?
Wolfgang Jeltsch (Nov 14 2021 at 16:18):I don’t know understand right now what the precise problem is, let alone whether there’s a workaround for it, but I would argue that generally id doesn’t fulfill the relevant axiom anyhow.
The representation of the partial function as a total function must use the None as the result for all arguments that don’t belong to the domain. However, id uses the arguments as the results. The point is that you’re not free to choose what to return for arguments outside the domain. While you don’t know what value the None really is, you’re still forced to pick this particular, unknown value.
This restriction is important: If you were free to let the total function have any results for the arguments outside the domain, for example, by replacing the defines declaration with a fixes declaration that just insists that the partial and total versions coincide on the domain, then, by choosing different results for the same arguments outside the domain, you could distinguish different interpretations that should morally be the same.
Therefore, my suggestion is: Just use totalize in the declaration of C as well.
Robert Soeldner (Nov 14 2021 at 17:30):Thank you Wolfgang for your support :)
The problem still remains:
locale C = B a b "λe. if e ∈ a then Some e else None" "totalize (λe. if e ∈ a then Some e else None)"
for a b
will result in the following error:
Bad head of lhs: "λaa. totalize (If (aa ∈ a) (Some aa)) None"
The error(s) above occurred in definition:
"λaa. totalize (If (aa ∈ a) (Some aa)) None ≡ λaa. totalize (If (aa ∈ a) (Some aa)) None"
Weird. It seems as if totalize is applied to a partial application of If instead of the function it is actually applied to, as if the totalized is pushed under the λ.
Last updated: Apr 19 2024 at 12:27 UTC