Re: [isabelle] Slow rule application in case of many parameters?



Lawrence Paulson wrote:
It looks like you are working on rather large problems! Still I don't think such runtimes should be normal. Are you using Poly/ML? Does your machine have ample memory?
Larry Paulson


On 15 Mar 2009, at 20:32, Dennis Walter wrote:

Hi all,

I'm having problems solving large structured goals involving many
parameters. Even rule applications like
 apply (rule allI | rule impI | erule conjE)+
take several minutes. I've experienced this slowdown in cases where
the number of parameters (bound meta-variables) is > 30, and these
repeatedly occur in various places within the goal (~2000 lines, no
abbreviations). I suspect that Isabelle's lifting of rules over
parameters is to blame, but I can't see why this should be the case.
Can anybody explain this phenomenon to me?

Thanks a lot,
 Dennis



I can't find the notation '+' in the Isar reference, but I'm guessing that what you're doing is the equivalent of

REPEAT (rtac allI 1 ORELSE rtac impI 1 ORELSE etac conjE 1)
(or perhaps REPEAT1)

so try instead

REPEAT_DETERM (rtac allI 1 ORELSE rtac impI 1 ORELSE etac conjE 1)

I've found in the past that this sort of change makes a difference. The reason (I guessed) is that although both versions do, in a sense, the same amount of useful work for you up to the point where you get the first new goal-state, the REPEAT version creates and saves all sorts of data structures which enable backtracking, whereas in the REPEAT_DETERM version, these get thrown away (REPEAT_DETERM will not allow backtracking).

Jeremy







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