Termination proofs for a lazy functional language by abstract reduction : (draft)

Automatic termination proofs of functional programming languages are an often challenged problem Most work in this area is done on strict languages Orderings for arguments of recursive calls are generated In lazily evaluated languages arguments for functions are not necessarily evaluated to a normal form It is not a trivial task to de ne orderings on expressions that are not in normal form or that do not even have a normal form We propose a method based on an abstract reduction process that reduces up to the point when su cient ordering relations can be found The proposed method is able to nd termination proofs for lazily evaluated programs that involve non terminating subexpressions Analysis is performed on a higher order polymorphic typed language and termi nation of higher order functions can be proved too The calculus can be used to derive information on a wide range on di erent notions of termination.

Metadaten
Verfasserangaben:	Sven Eric Panitz
URN:	urn:nbn:de:hebis:30-8938
URL:	http://www.ki.informatik.uni-frankfurt.de/papers/panitz/term.ps
Titel des übergeordneten Werkes (Englisch):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 6
Schriftenreihe (Bandnummer):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (6)
Verlag:	Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Verlagsort:	Frankfurt [am Main]
Dokumentart:	Arbeitspapier
Sprache:	Englisch
Jahr der Fertigstellung:	1996
Jahr der Erstveröffentlichung:	1996
Veröffentlichende Institution:	Universitätsbibliothek Johann Christian Senckenberg
Datum der Freischaltung:	12.05.2005
HeBIS-PPN:	190224711
Institute:	Informatik und Mathematik / Informatik
DDC-Klassifikation:	0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):	Deutsches Urheberrecht

Open Access