Re: [isabelle] Revisiting records, structures, locales, abelian_group, HOL-Algebra and Types-To-Sets



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:

1. Define an uninterpreted constant for each operation of the right arity and attach the notation to it. For example,

consts plus :: "'a => 'a => 'a"
notation plus (infixl "\<oplus>" 65)

2. Register on demand the operations for which you want to use the notation:

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

Am 05.08.2019 um 15:37 schrieb mailing-list anonymous:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.