# Re: [isabelle] Comparing polymorphic functions

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

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