Go backward to A.2 Explicit Predicate Definitions Go up to A Defining New Notions Go forward to A.4 Implicit Function Definitions |
f(x0, ..., xn-1) := Tis an explicit function definition (explizite Funktionsdefinition) which introduces an n-ary function constant f together with an axiom
forall x0, ..., xn-1: f(x0, ..., xn-1) = T.We call f(x0, ..., xn-1) the definiendum ("the one to be defined") and T the definiens ("the defining one").
A function f introduced by an explicit definition is uniquely characterized, i.e., there is exactly one f that satisfies the stated law (because for every x0, ..., xn-1, T has a single value).
The restriction that f must not occur in T avoids contradictions like in
f(x) := 1+f(x).All free variables of the definiendum must occur in the definens in order to avoid a dependence on the current variable assignment, such as in
f(x) := x+ywhere f(1) may be 2, 3, or any other number (depending on the current assignment of y).
Logic Evaluator A function is explicitly defined by a statement
which is to be read as f(x0, ..., xn-1) := T.fun f(x_0, ..., x_n-1) = T;
Conditional Definitions The value of a function is sometimes defined in different ways for different kinds of arguments, which can be expressed as
with terms T0 and T1 and formula F in all of which f does not occur and with no other free variables than x0, ..., xn-1. This is another form of writing
f(x0, ..., xn-1) := T0, if F T1, else (otherwise)
where the phrase (if F then T_0 else T_1) is introduced below.
f(x0, ..., xn-1) := if F then T0 else T1
(if F then T0 else T1)is a term whose value is the value of T0, if F holds, and the value of T1, otherwise. We omit the parentheses, if T1 is clear.
is another form of writing
|x| := -x, if x < 0 x, else
|x| := if x < 0 then -x else xwhich denotes the absolute value of x.
Logic Evaluator A conditional term is denoted as
which is to be read as (if F then T_0 else T_1).if(F, T_0, T_1)
Constrained Function Domains In a definition f(x0, ..., xn-1) := T, the value of T may not be defined for some x0, ..., xn-1, i.e., there is no knowledge that relates this value to any other value.
f(x) := 1/x.We do not know anything about f(0) because we do not know anything about the value 1/0.
In order to make undefined function values explicitly visible, we often write a definition in the following format (provided that we operate in the domain of sets):
is a constrained function definition which introduces an n-ary function constant f such that
f: A -> B f(x0, ..., xn-1) := T
forall x0, ..., xn-1, y: f(x0, ..., xn-1) = y <=> (<x0, ..., xn-1> in A /\ y = T).
Above definition characterizes f uniquely.
Please note that, for every x0, ..., xn-1, we have to prove
<x0, ..., xn-1> in Abefore we are allowed to deduce
f(x0, ..., xn-1) = T.
Furthermore, we still have to prove
(forall x0, ..., xn-1: <x0, ..., xn-1> in A => T in B)before we are allowed to assume
f(x0, ..., xn-1) in B.
where R denotes the set of real numbers and R >= 0 denotes the set of non-negative real numbers. For every a in R, we have
| |: R -> R >= 0 |x| := -x, if x < 0 x, else
|a| = if a < 0 then -a else a.However, the value of |i| (where i denotes the imaginary number) is undefined because i not in R.
Furthermore, we can prove
forall x: (if x < 0 then -x else x) in R >= 0because, for a real x < 0, -x in R >= 0, and for a real x not < 0, x in R >= 0. Thus we indeed have
| |: R -> R >= 0.
Logic Evaluator A constraint on the function domain can be expressed in various ways:
lets the evaluation of a function application f(a) abort with an error message, if P(a) does not hold. We have the predefined unary predicatesf(x: P)
Nat
, Set
, Tuple
that test whether a value is a natural
number, a set, or a tuple, respectively.
lets the evaluation of a function application f(a) abort if a not in S.f(x in S)
if
to define a function as
If the condition F does not hold on the input arguments, the evaluation of the function is aborted with an error message.fun f(x) = if(F, T);
which may speed up the evaluation.option check = false;