COURSE DIRECTOR	CLASSES (see also Lecture Schedule )
G. Tourlakis	Tuesdays and Thursdays
Room 2051,  LAS	11:30  - 13:00
e-mail: gt@cse.yorku.ca	Classrooms: VH 3005 (TUE) and BRG 213 (THURS)
	York Campus

• Can we ever invent a program that solves the program correctness problem? I.e., the question “Is this program faithful to its spec?”

• OK, how about doing it for "simple” programs only? Say programs that involve just loops that are never nested more than 2 levels? (like your familiar Quicksort).   Certainly the famous technique that uses "loop invariants" and induction would work as a mechanical, standard approach to answer the correctness question for all these problems? Yes?
  

• What can we say about "automatic theorem provers"? Those are great tools that assist you to verify that a given formula of a theory is indeed a theorem.

• Unfortunately we will also learn something unpleasant about the efficiency of theorem provers: Any theorem prover for number theory will take an unreasonably, hopelessly humongous number of steps (OK, OK, we will make this precise in the lectures :) to verify the theoremhood of each of a set of infinitely many trivial theorems of arithmetic — so trivial that you can readily verify by hand!

• We will even learn (after Gödel) that formal logic — like the one we study in MATH 1090 — has serious limitations too: There are infinitely many TRUE statements of number theory that have NO syntactic proofs! Interestingly the proof of this fact that uses computability theory is way simpler than Gödel's original proof.

So, the plan is to

1. Mathematically introduce our objects of study: Programs, and computations. We do so using the Unbounded Register Machines of Shepherdson and Sturgis (URMs).
2. Thoroughly study the theoretical and insurmountable limitations of computing: That is, study the theory of Computability and UNComputability, with an introduction to Complexity.

Topics will include: A mathematical model of computation (URMs); Primitive Recursion and Loop Programs; Arithmetisation of machines and computations;  Kleene's Predicate; Church's Thesis; Unsolvability via Diagonalisation and Reductions; The Recursion Theorem; The connection between Uncomputability and Unprovability: Gödel's First Incompleteness Theorem through the Halting Problem; The complexity of Primitive Recursive functions and relations via the hierarchy approach (Axt, Loop-Program, Grzegorczyk hierarchies) including the Ritchie-Cobham theorem.

This course delves deeper into work that started in EECS 2001.

Prerequisites. General Prerequisites, including EECS 3101 3.0 and, by transitivity, EECS 2001, MATH1090 3.0 and MATH(EECS)1019 3.0 or
similar courses.

The essential prerequisite for EECS4111/EECS5111 is a certain degree of proficiency in following and formulating
combinatorial arguments. Such proficiency should be normally acquired by a student who has successfully
completed a course such as EECS2001.03 (or EECS3101.03) and MATH 1090.03. 

Ideally (but not absolutely necessarily) the student should be familiar with the mathematical topics that are reviewed in the first chapter of the text. Students should visit said chapter as frequently as needed.

Students who have not completed any of the above courses, but who (strongly) believe nevertheless that they have
the equivalent background, should seek special permission to enrol in consultation with the instructor who can assess whether
indeed the equivalent background is in hand. This is a necessary condition for admission to the course without the on paper prerequisites. The EECS-gpa requirement cannot be waived.

Work-Load and Grading.

The course grade will solely be based  on about 3-4 homework assignments that will be completed
by students individually. These will be equally weighted. There will be no programming problems, but each assignment
will consist of a number of theoretical problems, for example "prove that such-and-such
a problem is unsolvable", or "prove that such-and-such function is primitive recursive", etc.

Graduate students in the course (registered in EECS5111) will be assigned additional problems and readings,
and will be expected to probe the material further and deeper through the completion of these problems.

The concept of "late assignments" does not exist (because solutions are posted typically on the due date).

Official textbook.

• G. Tourlakis, Theory of Computation, Wiley, 2012.
  

• Demonstrate knowledge of, via application: the concepts of “computation”, and “computable” and “uncomputable” functions, “decidable”, semi-decidable” (or “recursively enumerable”) and “undecidable” decision problems in terms of  mathematical models of computation (e.g., Unbounded Register Machines, Turing Machines).
• Design programs, in a mathematical model of computation, that compute specified functions or solve specified decision problems.
• Define Church’s Thesis and use it fluently to design “pseudo programs” that compute functions or decide/semi-decide decision problems.
• Prove undecidability and non-semi-decidability results via diagonalisation and/or reduction arguments.
• Understand and reproduce the argument that connects uncomputability in the theory of computation with unprovability in logic: Gödel's First Incompleteness Theorem through the viewpoint of the halting problem.
• Understand the concept of subrecursive complexity hierarchies (e.g., Axt, Grzegorczyk, Loop-program) and be able to place a given function or decision problem in a complexity class in such a hierarchy.
  

Additional References.

(1) G. Tourlakis, Computability, Reston Publishing Company, 1984.

For more on Primitive Recursive and (total) Recursive functions see:

(2) R. Péter, Recursive Functions, Academic Press (Number-theoretic approach, rigorous, fairly difficult).

For more on unsolvability of concrete problems of combinatorial or number theoretical nature, see:

(3) M. Davis, Computability and Unsolvability, McGraw-Hill (Turing approach, rigorous, fairly difficult).

Matijasevic’s proof of the unsolvability of Hilbert’s 10th problem, using methods initiated by Davis
in (3) can be found in:

(4) Y.I. Manin, A Course in Mathematical Logic, Springer-Verlag (quite difficult).

For more on recursion theory, in general, see:

(5) H. Rogers, Theory of Recursive Functions and Effective Computability, McGraw-Hill (Semi-formal
using Church’s thesis throughout; difficult).

Finally, for more on machines (at an elementary level), see:

(6) M. Minsky, Computation; Finite and Infinite Machines, Prentice-Hall. __
 
 
 
  Last changed: August 21, 2019.