Go backward to A.5 Recursive Definitions Go up to A Defining New Notions

A.6 Evaluating Definitions

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'

"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.

• 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)))".