Re: [isabelle] implicit beta normalization in the pretty-printer



On Wed, 18 Jan 2012, Ondřej Kunčar wrote:

I found out that the pretty-printer for terms in Isabelle do implicitly beta-normalization and this behavior can't be turned off (in contrast to eta-normalization).

Is there any serious reason why I can't turn off this feature like in the case of eta-normalization? It's a bit annoying if you want to do debugging on the ML level and you have to inspect every term by inspecting its ML representation (which is really tedious for larger terms).

(I am answering this on isabelle-users, not on isabelle-dev, because Isabelle/ML is perfectly normal user space; "the ML level" is actually part of the Isar toplevel. I also refrain from cross-posting (!) to isabelle-dev, because that list is de-facto a subset of isabelle-users and duplicates don't help.)


The beta contraction observed above is actually part of the treatment of term abbreviations, which uses principles from higher-order rewriting and that includes beta-contraction. Abbreviations are treated both in the "term check" phase for input and the "term uncheck" phase for output. So it is hard to input terms that are not beta normal, and the following uses some plain Isabelle/Isar/ML:

ML {*
  val t = @{term "%x::'a. x"} $ @{term "a::'a"};
  val u = singleton (Syntax.uncheck_terms @{context}) t;
*}

val t = Abs ("x", "'a", Bound 0) $ Free ("a", "'a"): term
val u = Free ("a", "'a"): term

The actual pretty printing is done in the so-called "unparse" phase and is innocent here: it does not do any beta contraction on its own. You could even try to make your own low-level printing for diagnostic purposes based on Syntax.uncheck_terms alone, which is mainly the pretty printer only.

In order to disable merely the contraction of abbreviations (with its beta conversion) during term-unchecking, you can use the following suitable configuration option on the context:

  declare [[show_abbrevs = false]]

Of course you need to use the correct context for printing to see the effect.


	Makarius


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