Re: [isabelle] Malformed dependency error with overloading
I've got a related follow up question on malformed dependencies. Why is the
f :: "'Î"
g == "f :: nat Ã int"
definition g :: "nat Ã int" where
"g = (1,2)"
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?
On 27 May 2016 at 12:18, OndÅej KunÄar <kuncar at in.tum.de> 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.
> 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
Dr. Simon Foster - Research Associate in Computer Science
High Integrity Systems Engineering Group, University of York
This archive was generated by a fusion of
Pipermail (Mailman edition) and