Detecting termination using size-change in parameter values

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/18058
Download file(s):
File Description SizeFormat 
exjobb.pdfFulltext430.9 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Detecting termination using size-change in parameter values
Authors: Wahlstedt, David
Abstract: We present a method to automatically detect termination in a strict, first order functional language. This is a first step towards an application of the method on Agda (C. Coquand 1996). The method is based on a paper of Neil Jones et al. To any program, seen as a set of equations defining recursive functions, we associate a graph of calls, whose arcs are themselves graphs. These graphs describe for each call the size relations between the formal parameters and the actual parameters. The termination condition can then be stated in terms of these graphs: each infinite path in the graph of calls must contain an infinitely decreasing thread. What is surprising is that this condition can then be ecided by a fully automatic algorithm. The method is quite general, and it is not dependent of auxiliary requirements like for example lexicographically ordered parameters. We have written a small Haskell prototype and tested this method on some examples.
Keywords: Datalogi;Computer science
Issue Date: 2000
Publisher: Chalmers tekniska högskola / Institutionen för datavetenskap
Chalmers University of Technology / Department of Computing Science
URI: https://hdl.handle.net/20.500.12380/18058
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.