Hostname: page-component-76fb5796d-vfjqv Total loading time: 0 Render date: 2024-04-26T17:39:53.537Z Has data issue: false hasContentIssue false

On termination of meta-programs

Published online by Cambridge University Press:  09 May 2005

ALEXANDER SEREBRENIK
Affiliation:
LaQuSo, TU/e, Den Dolech 2, 5600 MB Eindhoven, The Netherlands (e-mail: a.serebrenik@tue.nl)
DANNY DE SCHREYE
Affiliation:
Department of Computer Science, K.U. Leuven, Celestijnenlaan 200A, B-3001, Heverlee, Belgium (e-mail: Danny.DeSchreye@cs.kuleuven.ac.be)

Abstract

The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis for a broad class of practical meta-interpreters, including negation and performing different tasks during the execution. It is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs. The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of those implies termination of the other one, i.e. the meta-interpreter preserves termination. Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.

Type
Regular Papers
Copyright
© 2005 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)