author = {Alexander Zapletal},
title = {{Compilation of Theorema Programs}},
language = {english},
abstract = { In this thesis we present a compiler which is able to translate Theorema programs into executable Java code, which can then be used for extensive and fast calculations called from within Theorema. Generally, it can be observed that higher elegance in programming languages and software systems must be paid for by dramatically increasing computing times, see for example Prolog computations and original Theorema. One of the basic strategical goals of the Theorema system is to offer predicate logic as a uniform frame for the three main activities of mathematics: proving, solving, and computing. It is one of the strong features of Theorema that it combines automated theorem proving and computation in one logical and software frame. In fact, the same Theorema definitions that are used for stating and proving theorems can also be applied for computing. The actual motivation for this thesis was the slowness of computations in the current version of Theorema, which is due to the usage of special logical inference rules (directed equational logic) as an interpreter for the Theorema algorithms. Therefore, it is of utmost importance to find a way to drastically speed-up the execution of Theorema algorithms without losing the elegance of writing the algorithms in the same predicate logic version (namely that of Theorema) in which also general mathematical statements, in particular correctness theorems for algorithms, are expressed. The main approach for achieving this goal is compilation of Theorema algorithms into a machine-oriented language, in our case Java. It turns out that this is possible for Theorema algorithms, at least for a well defined and rich class of practically interesting algorithms that includes the full power of induction, sequence variables, and even functors. In this thesis we will show how this goal of compilation of Theorema programs can be achieved in a satisfactory way that brings the execution times of compiled Theorema programs drastically below the execution times of Mathematica algorithms and not more than a factor of 100 above the execution times of hand coded Java algorithms.},
number = {08-04},
year = {2008},
month = {May},
keywords = { Compilation, Predicate Logic, Theorema},
length = {124},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}