Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-14T11:18:07.433Z 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)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Information

Type
Regular Papers
Copyright
© 2005 Cambridge University Press