Also see Standard Basic Material for newer material .

next up previous contents index
Next: Lists and Arrays Up: Mathematics Libraries Previous: Mathematics Libraries

Basic Definitions

This  section presents a collection of definitions which are of general use. Most libraries will include these objects or ones similar to them.

It is convenient to have a singleton type available. We call it one.

     one == { x:int | x=0 in int }
Most programming languages contain a two--element type of ``booleans'' ; we use the two--element type two.
     two == { x:int | (x=0 in int | x=1 in int) }
Associated with the ``boolean'' type is the usual conditional operator, the ``if--then--else''  construct.
     if <x:two> then <t1:exp> else <t2:exp> fi
        == int_eq( <x>; 0; <t1>; <t2> )
To make selections from pairs we define the basic selectors as follows.
     1of( <P:pair> ) == spread( <P>; u,v.u )
     2of( <P:pair> ) == spread( <P>; u,v.v )
To define some of the most basic types the usual order  relations on integers are very useful. These must be defined from the simple < relation. Here are some of the basic order definitions as an example of how to proceed. The first is a definition of , and the following two define notation for chains of inequalities.
     <m:int> <= <n:int> == <n> < <m> -> void
     <m:int> < <n:int> < <k:int>
        == <m> < <n> & <n> < <k>
     <m:int> <= <n:int> <= <k:int>
        == <m> <= <n> & <n> <= <k>
Another useful concept is the idea of a finite  interval in int; it may be defined as follows.
     { <lb:int>, ..., <hb:int> }
        == { i:int | <lb> <= i <= <hb> }

The basic logic definitions were discussed in chapter 3, but they are repeated in figure gif for reference in the subsequent sections. To illustrate the kind of parenthesizing which it is wise to do in practice only white space has been added to the text of the actual library object.

Figure: Logic Definitions

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