Primitive Recursion with Existential Types1

1993 ◽  
Vol 19 (1-2) ◽  
pp. 201-222
Author(s):  
Pawel Urzyczyn
Keyword(s):  
Standard Approach ◽  
Halting Problem ◽  
Primitive Recursion ◽  
Representation Of Integers ◽  
Existential Quantification ◽  
Primitive Recursive ◽  
Recursive Definitions ◽  
Recursive Set

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.

A Hierarchy on the Class of Primitive Recursive Ordinal Functions

1976 ◽  
Vol 28 (6) ◽  
pp. 1205-1209
Author(s):  
Stanley H. Stahl
Keyword(s):  
Natural Numbers ◽  
Recursive Functions ◽  
Set Functions ◽  
Primitive Recursive ◽  
Class Of Functions ◽  
Recursive Set

The class of primitive recursive ordinal functions (PR) has been studied recently by numerous recursion theorists and set theorists (see, for example, Platek [3] and Jensen-Karp [2]). These investigations have been part of an inquiry concerning a larger class of functions; in Platek's case, the class of ordinal recursive functions and in the case of Jensen and Karp, the class of primitive recursive set functions. In [4] I began to study PR in depth and this paper is a report on an attractive analogy between PR and its progenitor, the class of primitive recursive functions on the natural numbers (Prim. Rec).

Every recursive linear ordering has a copy in DTIME-SPACE(n,log(n))

1990 ◽  
Vol 55 (1) ◽  
pp. 260-276 ◽  
Author(s):  
Serge Grigorieff
Keyword(s):  
Complexity Theory ◽  
Order Type ◽  
Linear Ordering ◽  
Binary Representation ◽  
Relational Structures ◽  
Time Space ◽  
Representation Of Integers ◽  
Recursive Structures ◽  
Primitive Recursive ◽  
Recursive Relations

This paper is a contribution to the following natural problem in complexity theory:(*) Is there a complexity theory for isomorphism types of recursive countable relational structures? I.e. given a recursive relational structure ℛ over the set N of nonnegative integers, is there a nontrivial lower bound for the time-space complexity of recursive structures isomorphic (resp. recursively isomorphic) to ℛ?For unary recursive relations R, the answer is trivially negative: either R is finite or coinfinite or 〈N, R〉 is recursively isomorphic to 〈N, {x ϵ N: x is even}〉.The general problem for relations with arity 2 (or greater) is open.Related to this problem, a classical result (going back to S. C. Kleene [4], 1955) states that every recursive ordinal is in fact primitive recursive.In [3] Patrick Dehornoy, using methods relevant to computer science, improves this result, showing that every recursive ordinal can be represented by a recursive total ordering over N which has linear deterministic time complexity relative to the binary representation of integers. As he notices, his proof applies to every recursive total order type α such that the isomorphism type of α is not changed if points are replaced by arbitrary finite nonempty subsets of consecutive points.In this paper we extend Dehornoy's result to all recursive total orderings over N and get minimal complexity for both time and space simultaneously.

Finite axiomatizability for equational theories of computable groupoids

1989 ◽  
Vol 54 (3) ◽  
pp. 1018-1022 ◽  
Author(s):  
Peter Perkins
Keyword(s):  
Binary Operation ◽  
Finite Algebra ◽  
Equational Theory ◽  
Natural Numbers ◽  
Finite Axiomatizability ◽  
Finite Algebras ◽  
Equational Theories ◽  
Primitive Recursive ◽  
Positive Integers ◽  
Recursive Set

A computable groupoid is an algebra ‹N, g› where N is the set of natural numbers and g is a recursive (total) binary operation on N. A set L of natural numbers is a computable list of computable groupoids iff L is recursive, ‹N, ϕe› is a computable groupoid for each e ∈ L, and e ∈ L whenever e codes a primitive recursive description of a binary operation on N.Theorem 1. Let L be any computable list of computable groupoids. The set {e ∈ L: the equational theory of ‹N, ϕe› is finitely axiomatizable} is not recursive.Theorem 2. Let S be any recursive set of positive integers. A computable groupoid GS can be constructed so that S is inifinite iff GS has a finitely axiomatizable equational theory.The problem of deciding which finite algebras have finitely axiomatizable equational theories has remained open since it was first posed by Tarski in the early 1960's. Indeed, it is still not known whether the set of such finite algebras is recursively (or corecursively) enumerable. McKenzie [7] has shown that this question of finite axiomatizability for any (finite) algebra of finite type can be reduced to that for a (finite) groupoid.

scholarly journals Primitive recursive algebraic theories and program schemes

1977 ◽  
Vol 17 (2) ◽  
pp. 207-233 ◽  
Author(s):  
W. Kühnel ◽  
J. Meseguer ◽  
M. Pfender ◽  
I. Sols
Keyword(s):  
Programming Language ◽  
Generation Process ◽  
Recursive Functions ◽  
Algebraic Theories ◽  
Primitive Recursion ◽  
Recursive Theory ◽  
Carry Over ◽  
Primitive Recursive

We introduce primitive recursion as a generation process for arrows of algebraic theories in the sense of Lawvere and carry over important results on algebraic theories and functorial semantics to the enriched setting of “primitive recursive algebra”: existence of free primitive recursive theories and of theories presented by operations and equations on primitive recursive functions; existence of free models presented by generators and equations. Finally semantical correctness of translations is reduced to correctness for the basic operations. There is a connection to the theory of program schemes: program schemes involving primitive recursion correspond to arrows of a primitive recursive theory freely generated over a graph of basic operations. This theory T can be viewed as a programming language with “arithmetics” given by the basic operations and with DO-loops. A machine loaded with a compiler for T can be interpreted as a T-model in Lawvere's sense, preserving primitive recursion.

scholarly journals SAFE RECURSIVE SET FUNCTIONS

2015 ◽  
Vol 80 (3) ◽  
pp. 730-762 ◽  
Author(s):  
ARNOLD BECKMANN ◽  
SAMUEL R. BUSS ◽  
SY-DAVID FRIEDMAN
Keyword(s):  
Growth Rate ◽  
Polynomial Growth ◽  
Turing Machines ◽  
Finite Sets ◽  
Infinite Time ◽  
Machine Model ◽  
Set Functions ◽  
Rate Functions ◽  
Primitive Recursive ◽  
Recursive Set

AbstractWe introduce the safe recursive set functions based on a Bellantoni–Cook style subclass of the primitive recursive set functions. We show that the functions computed by safe recursive set functions under a list encoding of finite strings by hereditarily finite sets are exactly the polynomial growth rate functions computed by alternating exponential time Turing machines with polynomially many alternations. We also show that the functions computed by safe recursive set functions under a more efficient binary tree encoding of finite strings by hereditarily finite sets are exactly the quasipolynomial growth rate functions computed by alternating quasipolynomial time Turing machines with polylogarithmic many alternations.We characterize the safe recursive set functions on arbitrary sets in definability-theoretic terms. In its strongest form, we show that a function on arbitrary sets is safe recursive if and only if it is uniformly definable in some polynomial level of a refinement of Jensen's J-hierarchy, relativized to the transitive closure of the function's arguments.We observe that safe recursive set functions on infinite binary strings are equivalent to functions computed by infinite-time Turing machines in time less than ωω. We also give a machine model for safe recursive set functions which is based on set-indexed parallel processors and the natural bound on running times.

Functionals defined by transfinite recursion

1965 ◽  
Vol 30 (2) ◽  
pp. 155-174 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Functional Equations ◽  
Partial Ordering ◽  
Closure Properties ◽  
Primitive Recursive Arithmetic ◽  
Primitive Recursion ◽  
Definition Of ◽  
Second Order Systems ◽  
Transfinite Recursion ◽  
Primitive Recursive ◽  
Elementary Closure

This paper deals mainly with quantifier-free second order systems (i.e., with free variables for numbers and functions, and constants for numbers, functions, and functionals) whose basic rules are those of primitive recursive arithmetic together with definition of functionals by primitive recursion and explicit definition. Precise descriptions are given in §2. The additional rules have the form of definition by transfinite recursion up to some ordinal ξ (where ξ is represented by a primitive recursive (p.r.) ordering). In §3 we discuss some elementary closure properties (under rules of inference and definition) of systems with recursion up to ξ. Let Rξ denote (temporarily) the system with recursion up to ξ. The main results of this paper are of two sorts:Sections 5–7 are concerned with less elementary closure properties of the systems Rξ. Namely, we show that certain classes of functional equations in Rη can be solved in Rη for some explicitly determined η < ε(η) (the least ε-number > ξ). The classes of functional equations considered all have roughly the form of definition by recursion on the partial ordering of unsecured sequences of a given functional F, or on some ordering which is obtained from this by simple ordinal operations. The key lemma (Theorem 1) needed for the reduction of these equations to transfinite recursion is simply a sharpening of the Brouwer-Kleene idea.

The substitution method

1965 ◽  
Vol 30 (2) ◽  
pp. 175-192 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Free Variable ◽  
Order System ◽  
Conservative Extension ◽  
Substitution Method ◽  
Recursive Definition ◽  
First Order ◽  
Variable Elimination ◽  
Primitive Recursion ◽  
Definition Of ◽  
Primitive Recursive

This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system S framed in the ε-calculus [2] the problem is to associate a system S' without bound variables and an effective procedure for transforming derivations in S into derivations in S′. The transform of a formula A derived in S is to be an “ε-substitution instance” of A, i.e. it is obtained by replacing terms εxB(x) in A by terms of S′. In general the choice of these terms will depend on the particular derivation of A, and not on A alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of A should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in S′; on the other hand, it generalizes Hilbert's formulation since S′ need not be restricted to finitist systems.The bound variable elimination procedure can always be taken to be primitive recursive in (the Gödel number of) the derivation of A. Constructions which transcend primitive recursion can simply be built into S′.In this paper we show that if S′ is taken to be a second order system with constants for functionals, then the existence of suitable ε-substitution instances can be expressed by the solvability of certain functional equations in S′. We deal with two cases here. If S is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for S′ the free variable part S* of S with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of S*.

scholarly journals Primitive recursion in the abstract

2020 ◽  
Vol 30 (1) ◽  
pp. 33-43
Author(s):  
Daniel Leivant ◽  
Jean-Yves Marion
Keyword(s):  
Computational Complexity ◽  
Free Algebra ◽  
Generic Programming ◽  
Underlying Structure ◽  
Free Algebras ◽  
Primitive Recursion ◽  
Function Definition ◽  
Primitive Recursive

AbstractRecurrence can be used as a function definition schema for any nontrivial free algebra, yielding the same computational complexity in all cases. We show that primitive-recursive computing is in fact independent of free algebras altogether, and can be characterized by a generic programming principle, namely the control of iteration by the depletion of finite components of the underlying structure.

Sign in / Sign up

Export Citation Format

Share Document