[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
Cc:


Hi,

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

Peter


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


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

theory Test
imports Main
begin

abbreviation x1 where "x1 f â f"

definition x2 where "x2 â x"

end

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.

Giuliano



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