*To*: Eg Gloor <egglue at gmail.com>*Subject*: Re: [isabelle] Comparing polymorphic functions*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 7 Feb 2011 12:25:19 +0000*Cc*: Makarius <makarius at sketis.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTinB9sfc=-yHDWT46tJNBUe=PKk-nhcHAo6h4qA=@mail.gmail.com>*References*: <AANLkTik_QPi0HNJ9WShk7s_nc9jsbwH7_X9H6a-UDja-@mail.gmail.com> <4D415A30.7000104@dfki.de> <AANLkTi=2yDP7JNzG-tJHJE7JOXybL5YWiQEnCKkrWLU=@mail.gmail.com> <alpine.LNX.1.10.1102011612220.14100@atbroy100.informatik.tu-muenchen.de> <AANLkTimUQ51ZCDy4q=n0UGoa9ufh05Q=rbXtHRbFnd-r@mail.gmail.com> <alpine.LNX.1.10.1102041611070.24398@atbroy100.informatik.tu-muenchen.de> <AANLkTinB9sfc=-yHDWT46tJNBUe=PKk-nhcHAo6h4qA=@mail.gmail.com>

I've only had time for a brief look at your problem. And I'm not an expert at reading proof objects. But it appears to me that in your first example, the first proof that is found instantiates f to the identity function, so naturally c must be a natural number. The other point is that unification cannot always be expected to instantiate a type variable to a function type, as the search space would become too large. Larry Paulson On 5 Feb 2011, at 01:22, Eg Gloor wrote: > Thanks for the explanation. > > >> * Schematic term/type variables can be instantiated. For type variables >> this effectively means some kind of naive polymorphism. >> >> > I see. But why do you call it naive? If the variables can be instantiated, > then that's polymorphism -- is it not? > > >> >> Before this is getting more complicated: What is your actual application? >> >> > Basically, I'm puzzled by two things: > > 1) If we look at the following: > > axiomatization > func1 :: "nat => nat" and > func2 :: "(nat => nat) => nat" and > func3 :: "'a => 'b => 'c" > where > *: "func2 func1 = 0" > > schematic_lemma lem: "EX f (c::?'a). f c = 0" > apply (intro exI) > apply (rule_tac[!] *) > done > > thm lem > > EX (f::nat => nat) c::nat. f c = (0::nat) > > I wasn't expecting c to be of type "nat". Since it uses *, c should be > instantiated to "func1", which is of type "nat => nat". According to the > prf: > > protectI % EX f c. f c = 0 %% > (exI % (%x. EX c. x c = 0) % (%a. a) %% (OfClass type_class % TYPE(nat => > nat)) %% (exI % (%x. x = 0) % func2 func1 %% (OfClass type_class % > TYPE(nat)) ... > > f is instantiated to func2 and c is instantiated to func1. How come ?'a is > instantiated to "nat" and not "nat => nat"? > > 2) For the following: > > declare [[unify_search_bound=5]] > > ML {* > val p = term_of @{cpat "?f (?c::?'a) = ?v"}; > val t = @{term "x (y::nat=>nat) (z::nat=>nat) = (0::nat)"}; > val mtchers = Unify.matchers @{theory} [(p,t)] |> Seq.list_of; > pretty_insts @{context} (map (fn x => (x,0)) mtchers) > *} > > It returns 3 matchers: > (1) [?c::nat := (x::(nat => nat) => (nat => nat) => nat) (y::nat => nat) > (z::nat => nat), ?f::nat => nat := %a::nat. a, ?v::nat := 0::nat] > > [?'a := nat, ?'a1 := nat] > > (2) [?c::?'a := ?c::?'a, ?f::?'a => nat := %a::?'a. (x::(nat => nat) => (nat > => nat) => nat) (y::nat => nat) (z::nat => nat), ?v::nat := 0::nat] > > [?'a1 := nat] > > (3) [?c::?'a := z::nat => nat, ?f::?'a => ?'a1 := (x::(nat => nat) => (nat > => nat) => nat) (y::nat => nat), ?v::?'a1 := 0::nat] > > [?'a := nat => nat, ?'a1 := nat] > > How come "?c" can't be instantiated to "z" but can be instantiated to > "y"? It can do that only if the type of ?c is changed from ?'a to, e.g., > ?'a=>?'b. Since the schematic type variables, e.g., ?'a can be instantiated, > e.g., to "nat" in (1) and to "nat => nat" in (3), why does the type of ?c > need to be explicitly rewritten to, e.g., ?a=>?'b, in order for ?c to be > instantiated to functions like "y" or %x.x? Is this what you mean by "naive > polymorphism"? > > Note that even when ?c::?'a=>?'b, there are 2 matchers with ?c := z whereas > there's only 1 matcher with ?c := y. Do you know what's behind > this asymmetry? > > Thanks, again, and look forward to your reply! > > Eg > > >> Makarius >>

**Follow-Ups**:**Re: [isabelle] Comparing polymorphic functions***From:*egglue

**References**:**Re: [isabelle] Comparing polymorphic functions***From:*Makarius

**Re: [isabelle] Comparing polymorphic functions***From:*Eg Gloor

**Re: [isabelle] Comparing polymorphic functions***From:*Makarius

**Re: [isabelle] Comparing polymorphic functions***From:*Eg Gloor

- Previous by Date: [isabelle] Quantifying over conditions
- Next by Date: Re: [isabelle] Quantifying over conditions
- Previous by Thread: Re: [isabelle] Comparing polymorphic functions
- Next by Thread: Re: [isabelle] Comparing polymorphic functions
- Cl-isabelle-users February 2011 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