BROADCASTS.com

b'

Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration.\\xa0 On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion.\\xa0 Subdata of the input data are available at type R only, not at the original datatype.\\xa0 This allows us to make explicit recursive calls, but only on subdata.