Re: [isabelle] Unify.matchers and term representation



The unification algorithm operates on eta-expanded terms. Is there any compelling reason why you need them to be eta-contracted?
Larry Paulson


On 29 Aug 2011, at 22:06, John Munroe wrote:

> Hello,
> 
> I see that the instantiations Unify.matchers finds may not necessarily
> have the simplest internal representation. For example:
> 
> ML {*
>  val trm = @{term "(bar::nat set) = bar"};
>  val pat = @{cpat "(?foo::(?'a => ?'b) => ?'c) (bar::(?'a => ?'b))"}
> |> term_of;
>  val mtchsq = Unify.matchers @{theory} [(pat,trm)];
>  val mtchs = Seq.list_of mtchsq;
> *}
> 
> The first match gives this instantiation for ?foo:
> 
> [?foo::(nat => bool) => ?'c := %a::nat => bool. a = a]
> 
> Now, if we look at the internal representation of the term, it actually is:
> 
>   Abs ("", "Nat.nat => HOL.bool",
>     Const ("HOL.eq", "(Nat.nat => HOL.bool) => (Nat.nat => HOL.bool)
> => HOL.bool") $
>       Abs ("", "Nat.nat", Bound 1 $ Bound 0) $ Abs ("", "Nat.nat",
> Bound 1 $ Bound 0))
> 
> It is unnecessarily large. A simpler representation would be:
> 
>   Abs ("", "Nat.nat  => HOL.bool",
>     Const ("HOL.eq", "(Nat.nat => HOL.bool) => (Nat.nat => HOL.bool)
> => HOL.bool") $ Bound 0 $
>       Bound 0)
> 
> My question is: Is there a way to reduce the internal representation
> of a term from one that contains "reducible" lambda expressions (like
> in the first) to one that is leaner (like in the second) in general?
> Or, is there a simple way to make the matcher algorithm spit out
> leaner internal representations?
> 
> Thank you for the help in advance.
> 
> John
> 






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