Discussion of normalization (there is some way to reach a normal form) versus termination (no matter how you execute the term you reach a normal form).\xa0 A little more discussion of strong FP.\xa0 For type theory, the need for normalization due to Curry-Howard and due to conversion checking.