Go backward to A.5 Recursive Definitions Go up to A Defining New Notions |
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.
x + y := if y = 0 then x else (x+y^{-})'The value of the term ((0'''+(0'+0'))+0'') is 0'''''''.
The value of "append(rest(cons(1, cons(2, nil))), cons(3, cons(4, nil)))" is "cons(2, cons(3, cons(4, nil)))".
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)).