Re: [isabelle] Malformed dependency error with overloading



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

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
checks.

Best,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.