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

On 27/05/16 13:18, OndÅej KunÄar wrote:

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.