Detecting termination using size-change in parameter values

Examensarbete för masterexamen

Använd denna länk för att citera eller länka till detta dokument: https://hdl.handle.net/20.500.12380/18058
Ladda ner:
Fil Beskrivning StorlekFormat 
exjobb.pdfFulltext430.9 kBAdobe PDFVisa
Typ: Examensarbete för masterexamen
Master Thesis
Titel: Detecting termination using size-change in parameter values
Författare: Wahlstedt, David
Sammanfattning: 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.
Nyckelord: Datalogi;Computer science
Utgivningsdatum: 2000
Utgivare: 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
Samling:Examensarbeten för masterexamen // Master Theses



Materialet i Chalmers öppna arkiv är upphovsrättsligt skyddat och får ej användas i kommersiellt syfte!