Detecting termination using size-change in parameter values

Examensarbete för masterexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
exjobb.pdfFulltext430.9 kBAdobe PDFView/Open
Full metadata record
DC FieldValueLanguage
dc.contributor.authorWahlstedt, David
dc.contributor.departmentChalmers tekniska högskola / Institutionen för datavetenskapsv
dc.contributor.departmentChalmers University of Technology / Department of Computing Scienceen
dc.description.abstractWe 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.
dc.subjectComputer science
dc.titleDetecting termination using size-change in parameter values
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
Collection:Examensarbeten för masterexamen // Master Theses

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