Email Gateway (Aug 18 2022 at 18:17): Email Gateway (Aug 18 2022 at 18:17):From: John Munroe <munddr@gmail.com>
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
Email Gateway (Aug 18 2022 at 18:17):From: Lawrence Paulson <lp15@cam.ac.uk>
The unification algorithm operates on eta-expanded terms. Is there any compelling reason why you need them to be eta-contracted?
Larry Paulson
Email Gateway (Aug 18 2022 at 18:17):From: Makarius <makarius@sketis.net>
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. Here you can contract or expand manually to
achieve a certain standard form, e.g. via Envir.eta_contract,
Envir.beta_eta_contract, Patter.eta_long. The Thm module also provides
some variants for actual theorems.
Makarius
Email Gateway (Aug 18 2022 at 18:18):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Aug 30, 2011 at 5:12 AM, Makarius <makarius@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).
Email Gateway (Aug 18 2022 at 18:20):From: Makarius <makarius@sketis.net>
Tobias (and maybe Stefan Berghofer) should be able to explain how the
simplifier works concerning eta contraction. (I have my own collection of
boundary cases and surprises, sometimes even with plain beta redexes.)
Nonetheless, the situation has been rather "stable" in the past 10 years
or so, in the sense that there are now known soundness holes (there used
to be several in ancient times). Any serious reforms deep down there,
which is below the inference kernel, has always been beyond my
imagination. This does not mean someone could not do a convincing formal
model in HOL-Nominal, say, that explains convicingly how evertything could
fit together nicely (and still correctly).
The "unfold" method and 'unfolding' command is a bit different, and in my
area of responsibility. Historically I have merely imitated Larry's
traditional rewrite_goals_tac suite, and was a bit too slow to turn it
into something more close to the idea of actual unfolding of simple
definitions: "c == %x y z. b" instead of rewriting with "c x y z == ...".
Last time I've tried this small reform (maybe around 2006), I ran into
various oddities in the library, theories depending on the odd behaviour
wrt. beta/eta conversion. Later the situation became much worse, e.g. in
Multivariate_Analysis which often emulated tactical rewriting in the
middle of Isar proofs, using 'unfolding' for this.
Since you have cleaned up a lot of Multivariate_Analysis recently, what
was your impression?
Makarius
Last updated: Nov 21 2024 at 12:39 UTC