+* [[!wikipedia Evaluation strategy]]
+* [[!wikipedia Eager evaluation]]
+* [[!wikipedia Lazy evaluation]]
+* [[!wikipedia Strict programming language]]<p>
+* [[!wikipedia Church-Rosser theorem]]
+* [[!wikipedia Normalization property]]
+* [[!wikipedia Turing completeness]]
+
+
+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.