Podcasts Technology Iowa Type Theory Commute Noncompositionality of syntactic structural-recursion checks

Noncompositionality of syntactic structural-recursion checks

Published: March 20, 2020, 4 a.m.

b'

Review of need for termination analysis for recursive functions on inductive datatypes.\\xa0 Discussion of a serious problem with syntactic termination checks, namely noncompositionality.\\xa0 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.\\xa0 So we need a compositional termination check, which will be discussed in subsequent episodes.

'