Foundations

  The primary areas of activity on the foundations of hardware representation are Abstract Computability (with V Stoltenberg-Hansen at Uppsala, and J Zucker at McMaster, Canada); SCA Theory; Algebraic Specification (both with J Bergstra, Amsterdam); and Higher-Order Algebraic Specification (with B Möller, Augsburg).

[Stoltenberg-Hansen, Tucker 94]

V Stoltenberg-Hansen and J V Tucker, Effective Algebra, Handbook of Logic for Computer Science. Volume IV (ed. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, Oxford (1994) 357 -- 526

An algebra is computable if it can be faithfully represented on a computer. Many algebras, such as algebras of real numbers, can only be approximately represented on a computer. This long paper describes a mathematical theory that covers exact and approximate data types. The work on approximation is new and uses the authors' notions of domain representability to give a general approximation theory for topological algebras. The real numbers are among the case studies.

[Tucker, Zucker 94]

J V Tucker and J I Zucker, Computable functions on stream algebras, Proc. NATO Advanced Study Institute Int. Summer School at Marktoberdorf on Proof and computation (ed. H Schwichtenberg), Series F: Computer and Systems Sciences, Springer-Verlag, Berlin (1994) 341 -- 382

Abstract computability theory gives a delicate theory of finite computations on any algebra (i.e. data type). An abstract computability model defines a class of functions on algebra A. Given an algebra A we may add streams to form algebra of streams over A.

This paper studies various classes of computable stream processing functions by applying an abstract model of computation to to define . Special attention is paid to various forms of primitive recursion over streams. These functions are fundamental in SCA theory.

[McConnell 94]

B McConnell, Infinite Synchronous Concurrent Algorithms, University of Wales Swansea, Department of Computer Science PhD thesis, 1994.

This thesis is a comprehensive study of infinite SCAs. It frames an algebraic treatment of approximating one SCA by another based on direct and inverse limits of SCA algebras. Case studies of hardware stacks, convolvers etc. are described.

[Bergstra, Tucker 95]

J A Bergstra and J V Tucker, The data type variety of stack algebras, Annals of Pure and Applied Logic, to appear.

There are many semantic models and implementations for the stack. In this paper they are unified using a simple equational specification of the core properties of the stack. The study is concerned with the class of all (minimal) models of their axioms. Techniques involving hidden sorts and functions are developed to perform the semantic analysis with total functions. Decision problems are classified as decidable/undecidable.

[Meinke 94]

K Meinke, A recursive second-order initial algebra specification of primitive recursion, Acta Informatica 31 (1994) 329 -- 340

Primitive recursive functions over the natural numbers and over an abstract structure are a natural mathematical foundation for modeling and studying synchronous systems such as SCAs, dynamical systems etc. Earlier work of Bergstra and Tucker has shown that the primitive recursive functions have no recursively enumerable equational specification under first-order initial semantics. In this paper we show that the primitive recursive functions on N have a simple and natural recursive equational specification under second-order initial semantics. This paper is the first in a series of papers which aim to characterise the expressive power of higher-order algebraic specifications.

[Meinke, Steggles 94]

K. Meinke and L.J. Steggles, Specification and verification in higher order algebra: a case study of convolution, Proc. First Int. Workshop on Higher-Order Algebra, Logic and Term Rewriting --- HOA '93 (ed. J. Heering, K. Meinke, B. Möller and T. Nipkow), Lecture Notes in Computer Science Vol. 816, Springer-Verlag, Berlin (1994) 189 -- 222

This paper is one of two contributions to the first international workshop on higher-order algebra, logic and term rewriting organised jointly with B Möller and members external to working group 8533. As a case study in specification and verification using higher-order equational logic we consider the classical systolic convolution algorithm proposed by H T Kung. We specify and verify two versions of this algorithm with programmable and non-programmable weights and we study the metamathematics of the verification proofs using a non-standard model of time. Specifically we show that the programmable convolver cannot be verified without the auxiliary principle of free variable induction over time. The verification of of the non-programmable convolver leads to a conjecture about the existence of normal forms for higher-order equational proofs which has been subsequently confirmed by KM.

[Hearn, Meinke 94]

B.M. Hearn and K. Meinke, ATLAS: a typed language for algebraic specification, Proc. First Int. Workshop on Higher-Order Algebra, Logic and Term Rewriting --- HOA '93 (ed. J. Heering, K. Meinke, B. Möller and T. Nipkow), Lecture Notes in Computer Science Vol. 816, Springer-Verlag, Berlin (1994) 146 -- 168

In this second contribution to HOA '93 we give a tutorial introduction to the algebraic specification language ATLAS which has been designed and implemented in Swansea. The ATLAS specification language is aimed at supporting equational specifications of both data and types within two level specifications. A number of case studies of specifications in ATLAS are given including the algebra of primitive recursive functions, a hardware convolution algorithm, and an encoding of propositional logic and its Hilbert style proof system (using typed combinators) following the Curry Howard correspondence. The ATLAS language has subsequently been revised and re-implemented but this document serves as a useful report indicating how the present language was developed.