Re: [isabelle] Malformed dependency error with overloading



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.

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


-- 
Dr. Simon Foster - Research Associate in Computer Science
High Integrity Systems Engineering Group, University of York
http://www.cs.york.ac.uk/~simonf



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