Stream: Beginner Questions

Topic: disable eta-conversion in term parsing


view this post on Zulip Qiyuan Xu (Jul 12 2021 at 04:25):

How to disable the η\eta-conversion in term parsing, which converts the term λx.Px\lambda x. P x to PP. It's sometimes an obstacle to syntax translations.
As an illustration, I copied the exact code used for sets from the system theory src/HOL/Set.thy (line 43 in Isabelle2021),

definition Collect :: "('a ⇒ bool) ⇒ 'a set" where "Collect = undefined"
translations
  "{x. P}"  "CONST Collect (λx. P)"

It works for all situations except the case of Collect (λx. Px)\mathrm{Collect}\ (\lambda x.\ P\,x) where it's printed as Collect P\mathrm{Collect}\ P rather than the expected {x. Px}\{x.\ P\,x\}, due to the unexpected aggressive η\eta-conversion.
However it's the exact code used in system theory, and Collect (λx. Px)\mathrm{Collect}\ (\lambda x.\ P\,x) is handled by the system theory rather well, printed as {x. Px}\{x.\ P\,x\}.
(Actually, I copied the whole theory Set.thy from the system source, but the copied version still doesn't work.)
It's really confusing that what the magic is taken by the system theory? And how could I disable the embarrassing η\eta-conversion to let the version of mine Collect\mathrm{Collect} work?

view this post on Zulip Qiyuan Xu (Jul 12 2021 at 04:31):

term "Collect (λx. P x)"

prints {x.Px}\{x. P x\} in the system version but CollectP\mathrm{Collect}\,P in the copied version.

view this post on Zulip Qiyuan Xu (Jul 12 2021 at 05:15):

It must be some magic, translations "{x. P}" ⇌ "CONST Set.Collect (λx. P)" works but translations "{x. P}" ⇌ "CONST My.Collect (λx. P)" not. The magic should be applied to the Set.Collect constant.


Last updated: Jul 15 2022 at 23:21 UTC