Extensions of higher-order algebra : fundamental theory and case studies

• Main Author: Steggles, L. J.
• Published: Swansea University 1995
• Subjects: 510
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.639103

In this thesis we take as our starting point the existing theory of higher-order algebra developed by K. Meinke and B. Möller. We will both apply and extend this theory. To illustrate the use of higher-order algebra as a formalism for formal specification and verification we present two case studies. In the first case study we consider the formal specification of two systolic algorithms for convolution. We formally verify the correctness of these two algorithms using higher-order equational logic and investigate the metamathematics of our verification proofs. The second case study considers the correctness of a dataflow algorithm for computing the Hamming stream. We present a non-constructive higher-order Horn specification of the Hamming stream and develop a semantic proof to verify the correctness of the dataflow algorithm. This second case study illustrates the power of higher-order algebraic methods using non-constructive techniques to capture abstract properties of the Hamming stream. For specification in the large we need to be able to structure specifications in a modular fashion and allow for the reuse of specifications. To this end we present a theory of <I>parameterised higher-order specifications</I>. We take a standard theory of parameterised first-order specifications and extend it to the higher-order case. We demonstrate our theory by presenting a parameterised specification of convolution in which the stream space is a parameter. One of the limitations of higher-order algebra using only ? and → types is the difficulty in modelling objects which are parametric in type, such as polymorphic functions, generic data structures and infinite families of algorithms and architectures. We propose to overcome this limitation by extending the type system of higher-order algebra with <I>limit types</I>. We refer to the resulting theory as <I>higher-order algebra with transfinite types</I>. The idea is that a limit type contains all the types below it in a natural transfinite type hierarchy and thus provides a "universal" type in which all the lower types can be embedded.