previous up next
Go backward to A.5 Recursive Definitions
Go up to A Defining New Notions
RISC-Linz logo

A.6 Evaluating Definitions

With the help of the notions theory and definition, we can state very precisely what "evaluating a term" or "computing the value of a term" or just "computing" means.

Definition 147 (Computing) We are given a theory with constants C and a set of definitions that extend the theory by additional constants C'. Let T' be a term constructed from the constants in C union C'.

The problem of  computing (berechnen) the value of T' is to find a term T that is constructed from the constants in C such that from the axioms of the extended theory

T = T'
can be derived.

"Computing" the value of a term is therefore a reduction of the notions of the extended theory to the notions of the core theory. If the definitions are given in particular "constructive" forms, the evaluation may proceed automatically by the application of certain substitution rules.


Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next