Re: [isabelle] Malformed dependency error with overloading
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.
On 05/27/2016 12:00 PM, Andreas Lochbihler wrote:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and