b'
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.
'