Primitive Recursion with Existential Types¹

Article type: Research Article

Authors: Urzyczyn, Pawel

Affiliations: Institute of Informatics, University of Warsaw, ul. Banacha 2, 02-097 Warszawa, Poland, E-mail: urzy@mimuw.edu.pl

Note: [1] This research was partly supported by NSF grant CCR-8901647.

Abstract: We consider computability over abstract structures with help of primitive recursive definitions (an appropriate modification of Gödel’s system T). Unlike the standard approach, we do not assume any fixed representation of integers, but instead we allow primitive recursion to be polymorphic, so that iteration is performed with help of counters viewed as objects of an abstract type Int of arbitrary (hidden) implementation. This approach involves the use of existential quantification in types, following the ideas of Mitchell and Plotkin. We show that the halting problem over finite interpretations is primitive recursive for each program involving primitive recursive definitions. Conversely, each primitive recursive set of interpretations is defined by the termination property of some program.

DOI: 10.3233/FI-1993-191-209

Journal: Fundamenta Informaticae, vol. 19, no. 1-2, pp. 201-222, 1993