next up previous contents index
Next: Cardinality Up: Mathematics Libraries Previous: Basic Definitions

Lists and Arrays

This  section presents a few basic objects from list theory and array theory. We start with the idea of a discrete  type, which is a type for which equality is decidable. Discreteness is required for the element comparisons that are needed, for example, in searching a list for a given element. Also, we need the idea that a proposition is decidable , i.e., that it is either true or false.

     discrete(<T:type>) ==
        all x,y:<T>. (x=y in <T>) | ~(x=y in <T>)
     < P: T->prop > is decidable on <T:type> ==
        all x:<T>. P(x) | ~P(x)
Figure gif gives two versions of the list head  function, which differ only on how they treat the empty list. The theorem statements following each definition define the behavior of the respective head function.

Figure: Definition of Head

The definition of the tail function  is straightforward.

     tl(<l:list>) == list_ind( <l>; nil; h,t,v. t )
Given a function of the appropriate type, the first theorem (named `` generalize_to_list'') listed in figure gif specifies the construction of another function that iterates the given function over a list. The object extracted from the proof is used in a function which sums the elements of a list.

Figure: Defining the Sum of a List of Integers

The definition of the membership predicate for lists uses a recursive proposition .

     <e:element> on <l:list> over <T:type> ==
        list_ind( <l>; void; h,t,v. (<e>=h in <T>) | v )
     >> all A:U1. all x:A. all l:A list.
           (x on L over A) in U1
The above type of use of list_ind to define a proposition is common and is worth a bit of explanation. Suppose that is some list whose elements come from a type T, and let e be in T. Then e on l over T evaluates to the type expression

this type (proposition) is inhabited (true) exactly when one of the is true.

The following is another example of a recursively defined proposition; it defines a predicate over lists of a certain type which is true of list l exactly when l has no repeated elements.

     <l:list> is nonrepetitious over <T:type> ==
        list_ind( <l>; one; h,t,v. ~(h on t over <T>) and v )
Given this definition, the following theorems are provable.
     >> all A:U1. nil is nonrepetitious over A
     >> all A:U1. all x:A. all l:A list.
          ~(x on l over A) & l is nonrepetitious over A
          =>  x.l is nonrepetitious over A

The next theorem defines a function which searches an array for the first occurrence of an element with a given property. (Arrays  are taken to be functions on segments of the integers.)

     >> all A:U1. all n:int. 
        all f:{1,...,n}->A. all P:A->prop.
           P is decidable on A
           => all k:int.
                 =>   all x:{1,...,k}. ~P(f(x))
                    | some x:{1,...,k}. P(f(x))
                        & all y:{1,...,x-1}. ~P(f(y))

next up previous contents index
Next: Cardinality Up: Mathematics Libraries Previous: Basic Definitions

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995