cs103l
cs103l is a CS theory class designed over a long period of time with college roommate Lucas Garron. It was intended to fill a void in the current Stanford CS curriculum.
The class can be summarized as "uncomputability and unprovability". The course description was: Topics in mathematical logic introduced from a computer science perspective, focused around unprovability and uncomputability. Gödel’s incompleteness theorems and the Church-Turing Thesis as limits in various models of computation: Turing machines, lambda calculus, and recursive functions. Formal systems, models, provability, consistency, and completeness. Fixed-point theorems and paradoxes. Connections and implications for computer programs.
This video I made illustrates sample content from Week 6, Lecture 2. The following was our syllabus: • Week 1: Proof Systems • Lecture 1: Introduction, Axiom Systems, and Theorem Space • Lecture 2: Math vs. Metamath • Week 2: Syntax and Semantics • Lecture 1: Syntax and Semantics • Lecture 2: Interpretations on Systems • Week 3: Formal Systems • Lecture 1: Models • Lecture 2: Compactness, Completeness, and Consistency • Week 4: Preparation for Incompleteness • Lecture 1: Gödel-numbering • Lecture 2: Proof-pairs • Week 5: Incompleteness • Lecture 1: Fixed Points • Lecture 2: Constructing Gödel’s sentence G • Week 6: Turing Machines • Lecture 1: Turing Machines, the Busy Beaver function • Lecture 2: Incompleteness/Uncomputability in Turing Machines • Week 7: Primitive Recursive Functions and Recursive Functions • Lecture 1: Recursion Theory • Lecture 2: Incompleteness/Uncomputability in Recursive Functions • Week 8: Lambda Calculus • Lecture 1: Lambda Calculus • Lecture 2: Incompleteness/Uncomputability in lambda calculus • Week 9: Theory of Programming • Lecture 1: Programming Languages as Proof Systems • Lecture 2: Syntax and Semantics in Programming Languages • Week 10: In Practice • Lecture 1: Uncomputability and You: A Programmer's Guide to Modest Intuitions • Lecture 2: (buffer slot) We had the following homework plan: 1. Programming Assignment: Proof Search 2. Problem Set: Semantics and Provability 3. Programming Assignment: Higher-Order Quines 4. Problem Set: Models of Computation To see lecture slides, e-mail me or Lucas Garron. cs103l was never finished, and is currently on hiatus, to be resumed at an indeterminate point in the future. |