TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES

2018 ◽  
Vol 83 (3) ◽  
pp. 967-990
Author(s):  
GERHARD JÄGER ◽  
TIMOTEJ ROSEBROCK ◽  
SATO KENTARO
Keyword(s):  
Recursion Theory ◽  
Natural Numbers ◽  
First Order ◽  
Recursive Functions ◽  
Partial Recursive Functions

AbstractBON+ is an applicative theory and closely related to the first order parts of the standard systems of explicit mathematics. As such it is also a natural framework for abstract computations. In this article we analyze this aspect of BON+ more closely. First a point is made for introducing a new operation τN, called truncation, to obtain a natural formalization of partial recursive functions in our applicative framework. Then we introduce the operational versions of a series of notions that are all equivalent to semi-decidability in ordinary recursion theory on the natural numbers, and study their mutual relationships over BON+ with τN.

The hereditary partial effective functionals and recursion theory in higher types

1984 ◽  
Vol 49 (4) ◽  
pp. 1319-1332 ◽  
Author(s):  
G. Longo ◽  
E. Moggi
Keyword(s):  
Recursion Theory ◽  
Type Structure ◽  
Natural Numbers ◽  
Recursive Functions ◽  
Partial Recursive Functions ◽  
Higher Types ◽  
Elementary Technique

AbstractA type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings).By this and by results in [1] and [2], the Kleene-Kreisel countable functionals and the hereditary effective operations (HEO) are easily characterized.

On homogeneity and definability in the first-order theory of the Turing degrees

1982 ◽  
Vol 47 (1) ◽  
pp. 8-16 ◽  
Author(s):  
Richard A. Shore
Keyword(s):  
Recursion Theory ◽  
Order Theory ◽  
Partial Ordering ◽  
Turing Degrees ◽  
First Order ◽  
Recursive Functions ◽  
First Order Theory ◽  
Partial Recursive Functions ◽  
Carry Over

Relativization—the principle that says one can carry over proofs and theorems about partial recursive functions and Turing degrees to functions partial recursive in any given set A and the Turing degrees of sets in which A is recursive—is a pervasive phenomenon in recursion theory. It led H. Rogers, Jr. [15] to ask if, for every degree d, (≥ d), the partial ordering of Turing degrees above d, is isomorphic to all the degrees . We showed in Shore [17] that this homogeneity conjecture is false. More specifically we proved that if, for some n, the degree of Kleene's (the complete set) is recursive in d(n) then ≇ (≤ d). The key ingredient of the proof was a new version of a result from Nerode and Shore [13] (hereafter NS I) that any isomorphism φ: → (≥ d) must be the identity on some cone, i.e., there is an a called the base of the cone such that b ≥ a ⇒ φ(b) = b. This result was combined with information about minimal covers from Jockusch and Soare [8] and Harrington and Kechris [3] to derive a contradiction from the existence of such an isomorphism if deg() ≤ d(n).

Definability of r. e. sets in a class of recursion theoretic structures

1983 ◽  
Vol 48 (3) ◽  
pp. 662-669 ◽  
Author(s):  
Robert E. Byerly
Keyword(s):  
Recursion Theory ◽  
Universal Function ◽  
Independent Interest ◽  
Suitable Model ◽  
Natural Numbers ◽  
Construction Techniques ◽  
Partial Recursive Functions ◽  
Priority Method ◽  
Recursive Isomorphism ◽  
Direct Attack

It is known [4, Theorem 11-X(b)] that there is only one acceptable universal function up to recursive isomorphism. It follows from this that sets definable in terms of a universal function alone are specified uniquely up to recursive isomorphism. (An example is the set K, which consists of all n such that {n}(n) is defined, where λn, m{n}(m) is an acceptable universal function.) Many of the interesting sets constructed and studied by recursion theorists, however, have definitions which involve additional notions, such as a specific enumeration of the graph of a universal function. In particular, many of these definitions make use of the interplay between the purely number-theoretic properties of indices of partial recursive functions and their purely recursion-theoretic properties.This paper concerns r.e. sets that can be defined using only a universal function and some purely number-theoretic concepts. In particular, we would like to know when certain recursion-theoretic properties of r.e. sets definable in this way are independent of the particular choice of universal function (equivalently, independent of the particular way in which godel numbers are identified with natural numbers).We will first develop a suitable model-theoretic framework for discussing this question. This will enable us to classify the formulas defining r.e. sets by their logical complexity. (We use the number of alternations of quantifiers in the prenex form of a formula as a measure of logical complexity.) We will then be able to examine the question at each level.This work is an approach to the question of when the recursion-theoretic properties of an r.e. set are independent of the particular parameters used in its construction. As such, it does not apply directly to the construction techniques most commonly used at this time for defining particular r.e. sets, e.g., the priority method. A more direct attack on this question for these techniques is represented by such works as [3] and [5]. However, the present work should be of independent interest to the logician interested in recursion theory.

Recursion theory and the lambda-calculus

1982 ◽  
Vol 47 (1) ◽  
pp. 67-83 ◽  
Author(s):  
Robert E. Byerly
Keyword(s):  
Lambda Calculus ◽  
Recursion Theory ◽  
Natural Class ◽  
Recursive Functions ◽  
Partial Recursive Functions

AbstractA semantics for the lambda-calculus due to Friedman is used to describe a large and natural class of categorical recursion-theoretic notions. It is shown that if e1 and e2 are gödel numbers for partial recursive functions in two standard ω-URS's which both act like the same closed lambda-term, then there is an isomorphism of the two ω-URS's which carries e1 to e2.

On decomposition of Gödelnumberings into Friedbergnumberings

1982 ◽  
Vol 47 (2) ◽  
pp. 267-274 ◽  
Author(s):  
Britta Schinzel
Keyword(s):  
Partial Ordering ◽  
Universal Property ◽  
Natural Numbers ◽  
Direct Sums ◽  
Recursive Functions ◽  
Direct Sum ◽  
Recursively Enumerable ◽  
Pairing Function ◽  
Partial Recursive Functions ◽  
Effective Function

The category of enumerations over P1 is investigated. Objects are the enumerations of the set of partial recursive functions in one variable φ: N → P1 where φ is a total effective function from the natural numbers N onto P1.To each a ∈ P1 we call φ−1(a) the set of all indices for a, the fibre over a.Morphisms from one enumeration φ to another one ψ are (partial) recursive functions f, for which φ(n) = ψ(f(n)) holds for all n where f is denned, i.e. f is fibrepreserving. They are also called translators if f is total. The existence of a translator induces a partial ordering on the enumerations:Let φ ≤ ψ, iff there exists a translator f with φ = ψ·f; φ ≡ ψ iff φ ≤ ψ and ψ ≤ φ. Two enumerations are called incomparable iff φ ≰,ψ and ψ ≰ φ.Given a recursively enumerable family of enumerations {φi}i∈ω then their direct sum = π is defined by a bijective recursive pairing function g(i, n) (e.g. g(i, n) = (i + n)(i + n + 1)/2 + i) summing up the φi by φi(n) = = πg(i, n) into π. We also say π decomposes into .Direct sums satisfy the universal property of sums in categories.We want to operate decompositiontheory on special kinds of objects in our category, the Gödelnumberings and the Friedbergnumberings.A Gödelnumbering φ is defined by (a) enumeration theorem (i.e. φ is object of our category) and (b) -theorem, which means that each m + n-place p.r. function can be effectively replaced by an enumeration of n-place p.r. functions given by means of the total -function (see Rogers [3]).

Diagonals and semihyperhypersimple sets

1991 ◽  
Vol 56 (3) ◽  
pp. 1068-1074 ◽  
Author(s):  
Martin Kummer
Keyword(s):  
Recursion Theory ◽  
Index Set ◽  
Computable Numbering ◽  
Recursive Functions ◽  
Simple Set ◽  
Elementary Lattice ◽  
Computable Numberings ◽  
Partial Recursive Functions

The most basic construction of an r.e. nonrecursive set—e.g. of the halting problem—proceeds by taking the diagonal of a recursive enumeration of all r.e. sets. We will answer the question of which r.e. sets can be constructed in this manner.If ψ is a computable numbering of some class of partial recursive functions, we define the diagonal of ψ to be the set Kψ ≔ {i ∈ ω ∣ ψi(i)↓}- It is well known that Kφ is creative if φ is a Gödelnumbering, and that for each creative set K there exists a Gödelnumbering φ such that K = Kφ. That is to say, the class of diagonals of Gödelnumberings is characterized as the class of creative sets. This class was shown to be elementary lattice theoretic (e.l.t.) by Harrington (see [So87, XV. 1.1]).We give a characterization of diagonals of arbitrary computable numberings of the class P1 of all partial recursive functions. To this end we introduce the notion of a semihyperhypersimple (shhs) set, which generalizes the notion of hyperhypersimplicity to nonsimple sets. It is shown that the diagonals of numberings of P1 are exactly the non-shhs sets. Then, properties of shhs sets are discussed. For example, for each nonrecursive r.e. set A there exists a nonrecursive shhs set B ≤TA, but not every r.e. T-degree contains a shhs set. These results build upon previous work by Downey and Stob [DSta].The question whether the property “shhs” is (elementary) lattice theoretic remains open. A positive answer would give both an analog of Harrington's result mentioned above, and a generalization of the well-known fact, due to Lachlan [La68], that hyperhypersimplicity is e.l.t. Therefore, we suspect that shhs sets turn out to be useful in the study of the lattice of r.e. sets.Previously, for several constructions from recursion theory the role of the underlying numbering of P1 was investigated; see Martin ([Ma66a] or [So87, V.4.1]) and Lachlan ([La75] or [Od89, III.9.2]) for Post's simple set, and Jockusch and Soare ([JS73]; cf. also [So87, XII.3.6, 3.7]) for Post's hypersimple set. However, only Gödelnumberings were considered. An explanation for the greater variety which arises when arbitrary numberings of P1 are admitted is provided by the fact that the index set of Gödelnumberings is less complex than the index set of all numberings of P1. The former is Σ1-complete; the latter is Π4-complete.

An invariance notion in recursion theory

1982 ◽  
Vol 47 (1) ◽  
pp. 48-66 ◽  
Author(s):  
Robert E. Byerly
Keyword(s):  
Recursion Theory ◽  
Recursive Functions ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Partial Recursive Functions

AbstractA set of gödel numbers is invariant if it is closed under automorphisms of (ω, ·), where ω is the set of all gödel numbers of partial recursive functions and · is application (i.e., n · m ≃ φn(m)). The invariant arithmetic sets are investigated, and the invariant recursively enumerable sets and partial recursive functions are partially characterized.

Preliminaries

2017 ◽  
Author(s):  
David J. Lobina
Keyword(s):  
Data Structures ◽  
Production Systems ◽  
Specific Data ◽  
Recursive Functions ◽  
Recursive Solution ◽  
Partial Recursive Functions ◽  
Recursive Structures ◽  
Recursive Data Structures ◽  
Recursive Data ◽  
The Relationship

Recursion, or the capacity of ‘self-reference’, has played a central role within mathematical approaches to understanding the nature of computation, from the general recursive functions of Alonzo Church to the partial recursive functions of Stephen C. Kleene and the production systems of Emil Post. Recursion has also played a significant role in the analysis and running of certain computational processes within computer science (viz., those with self-calls and deferred operations). Yet the relationship between the mathematical and computer versions of recursion is subtle and intricate. A recursively specified algorithm, for example, may well proceed iteratively if time and space constraints permit; but the nature of specific data structures—viz., recursive data structures—will also return a recursive solution as the most optimal process. In other words, the correspondence between recursive structures and recursive processes is not automatic; it needs to be demonstrated on a case-by-case basis.

PAL – Propositional Algorithmic Logic

1981 ◽  
Vol 4 (3) ◽  
pp. 675-760
Author(s):  
Grażyna Mirkowska
Keyword(s):  
Data Structures ◽  
Completeness Theorem ◽  
Natural Numbers ◽  
First Order ◽  
Algorithmic Logic ◽  
Axiomatic Systems ◽  
Nondeterministic Program ◽  
Basic Sets

The aim of propositional algorithmic logic is to investigate the properties of program connectives. Complete axiomatic systems for deterministic as well as for nondeterministic interpretations of program variables are presented. They constitute basic sets of tools useful in the practice of proving the properties of program schemes. Propositional theories of data structures, e.g. the arithmetic of natural numbers and stacks, are constructed. This shows that in many aspects PAL is close to first-order algorithmic logic. Tautologies of PAL become tautologies of algorithmic logic after replacing program variables by programs and propositional variables by formulas. Another corollary to the completeness theorem asserts that it is possible to eliminate nondeterministic program variables and replace them by schemes with deterministic atoms.

Sign in / Sign up

Export Citation Format

Share Document