Doctoral seminars

< back

Tuesday November 13 at 14h00 in Celestijnenlaan 200A, room 03.14 (Cafetaria) On termination of meta-programs by Alexander Serebrenik

On termination of meta-programs

Alexander Serebrenik

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, together with different classes of object programs. It is based on combining power of general term-orders, 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 order needed to prove termination of the object program and the order needed to prove termination of the meta-interpreter together with this object program. If such a relationship is established, termination of one of those implies termination of the other one, i.e., that the meta-interpreter improves (preserves) termination.

Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.