patternMinor
Set theory and computer science
Viewed 0 times
sciencetheorycomputerandset
Problem
It's said that in Zermelo–Fraenkel set theory (ZFC) one can develop all of mathematics. How about computer science?
Is it possible to define algorithms as a first step? More specifically, how to define "if x = 1 then y else z"? How about loops?
Is it possible to define algorithms as a first step? More specifically, how to define "if x = 1 then y else z"? How about loops?
Solution
It all depends what you consider "computer science."
For what I would call "classical computer science" i.e. the theory of Algorithms, Turing Machines, etc. it can all be modelled in set theory.
A Turing Machine is just a tuple (which can be modelled using sets): a set of states, a tape-alphabet set, a transition function, etc. All of these are set-theoretic constructs, and even with nondeterminism, we replace the transition function with a relation, which is again set theoretic.
Similarly, we can define the semantics of programming languages using sets. Usually this just boils down to a big-step or small-step operational semantics, which again, is just defining relations.
Where things get iffy is with the so-called "alternate foundations of mathematics". This includes things like:
They provide alternate sets of axioms from which mathematics can be built up. For example, the usually discard excluded middle and axiom of choice. Homotopy type theory, for example, introduces the Univalence Axiom.
These systems tend to be heavily oriented towards computation through the Curry-Howard Correspondence, so that a proof can "run" on a computer. So they don't quite fit into ZFC, but are generally considered part of computer science.
For what I would call "classical computer science" i.e. the theory of Algorithms, Turing Machines, etc. it can all be modelled in set theory.
A Turing Machine is just a tuple (which can be modelled using sets): a set of states, a tape-alphabet set, a transition function, etc. All of these are set-theoretic constructs, and even with nondeterminism, we replace the transition function with a relation, which is again set theoretic.
Similarly, we can define the semantics of programming languages using sets. Usually this just boils down to a big-step or small-step operational semantics, which again, is just defining relations.
Where things get iffy is with the so-called "alternate foundations of mathematics". This includes things like:
- Martin-Lof type theory
- Coqand's Calculus of Constructions
- Homotopy type theory
They provide alternate sets of axioms from which mathematics can be built up. For example, the usually discard excluded middle and axiom of choice. Homotopy type theory, for example, introduces the Univalence Axiom.
These systems tend to be heavily oriented towards computation through the Curry-Howard Correspondence, so that a proof can "run" on a computer. So they don't quite fit into ZFC, but are generally considered part of computer science.
Context
StackExchange Computer Science Q#81688, answer score: 4
Revisions (0)
No revisions yet.