*To*: OndÅej KunÄar <kuncar at in.tum.de>*Subject*: Re: [isabelle] Malformed dependency error with overloading*From*: Simon Foster <simon.foster at york.ac.uk>*Date*: Mon, 20 Jun 2016 16:22:45 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <af2fb3c5-e743-6b48-886c-8745f4629420@in.tum.de>*References*: <57481AA9.3030403@inf.ethz.ch> <af2fb3c5-e743-6b48-886c-8745f4629420@in.tum.de>

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

- Previous by Date: [isabelle] Parametricity for functions which ignore arguments
- Next by Date: Re: [isabelle] Parametricity for functions which ignore arguments
- Previous by Thread: Re: [isabelle] [SPAM: 3.000] Re: Parametricity for functions which ignore arguments
- Next by Thread: [isabelle] ITP 2016: Call for participation
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list