*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Unify.matchers and term representation*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 30 Aug 2011 09:47:04 -0700*In-reply-to*: <alpine.LNX.1.10.1108301409190.23069@atbroy100.informatik.tu-muenchen.de>*References*: <CAP0k5J6QPaNgCGV2jcBS1Hqnf2P5ygPE8uVLDqNBvhFWW66ftA@mail.gmail.com> <DDF07D6F-92C5-4D9E-9967-41F1F15D0ED9@cam.ac.uk> <alpine.LNX.1.10.1108301409190.23069@atbroy100.informatik.tu-muenchen.de>*Sender*: huffman.brian.c at gmail.com

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

**References**:**[isabelle] Unify.matchers and term representation***From:*John Munroe

**Re: [isabelle] Unify.matchers and term representation***From:*Lawrence Paulson

**Re: [isabelle] Unify.matchers and term representation***From:*Makarius

- Previous by Date: Re: [isabelle] list_size_pointwise
- Next by Date: Re: [isabelle] list_size_pointwise
- Previous by Thread: Re: [isabelle] Unify.matchers and term representation
- Next by Thread: [isabelle] list_size_pointwise
- Cl-isabelle-users August 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