CM2207: Introduction to the Theory of Computation
School | Cardiff School of Computer Science and Informatics |
Department Code | COMSC |
Module Code | CM2207 |
External Subject Code | 100366 |
Number of Credits | 10 |
Level | L5 |
Language of Delivery | English |
Module Leader | DR Richard Booth |
Semester | Spring Semester |
Academic Year | 2017/8 |
Outline Description of Module
The theory of computing deals with questions such as: what is computation? What problems can be computed? What is the inherent difficulty of a given problem? To answer such questions in a satisfactory manner, we need a formal definition of computation, which does not rely on any specific hardware or programming language. It is perhaps surprising that some real-world problems can be mathematically proven to be undecidable, i.e. regardless of any future advances in hardware, such problems are provably impossible to solve on a computer. In this module we will discuss the main models of computability and provide several examples of undecidable problems. While questions about computability have initially been studied from a theoretical perspective, the resulting theories have had many important practical applications. Among others, the methods discussed in this module are used for implementing compilers (in particular for parsing), for defining functional programming languages, and for formally verifying the correctness of software and hardware.
On completion of the module a student should be able to
1. Use standard methods for proving mathematical properties
2. Understand the basic rules of classical logic
3. Apply formal methods to prove the correctness of a program
4. Use propositional logic to simplify Boolean circuits
5. Understand the application of formal languages and automata theory to problems in computer science
6. Demonstrate an understanding of formal languages and automata
7. Explain the notion of undecidability and its importance for computer science
8. Explain the basic concepts from complexity theory
9. Understand the use of reductions to characterise the complexity of a decision problem
How the module will be delivered
The module will be delivered through a combination of lectures, supervised lab sessions, example classes and tutorials as appropriate.
Skills that will be practised and developed
Formally verifying the correctness of a program
Implementing a simple parser
Designing and implementing automata and Turing Machines to carry out various tasks
How the module will be assessed
Coursework: The coursework will allow the student to demonstrate their knowledge and practical skills and to apply the principles taught in lectures.
Exam: A written exam (2 h) will test the student's knowledge and understanding as elaborated under the learning outcomes.
Assessment Breakdown
Type | % | Title | Duration(hrs) |
---|---|---|---|
Written Assessment | 30 | Programming Project | N/A |
Exam - Spring Semester | 70 | Introduction To The Theory Of Computation | 2 |
Syllabus content
Formal methods in computer science
Basic proof techniques: proof by contradiction, proof by induction, case analysis
Propositional logic
Application: Boolean circuits
Application: Hoare calculus
Formal Languages and Automata
Regular expressions, finite state machines, Kleene's theorem
Push-down automata, context-free grammars, the pumping lemma
Application: parsing
Context-sensitive grammars
Models of computation
Turing machines
Application: functional programming
Undecidability, the halting problem, the domino problem
Computational complexity
Non-determinism
The complexity classes P, NP, PSPACE, EXPTIME
Reductions, the SAT problem
P vs NP problem
Essential Reading and Resource List
Velleman, D. 2006. How to prove it: a structured approach. 2nd ed. Cambridge: Cambridge University Press.
Sipser, M. 2013. Introduction to the theory of computation. 3rd ed. Andover: Cengage Learning