Email Gateway (Apr 13 2021 at 10:12): Email Gateway (Apr 13 2021 at 10:12):From: "He, Shuhan" <13061136@buaa.edu.cn>
Hello fellow researchers,
I'm working on a translator from an ML-like language to HOL, and I'm having a
difficulty with translation of inductive datatype definitions.
Datatype definition in Isabelle can be quite slow (at least compared to HOL4)
when the number of constructors goes up (say a few dozen), and time consumption
seems to be super-linear in the number of constructors. This has a significant
impact on usability since some programs in the source language have very large
datatypes, and it's not always feasible to modify the source programs to make
them friendlier to Isabelle. Is the poor performance caused by inherent
limitation of the theoretical foundation of the datatype definition package, or
suboptimality of implementation of the package? Also, does the package provide
a "quick mode" that skips the slow part of the definition process, while
retaining the essential theorems about the datatype being defined?
I once tried to poke into the implementation of the 'datatype' command to find
out what's slowing the thing down, but finally got lost in its sheer
complexity. The only potential culprit I found is the simplification theorems,
the number of which is quadratic in the number of constructors.
It would be nice to have a datatype definition package without the
aforementioned drawback, but given the size and complexity of current
implementation, improving it seems extremely difficult.
Your thoughts are greatly appreciated.
Email Gateway (Apr 13 2021 at 14:51):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Shuhan,
There are a couple of knobs one can turn. For example, a definition like
datatype t =
A00 | A01 | A02 | A03 | A04 | A05 | A06 | A07 | A08 | A09 |
A10 | A11 | A12 | A13 | A14 | A15 | A16 | A17 | A18 | A19 |
A20 | A21 | A22 | A23 | A24 | A25 | A26 | A27 | A28 | A29 |
A30 | A31 | A32 | A33 | A34 | A35 | A36 | A37 | A38 | A39 |
A40 | A41 | A42 | A43 | A44 | A45 | A46 | A47 | A48 | A49
takes something like 30 seconds on my machine. In contrast,
datatype (plugins only: ) t =
A00 | A01 | A02 | A03 | A04 | A05 | A06 | A07 | A08 | A09 |
A10 | A11 | A12 | A13 | A14 | A15 | A16 | A17 | A18 | A19 |
A20 | A21 | A22 | A23 | A24 | A25 | A26 | A27 | A28 | A29 |
A30 | A31 | A32 | A33 | A34 | A35 | A36 | A37 | A38 | A39 |
A40 | A41 | A42 | A43 | A44 | A45 | A46 | A47 | A48 | A49
takes only something like 3 seconds. So the actual datatype constructions (including the simplification theorems which are indeed quadratic in the number
of constructors) is reasonably fast. The plugins (e.g., size function, code generation setup, transfer theorems, etc.) that were disabled in the second definition provide many useful things too, but have their cost for large datatypes. It depends on the actual application which plugins are actually needed.
It would help to see your specific example and your requirements (what do you want to do with the type?) to provide further hints.
Dmitriy
Email Gateway (Apr 13 2021 at 15:01):From: Manuel Eberl <eberlm@in.tum.de>
Somebody once voiced the possibility of making it possible to switch off
the simplification lemmas (e.g. for constructor distinctness, of which
there are quadratically many) and replace them by a simproc that proves
them ad-hoc whenever one of them is needed.
This would make applying the theorems slightly more expensive, but
eliminate the need to prove all of them beforehand.
Not sure if this becomes enough of a problem to be worth it or if the
existing construction is fast enough for any reasonably-sized datatype.
Manuel
smime.p7s
Email Gateway (Apr 13 2021 at 16:07):From: Dominique Unruh <unruh@ut.ee>
Maybe the following approach would be nice:
Instead of generating pairwise inequalities, a function constructor_num
is generated with the simp-rules "constructor_num A00 = 1"
"constructor_num A01 = 2" "constructor_num A03 = 3" etc. (Where
"constructor_num" is an overloaded function like size.)
Then we additionally add the simp-rule "constructor_num x !=
constructor_num y ==> x != y". (For each datatype one instances because
the generic one would loop. Or alternatively, have a no-assumptions type
class for which that rule holds is added to the simplifier.)
Now I believe that this would be enough to decide inequalities the same
way as simp can do now. (Haven't tested this.)
To avoid unnecessary simplifications, maybe add a cong-rule that forbids
simplifications in the argument of constructor_num.
(Sorry if this is obvious and anyway what you had in mind for the inner
workings of the simproc.)
Best wishes,
Dominique.
Email Gateway (Apr 13 2021 at 16:12):From: Manuel Eberl <eberlm@in.tum.de>
"constructor_num x != constructor_num y ==> x != y"
That works in this very simple case where your datatype is just an
"enum"-like type. But in general, it should probably be something like
"constructor_num x != constructor_num y ==> x a b c != y d e"
because constructors, of course, can take parameters.
In any case, I don't think that works because you cannot really quantify
over constructors like this. In general, the constructors may not even
have the same type.
What I had in mind was that the simproc unfolds the internal
construction that the datatype uses and then proves the inequality from
that. I am not familiar with the details of that; there is probably a
little bit of overhead involved, but probably not too much.
Manuel
smime.p7s
Email Gateway (Apr 13 2021 at 16:14):From: Jakub Kądziołka <kuba@kadziolka.net>
No, Dominique's statement works. For example, for "option", it could be
defined as
"constructor_num None = 0" |
"constructor_num (Some x) = 1"
Regards,
Jakub Kądziołka
Email Gateway (Apr 13 2021 at 16:16):From: Manuel Eberl <eberlm@in.tum.de>
Ah, okay, I misunderstood. Yes, I suppose that should work. Might indeed
be the easiest and fastest way to do it.
Nice idea!
Manuel
smime.p7s
Email Gateway (Apr 13 2021 at 16:37):From: Dominique Unruh <unruh@ut.ee>
Yes, that's what I had in mind.
Best wishes,
Dominique.
Email Gateway (Apr 13 2021 at 23:02):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Dominique & Manuel,
Using a simproc for proving distinctness for datatypes with a large number of constructors was the behavior for the old datatype package, see e.g., [1, p32].
When developing the new package it was a deliberate decision to get rid of this special case. IIRC the reasoning was that distinctness is just one example of a quadratic fact (quadratically many theorems of constant size). There are others, e.g., the case theorems, which are linearly many each of linear size, so also quadratic altogether. So if one decides to seriously battle the quadratic behavior, one has to develop special cases for every such fact (and the cute constructor’s numbering trick will not always work). Also, a simproc has the big downside of being virtually invisible for Sledgehammer (and other tools that are not simp).
Moreover considering my below measurements: before optimizing the 3 second datatype declaration (which proves all 2450 distinctness theorems), I think we should rather understand the 27 seconds that are spend in the plugins (specifically, code, transfer, and quickcheck seem to be the culprits).
I would still be interested to see the original problematic example (the number of constructors is only one aspect that affects performance).
Dmitriy
[1] https://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/logics-HOL.pdf
Email Gateway (Apr 16 2021 at 02:39):From: "He, Shuhan" <13061136@buaa.edu.cn>
Hi Dmitriy,
Thank you for your suggestion. I can't give a specific example at the moment,
but generally I need to faithfully translate mutually recursive (typically no
more than 4) datatype definitions from a variant of ML into HOL, so I can prove
properties of source programs involving these types using standard proof
techniques like induction. The ultimate goal is to verify that the source
program conforms to some formal specification expressed in HOL.
A quick test showed that without plugins the definition command finished in a
few seconds for some of the larger datatypes in my source program. Not very
fast, but acceptable.
Last updated: Jul 15 2022 at 23:21 UTC