192.017 Theoretical Computer Science

1. Decidability (Reinhard Pichler):
   • Problem
     • Co Decision Problem
     • Problems:
       • Halting Problem
         • Co-Halting Problem
       • Same Output Problem
       • Correctness Problem
       • k-Colouring Problem
       • 2-SAT
       • Exactly One of Two Reachable Code Problem
   • Algorithm
   • Computable Function
     • Computable Total Function
     • Computable Partial Function
   • Decision Problem
     • Decidable Decision Problem
     • Undecidable Decision Problem
     • Semi-Decidable Decision Problem
     • Co Decision Problem
   • Cantor’s Theorem
     • Countable Set
     • Uncountable Set
     • Rational Numbers
   • Reduction
     • Turing Reduction
     • Many-One Reduction
2. Computability (Christian Fermüller):
   • Church-Turing Thesis
     • Hilbert’s Programme
     • On Computable Numbers, with an Application to the Entscheidungsproblem
   • Turing Machine
     • Configuration
     • Deterministic Turing Machine
     • Accepted Language
     • Recursively Enumerable Language
     • Recursive Language
   • Arithmetic Function
     • Turing-Computable Arithmetic Function
   • Register Machine
     • Register Machine Program
   • Lambda Calculus
     • Lambda Term
       • Lambda Abstraction
       • Lambda Variable
     • Combinator
     • Reductions
       • Alpha Reduction
       • Beta Reduction
         • Beta Equivalence
       • Church-Rosser Theorem
       • Redex
       • Normal Form
     • Currying
     • Church Encoding
       • Church Numeral
       • Successor Function
     • Fixed Point
       • Fixed-Point Combinator
       • Fixed-Point Theorem
       • Y Combinator
   • Primitive Recursion
     • Primitive-Recursive Function
     • MuZero Operator
     • MuBar Operator
     • Mu-Recursive Function
   • Rice’s Theorem
     • Language Property
       • Extensional Language Property
       • Trivial Extensional Language Property
     • Function Property
       • Extensional Function Property
       • Non-Trivial Function Property
3. Formal Languages (Marion Oswald):
   • Alphabet
     • Finite Alphabet
     • Word
     • Empty Word
     • Palindrome
     • Set of all Strings
     • Set of all Languages
     • Word Homomorphism
   • Turing Machine (second definition, i.e. with boundary symbols $Z_0,Z_1,Z_2$)
     • Normal Form
     • Linear Bounded Automaton
     • Normal Form (Turing Machine)
     • Pushdown Automaton Criterion
       • Normal Form
     • Finite Automaton
       • Deterministic Finite Automaton
       • Nondeterministic Finite Automaton
       • Equivalent Expressiveness of NFA and DFA
       • Determinisation
     • Automaton Equivalence: $\mathcal{L}(A_1)=\mathcal{L}(A_2)$
   • Formal Language
     • Recursively Enumerable Language
     • Context-Sensitive Language
     • Context-Free Language
       • Pumping Lemma (Context-free Languages)
     • Regular Language
       • Pumping Lemma (Regular Languages);
   • Word Problem
   • Grammar
     • Sentential Form
     • Generated Language
     • Production Rule
     • Monotone Grammar
     • Type-i Grammar
       • Regular Grammar
       • Context-Free Grammar
         • Ambiguous Context-Free Grammar
         • Inherently Ambiguous Context-Free Language
         • Unambiguous Context-Free Grammar
         • Reduced Context-Free Grammar
       • Context-Sensitive Grammar
       • Unconstrained Grammar
     • equivalent expressiveness: monotone and context-free grammar
   • Chomsky Hierarchy
     • Closure (bold are important)
   • Normal Forms:
     • Chomsky Normal Form
     • Greibach Normal Form
       • Extended Greibach Normal Form
   • Dyck Language
     • Chomsky–Schützenberger Theorem
4. Complexity Theory (Stefan Woltran):
   • Extended Church-Turing Thesis
   • Interpretation
   • Problems:
     • Model-Checking Problem
     • SAT Problem
       • 3-Satisfiability Problem
     • k-Coloring Problem
     • 3-Colouring Problem
       • Reduction to SAT
     • Graph-Reachability Problem
     • Independent Set Problem
       • Independent Set
     • Vertex Cover Problem
       • Vertex Cover
     • Clique Problem
       • Clique
     • Hamiltonian Path Problem
       • Hamiltonian Path
   • Reduction
     • Turing Reduction
     • Many-One Reduction
       • reduction must be easier to compute than each problem
       • reduction must be efficiently ($O(n^k)$) computable
       • Correct Many-One Reduction
     • Correct Reduction
     • Complexity Transfer
       • Sub-problems of a problem are special cases of that problem and have a the complexity of the problem as upper bound
   • Complexity Class
     • Class L
     • Class PSPACE
     • EXPTIME
     • Polynomial Complexity Class
       • Tractable Problem
       • Intractable Problem
     • Nondeterministic Polynomial Complexity Class
       • Certificate
       • Polynomial Balanced Binary Relation
       • Polynomial Decidable Binary Relation
       • NP-complete Problem
       • NP-hard Problem
     • P vs NP Problem
5. Formal Correctness of Programs (Gernot Salzer):
   • Syntax
   • Semantic
     • Operational Semantics
       • Structural Operational Semantics
       • Natural Semantics
     • Axiomatic Semantics
   • Entailment
     • Logical Strength
   • Program
     • Program State
     • Program Configuration
       • Final Program Configuration
       • Stuck Program Configuration
     • Program Transition
       • Deterministic Program Transition
       • Nondeterministic Program Transition
     • Program Run
       • Complete Program Run
       • Finite Program Run
       • Infinite Program Run
     • Program Semantics
       • Semantic Equivalence
       • Program Sequencing
     • Formula Satisfaction Set
     • Correct Program
       • Partially Correct Program
       • Totally Correct Program
   • Hoare Calculus
     • Empty Program
     • Implication
     • Sequential Composition
     • Standard Backward Assignment
     • Forward Assignment
     • Simplified Forward Assignment
     • Conditional Rule
     • Loop Termination
   • Weakest Precondition
     • Weakest Liberal Precondition
   • Strongest Postcondition
   • Annotation Calculus