Start / Iowa Type Theory Commute / Noncompositionality of syntactic structural recursion checks

Noncompositionality of syntactic structural-recursion checks

13 min • 20 mars 2020

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.