School of Computing

A hierarchy of languages with strong termination properties

Alastair Telford and David Turner

Technical Report TR 2-00, Computing Lab, University of Kent at Canterbury, The Computing Laboratory, The University, Canterbury, Kent, CT2 7NF, February 2000 Paper currently under revision.

Abstract

In previous papers we have proposed an elementary discipline of strong functional programming (ESFP), in which all computations terminate. A key feature of the discipline is that we introduce a type distinction between data which is known to be finite, and codata which is (potentially) infinite. To ensure termination, recursion over data must be well-founded, and corecursion (the definition schema for codata) must be productive, and both of these restrictions must be enforced automatically by the compiler. In our previous work we used abstract interpretation to establish the productivity of corecursive definitions in an elementary strong functional language. We show here that similar ideas can be applied in the dual case to check whether recursive function definitions are strongly normalising. We thus exhibit a powerful termination analysis technique which we demonstrate can be extended to partial functions.

Download publication 267 kbytes

Bibtex Record

@techreport{964,
author = {Alastair Telford and David Turner},
title = {A Hierarchy of Languages with Strong Termination Properties},
month = {February},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Paper currently under revision},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/964},
    address = {The Computing Laboratory, The University, Canterbury, Kent, CT2 7NF},
    institution = {Computing Lab, University of Kent at Canterbury},
    number = {TR 2-00},
    publication_type = {techreport},
    submission_id = {2320_949787316},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014