Email Gateway (Aug 22 2022 at 10:37): Email Gateway (Aug 22 2022 at 10:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the record package,
Last week, Jasmin and I had a long discussion about integrating the record package further
with the free_constructors package. In the end, we found out that things are not so
simple. The main obstacle was the somewhat non-uniform treatment of record extensions when
it comes to the different generated constants. Let me illustrate the problem with an example.
record foo = foo :: nat
record bar = foo + bar :: int
The first command creates a type "'m1 foo_ext"
and synonyms "'m1 foo_scheme = 'm1 foo_ext" and "foo = unit foo_scheme".
The second a type "'m2 bar_ext"
and synonyms "'m2 bar_scheme == 'm2 bar_ext foo_ext" and "bar = unit bar_scheme".
The record notation (| ... |) gets translated to constants foo_ext and bar_ext, which
serve as free constructors for the types foo_ext and bar_ext. Thus, a value of type 'm2
bar_scheme is composed of two nested constructors, namely bar_ext in the extension
parameter for foo_ext. If it were only for this, it would be easy to register the
constants foo_ext and bar_ext as free constructors of the respective types.
However, the free_constructor command also supports selectors and therefore, it would be
good to register them too. Unfortunately, I have not been able to find a proper selector
for the bar_ext type. The selector bar is generated as a constant of its own rather than
an abbreviation like
bar x == bar_ext.bar (foo.more x) (* bar_ext.bar does not exist at the moment *)
Can anyone remember why the selectors for _scheme are constants rather than abbreviations
of selectors for the _ext types?
In the present form, free_constructors cannot handle compound types such as bar_scheme. So
we cannot register bar reasonably with free_constructors.
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:38):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hey Andreas.
The record package builds records out of layers of "ext" record
extensions, as you've understood.
In the distant past, the record package defined two layers of selectors
and updators, one (mostly hidden) for each "ext" layer, and surface
selectors/updators which operate on the "completed" type. These were all
new constant definitions - it may be relevant that this design predates
abbreviations.
When I last attacked the record package, I got rid of the duplication in
order to reduce the proof times, and just kept the surface
selectors/updators.
In hindsight, we could have instead kept the layer-by-layer
selectors/updators, and turned them into the final selectors/updators
with abbreviations or other syntax tricks. I didn't think of this at the
time. Also, I wanted to change as little of the old design as possible,
in particular I didn't want to try to understand the syntax aspects.
I suspect that making this change would require a modest amount of work,
probably a few weeks for someone who knows what they're doing. It would
also simplify the simprocs a little - they have to think a lot about the
special cases for the more/"..." selector/updator.
A final complexity you might want to think about: the reason I got
involved in this in the first place is that the record package can be
used to define some really big records (> 500 fields). I don't think
that the corresponding datatype proofs can be done in a reasonable
amount of time. This is one reason why records aren't given the datatype
treatment by default. There might be an argument for switching the
default here, and providing a richer theorem set by default with a
"simple mode" switch available for bigger records.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:38):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hey Thomas,
Thanks for the quick reply. I still wonder how a change from selectors on _scheme to
layer-by-layer would affect efficiency. With layer-by-layer, we'd get less
selector/updator pairs, because we only need them for the fields of one record
specification, not for the fields inherited from existing records. On the other hand,
selectors then consist of several constants and pretty-printing has to collapse the
abbreviations. In the end, it certainly depends on the depth of the record extensions. I
myself have never exceeded depth 5, but how about at NICTA?
Despite the explanation at the beginning of Record.thy, I have not yet understood how you
manage to state and prove O(n ^ 2) theorems (for the selector-updator rules) in
O(log(n)^2) step. In the end, there are O(n ^ 2) theorems, aren't there?
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:39):From: Thomas Sewell <thomas.sewell@nicta.com.au>
The "NICTA record problem" is with a single flat record that has a lot
of fields (~ 500 I think). I don't think we use record extensions much
at all. I've never seen a record extension more than 2 deep.
The change would impact syntax performance somehow, more work, or
different work. I don't understand the syntax layer at all though, so I
can't really comment on that.
There are less selector/updator pairs, but this essentially doesn't
matter. There are in any case far too many pairs (for a record with >
100 fields) to generate all the simp rules ahead of time. Anyway, only a
tiny proportion of them would be syntactically encountered. The record
simproc proves the relevant rules each time they are needed. The proof
of each one is O (log(n)), so we don't even bother to cache them.
Your suggested change would make this simproc proof process fire
multiple times for some cases where it currently fires once, but I think
the total amount of work would stay about the same, so I suspect the
performance impact would be minor.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Thomas,
Thanks for the clarification, I did not know that the theorems are only generated inside
the simproc on demand. This indeed adds some complication.
For the moment, I'll wait and see what Dmitriy's new tool for lifting BNFs over typedefs
brings and how he integrates the record selectors.
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC