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