Re: [isabelle] Unify.matchers and term representation



On Tue, 30 Aug 2011, Brian Huffman wrote:

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

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





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