Operational Semantics of Termination Types

In principle termination analysis is easy: find a well-founded ordering and prove that calls decrease with respect to the ordering. We show how to embed termination information into a polymorphic type system for an eager higher-order functional language allowing multiple-argument functions and algebraic data types. The well-founded orderings are defined by pattern matching against the definition of the algebraic data types. We prove that the analysis is semantically sound with respect to a big-step (or natural) operational semantics. We compare our approach based on operational semantics to one based on denotational semantics and we identify the need for extending the semantic universe with low constructs whose sole purpose is to facilitate the proof. For dealing with partial correctness it suffices to consider approximations that are less defined than the desired fixed points; for dealing with total correctness we introduce functions that are more defined than the fixed points