[isabelle] Failing to handle a fairly large dataype · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Failing to handle a fairly large dataype

Email Gateway (Aug 22 2022 at 15:20):

From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Isabelle Community,

I and a graduate student of mine, Liyi Li, have been working on
formalizing the K specification language of Grigore Rosu in Isabelle.
One of the very first datatypes we have, giving the bulk of the syntax
definition for K chokes Isabelle on my machine (MacBook Pro 2.8 GHz Core
i7 with 16 GB DDR3 memory). The error message I get is

Welcome to Isabelle/HOL (Isabelle2016-1: December 2016)
Run out of store - interrupting threads

Run out of store - interrupting threads

Failed to recover - exiting

message_output terminated
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 1

The code that is causing the choke is:

datatype ('upVar, 'var, 'svar, 'metaVar) kLabel
= KLabel 'svar
| KLabelFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
| IdKLabel 'metaVar
and ('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite
= KLabelTerm "('upVar, 'var, 'svar, 'metaVar) kLabel"
| KLabelRewrite "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kLabel"
and ('upVar, 'var, 'svar, 'metaVar) kItem =
KItem "('upVar, 'var, 'svar,
'metaVar) kLabelWithRewrite"
"('upVar, 'var, 'svar,
'metaVar) kListWithRewrite"
'upVar
| Constant "'var theConstant" 'upVar
| IdKItem "'metaVar" 'upVar
| HOLE 'upVar
and ('upVar, 'var, 'svar, 'metaVar) kItemWithRewrite
= KItemTerm "('upVar, 'var, 'svar, 'metaVar) kItem"
| KItemRewrite "('upVar, 'var, 'svar, 'metaVar) kItem"
"('upVar, 'var, 'svar, 'metaVar) kItem"
and ('upVar, 'var, 'svar, 'metaVar) kList =
KListCon "('upVar, 'var, 'svar,
'metaVar) kListWithRewrite"
"('upVar, 'var, 'svar,
'metaVar) kListWithRewrite"
| UnitKList
| KListItem "('upVar, 'var, 'svar,
'metaVar) bigKWithBag"
| IdKList "'metaVar"
and ('upVar, 'var, 'svar, 'metaVar) kListWithRewrite
= KListTerm "('upVar, 'var, 'svar, 'metaVar) kList"
| KListRewrite "('upVar, 'var, 'svar, 'metaVar) kList"
"('upVar, 'var, 'svar, 'metaVar) kList"
and ('upVar, 'var, 'svar, 'metaVar) bigK = TheK "('upVar, 'var, 'svar,
'metaVar) kWithRewrite"
| TheList "('upVar, 'var, 'svar,
'metaVar) theListRewrite"
| TheSet "('upVar, 'var, 'svar,
'metaVar) theSetRewrite"
| TheMap "('upVar, 'var, 'svar,
'metaVar) theMapRewrite"
and ('upVar, 'var, 'svar, 'metaVar) bigKWithBag = TheBigK "('upVar,
'var, 'svar, 'metaVar) bigK"
| TheBigBag "('upVar, 'var, 'svar,
'metaVar) bagWithRewrite"
| TheLabel "('upVar, 'var, 'svar,
'metaVar) kLabelWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) k
= Tilda "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
"('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
| UnitK | IdK 'metaVar | SingleK "('upVar, 'var, 'svar,
'metaVar) kItemWithRewrite"
| KFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) kWithRewrite = KTerm "('upVar, 'var,
'svar, 'metaVar) k"
| KRewrite "('upVar, 'var, 'svar, 'metaVar) k" "('upVar,
'var, 'svar, 'metaVar) k"

and ('upVar, 'var, 'svar, 'metaVar) theList = ListCon "('upVar, 'var,
'svar, 'metaVar) theListRewrite"
"('upVar, 'var, 'svar, 'metaVar)
theListRewrite"
| UnitList
| IdList 'metaVar
| ListItem "('upVar, 'var, 'svar,
'metaVar) kWithRewrite"
| ListFun "('upVar, 'var, 'svar,
'metaVar) kLabel"
"('upVar, 'var, 'svar,
'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theListRewrite =
TheListTerm "('upVar, 'var, 'svar, 'metaVar) theList"
| TheListRewrite "('upVar, 'var, 'svar, 'metaVar) theList"
"('upVar, 'var, 'svar, 'metaVar) theList"
and ('upVar, 'var, 'svar, 'metaVar) theSet = SetCon "('upVar, 'var,
'svar, 'metaVar) theSetRewrite"
"('upVar, 'var, 'svar, 'metaVar)
theSetRewrite"
| UnitSet
| IdSet 'metaVar
| SetItem "('upVar, 'var, 'svar,
'metaVar) kWithRewrite"
| SetFun "('upVar, 'var, 'svar,
'metaVar) kLabel"
"('upVar, 'var, 'svar,
'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theSetRewrite =
TheSetTerm "('upVar, 'var, 'svar, 'metaVar) theSet"
| TheSetRewrite "('upVar, 'var, 'svar, 'metaVar) theSet"
"('upVar, 'var, 'svar, 'metaVar) theSet"
and ('upVar, 'var, 'svar, 'metaVar) theMap
= MapCon "('upVar, 'var, 'svar, 'metaVar) theMapRewrite"
"('upVar, 'var, 'svar, 'metaVar) theMapRewrite"
| UnitMap
| IdMap 'metaVar
| MapItem "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
"('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
| MapFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theMapRewrite =
TheMapTerm "('upVar, 'var, 'svar, 'metaVar) theMap"
| TheMapRewrite "('upVar, 'var, 'svar, 'metaVar) theMap" "('upVar,
'var, 'svar, 'metaVar) theMap"
and ('upVar, 'var, 'svar, 'metaVar) bag
= BagCon "('upVar, 'var, 'svar, 'metaVar) bagWithRewrite"
"('upVar, 'var, 'svar, 'metaVar) bagWithRewrite"
| UnitBag
| IdBag 'metaVar
| Xml 'var "feature list" "('upVar, 'var, 'svar, 'metaVar)
bagWithRewrite"
| SingleCell 'var "feature list" "('upVar, 'var, 'svar,
'metaVar) bigK"
and ('upVar, 'var, 'svar, 'metaVar) bagWithRewrite =
BagTerm "('upVar, 'var, 'svar, 'metaVar) bag"
| BagRewrite "('upVar, 'var, 'svar, 'metaVar) bag" "('upVar, 'var,
'svar, 'metaVar) bag"

It takes something like three to four hours on my student's computer
(Windows machine with the same amount of memory), but it does complete.
Is there some way to tweak Isabelle or this definition to make it more
likely to go through?

---Elsa

Email Gateway (Aug 22 2022 at 15:21):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Dear Elsa and Liyi,

Such large specifications of dependent types are unfortunately cases where our new datatype package scores less well than the previous one.

(We do score better in the presence of nesting, though.) See also the thread

"A large mutually recursive datatype"

from https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-March/thread.html

Replacing as much as possible from "mutual" to "nested" should help a lot. In your case, there is a very

natural opportunity for nesting, which would remove duplication and improve modularity. Namely, isolating

your heavily used "withRewrite" monad as the following generic datatype:

datatype 'a withRewrite = KTerm 'a | KRewrite 'a 'a

Then your specification becomes much smaller, and is processed on my computer in about three minutes:

typedecl 'var theConstant
typedecl feature

datatype ('upVar, 'var, 'svar, 'metaVar) kLabel
= KLabel 'svar
| KLabelFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
| IdKLabel 'metaVar
and ('upVar, 'var, 'svar, 'metaVar) kItem =
KItem "('upVar, 'var, 'svar, 'metaVar) kLabel withRewrite"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
'upVar
| Constant "'var theConstant" 'upVar
| IdKItem "'metaVar" 'upVar
| HOLE 'upVar
and ('upVar, 'var, 'svar, 'metaVar) kList =
KListCon "('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
| UnitKList
| KListItem "('upVar, 'var, 'svar, 'metaVar) bigKWithBag"
| IdKList "'metaVar"
and ('upVar, 'var, 'svar, 'metaVar) bigK =
TheK "('upVar, 'var, 'svar, 'metaVar) k withRewrite"
| TheList "('upVar, 'var, 'svar, 'metaVar) theList withRewrite"
| TheSet "('upVar, 'var, 'svar, 'metaVar) theSet withRewrite"
| TheMap "('upVar, 'var, 'svar, 'metaVar) theMap withRewrite"
and ('upVar, 'var, 'svar, 'metaVar) bigKWithBag =
TheBigK "('upVar, 'var, 'svar, 'metaVar) bigK"
| TheBigBag "('upVar, 'var, 'svar, 'metaVar) bag withRewrite"
| TheLabel "('upVar, 'var, 'svar, 'metaVar) kLabel withRewrite"
and ('upVar, 'var, 'svar, 'metaVar) k =
Tilda "('upVar, 'var, 'svar, 'metaVar) k withRewrite"
"('upVar, 'var, 'svar, 'metaVar) k withRewrite"
| UnitK | IdK 'metaVar
| SingleK "('upVar, 'var, 'svar, 'metaVar) kItem withRewrite"
| KFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theSet =
SetCon "('upVar, 'var, 'svar, 'metaVar) theSet withRewrite"
"('upVar, 'var, 'svar, 'metaVar) theSet withRewrite"
| UnitSet
| IdSet 'metaVar
| SetItem "('upVar, 'var, 'svar, 'metaVar) k withRewrite"
| SetFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theList =
ListCon "('upVar, 'var, 'svar, 'metaVar) theList withRewrite"
"('upVar, 'var, 'svar, 'metaVar) theList withRewrite"
| UnitList
| IdList 'metaVar
| ListItem "('upVar, 'var, 'svar, 'metaVar) k withRewrite"
| ListFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theMap =
MapCon "('upVar, 'var, 'svar, 'metaVar) theMap withRewrite"
"('upVar, 'var, 'svar, 'metaVar) theMap withRewrite"
| UnitMap
| IdMap 'metaVar
| MapItem "('upVar, 'var, 'svar, 'metaVar) k withRewrite"
"('upVar, 'var, 'svar, 'metaVar) k withRewrite"
| MapFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kList withRewrite"
and ('upVar, 'var, 'svar, 'metaVar) bag =
BagCon "('upVar, 'var, 'svar, 'metaVar) bag withRewrite"
"('upVar, 'var, 'svar, 'metaVar) bag withRewrite"
| UnitBag
| IdBag 'metaVar
| Xml 'var "feature list" "('upVar, 'var, 'svar, 'metaVar) bag withRewrite"
| SingleCell 'var "feature list" "('upVar, 'var, 'svar, 'metaVar) bigK"

Other natural opportunities for nesting exist, such as separating the various collection monads.
But hopefully the above is already acceptable.

All the best,

Andrei

Email Gateway (Aug 22 2022 at 15:22):

From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Andrei,

Thank you very much. I guess I haven't kept up as well as I should
and assumed nesting would make the last one where you put it all
together that much worse. You are absolutely right the introducing
nesting is quite ossible and could even make the whole grammar more
readable. Thank you and we'll give it a try.

---Elsa

Email Gateway (Aug 22 2022 at 15:23):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>

large specifications of dependent types

I meant to write

large specifications of mutually dependent types

Andrei

From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Andrei Popescu <a.popescu@mdx.ac.uk>
Sent: 01 April 2017 14:59
To: Elsa L. Gunter; cl-isabelle-users@lists.cam.ac.uk; Liyi Li
Cc: j.c.blanchette@vu.nl; Dmitriy Traytel
Subject: Re: [isabelle] Failing to handle a fairly large dataype

Dear Elsa and Liyi,

Such large specifications of dependent types are unfortunately cases where our new datatype package scores less well than the previous one.

(We do score better in the presence of nesting, though.) See also the thread

"A large mutually recursive datatype"

from https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-March/thread.html

Replacing as much as possible from "mutual" to "nested" should help a lot. In your case, there is a very

natural opportunity for nesting, which would remove duplication and improve modularity. Namely, isolating

your heavily used "withRewrite" monad as the following generic datatype:

datatype 'a withRewrite = KTerm 'a | KRewrite 'a 'a

Then your specification becomes much smaller, and is processed on my computer in about three minutes:

typedecl 'var theConstant
typedecl feature

Other natural opportunities for nesting exist, such as separating the various collection monads.
But hopefully the above is already acceptable.

All the best,

Andrei

From: Elsa L. Gunter <egunter@illinois.edu>
Sent: 01 April 2017 02:52
To: cl-isabelle-users@lists.cam.ac.uk; Liyi Li
Cc: Andrei Popescu
Subject: Failing to handle a fairly large dataype

Dear Isabelle Community,

I and a graduate student of mine, Liyi Li, have been working on formalizing the K specification language of Grigore Rosu in Isabelle. One of the very first datatypes we have, giving the bulk of the syntax definition for K chokes Isabelle on my machine (MacBook Pro 2.8 GHz Core i7 with 16 GB DDR3 memory). The error message I get is

Welcome to Isabelle/HOL (Isabelle2016-1: December 2016)
Run out of store - interrupting threads

Run out of store - interrupting threads

Failed to recover - exiting

message_output terminated
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 1

The code that is causing the choke is:

datatype ('upVar, 'var, 'svar, 'metaVar) kLabel
= KLabel 'svar
| KLabelFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
| IdKLabel 'metaVar
and ('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite
= KLabelTerm "('upVar, 'var, 'svar, 'metaVar) kLabel"
| KLabelRewrite "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kLabel"
and ('upVar, 'var, 'svar, 'metaVar) kItem =
KItem "('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
'upVar
| Constant "'var theConstant" 'upVar
| IdKItem "'metaVar" 'upVar
| HOLE 'upVar
and ('upVar, 'var, 'svar, 'metaVar) kItemWithRewrite
= KItemTerm "('upVar, 'var, 'svar, 'metaVar) kItem"
| KItemRewrite "('upVar, 'var, 'svar, 'metaVar) kItem"
"('upVar, 'var, 'svar, 'metaVar) kItem"
and ('upVar, 'var, 'svar, 'metaVar) kList =
KListCon "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
| UnitKList
| KListItem "('upVar, 'var, 'svar, 'metaVar) bigKWithBag"
| IdKList "'metaVar"
and ('upVar, 'var, 'svar, 'metaVar) kListWithRewrite
= KListTerm "('upVar, 'var, 'svar, 'metaVar) kList"
| KListRewrite "('upVar, 'var, 'svar, 'metaVar) kList"
"('upVar, 'var, 'svar, 'metaVar) kList"
and ('upVar, 'var, 'svar, 'metaVar) bigK = TheK "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
| TheList "('upVar, 'var, 'svar, 'metaVar) theListRewrite"
| TheSet "('upVar, 'var, 'svar, 'metaVar) theSetRewrite"
| TheMap "('upVar, 'var, 'svar, 'metaVar) theMapRewrite"
and ('upVar, 'var, 'svar, 'metaVar) bigKWithBag = TheBigK "('upVar, 'var, 'svar, 'metaVar) bigK"
| TheBigBag "('upVar, 'var, 'svar, 'metaVar) bagWithRewrite"
| TheLabel "('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) k
= Tilda "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
"('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
| UnitK | IdK 'metaVar | SingleK "('upVar, 'var, 'svar, 'metaVar) kItemWithRewrite"
| KFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
"('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) kWithRewrite = KTerm "('upVar, 'var, 'svar, 'metaVar) k"
| KRewrite "('upVar, 'var, 'svar, 'metaVar) k" "('upVar, 'var, 'svar, 'metaVar) k"

Email Gateway (Aug 22 2022 at 15:24):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Dear Elsa,

Thank you very much. I guess I haven't kept up as well as I should and assumed nesting would make the last one where you put it all together that much worse.

Since the new package no longer transforms "nested" into "mutual," there is no "unfolding hazard" with nested types.

You are absolutely right the introducing nesting is quite possible and could even make the whole grammar more readable.

I fully agree. I believe this will also encourage more modular proofs.

Thank you and we'll give it a try.

Best of luck with this ambitious development! What meta-properties of the K framework do you plan to prove?

Andrei

Last updated: Nov 21 2024 at 12:39 UTC