HOL: Description

Tree-Structured Finite Sets and Finite Maps

The source files behind this library are found in src/finite_maps. There are theories, generated by script files (with Script.sml suffixes): toto (total orders mapping pairs of objects into a ternary ordering type), enumeral (sets as binary trees), tc (transitive closure calculation via Warshall's algorithm) and fmapal (tree-based finite-map representation); along with supporting library files (with suffixes .sig and .sml): totoTacs, tcTacs, fmapalTacs, enumTacs. The library was written by F. Lockwood Morris.

For any type ty that has been equipped with a total order and a conversion for evaluating it, new terms of type ty set are provided which embody minimum-depth binary search trees. The primary objective has been to supply an IN_CONV for such terms with running time logarithmic in the cost of a single order comparison together with additional set operations which have reasonable running times.

Similarly, for ty as above and any type ty', new terms of type ty |-> ty' embody binary search trees, and enable a logarithmic-time FAPPLY_CONV and various other operations on finite maps.

Total orders: the type 'a toto

The use of binary search trees naturally requires that a total order be supplied for whatever type ty of elements [arguments] the sets [finite maps] are to have. Rather than the relation type ty -> ty -> bool, it is found computationally advantageous to use the type ty -> ty -> cpn, where cpn is the HOL datatype of three elements LESS, EQUAL, GREATER. A polymorphic defined type, 'a toto, has been created isomorphic to the class of functions : 'a -> 'a -> cpn satisfying a predicate totoTheory.TotOrd which axiomatizes total order-hood. The representation function for the type is called apto (for “apply total order”). Specifically what is needed in order to use ty as an element [argument] type is (the name of) an element of type ty toto, say tyto, and a conversion, say tyto_CONV, that will reduce terms of the form apto tyto x y to one of LESS, EQUAL, GREATER.

Provided in totoTheory are orders numto, intto, charto, stringto, and qk_numto (the last is an unnatural order on type num that should in principle be quicker to compute on NUMERAL terms than the usual order) with corresponding conversions numto_CONV, etc. Also, for lexicographic order on pairs, there are the object language function lextoto : 'a toto -> 'b toto -> ('a#'b)toto and the ML function lextoto_CONV : conv -> conv -> conv; if cva and cvb are conversions for evaluating terms that start apto toa ... and apto tob ... respectively, lextoto_CONV cva cvb is a conversion for evaluating terms starting apto (toa lextoto tob) ... . Similarly, there are listoto : 'a toto -> 'a list toto and listoto_CONV : conv -> conv. Inspection of listoto and listoto_CONV, possibly also of qk_numto and qk_numto_CONV, should make it feasible to define orders directly as toto's and corresponding conversions as needed for other HOL datatypes.

Additionally, given any linear order R : ty -> ty -> bool, if one supplies the theorem and definition

        lin_ord_thm:  |- LinearOrder $R
        toto_of_dfn:  |- cmp = toto_of_LinearOrder $R

and two conversions, say eq_conv for reducing equations of ground terms (of R's argument type) to T or to F, and lo_conv for reducing terms t R t' to T or to F, then

        toto_CONV lin_ord_thm toto_of_dfn eq_conv lo_conv

is a corresponding conversion for evaluating terms of the form apto cmp c c'.

Interpretation of binary trees as sets; IN_CONV

The datatype

        bt = nt | node of 'a bt => 'a => 'a bt

is defined with the objective of forming terms ENUMERAL cmp b, where cmp is a ty toto and b is a ty bt. These should justify the pair of theorems

⊢ ∀ cmp y. y ∈ ENUMERAL cmp nt ⇔ F

and

⊢ ∀ cmp x l y r.
     x ∈ ENUMERAL cmp (node l y r) ⇔
     case apto cmp x y of
       LESS  ⇒ x ∈ ENUMERAL cmp l
     | EQUAL ⇒ T
     | GREATER ⇒ x ∈ ENUMERAL cmp r

To make these theorems come out true requires the following definition of ENUMERAL:

⊢ (∀ cmp. ENUMERAL cmp nt = {}) ∧
   ∀ cmp l x r.
     ENUMERAL cmp (node l x r) =
     {y | y ∈ ENUMERAL cmp l ∧ (apto cmp y x = LESS)} ∪ {x} ∪
     {z | z ∈ ENUMERAL cmp r ∧ (apto cmp x z = LESS)} .

Invoking IN_CONV keyconv ``x IN ENUMERAL cmp b```, where keyconvis a conversion for evaluating applications ofcmp, will convert the term to whichever truth value the definition of ENUMERALcompels; that is, toTif and only if top-down tree search discoversxinb. Operations that create ENUMERALterms, discussed below, will ensure thatbis a well-formed binary search tree of minimal depth. (The newIN_CONV, if it is given an equality-deciding conversion and a set built with INSERTrather than atoto-evaluating conversion and an ENUMERALset, will revert topred_setLib.IN_CONV`.)

Translating between set representations

HOL offers two notations for explicit finite sets: the display notation {x1; ...; xn}, which is short for x1 INSERT ... INSERT xn INSERT {}, and notation with an explicit list: set [x1; ...; xn]. We provide here conversions back and forth between these:

        DISPLAY_TO_set_CONV: conv
        set_TO_DISPLAY_CONV: conv

and to create ENUMERAL sets from either:

        set_TO_ENUMERAL_CONV: conv -> term -> conv
        DISPLAY_TO_ENUMERAL_CONV: conv -> term -> conv

(these demanding a toto order on the element type and a conversion for evaluating it), and to recover either from an ENUMERAL:

        ENUMERAL_TO_set_CONV: conv -> conv
        ENUMERAL_TO_DISPLAY_CONV: conv -> conv

requiring only the order-evaluating conversion. Additionally,

        TO_set_CONV: conv -> conv

will normalize any of the three forms to the set [ ... ] form. (NO_CONV will suffice as the conversion argument if it is not an ENUMERAL that is to be normalized.) The conversions from the ENUMERAL form have to execute, for a well-formed $n$-element binary search tree, $n-1$ comparisons to verify that all the tree elements belong to the represented set; they will also succeed, in conformance with the definition of ENUMERAL, for ill-formed trees, if such are ever created, at the cost of between $2n$ and $3n$ comparisons.

Creation of an ENUMERAL form from either of the others entails sorting, performed by an $n\log n$ list-merging algorithm, followed by a detour through another datatype, 'a bl, which could as well have been ('a # 'a bt) option list, where the list element of index $k$, if present, consists of a full binary tree of $2^k - 1$ set elements and one more, which may be thought of as a root of which the full tree is the right subtree. A sorted linear list is copied into a bl by successive "BL_CONS" operations imitating the incrementation of a binary counter; when the copy is complete, it is collapsed into a single bt of which the biggest constituent full bt is indeed the right subtree. The upshot is that going from an ordered linear list to the ENUMERAL form is a linear-time operation, and that the bt in any ENUMERAL set has a unique shape for its size: that of a minimal-depth tree with all right subtrees full as one proceeds down the left spine.

Binary operations on sets

The functions

        UNION_CONV: conv -> conv
        INTER_CONV: conv -> conv
        SET_DIFF_CONV: conv -> conv

will work out applications of UNION, INTER, DIFF respectively to two ENUMERAL sets, given a conversion to evaluate the relevant order. UNION_CONV will revert to pred_setLib.UNION_CONV if that is what fits its arguments.

These operations work by list merging, hence with a linear number of comparisons. The strategy is to convert each input, say ENUMERAL cmp b, to a theorem,

        |- OWL cmp (ENUMERAL cmp b) l

asserting that it could have been created with set_TO_ENUMERAL_CONV from a certain list, which moreover is in strict ascending order:

      OWL
        |- !cmp s l. OWL cmp s l <=> (s = set l) /\ OL cmp l
      OL
        |- (!cmp. OL cmp [] <=> T) /\
           !cmp a l. OL cmp (a::l) <=>
                     OL cmp l /\ !p. MEM p l ==> (apto cmp a p = LESS) .

Underlying conversions OWL_UNION, OWL_INTER, OWL_DIFF, each of type conv -> thm -> thm -> thm, combine two such theorems to produce a third; the result, known to be ordered, is retransformed into an ENUMERAL term without further comparisons, as in the post-sorting steps of set_TO_ENUMERAL_CONV.

Explicit translations

        OWL_TO_ENUMERAL: thm -> thm
        ENUMERAL_TO_OWL: conv -> term -> thm
        set_TO_OWL: conv -> term -> term -> thm

between ENUMERAL terms and OWL theorems permit OWL_UNION, etc. to be invoked directly. (set_TO_OWL allows to create an OWL theorem from either a set [ ... ] term or a { ... } term without first making an ENUMERAL.)

In addition, there is

        SET_EXPR_CONV: conv -> conv

which, given a conversion to evaluate the order cmp, will work out the value of any set expression built up with UNION, INTER, and DIFF from ENUMERAL terms, avoiding intermediate translations.

Interpretation of binary trees as finite maps; FAPPLY_CONV

The treatment of finite maps parallels that of sets: the new terms denoting maps of type ty |-> ty' are terms FMAPAL cmp b, where cmp is a ty toto and b is a (ty#ty') bt. The theorems supporting tree search are

⊢ ∀ cmp x. FMAPAL cmp nt ' x = FEMPTY ' x

and

⊢ ∀ cmp x l a b r.
     FMAPAL cmp (node l (a,b) r) ' x =
     case apto cmp x a of
       LESS  ⇒ FMAPAL cmp l ' x
     | EQUAL ⇒ b
     | GREATER ⇒ FMAPAL cmp r ' x ,

and the definition of FMAPAL is

⊢ (∀ cmp. FMAPAL cmp nt = FEMPTY) ∧
   ∀ x v r l cmp.
     FMAPAL cmp (node l (x,v) r) =
     DRESTRICT (FMAPAL cmp l) {y | apto cmp y x = LESS} FUNION
     FEMPTY |+ (x,v) FUNION
     DRESTRICT (FMAPAL cmp r) {z | apto cmp x z = LESS} .

An invocation FAPPLY_CONV keyconv ``(FMAPAL cmp b) ' x```, where keyconvis a conversion to evaluate applications ofcmp, will yield the value paired with xifxis in the domain ofFMAPAL cmp b, or `` ``FEMPTY ' x`` `` if xis not to be found. IfFAPPLY_CONVis instead given an equality-deciding conversion and a termfmap [ ... ] ' x, it will produce the first value paired with x` in the list if any, FEMPTY ' x if none.

Translating between finite map representations

A compact list representation for finite maps is defined:

      fmap
        |- !l. fmap l = FEMPTY |++ REVERSE l

The point of the reversal is that l is now treated as an association list — in case of duplicated arguments, the pair nearest the front of the list will take precedence. Translating between fmap [ ... ] and FMAPAL cmp ... terms for finite maps we have

        fmap_TO_FMAPAL_CONV: conv -> term -> conv
        FMAPAL_TO_fmap_CONV: conv -> conv

the first of which demands the name of a toto-evaluating function as well as a conversion for computing its value.

Given a term FUN_FMAP f (set [ ... ]) and a conversion f_conv for working out applications of f,

        FUN_fmap_CONV: conv -> conv

will convert the term to the form fmap [ ... ], and

        FUN_FMAPAL_CONV: conv -> term -> conv -> conv,

which expects the conversion and term arguments to fmap_TO_FMAPAL_CONV followed by the conversion argument for FUN_fmap_CONV, will apply the latter and then the former to yield a FMAPAL term.

Binary operations involving finite maps

Parallel to the treatment of sets, a theorem representation of a finite map FMAPAL cmp b, namely

        ORWL cmp (FMAPAL cmp b) l,

asserting that it corresponds to a certain ordered list, is used for operations involving merging:

      ORWL
        |- !cmp f l. ORWL cmp f l <=> (f = fmap l) /\ ORL cmp l
      ORL
        |- (!cmp. ORL cmp [] <=> T) /\
           !l cmp b a. ORL cmp ((a,b)::l) <=>
                 ORL cmp l /\ !p q. MEM (p,q) l ==> (apto cmp a p = LESS) .

Functions

        FMAPAL_TO_ORWL: conv -> term -> thm
        ORWL_TO_FMAPAL: thm -> thm

translate between FMAPAL terms and ORWL theorems, and the latter can be produced directly from fmap [ ... ] terms by

        fmap_TO_ORWL: conv -> term -> term -> thm

which might find use, independent of finite maps, as a list sorting routine.

The only binary operation on FMAPAL terms is

        FUNION_CONV: conv -> conv

which will convert a term FUNION cmp (FMAPAL cmp b) (FMAPAL cmp b') to a FMAPAL term denoting a map defined on the union of the two domains, with the first argument map taking precedence where these overlap. But there are also two forms of domain restriction:

        DRESTRICT f s
        DRESTRICT f (COMP s)

for f a FMAPAL term and s an ENUMERAL term with the same order as f. A single conversion

        DRESTRICT_CONV: conv -> conv

will work out either of these forms to a FMAPAL result.

Like UNION_CONV, INTER_CONV, SET_DIFF_CONV, both FUNION_CONV and DRESTRICT_CONV entail two preliminary computations of FMAPAL_TO_ORWL or ENUMERAL_TO_OWL, a list-merging working part, one of

        ORWL_FUNION: conv -> thm -> thm -> thm
        ORWL_DRESTRICT: conv -> thm -> thm -> thm
        ORWL_DRESTRICT_COMPL: conv -> thm -> thm -> thm,

and a final use of ORWL_TO_FMAPAL. As with sets, the working parts may be used directly. Alternatively, translations between terms and theorems may be held to a minimum by the use of

        FMAP_EXPR_CONV: conv -> conv

on any expression built up with FUNION, DRESTRICT, and COMP from compatible FMAPAL and ENUMERAL terms.

Other operations on finite maps

The following operations on FMAPAL terms have no need to translate to the ORWL theorem form; two of them are unconcerned with the total ordering.

The conversion

        FDOM_CONV: conv

will reduce any term FDOM (FMAPAL ... ) to the isomorphic ENUMERAL ... , also any term FDOM (fmap [ ... ]) to set [ ... ].

The conversion-valued functon

        IN_FDOM_CONV: conv -> conv,

given a conversion to evaluate the applications of cmp, will reduce any term x IN FDOM (FMAPAL cmp b) to a truth value, or if given an equality-deciding conversion, it will reduce a term x IN FDOM (fmap [ ... ]) to a truth value.

The conversion-valued function

        o_f_CONV: conv -> conv,

given a conversion for working out applications of the function f, will reduce a term f o_f (FMAPAL ... ) to an isomorphic FMAPAL term, alternatively a term f o_f fmap [ ... ] to an isomorphic fmap term.

Similarly,

        FUPDATE_CONV: conv -> conv

expects either a cmp-evaluating conversion and a term FMAPAL cmp b |+ (x, y) or an equality-deciding conversion and a term fmap [ ... ] |+ (x, y), and if x is already in the domain of the finite map, will produce an isomorphic structure in which the value paired with x has been replaced by y. If x is not in the domain of the finite map, an error is reported.

It may be noted that FUN_FMAPAL_CONV, FAPPLY_CONV, and FUPDATE_CONV combine to provide a functional array facility with logarithmic number of index comparisons for both reading and writing.

An application: transitive closure

The idea of Warshall's algorithm for transitive closure of a relation, to build up an approximation to the answer by repeatedly allowing one fresh element as an intermediate stop in building a path between any two elements, is captured by the definition

subTC R s x y ⇔
  R x y ∨ ∃ a b. (R ^|^ s)* a b ∧ a ∈ s ∧ b ∈ s ∧ R x a ∧ R b y

where $\left(R\right.$ ^|^ $\left.s\right)^*$ denotes the reflexive transitive closure of the relation $R$ restricted fore and aft to the set $s$, and by the theorem (note that it is a set equation, as the Curried relations have been given only one argument)

⊢ ∀ R s x a. subTC R (x INSERT s) a =
     if x ∈ subTC R s a then subTC R s a ∪ subTC R s x else subTC R s a .

A representation of finite relations by set-valued finite maps is defined by

      FMAP_TO_RELN (f:'a |-> 'a set) x = if x IN FDOM f then f ' x else {}.

The conversion-valued function

        TC_CONV: conv -> conv,

given a conversion for evaluating cmp, will transform a term

        (FMAP_TO_RELN (FMAPAL cmp ... ))^+,

where the bt "..." stores (element, ENUMERAL) pairs, to the form FMAP_TO_RELN (FMAPAL cmp ...... ), or given an equality-deciding conversion, will turn

        (FMAP_TO_RELN (fmap [ ... ]))^+,

where now "..." is a list of elements paired with { ... } sets, into FMAP_TO_RELN (fmap [ ....... ]). It is because TC_CONV uses only the operations TO_set_CONV, IN_CONV, UNION_CONV, FDOM_CONV, and o_f_CONV that it is insensitive to which pair of representations is chosen for finite maps and sets.

As a convenience in preparing the tree-structured representation of a finite relation, the conversion

        ENUF_CONV: conv -> term -> conv,

given a conversion for evaluating a toto and its name, will convert a term fmap [ ... ] whose list members pair elements with either { ... } sets or set [ ... ] sets into a FMAPAL term with ENUMERAL values.