[isabelle] WG:AW: Abbreviation makes Isabelle/HOL very slow

-------- Originalnachricht --------
Betreff: AW:[isabelle] Abbreviation makes Isabelle/HOL very slow
Von: Peter Lammich
An: Giuliano Losa


In the first example, it tries to fold the abbreviation infinitely often on pretty printing. In the second example, it's also infinite folding, as higher-order unification is very creative at finding unexpected unifiers if you have function variables


-------- Originalnachricht --------
Betreff: [isabelle] Abbreviation makes Isabelle/HOL very slow
Von: Giuliano Losa
An: isabelle-users at cl.cam.ac.uk

in the following theory, the processing of the definition of x2 takes
minutes on my machine.

theory Test
imports Main

abbreviation x1 where "x1 f â f"

definition x2 where "x2 â x"


If I remove the abbreviation, it becomes instantaneous.

I came across this problem because I made the following abbreviation:

abbreviation flip where "flip f â Î x y . f y x"

It rendered Isabelle unusable, as the processing of some commands (not
only definition, but also other commands) started to take minutes.

I fixed the problem by using a definition instead of an abbreviation,
but there might be something worth investigating going on here.

I observed this behavior using Isabelle-2016 and Isabelle_15-Aug-2016.


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