Review of need for termination analysis for recursive functions on inductive datatypes.  Discussion of a serious problem with syntactic termination checks, namely noncompositionality.  A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check.  So we need a compositional termination check, which will be discussed in subsequent episodes.