Semi-continuous Sized Types and Termination

Some type-based approaches to termination use sized types: an ordinal boundfor the size of a data structure is stored in its type. A recursive functionover a sized type is accepted if it is visible in the type system thatrecursive calls occur just at a smaller size. This approach is only sound ifthe type of the recursive function is admissible, i.e., depends on the sizeindex in a certain way. To explore the space of admissible functions in thepresence of higher-kinded data types and impredicative polymorphism, asemantics is developed where sized types are interpreted as functions fromordinals into sets of strongly normalizing terms. It is shown that uppersemi-continuity of such functions is a sufficient semantic criterion foradmissibility. To provide a syntactical criterion, a calculus forsemi-continuous functions is developed.Comment: 33 pages, extended version of CSL'0