Computer Aided Formal Reasoning 1996/7 Lecture notes 14 and 15 Judith Underwood

Abstract Data Types in Type Theory

We have seen how we can give a specification for a function through its type, as in the integer square root function

{x:nat}<y:nat> (and (Le (times y y) x)
                    (Lt x (times (suc y) (suc y))))

Today we shall use the descriptive power of type theory to describe abstract data types and their implementations.

An abstract data type (ADT) is a description of a data structure and the operations on it. Using abstract data types prevents programs from relying on details of the implementation of a data structure, thus allowing modification of the data structure’s implementation without requiring modification of other parts of the code.

A specification of an abstract data type has two parts: a signature which gives names (and usually types) to the operations on the ADT and some axioms which describe the behaviour of the operations. In type theory, of course, these axioms are types as well. For example, to specify the data type of stacks of natural numbers we would say something like:

(* signature *)
empty : Stack
push  : nat -> Stack -> Stack
pop   : Stack -> Stack
top   : Stack -> nat
(* axioms *)
{n:nat}{s:Stack} pop (push n s) = s
{n:nat}{s:Stack} top (push n s) = n
pop empty = empty
top empty = zero

The last two axioms ensure that pop and top are defined for all stacks. An implementation of this ADT is a choice of a carrier set for Stack along with functions empty, push, pop, and top which satisfy the axioms.

How can we represent this in Lego? The first problem is to give a type to the type of stacks. This is not as easy as it might seem. The first impulse would be to say Stack:Type, so that any implementation of Stack will be a type. Notice, however, that the equality = in the axioms must apply to stacks; we will not, in general, want this equality to be the equality in the type used to implement the ADT. Instead, we want an abstract equality which agrees with the axioms for the type. The idea is that if we are specifying a new type, we must also specify the equality relation on that type.

So, instead of Stack:Type, we will introduce a new type of “types with equality”. We call this a Setoid, and it is defined in lib_setoid as follows:

Record [Setoid:SET]
Fields [dom:SET]
       [eq1:dom->dom->Prop];
[eq [S|Setoid] = eq1 S];

This definition uses the Lego Record constructor, which makes a record out of the given fields by introducing a record constructor

make_Setoid : {dom:SET}(dom->dom->Prop)->Setoid

and projections

dom:Setoid -> SET
eq1:{S:Setoid}S.dom->S.dom->Prop

Lego actually generates a general elimination rule

Setoid_elim: {P:Setoid->TYPE}
    ({dom:SET}{eq1:dom->dom->Prop}P (make_Setoid dom eq1))->
    {z:Setoid}P z

along with a computation rule for Setoid_elim The projection functions dom and eq1 are then defined in terms of Setoid_elim.

Note that given S:Setoid, we may write S.dom and S.eq as is common with records; this is because Lego considers S.eq to be the same as eq S. The defined eq is just eq1 with S as an implicit argument. It is not actually specified here to be an equivalence relation – we will add that later.

Given this record type Setoid as “types with equality” (really “types with a relation”), we can now say what type Stack should be. We can also rewrite the axioms to use the appropriate equality, and require that the stack’s eq actually be an equivalence relation.

Stack : Setoid
empty : Stack.dom
push  : nat -> Stack.dom -> Stack.dom
pop   : Stack.dom -> Stack.dom
top   : Stack.dom -> nat
Equivalence (eq|Stack)
(* Recall eq|Stack = eq1 Stack *)
(* Equivalence is defined in lib_logic :
 Equivalence = [T|Type][R:T->T->Prop]and3 (refl R) (sym R) (trans R) *)
{n:nat}{s:Stack.dom} eq (pop (push n s))  s   (* eq on stack *)
{n:nat}{s:Stack.dom} Eq (top (push n s))  n   (* Eq on nat *)
eq (pop empty) empty    (* eq on stack *)
Eq (top empty) zero     (* Eq on nat *)

To collect the elements of the signature and the axioms into manageable entities, we combine the signature into a record structure:

(* structure type *)
Record [Str_STACK:STR] ElimOver Type
Fields [Stack:Setoid]
       [empty:Stack.dom]
       [push :nat->Stack.dom->Stack.dom]
       [pop  :Stack.dom->Stack.dom]
       [top  :Stack.dom->nat];

and we name the axioms and combine them with and:

(* axioms *)
[S:Str_STACK];
[EqSTACK  = Equivalence (eq|S.Stack)];
[AxSTACK1 = eq (S.pop S.empty) S.empty];

[AxSTACK2 = Eq (S.top S.empty) zero];
[AxSTACK3 = {n:nat}{s:S.Stack.dom}eq (S.pop (S.push n s)) s];
[AxSTACK4 = {n:nat}{s:S.Stack.dom}Eq (S.top (S.push n s)) n];
[Ax_STACK = and5 EqSTACK AxSTACK1 AxSTACK2 AxSTACK3 AxSTACK4];
Discharge S;

We now have a representation of the signature as a single record type Str_STACK and the axioms packaged together in Ax_STACK. (Note that since we abstracted S, Ax_STACK is really of type Str_STACK->Prop.) We combine these into a specification using make_SPEC:

[STACK = make_SPEC Str_STACK Ax_STACK];

. This makes a record of type SPEC with two fields, Str (structure) and Ax. The declaration of

SPEC is in lib_adt_basics:
Record [SPEC:Type] ElimOver Type
Fields [Str:STR]
       [Ax: Str->Prop];

Now we describe a concrete implementation of stacks, using lists. The first goal is to produce an element listStack of Str_STACK; we then verify that the axioms hold for listStack.

Goal listStack : Str_STACK;
Refine make_Str_STACK;
Lego> Refine make_Str_STACK;
Refine by  make_Str_STACK
  ?1 : Setoid
  ?2 : dom ?1
  ?3 : nat->(dom ?1)->dom ?1
  ?4 : (dom ?1)->dom ?1
  ?5 : (dom ?1)->nat
Refine make_Setoid (list nat) (Eq|(list nat));
          (* domain is (list nat) and Eq as eq *)
Refine (nil nat);              (* empty stack *)
Refine cons;                   (* push *)
Refine tail;                   (* pop *)
Refine hd zero;                (* top *)
Save listStack;

The functions hd and tail are from lib_list_basics.

Verifying the implementation is straightforward. We first prove each axiom separately, then package them together.

Goal eqStackL :
     (EqSTACK listStack);
Refine pair3;
Refine Eq_refl; Refine Eq_sym; Refine Eq_trans;
Save;
Goal axStack1L :
     (AxSTACK1 listStack);
Refine Eq_refl;
Save;
(* etc. *)

Goal listStack_correct : (Ax_STACK listStack);
Refine pair5; Refine eqStackL;
Refine axStack1L; Refine axStack2L;
Refine axStack3L; Refine axStack4L;
Save;

Now suppose we try to prove some general properties of stacks. We will quickly find that our specification is insufficient to show that, for example,

(eq s s') -> eq (push n s) (push n s')

This is because although eq is an equivalence relation, we do not have a guarantee that it is a congruence. So now we may wish to extend the specification with a new axiom about eq describing the fact that equality is respected by all stack operations.

[S:Str_STACK];
[RespSTACKpush= {n,m:nat}{s,s':S.Stack.dom}
     (Eq n m)->(eq s s')->eq (S.push n s) (S.push m s')];
[RespSTACKpop = {s,s':S.Stack.dom}
     (eq s s')->(eq (S.pop s) (S.pop s'))];
[RespSTACKtop = {s,s':S.Stack.dom}
     (eq s s')->(Eq  (S.top s) (S.top s'))];
[RespSTACK    =
     and3 RespSTACKpush RespSTACKpop RespSTACKtop];
Discharge S;

Fortunately, we do not need to redo everything – the Lego ADT library includes operations for manipulating specifications, so that to create a new specification for stacks with a congruence relation we need only say:

[STACK_CONG = Extend_AxOnly STACK RespSTACK];

This just adds the new axiom RespSTACK to the other axioms, using and. We can also reuse the correctness proof, once we have verified the extra axiom:

Goal respStackL :  (RespSTACK listStack);
Refine pair3;
Expand RespSTACKpush; intros; Qrepl H; Qrepl H1; Refine Eq_refl;
Expand RespSTACKpop;  intros; Qrepl H; Refine Eq_refl;
Expand RespSTACKtop;  intros; Qrepl H; Refine Eq_refl;
Save;
Goal listStack_correct_cong : STACK_CONG.Ax listStack;
Refine pair; Refine listStack_correct; Refine respStackL;
Save;

Next time we will look at the tools for ADT manipulation in more detail; we will also see how to implement one ADT by another (abstract implementation).

Abstract Data Types, Part II

Today we’ll continue to look at abstract data types and their implementations; we’ll then examine specifications in general and tools available for developing a specification into an implementation.

Abstract Implementation

Last time we saw how to give a concrete implementation of an abstract data type and check that it satisfies the axioms in the specification. As an example, we looked at implementing stacks of natural numbers with the type list nat. We can also use one abstract data type to give an abstract implementation of another, and we will demonstrate this by using an abstract data type for arrays to implement stacks.

First, we describe the ADT for arrays (of natural numbers). We begin with the structure:

(* structure type *)
Record [Str_ARRAY:STR] ElimOver Type
Fields [Array   :Setoid]
       [newarray:Array.dom]
       [assign  :nat->Array.dom->nat->Array.dom]
       [access  :Array.dom->nat->nat];

Recall that Array:Setoid means Array is a type with equality. There are three array operations. First, newarray is an array with all elements zero (as we shall see). Second, assign, given a natural number n, an array A, and an index i, returns a new array identical to A except with A[i] set to n. Finally, access, given A and i, returns the value of A[i].

These intended behaviours are described by the axioms in the specification:

(* axioms *)
[A:Str_ARRAY];
[EqARRAY  = Equivalence (eq|A.Array)];
[AxARRAY1 = {i:nat}Eq (A.access A.newarray i) zero];
[AxARRAY2 = {n,i,j:nat}{arr:A.Array.dom}
    and ((Eq i j) ->
          (Eq (A.access (A.assign n arr i) j) n))
        ((not (Eq i j)) ->
          (Eq (A.access (A.assign n arr i) j) (A.access arr j)))
];
[Ax_ARRAY = and3 EqARRAY AxARRAY1 AxARRAY2];
Discharge A;
[ARRAY = make_SPEC Str_ARRAY Ax_ARRAY : SPEC];

Now we will use this ADT to provide an abstract implementation for stacks. Recall the (simple) ADT for stacks was:

Record [Str_STACK:STR] ElimOver Type
Fields [Stack:Setoid]
       [empty:Stack.dom]
       [push :nat->Stack.dom->Stack.dom]
       [pop  :Stack.dom->Stack.dom]
       [top  :Stack.dom->nat];
(* axioms *)
[S:Str_STACK];
[EqSTACK  = Equivalence (eq|S.Stack)];

[AxSTACK1 = eq (S.pop S.empty) S.empty];
[AxSTACK2 = Eq (S.top S.empty) zero];
[AxSTACK3 = {n:nat}{s:S.Stack.dom}eq (S.pop (S.push n s)) s];
[AxSTACK4 = {n:nat}{s:S.Stack.dom}Eq (S.top (S.push n s)) n];
[STACK = make_SPEC Str_STACK Ax_STACK : SPEC];

To give an abstract implementation of stacks using arrays, we provide a function from ARRAY.Str

to STACK.Str:
Goal refine_STACK_to_ARRAY :
     ARRAY.Str -> STACK.Str;
Intros A;
Lego> Refine make_Str_STACK;
Refine by  make_Str_STACK
  ?2 : Setoid
  ?3 : dom ?2
  ?4 : nat->(dom ?2)->dom ?2
  ?5 : (dom ?2)->dom ?2
  ?6 : (dom ?2)->nat

The idea is that a stack is a pair consisting of an array and a pointer to the array element just beyond the top of the stack. The pointer will be represented by a natural number, so that if the pointer is zero, we have the empty stack. We must describe these pairs and the intended equality on them in the Setoid part of the implementation:

Lego> Refine make_Setoid;
Refine by  make_Setoid
  ?7 : SET
  ?8 : ?7->?7->Prop
  ?3 : dom (make_Setoid ?7 ?8)
  ?4 : nat->(dom (make_Setoid ?7 ?8))->dom (make_Setoid ?7 ?8)
  ?5 : (dom (make_Setoid ?7 ?8))->dom (make_Setoid ?7 ?8)
  ?6 : (dom (make_Setoid ?7 ?8))->nat

The domain is a pair consisting of the carrier set of Array, extracted from A, along with nat. To make future goals look nicer, we give it a name:

[domImpl =  A.Array.dom # nat];
Lego> defn  domImpl = (dom (Array A))#nat
      domImpl : Type
Lego> Refine domImpl;
Refine by  domImpl
  ?8 : domImpl->domImpl->Prop

We now need to supply the equality predicate on these stacks; we’ll do this explicitly, by defining

eqImpl:
(* equality over the impl domain *)
[eqImpl [s,s':domImpl] =
       and (Eq s.2 s'.2)
          ({i:nat}(Lt i s.2)->
              (Eq (A.access s.1 i) (A.access s'.1 i)))];
Lego> Refine eqImpl;
Refine by  eqImpl
  ?3 : dom (make_Setoid domImpl eqImpl)

  ?4 : nat->(dom (make_Setoid domImpl eqImpl))->
                        dom (make_Setoid domImpl eqImpl)
  ?5 : (dom (make_Setoid domImpl eqImpl))->dom (make_Setoid domImpl eqImpl)
  ?6 : (dom (make_Setoid domImpl eqImpl))->nat

This says that two array-stacks are equal when their pointers are equal (as natural numbers) and for all indices i less than the pointer value, the arrays are equal at i.

The remainder of the implementation is fairly straightforward. The empty stack is

(A.newarray,zero)

push n s is implemented by assign:

(A.assign n s.1 s.2,suc s.2)

The new stack consists of the old array s.1 with place s.2 set equal to n. Note that push also increments the pointer (s.2).

pop s just decrements the pointer:

(s.1, pred s.2)

and top s returns either zero or the top of the stack if the pointer is nonzero. Recall that the pointer is the successor of the position of the top element of the stack.

if_zero s.2 zero (A.access s.1 (pred s.2));

The proof that, given an A:ARRAY.Str, the resulting implementation of stacks satisfies the axioms is reasonably straightforward.

General specification operations

Specification languages often include tools for manipulating specifications. These can be reflected in type theory as well. We can also describe some semantic properties we wish specifications to have. The definitions in this section are from lib_adt, which imports lib_sigma and lib_setoid. lib_sigma redefines sigma types as an inductive type and introduces fresh notation for working with them.

The basic definitions in the library are:

[STR = Type];                           (* class of structure types *)
(* class of specifications/ADTs *)
Record [SPEC:Type] ElimOver Type
Fields [Str:STR]
       [Ax: Str->Prop];
[Spec[S:STR]  = S->Prop];                   (* class of S-specifications *)
[Mod [SP:SPEC]= Sigma SP.Str SP.Ax];      (* model set of SP with proofs *)
[Consistent [SP:SPEC] = Ex [s:SP.Str] SP.Ax s]; (* consistency of a spec *)

The idea is that Mod SP is the type of models of the specification; a specification is consistent if it has a model.

We saw last time that we may wish to extend a specification with extra information – either by simply adding an axiom or by extending the signature as well. To extend the structure part of a specification, we combine the parts with a sigma type:

[Extend [SP:SPEC][ext_str:SP.Str->STR]
        [S'=Sigma SP.Str [s:SP.Str]s.ext_str]
        [ext_ax:S'->Prop]
      = make_SPEC S' [s':S']and (SP.Ax s'.sig_pi1) (ext_ax s')
      : SPEC
];

Note that ext_str can depend on SP. The new structure is a sigma type which pairs SP.Str and ext_str. The axioms must be expressed as a function from this new structure to Prop. Extending the axioms only is simpler:

[Extend_AxOnly [SP:SPEC][ext_ax:SP.Str->Prop]
      = make_SPEC SP.Str [s:SP.Str]and (SP.Ax s) (ext_ax s)
      : SPEC
];

Tools for combining specifications allow for modular implementation; a problem may be broken down into two or more independent parts which can be implemented separately, then recombined to form an implementation of the whole. Here are two such operations.

[Join [S|STR][SP,SP':S.Spec]
    = make_SPEC S [s:S]and (SP s) (SP' s)
    : SPEC
];

Join combines two axiom sets for a given structure S; to merge two different structures, we would

use Cross:
(* Cross *)
[Cross [SP,SP':SPEC]
     = [S= Prod SP.Str SP'.Str]
       make_SPEC S [s:S]and (SP.Ax s.sig_pi1) (SP'.Ax s.sig_pi2)
     : SPEC
];

Cross combines two specifications by creating a new specification consisting of the product of the two structures and the conjunction of the two sets of axioms.