Email Gateway (Aug 22 2022 at 20:21): Email Gateway (Aug 22 2022 at 20:21):From: Fabian Immler <immler@in.tum.de>
On 8/5/2019 3:37 PM, mailing-list anonymous wrote:
I would like to understand if one was to, hypothetically, implement a
large-scale overhaul of HOL-Algebra using the modern locale features, what
would the structure of the new library look like?
I never thought about what a "modern" HOL-Algebra would look like.
However, I am still not certain as to what would be the best way to
structure the set-based library. At the moment, the development follows the
approach that merely extends the locales that exist in the main HOL library
with an additional locale parameter that represents a carrier set (or
several locale parameters for multiple carrier sets) - this approach is
consistent with the existing library of relativised results (primarily,
about vector spaces) that was previously developed by Bohua Zhan and Fabian
Immler. This approach, straightforward as it may seem, has several
problems.
All I can say is that we chose the locale-with-carrier approach not
because we thought it was a superior structuring mechanism, but because
it was easier to deal with in the context of relativising results
automatically (e.g., no need to transfer record types).
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 20:21):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi,
Here are my thoughts on this topic. I have played around with various
options that you mention and I also ran into the problems you mentioned.
Records in Isabelle/HOL provide only one extension slot. So fields must
be added linearly. You cannot have one record (such as partial_object)
be extended independently (ord and topology) and then later combine
them. To do that smoothly, we would need to have a unification mechanism
that can work modulo type isomorphisms, which basically adds the
conversions as needed. The coercions functionality implements something
like that, but I could never get this to work properly because the
conversions are added during parsing and not during reasoning. I'm
pretty sure, though, that one could implement such a coercion insertion
algorithm, at least for first-order unification or higher-order pattern
matching, in Isabelle/ML. Yet, this would not be integrated with all the
proof methods (simp, clarify, auto, ...) and therefore of little use.
In my AFP entry Monomorphic_Monad [1], I therefore gave up on using
records and went for listing every parameter individually. I found that
I could get a long way by judiciously using nested
"context fixes ... begin" with interspersed "interpretation" commands.
This approach works well with higher-order unification and all proof
tools. The main drawback is that the terms get rather large, in
particular if you stack several algebraic constructions on top of each
other. Consequently, type checking the terms and folding the
abbreviations for displaying terms may get slow.
If your types are sufficiently distinct, the notation problem can be
worked around with adhoc_overloading as follows:
consts plus :: "'a => 'a => 'a"
notation plus (infixl "\<oplus>" 65)
context
fixes plus1 :: "'a => 'a => 'a"
and plus2 :: "'b => 'b => 'b"
begin
adhoc_overloading plus plus1
adhoc_overloading plus plus2
You can now use \<oplus> for both plus1 and plus2 in your lemmas
provided that type inference can unoverload all occurrences. You may
have to add occasional type constraints. Clearly, this does not work if
the types overlap.
Finally, here's another proposal that might be worth a try: unrestricted
overloading. If Isabelle/HOL had multi-parameter type classes, we could
formalize all these things as type classes. In Haskell, we'd say
class PartialObject a b where carrier :: a => b set
with a dependency from a to b, i.e., if a is known, then so is b. In
Isabelle/HOL, type class operations may only have one type parameter, so
this does not work directly. However, type classes are internally
implemented with unrestricted overloading + some type inference magic.
So we can achieve something if we don't care too much about the type
inference convenience. Here's a sketch:
consts
carrier :: "'a => 'b set"
le :: "'a => 'b => 'b => bool"
tau :: "'a => 'b set => bool"
Here, the algebraic structure is left abstract as "'a" and you phrase
all your definitions and theorems such that the structure is always an
abstract type.
For example, to specify that a structure of type 'a is an order on
elements of type 'b, you'd write
definition order :: "'a itself => 'b itself => bool" where
"order G _ = (ALL x :: 'b. x \<in> carrier G --> le G x x) & ..."
In practice, you'll have to add many type constraints to guide type
inference into the right direction. This can be alleviated with custom
syntax that shortens the type syntax. An example for this is the
CARD('a) syntax from HOL-Library.Cardinality [2]. So you'd write
"ORDER('b) G"
instead of
"order G (Pure.type :: 'b itself)"
and "CARRIER('b) G" instead of "carrier G :: 'b set"
Combining two structures in this way is then very simple, as the
definitions and proofs do not assume any particular repesentation of the
structure. Accordingly, I'd recommend to also do constructions
abstractly. For example, the product construction would look like
datatype ('a1, 'a2) product = Product (proj1: 'a1) (proj2: 'a2)
overloading
carrier_product == "carrier :: ('a1, 'a2) product => ('b1 * 'b2) set"
begin
definition carrier_product :: "('a1, 'a2) product => ('b1 * 'b2) set"
where
"carrier_product G =
CARRIER('b1) (proj1 G) <*>
CARRIER('b2) (proj2 G)"
end
Here, I've introduced a separate type "product" for the generic product
construction such that we keep the types of abstract constructions (like
products) separate from types that may show up in normal applications
(like the type constructor for pairs).
Hope this helps,
Andreas
[1] https://www.isa-afp.org/entries/Monomorphic_Monad.html
[2]
http://isabelle.in.tum.de/repos/isabelle/file/5c1b2f616d15/src/HOL/Library/Cardinality.thy#l33
Email Gateway (Aug 22 2022 at 20:22):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Fabian Immler and Andreas Lochbihler,
Thank you very much for your replies.
I believe that records with the support for multiple inheritance would
be exceptionally useful for Isabelle/HOL users. However, I guess, it
would be too much to hope that this technology will become available
in the near future.
Having, to an extent, tried the various approaches that I was aware of
before asking the question and, also, the methods suggested by Andreas
Lochbihler, I am beginning to converge on the thought that, for my use
case, the best methodology might be the one that I am already using
(i.e. the methodology similar to the one used by Bohua Zhan and Fabian
Immler in their development). Unfortunately, by now, I have completely
convinced myself that records are not suitable for libraries with
complex locale inheritance trees, primarily, due to the absence of
support for multiple inheritance.
I liked the method proposed by Andreas Lochbihler that uses constants
parameterised by the spaces/algebraic structures themselves. However,
even ignoring the problem of the type inference, I am not certain how
would one deal with the interpretation of the theorems stated for the
parametric constants using suitable arbitrary user-supplied terms.
Would it not be necessary for the users to combine and abstract the
terms as an element of some newly designed type before the can be
achieved? In this case, as it seems, making the interpretation
mechanism as convenient for the users as the locale interpretation for
the approach that is used at the moment would require a substantial
amount of effort for the developer.
Thank you
Email Gateway (Aug 22 2022 at 20:27):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to ask a question in the context of one of the existing
threads:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-April/msg00090.html
.
To set the context for the question, I would like to provide two quotes
from the aforementioned thread:
On Fri, 12 Apr 2019 22:36:17 Clemens Ballarin wrote:
>
... The approach of combining locales with records dates back to that time.
Definitions in locales were unavailable, and the solution was to extract
the signature part of an algebraic structure into a record, on which
definitions could be made globally. ...
On Fri, 12 Apr 2019 22:51:32 Manuel Eberl wrote (in reply to the comments
made by Clemens Ballarin on Fri, 12 Apr 2019 22:36:17):
>
... That's interesting. It would certainly be of interest to think of a
large-scale overhaul of HOL-Algebra using modern locale features. ...
I would like to understand if one was to, hypothetically, implement a
large-scale overhaul of HOL-Algebra using the modern locale features, what
would the structure of the new library look like? Would the records still
be used or would it be implemented in the style of the main HOL library
with all parameters stated explicitly and all definitions stated implicitly
in the locale context? Would it be too much to ask to provide a small
example that demonstrates this modern approach based on the existing
locales in HOL-Algebra?
The primary reason why I am asking the question is that I would like to
understand what is considered to be a canonical methodology for the
implementation of a library about abstract spaces/algebraic structures with
the explicit carrier sets using locales.
I provide further (and, perhaps, superfluous) details with regard to my
enquiry. I am working on the relativization of the main HOL library using
Types-To-Sets: https://github.com/xanonec/HOL-SML-Relativization. I believe
that this development directly addresses some of the existing concerns of
the users of HOL. For example, in the context of the previously referenced
thread:
On Sat, 13 Apr 2019 10:37:23 Dominique Unruh wrote:
The classes have the advantage of being easier to use than locales in many
cases (at least I feel that way), but they have the limitation of always
having UNIV as the carrier.
As far as I know, all proofs are simply done twice. And someone building a
development on these things needs to pick on approach and is then "locked
in", which is problematic, since some material is only available in the HOL
approach and some only in the HOL-Algebra approach. In case of an overhaul,
perhaps these concepts could be unified as well?
My own development, effectively, unifies both approaches using
Types-To-Sets as the conceptual glue. The proofs of the set-based theorems
no longer need to be stated explicitly: the type-based theorems from the
main library are converted to the set-based theorems automatically.
Moreover, the adopted methodology explicitly establishes an injection
(potentially, there can be several distinct relativisations of the same
type-based theorem) from the set-based theorems to the type-based theorems
and this injection can be visualised using the features of the framework.
However, I am still not certain as to what would be the best way to
structure the set-based library. At the moment, the development follows the
approach that merely extends the locales that exist in the main HOL library
with an additional locale parameter that represents a carrier set (or
several locale parameters for multiple carrier sets) - this approach is
consistent with the existing library of relativised results (primarily,
about vector spaces) that was previously developed by Bohua Zhan and Fabian
Immler. This approach, straightforward as it may seem, has several
problems. Firstly, whenever reasoning about the spaces/algebraic structures
themselves, the long list of the locale parameters always needs to be
provided explicitly in each theorem. This problem is exaggerated further
whenever dealing with pairs/triples of spaces/algebraic structures - the
lists of parameters can become dramatically long. For example, a context
that describes a pair of complete lattices would look similar to (of
course, explicit context can be replaced with a locale named, for example,
complete_lattice_pair_ow, but the problem remains the same)
context
fixes πA :: "'at set"
fixes πB :: "'bt set"
fixes lea leb
and lsa lsb
and infa infb
and supa supb
and bota botb
and topa topb
and Infa Infb
and Supa Supb
assumes clow_a: "complete_lattice_ow πA Infa Supa infa lea lsa supa bota
topa"
assumes clow_b: "complete_lattice_ow πB Infb Supb infb leb lsb supb botb
topb"
Furthermore, the notation associated with the locale parameters for a
single space/algebraic structure, as far as I know, cannot be reused
directly when dealing with pairs/triples of spaces/algebraic structures due
to overlaps. Also, I am not aware of any methodology that would enable one
to make the notation associated with the locale parameters to depend on,
for example, other locale parameters. In the context of the example above,
if one is to define the notation for Infa as (βΉβ¨
β©oβ©wβ©aβΊ), then it becomes
non-sensical if πA is interpreted as a set named πB and πB is
interpreted as a set named πA. The same problem also occurs when trying to
transfer the notation for the implicit definitions (i.e. definitions stated
in a locale context) from a single space/algebraic structure to a pair of
spaces/algebraic structures. Moreover, even restating the notation for the
locale parameters and implicit definitions when providing the locales for
the pairs/triples of algebraic structures/abstract spaces can be a very
irritating, tedious and error-prone process that results in a substantial
amount of seemingly boilerplate code.
I believe that the use of records/schemes with the explicitly stated
definitions (i.e. outside of the context of locales), as archaic as it may
seem, resolves all of the aforementioned issues. However, the lack of
support for multiple inheritance creates its own problems. While in some
cases, using a scheme that has more fields than necessary is bearable (as
the referenced example from HOL-Algebra demonstrates), in certain cases, it
becomes impossible. For example, in my attempt to use records/structures in
the library of relativised results, I defined
record 'a ord = "'a partial_object" +
le :: "['a, 'a] β bool" (infix βΉβΔ±βΊ 50)
ls :: "['a, 'a] β bool" (infix βΉβΔ±βΊ 50)
and
record 'a topology = "'a partial_object" +
Ο :: "'a set β bool" (βΉΟΔ±βΊ)
Now, I would like to define an order topology. It does not seem that
records provide a natural way to combine the two concepts together. The
best methodology that I was able to come up with is exhibited via the
following locale that uses two structures:
locale order_topology_ow =
order_ow πͺ for πͺ :: "('at, 'bt) ord_scheme" (structure) +
fixes π― :: "('at, 'bt) topology_scheme" (structure)
and π :: "'at set"
assumes ππͺ: "π = carrier πͺ"
and ππ―: "π = carrier π―"
and open_generated_order:
"s β π βΉ Οβπ―β s = generate_topology_on ((Ξ»a. {..βa}) π βͺ (Ξ»a.
{aβ..}) π) π s"
In my view, this approach is still better than providing all definitional
elements explicitly. However, this approach is still quite limiting and, in
certain cases, even the list of schemes can become quite long.
I would be curious to know if anyone has dealt with similar problems in the
past and knows a solution that is better than using explicitly listed
parameters. Alternatively, perhaps, someone could suggest a canonical
approach for combining two distinct schemes into one scheme with a 'shared'
field.
Thank you
Email Gateway (Aug 22 2022 at 20:29):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to submit a short errata for two of my posts in the thread
"Revisiting records, structures, locales, abelian_group, HOL-Algebra and
Types-To-Sets". Unfortunately, recently, I noticed that my posts contain
two grievous errors (I believe that it is best to classify them as
typographical errors because I am unable to identify their root cause):
The first error occurs in the statement of the question (
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-August/msg00006.html
):
... the adopted methodology explicitly establishes an injection
(potentially, there can be several distinct relativisations of the same
type-based theorem) from the set-based theorems to the type-based theorems
...Of course, the excerpt above can be interpreted as equivalent to
(βf::sb_to_tb. injective f) β§ (βf::sb_to_tb. Β¬injective f) and, of course,
my goal was to emphasize that a function that maps the set-based theorems
to their type-based counterparts (represented as a term of a type sb_to_tb
above) is not, necessarily, injective. I am not certain why I stated that
the function of this type is always injective immediately before stating
that there exist non-injective functions of this type.
The second error occurs in my first answer in the thread (
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-August/msg00020.html
):
...locale inheritance trees...
Of course, I meant to use the word 'graphs' instead of the word 'trees' and
the phrase 'sublocale relations' instead of 'locale inheritance'.
Please accept my sincere apologies for making these errors. I will try to
be more careful in the future.
Thank you
On Mon, Aug 5, 2019 at 4:37 PM mailing-list anonymous <
mailing.list.anonymous@gmail.com> wrote:
Dear All,
I would like to ask a question in the context of one of the existing
threads:https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-April/msg00090.html
.To set the context for the question, I would like to provide two quotes
from the aforementioned thread: ...--
Please accept my apologies for posting anonymously. This is done to
protect my privacy. I can make my identity and my real contact details
available upon request in private communication under the condition that
they are not to be mentioned on the mailing list....
Last updated: Nov 21 2024 at 12:39 UTC