If you understand what the package is doing (and I admit that this is not
easy), then the behaviour of the simplifier on big records is in turn fairly
understandable.
The advantage of the package is not suffering a quadratic blow-up in elapsed
time and theorem sizes (in turn leading to quadratic theory sizes and similar
time in loading said theories) when defining the record type. The simplifier’s
normalisation of record expressions is also an implementation of bubble sort,
so there are conceivably simplification scenarios which might exhibit quadratic
time costs.
All that said, I think that there’s probably a strong case for simply forcing
users to suffer (perhaps with warning messages), and encouraging them to define
nested records themselves to group related fields of their super-large records.
They would thus be manually doing what the big record package is doing not
quite invisibly.
Pull requests gratefully accepted.
Michael
From: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
Date: Wednesday, 6 June 2018 at 19:18
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] big records
Dear HOL users,
Does anyone know how to use the big record package? I always find I want to
turn it off (by increasing the big record size to above the max number of
fields in my types) because many things don't work on big records (in
particular the simplifier and EVAL) whereas they do work on "small" records.
Would it be OK to disable the big record package by default (e.g., set the size
limit to "infinity" by default)? Or would it be easy to make the above tooling
work for big records too? What are the advantages of big records anyway?
Cheers,
Ramana
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
