Skip to main content

1982 | Buch

A Programming Approach to Computability

verfasst von: A. J. Kfoury, Robert N. Moll, Michael A. Arbib

Verlag: Springer New York

Buchreihe : Monographs in Computer Science

insite
SUCHEN

Über dieses Buch

Computability theory is at the heart of theoretical computer science. Yet, ironically, many of its basic results were discovered by mathematical logicians prior to the development of the first stored-program computer. As a result, many texts on computability theory strike today's computer science students as far removed from their concerns. To remedy this, we base our approach to computability on the language of while-programs, a lean subset of PASCAL, and postpone consideration of such classic models as Turing machines, string-rewriting systems, and p. -recursive functions till the final chapter. Moreover, we balance the presentation of un solvability results such as the unsolvability of the Halting Problem with a presentation of the positive results of modern programming methodology, including the use of proof rules, and the denotational semantics of programs. Computer science seeks to provide a scientific basis for the study of information processing, the solution of problems by algorithms, and the design and programming of computers. The last 40 years have seen increasing sophistication in the science, in the microelectronics which has made machines of staggering complexity economically feasible, in the advances in programming methodology which allow immense programs to be designed with increasing speed and reduced error, and in the develop­ ment of mathematical techniques to allow the rigorous specification of program, process, and machine.

Inhaltsverzeichnis

Frontmatter
Chapter 1. Introduction
Abstract
Computability theory looks at the functions computed by algorithms, such as computer programs. Since a program may not halt for a given input, the functions so computed will be partial functions. In Section 1.1 we discuss partial functions and their computability by different families of algorithms. In Section 1.2 we give an example of an unsolvability or noncom-putability result—showing that no program can compute for an arbitrary number n whether or not the pascal program with ASCII code n will halt when also given n as input data. Section 1.3 shows that the method of proof used to show the noncomputability of this halting problem is akin to Cantor’s diagonal argument that the real numbers are uncountable. This chapter thus gives the reader a taste for a number of techniques to be used again and again throughout this volume.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 2. The Syntax and Semantics of while-Programs
Abstract
In Chapter 1 we presented a version of the unsolvability of the Halting Program for pascal. The generality of that result rests on the crucial assumption—embodied in our formulation of Church’s Thesis—that the notion of “algorithmic” coincides with the notion of “programmable”. In this chapter we examine the relationship between algorithms and programs more carefully. We define a particularly simple language, a pascal subset called while-programs, with the intent of isolating a set of primitive operations and combination rules which form a convenient and tractable basis for our formulation of computability theory.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 3. Enumeration and Universality of the Computable Functions
Abstract
We began our discussion of the Halting Problem in Chapter 1 by showing how to make a systematic listing, based on ASCII character codes, of all pascal programs. Each pascal program had a unique number, or index. This number was obtained by concatenating the ASCII bit strings representing the resulting binary sequence as an integer in binary. Of course, not every number corresponded to a legal program, or even to a legal sequence of ASCII blocks. Under these circumstances an invalid program in our listing was interpreted, by default, to be a particular program for the empty function. In Section 3.1 we follow a similar plan and present an enumeration of the while-programs. Then, in Section 3.2, we develop an “interpreter”, also called a universal program, which can decode the index n of a program P n to process data just as P n would have done. Sections 3.3 and 3.4 develop “subroutines” for the construction of the interpreter showing, respectively, how string-processing functions may be simulated by numerical functions and how vectors of natural numbers may be coded by a single such number.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 4. Techniques of Elementary Computability Theory
Abstract
In this chapter we illustrate several techniques for judging a function’s computational status. Sometimes we can prove that a function is computable by writing down a concrete while-program that calculates the function’s values. Often this involves an appeal to the Enumeration Theorem, which permits us to use the interpreter macro
$$ X: = \Phi \left( {Y,Z} \right) $$
.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 5. Program Methodology
Abstract
We have now introduced the language of while-programs and shown how, with the use of macros, we can attain much of the power of a “real” programming language like pascal. We have gone far to justify the claim that while-programs are complete, i.e., that any algorithm at all can be translated into a while-program. As we have already seen in our discussion of various undecidable problems in Section 4.3, this very breadth of expressive power exacts a price. Many interesting questions about programs cannot be answered by an algorithm which is guaranteed to work for all programs as input data.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 6. The Recursion Theorem and Properties of Enumerations
Abstract
Recursion is an important programming technique in computer science. We examined this notion initially in Section 5.2, where we also proved the First Recursion Theorem. Here we discuss a more general result, the Second Recursion Theorem (or more simply, the Recursion Theorem), perhaps the most fascinating result in elementary computability theory. The Recursion Theorem legitimizes self-reference in the descriptions of algorithms. Self-reference arguments add elegance and economy to the methods of computability theory, and guarantee that certain completely unexpected properties of any effective enumeration of algorithms must hold.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 7. Computable Properties of Sets (Part 1)
Abstract
In preceding chapters we examined the class of computable functions in detail. We set up a coding system for these functions, using the natural numbers to represent the programs which compute these functions. Conveniently, the natural numbers also serve as the domain and codomain for functions in the class. Using this machinery, we were able to identify an important role for self-reference in our theory, and we were able to present natural examples of functions which are not computable, i.e., not calculable by an algorithm.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 8. Computable Properties of Sets (Part 2)
Abstract
Here we continue the previous chapter’s discussion of computable properties of sets.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Chapter 9. Alternative Approaches to Computability
Abstract
In the previous chapters we have developed a theory of computability based on while-programs. The legitimacy of this programming language approach has rested on the belief, embodied in Church’s Thesis, that the class of computable functions is model invariant: The while-program computable functions include the function classes that are definable by any other system, so long as that system matches our informal notion of algorithmic specification.
A. J. Kfoury, Robert N. Moll, Michael A. Arbib
Backmatter
Metadaten
Titel
A Programming Approach to Computability
verfasst von
A. J. Kfoury
Robert N. Moll
Michael A. Arbib
Copyright-Jahr
1982
Verlag
Springer New York
Electronic ISBN
978-1-4612-5749-3
Print ISBN
978-1-4612-5751-6
DOI
https://doi.org/10.1007/978-1-4612-5749-3