Provable computable selection functions on abstract structures

Summary

ABSTRACT. We work in the context of abstract data types, modelled as classes of many-sorted algebras closed under isomorphism. We develop notions of computability over such classes, in particular notions of primitive recursiveness and μ-recursiveness, which generalize the corresponding classical notions over the natural numbers. We also develop classical and intuitionistic formal systems for theories about such data types, and prove (in the case of universal theories) that if an existential assertion is provable in either of these systems, then it has a primitive recursive selection function. It is a corollary that if a μ-recursive scheme is provably total, then it is extensionally equivalent to a primitive recursive scheme. The methods are proof-theoretical, involving cut elimination. These results generalize to an abstract setting previous results of C. Parsons and G. Mints over the natural numbers.

INTRODUCTION

We will examine the provability or verifiability in formal systems of program properties, such as termination or correctness, from the point of view of the general theory of computable functions over abstract data types. In this theory an abstract data type is modelled semantically by a class K of many-sorted algebras, closed under isomorphism, and many equivalent formalisms are used to define computable functions and relations on an algebra A, uniformly for all A ∈ K. Some of these formalisms are generalizations to A and K of sequential deterministic models of computation on the natural numbers.