Email Gateway (Aug 22 2022 at 13:14): Email Gateway (Aug 22 2022 at 13:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle experts,
For the attached theory, Isabelle2016 yields the following error, which I do not
understand at all.
Malformed dependency of test('a) -> sample(bool, 'a)
(restriction sample('a, ('b, 'c) envT) from "TEst.sample_envT_def_raw")
The error(s) above occurred in definition "test_def_raw":
"test ≡ sample my_pmf"
Why is the definition rejected? What could possibly go wrong here? What are the
requirements on a well-formed dependency? Section 5.10 of the Isabelle2016 Isar-Ref manual
does not say much about those dependency checks.
Best,
Andreas
TEst.thy
Email Gateway (Aug 22 2022 at 13:15):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Andreas,
the set of (overloaded) defining equations cannot be arbitrary since
then the problem of detecting a cycle in them would undecidable.
Therefore we impose an additional restriction that makes the problem
quadratic. I call the restriction composability:
for all d_\tau == ... and
c == ... d_\sigma ...
\sigma must be an instance of \tau or \tau must be an instance of \sigma.
(More can be found in my PhD thesis (chapter 3.5)).
The composability does not hold in your example:
You overload "sample :: ('a, ... evnT) sample"
and then in the definition of test you use "sample :: (bool, 'a) sample".
You have two choices now:
a) you either refactor your definitions such that you don't run into
this problem (for example by using more specific types)
b) or you can use unchecked overloading by then you are on your own
(i.e., the definition will be axiomatic).
I hope this helps.
Ondrej
Email Gateway (Aug 22 2022 at 13:15):From: Ondřej Kunčar <kuncar@in.tum.de>
Of course, I missed one case.
\sigma must be an instance of \tau or \tau must be an instance of \sigma
or they are not unifiable.
That said, composability wants to rule out the case that the two types
have a non-trivial common instance.
Email Gateway (Aug 22 2022 at 13:15):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondrej,
Thanks for the quick explanation. It does explain the error message. I'll have to think
about which of the suggested options are feasible.
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 13:38):From: Simon Foster <simon.foster@york.ac.uk>
Hi Ondrej,
I've got a related follow up question on malformed dependencies. Why is the
following rejected?
consts
f :: "'α"
overloading
g == "f :: nat × int"
begin
definition g :: "nat × int" where
"g = (1,2)"
end
definition "l1 (t1 :: 'a × int) ≡ f = t1" (* Rejected *)
Malformed dependency of l1('a) -> f('a × int)
(restriction f(nat × int) from "Scratch.g_def_raw"
If I understand correctly, here nat × int is indeed an instance of 'a ×
int, so why is this rejected? I note that it seems to only be accepted if
the type of f used by l1 specialises that of g, or is orthogonal to it; so
does the specialisation path in fact have to go from l1 -> g?
Thanks,
-Simon.
Email Gateway (Aug 22 2022 at 15:00):From: Simon Foster <simon.foster@york.ac.uk>
Dear Ondrej,
I asked the question below about overloaded definitions and permissible
dependencies. I'm still interested in this kind of overloading scheme, so I
just tried my example in Isabelle 2016-1 and note that it is still rejected:
consts
f :: "'a"
overloading
g == "f :: nat * int"
begin
definition g :: "nat * int" where
"g = (1,2)"
end
definition "l1 (t1 :: 'a * int) ≡ f = t1" (* Rejected *)
Please could you elaborate why it is not possible to specialise a
polymorphic constant in this way? It seems to satisfy your composability
criterion (nat * int is an instance of 'a * int).
Thanks,
-Simon.
Last updated: Apr 25 2024 at 20:15 UTC