Re: [isabelle] Comparing polymorphic functions



On Feb 7, 2011 12:25pm, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
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.


Thanks. I should note that the schematic_lemma lem: "EX f (c::?'a). fc = (0::nat)", but the proof object is right. I think you're right -- f is instantiated to the identity function. If I explicitly instantiate each variable explicitly, I get the right type.


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.


Is this a limitation of the logic or is it a restriction intended by the implementation? Do you know in what circumstances does the unification not instantiate a type variable to a function type?

Thanks
Eg


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). fc = 0"

> apply (intro exI)

> apply (rule_tac[!] *)

> done

>

> thm lem

>

> EX (f::nat => nat) c::nat. fc = (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. fc = 0 %%

> (exI % (%x. EX c. xc = 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, eg,

> ?'a=>?'b. Since the schematic type variables, eg, ?'a can be instantiated,

> eg, to "nat" in (1) and to "nat => nat" in (3), why does the type of ?c

> need to be explicitly rewritten to, eg, ?a=>?'b, in order for ?c to be

> instantiated to functions like "y" or %xx? 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

>>








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