Sipser's Theory of Computation

I stayed up late reading Sipser's Introduction to the Theory of Computation looking for high level connections between chapters. When I woke up I remembered that:

Finite Automata (FA) can recognize formal languages. A Deterministic Finite Automata's (DFA) next state for a given input is certain but a Non-deterministic Finite Automata's (NFA) is not: it might have two transitions for the same state. An algorithm exists to convert NFA into DFA. FA can recognize regular languages and an algorithm exists to convert FA into regular expressions. However FA have trouble with non-regular languages like {(0^n|1^n) for all n > 0}. Push down automata (PDA) are like finite automata but they have an infinite stack which they can use to recognize said language. We can describe languages by generating them from a context free grammar (CFG) OR recognizing them with a PDA. A CFG and PDA are equivalent. The church-turing thesis precisely defines what an algorithm is such that it must be computable by the lambda calculus or a turing machine; which are equivalent. A turing machine is like a PDA but has an infinite array for random access, which is less restrictive than a stack, so it is more powerful. If a turing machine will stop while carrying out an algorithm then the algorithm is decidable. The halting problem is undecidable.