Re: [isabelle] Unify.matchers and term representation



On Tue, Aug 30, 2011 at 5:12 AM, Makarius <makarius at sketis.net> 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
random.)

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.

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-May/msg00032.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-May/msg00046.html

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

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-August/001803.html

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

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-August/001687.html
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-August/001733.html

> 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
eta-contractions.

(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
variables.)

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.