AbstractIn 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 new 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.
Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.2 [Programming Languages]: Language Classifications; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
Additional Key Words and Phrases: semantics of programming languages, annotated type and effect systems, proof techniques for operational semantics, higher-order functional languages
Selected references
- Marianne Baudinet. Proving termination properties of {\sc prolog} programs: A semantic approach. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 336-347, Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.
- Patrick Cousot and Radhia Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 83-94, Albequerque, New Mexico, January 1992.
- Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84-96, Tucson, Arizona, January 1978.
- Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279-301, March 1982.
- Philippe Flajolet, Bruno Salvy, and Paul Zimmermann. Automatic average-case analysis of algorithms. Theoretical Computer Science, 79(1):37-109, 21 February 1991.
- David MacQueen, Gordon G. Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. In Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, pages 165-174, Salt Lake City, Utah, January 1984.
- Ursula Martin and Elizabeth Scott. The order types of termination orderings on monadic terms, strings and multisets. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 356-363, Montreal, Canada, 19-23 June 1993. IEEE Computer Society Press.
- Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, December 1978.
- Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 162-173, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.
- Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245-296, June 1994.
- H. Zantema. Termination of term rewriting: Interpretion and type elimination. Journal of Symbolic Computation, 17(1):23-50, January 1994.