Re: [isabelle] Unify.matchers and term representation

On Tue, Aug 30, 2011 at 5:12 AM, Makarius <makarius at> wrote:
> Larry is right that according to the natural order of things it is better to
> leave things as they are produced, and work conceptually with arbitrary
> representatives of the alpha/beta/eta equivalence classes.
> In some boundary cases this might fails, because certain tools do not
> observe this equivalence.

I want to point out that the *simplifier* is one of those "certain
tools" whose behavior depends on whether or not terms are
eta-expanded. (This includes not only the "simp" method, but also
"unfold", "auto", "fastsimp", etc.)

Many simplification rules, such as "id x = x" or "(f o g) x = f (g
x)", are intended to unfold a definition of a constant *only* when it
is applied to an argument. Eta expansion can cause the simplifier to
apply these rules in unexpected situations. (When users have the "eta
contract" pretty printing option enabled, as is the default,
replacements like "f o g" -> "%x. f (g x)" can appear to happen at

Eta-expansion can cause some confusion with congruence rules in the
simplifier, since a congruence rule only applies when the given
constant is applied to a sufficient number of arguments.

Eta expansion also interferes with the feature of the "rule" tactic
where it tries to preserve bound variable names:

With type "'a set" being an abbreviation for "'a => bool",
eta-expansion can happen to set expressions, which causes other
problems. For example, "A \<inter> B" might get expanded to "%a. (A
\<inter> B) a". Because of this, the otherwise-entirely-reasonable
simp rule "inf f g x = inf (f x) (g x)" would cause  "%a. (A \<inter>
B) a" (which pretty-prints as "A \<inter> B") to simplify to "%x. A x
& B x", violating the set/predicate discipline and messing up a lot of

> On Tue, 30 Aug 2011, Lawrence Paulson wrote:
>> The unification algorithm operates on eta-expanded terms. Is there any
>> compelling reason why you need them to be eta-contracted?

For reasons including (but not limited to) the ones listed above, I
would greatly prefer to have a unification algorithm that preserves
terms as much as possible, performing NO unnecessary eta-expansions OR

(Implementation idea: When eta-expanding, mark all of the
newly-introduced bound variables in some way; then do an
eta-contraction at the end, contracting *only* newly-introduced

A unification algorithm with this property would allow us to simplify
Isabelle's pretty printer quite a bit: The ridiculous "eta contract"
pretty-printing option would no longer be needed, and we could also
get rid of a lot of ML code used for preventing or reversing
eta-contraction with binders (e.g. the print translations for "split"
in Product_Type.thy).

- Brian

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