+Decidability
+============
+
+The question whether two formulas are syntactically equal is "decidable": we can construct a computation that's guaranteed to always give us the answer.
+
+What about the question whether two formulas are convertible? Well, to answer that, we just need to reduce them to normal form, if possible, and check whether the results are syntactically equal. The crux is that "if possible." Some computations can't be reduced to normal form. Their evaluation paths never terminate. And if we just kept trying blindly to reduce them, our computation of what they're convertible to would also never terminate.
+
+So it'd be handy to have some way to check in advance whether a formula has a normal form: whether there's any evaluation path for it that terminates.
+
+Is it possible to do that? Sure, sometimes. For instance, check whether the formula is syntactically equal to Ω. If it is, it never terminates.
+
+But is there any method for doing this in general---for telling, of any given computation, whether that computation would terminate? Unfortunately, there is not. Church proved this in 1936; Turing also essentially proved it at the same time. Geoff Pullum gives a very reader-friendly outline of the proofs here:
+
+* [Scooping the Loop Snooper](http://www.cl.cam.ac.uk/teaching/0910/CompTheory/scooping.pdf), a proof of the undecidability of the halting problem in the style of Dr Seuss by Geoffrey K. Pullum
+
+
+
+##[[Lists and Numbers]]##
+