   Go backward to A.5 Recursive DefinitionsGo up to A Defining New Notions ## 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.

Example
• Take the theory of natural numbers with function constants 0 and '. We define a new function constant
x + y := if y = 0 then x else (x+y-)'
The value of the term ((0'''+(0'+0'))+0'') is 0'''''''.
• Take the theory of lists with function constants "nil" and "cons". We define new function constants
 first(x) := such a: exists b: x=cons(a, b); rest(x) := such b: exists a: x=cons(a, b); append(x, y) := if x = nil then y else cons(first(x), append(rest(x), y)).
The value of "append(rest(cons(1, cons(2, nil))), cons(3, cons(4, nil)))" is "cons(2, cons(3, cons(4, nil)))".

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   