*To*: Lawrence Paulson <lp15 at cam.ac.uk>, Eg Gloor <egglue at gmail.com>*Subject*: Re: [isabelle] Comparing polymorphic functions*From*: egglue at gmail.com*Date*: Mon, 07 Feb 2011 16:27:45 +0000*Cc*: Makarius <makarius at sketis.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <231062B3-B185-4AE0-B4A5-397302B38313@cam.ac.uk>

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 anexpert at reading proof objects. But it appears to me that in your firstexample, the first proof that is found instantiates f to the identityfunction, so naturally c must be a natural number.

The other point is that unification cannot always be expected toinstantiate a type variable to a function type, as the search space wouldbecome too large.

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

> then that's polymorphism -- is it not?

>

>

>>

>> Before this is getting more complicated: What is your actualapplication?

>>

>>

> 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 ?'ais

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

> 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 meanby "naive

> polymorphism"?

>

> Note that even when ?c::?'a=>?'b, there are 2 matchers with ?c := zwhereas

> 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:*Lawrence Paulson

**References**:**Re: [isabelle] Comparing polymorphic functions***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Quantifying over conditions
- Next by Date: [isabelle] Isabelle2011 Z3 issue
- 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