The philosophy of computer science is concerned with the philosophical questions that arise with the study of computer science, which is understood to mean not just programming but the whole study of concepts and methods that assist in the development and maintenance of computer systems. There is still no common understanding of the content, aim, focus, or topic of the philosophy of computer science, despite some attempts to develop a philosophy of computer science like the philosophy of physics or the philosophy of mathematics.
The philosophy of computer science as such deals with the meta-activity that is associated with the development of the concepts and methodologies that implement and analyze the computational systems.
In computability theory, the Church–Turing thesis (also known as computability thesis, the Turing–Church thesis, the Church–Turing conjecture, Church's thesis, Church's conjecture, and Turing's thesis) is a hypothesis about the nature of computable functions. It states that a function on the natural numbers is computable by a human being following an algorithm, ignoring resource limitations, if and only if it is computable by a Turing machine. The thesis is named after American mathematician Alonzo Church and the British mathematician Alan Turing. Before the precise definition of computable function, mathematicians often used the informal term effectively calculable to describe functions that are computable by paper-and-pencil methods. In the 1930s, several independent attempts were made to formalize the notion of computability:
In 1933, Kurt Gödel, with Jacques Herbrand, created a formal definition of a class called general recursive functions. The class of general recursive functions is the smallest class of functions (possibly with more than one argument) which includes all constant functions, projections, the successor function, and which is closed under function composition, recursion, and minimization.
In 1936, Alonzo Church created a method for defining functions called the λ-calculus. Within λ-calculus, he defined an encoding of the natural numbers called the Church numerals. A function on the natural numbers is called λ-computable if the corresponding function on the Church numerals can be represented by a term of the λ-calculus.
Also in 1936, before learning of Church's work, Alan Turing created a theoretical model for machines, now called Turing machines, that could carry out calculations from inputs by manipulating symbols on a tape. Given a suitable encoding of the natural numbers as sequences of symbols, a function on the natural numbers is called Turing computable if some Turing machine computes the corresponding function on encoded natural numbers.Church and Turing proved that these three formally defined classes of computable functions coincide: a function is λ-computable if and only if it is Turing computable if and only if it is general recursive. This has led mathematicians and computer scientists to believe that the concept of computability is accurately characterized by these three equivalent processes. Other formal attempts to characterize computability have subsequently strengthened this belief (see below).
On the other hand, the Church–Turing thesis states that the above three formally-defined classes of computable functions coincide with the informal notion of an effectively calculable function. Since, as an informal notion, the concept of effective calculability does not have a formal definition, the thesis, although it has near-universal acceptance, cannot be formally proven.
Since its inception, variations on the original thesis have arisen, including statements about what can physically be realized by a computer in our universe (physical Church-Turing thesis) and what can be efficiently computed (Church–Turing thesis (complexity theory)). These variations are not due to Church or Turing, but arise from later work in complexity theory and digital physics. The thesis also has implications for the philosophy of mind (see below).Correctness (computer science)
In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e., for each input it produces the expected output).A distinction is made between partial correctness, which requires that if an answer is returned it will be correct, and total correctness, which additionally requires that the algorithm terminates. Since there is no general solution to the halting problem, a total correctness assertion may lie much deeper. A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.For example, successively searching through integers 1, 2, 3, … to see if we can find an example of some phenomenon—say an odd perfect number—it is quite easy to write a partially correct program (using long division by two to check n as perfect or not). But to say this program is totally correct would be to assert something currently not known in number theory.
A proof would have to be a mathematical proof, assuming both the algorithm and specification are given formally. In particular it is not expected to be a correctness assertion for a given program implementing the algorithm on a given machine. That would involve such considerations as limitations on computer memory.
A deep result in proof theory, the Curry-Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus. Converting a proof in this way is called program extraction.
Hoare logic is a specific formal system for reasoning rigorously about the correctness of computer programs. It uses axiomatic techniques to define programming language semantics and argue about the correctness of programs through assertions known as Hoare triples.
Software testing is any activity aimed at evaluating an attribute or capability of a program or system and determining that it meets its required results. Although crucial to software quality and widely deployed by programmers and testers, software testing still remains an art, due to limited understanding of the principles of software. The difficulty in software testing stems from the complexity of software: we can not completely test a program with moderate complexity. Testing is more than just debugging. The purpose of testing can be quality assurance, verification and validation, or reliability estimation. Testing can be used as a generic metric as well. Correctness testing and reliability testing are two major areas of testing. Software testing is a trade-off between budget, time and quality.Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.
It is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard. It is the link between logic and computation that is usually attributed to Curry and Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various formulations by L. E. J. Brouwer, Arend Heyting and Andrey Kolmogorov (see Brouwer–Heyting–Kolmogorov interpretation) and Stephen Kleene (see Realizability). The relationship has been extended to include category theory as the three-way Curry–Howard–Lambek correspondence.Dataism
Dataism is a term that has been used to describe the mindset or philosophy created by the emerging significance of Big Data. It was first used by David Brooks in the New York Times in 2013. More recently, the term has been expanded to describe what social scientist Yuval Noah Harari has called an emerging ideology or even a new form of religion, in which 'information flow' is the 'supreme value'.Index of philosophy of science articles
An index list of articles about the philosophy of science.Philosophy of artificial intelligence
Artificial intelligence has close connections with philosophy because both share several concepts and these include intelligence, action, consciousness, epistemology, and even free will. Furthermore, the technology is concerned with the creation of artificial animals or artificial people (or, at least, artificial creatures) so the discipline is of considerable interest to philosophers. These factors contributed to the emergence of the philosophy of artificial intelligence. Some scholars argue that the AI community's dismissal of philosophy is detrimental.The philosophy of artificial intelligence attempts to answer such questions as follows:
Can a machine act intelligently? Can it solve any problem that a person would solve by thinking?
Are human intelligence and machine intelligence the same? Is the human brain essentially a computer?
Can a machine have a mind, mental states, and consciousness in the same way that a human being can? Can it feel how things are?Questions like these reflect the divergent interests of AI researchers, linguists, cognitive scientists and philosophers respectively. The scientific answers to these questions depend on the definition of "intelligence" and "consciousness" and exactly which "machines" are under discussion.
Important propositions in the philosophy of AI include:
Turing's "polite convention": If a machine behaves as intelligently as a human being, then it is as intelligent as a human being.
The Dartmouth proposal: "Every aspect of learning or any other feature of intelligence can be so precisely described that a machine can be made to simulate it."
Newell and Simon's physical symbol system hypothesis: "A physical symbol system has the necessary and sufficient means of general intelligent action."
Searle's strong AI hypothesis: "The appropriately programmed computer with the right inputs and outputs would thereby have a mind in exactly the same sense human beings have minds."
Hobbes' mechanism: "For 'reason' ... is nothing but 'reckoning,' that is adding and subtracting, of the consequences of general names agreed upon for the 'marking' and 'signifying' of our thoughts..."Philosophy of information
The philosophy of information (PI) is a branch of philosophy that studies topics relevant to computer science, information science and information technology.
the critical investigation of the conceptual nature and basic principles of information, including its dynamics, utilisation and sciences
the elaboration and application of information-theoretic and computational methodologies to philosophical problems.Philosophy of technology
The philosophy of technology is a sub-field of philosophy that studies the nature of technology and its social effects.
Philosophical discussion of questions relating to technology (or its Greek ancestor techne) dates back to the very dawn of Western philosophy. The phrase "philosophy of technology" was first used in the late 19th century by German-born philosopher and geographer Ernst Kapp, who published a book titled "Grundlinien einer Philosophie der Technik".Ray Turner (computer scientist)
Professor Raymond Turner (born 28 April 1947) is an English logician, philosopher, and theoretical computer scientist based at the University of Essex. He is best known for his work on logic in computer science and for his pioneering work in the philosophy of computer science. He is on the editorial boards for the Journal of Logic and Computation and the Stanford Encyclopaedia of Philosophy, for Logic, Computation, and Agency.School of Computer Science and Electronic Engineering (Essex University)
The School of Computer Science and Electronic Engineering at the University of Essex is an academic department that focuses on educating and researching into Computer Science and Electronic Engineering specific matters. It was formed by the merger of two departments, notable for being amongst the first in England in their fields, the Department of Electronic Systems Engineering(1966) and the Department of Computer Science (1966).The Master Algorithm
The Master Algorithm: How the Quest for the Ultimate Learning Machine Will Remake Our World is a book by Pedro Domingos released in 2015. Domingos wrote the book in order to generate interest from people outside the field.
The book outlines five tribes of machine learning: inductive reasoning, connectionism, evolutionary computation, bayes theorem and analogical modelling. The author explains these tribes to the reader by referring to more understandable processes of logic, connections made in the brain, natural selection, probability and similarity judgements. Throughout the book, it is suggested that each different tribe has the potential to contribute to a unifying "master algorithm".
Towards the end of the book the author pictures a "master algorithm" in the near future, where machine learning algorithms asymptotically grow to a perfect understanding of how the world and people in it work. Although the algorithm doesn't yet exist, he briefly reviews his own invention of the Markov logic network.
Note: This template roughly follows the 2012 ACM Computing Classification System.
|Theory of computation|