Go backward to A.2 Explicit Predicate DefinitionsGo up to A Defining New NotionsGo forward to A.4 Implicit Function Definitions

## A.3 Explicit Function Definitions

Definition 139 (Explicit Function Definition) Let f be a function constant of arity n that is not yet in use, x0, ..., xn-1 be n distinct variables, and T be a term in which f does not occur and with no other free variables than x0, ..., xn-1. Then the phrase
f(x0, ..., xn-1) := T
is 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+y
where 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

```fun f(x_0, ..., x_n-1) = T;
```
which is to be read as f(x0, ..., xn-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

 f(x0, ..., xn-1) := T0, if F T1, else (otherwise)
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) := if F then T0 else T1
where the phrase (if F then T_0 else T_1) is introduced below.

Definition 140 (Conditional Term) For every formula F and terms T0 and T1, the phrase
(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.

Example  The definition
 |x| := -x, if x < 0 x, else
is another form of writing
|x| := if x < 0 then -x else x
which denotes the absolute value of x.

Logic Evaluator  A conditional term is denoted as

```if(F, T_0, T_1)
```
which is to be read as (if F then T_0 else 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.

Example  We define the function over the real numbers
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):

Definition 141 (Constrained Function Definition) Let f be a function constant of arity n that is not yet in use, A and B be terms in which f does not occur, x0, ..., xn-1 be n distinct variables, and T be a term in which f does not occur and with no other free variables than x0, ..., xn-1. Then
 f: A -> B f(x0, ..., xn-1) := T
is a  constrained function definition which introduces an n-ary function constant f such that
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 A
before 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.

Example  We define
 |  |: R -> R >= 0 |x| := -x, if x < 0 x, else
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
|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 >= 0
because, 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:

• For a unary predicate P, a parameter declaration
```f(x: P)
```
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 predicates `Nat`, `Set`, `Tuple` that test whether a value is a natural number, a set, or a tuple, respectively.
• Likewise for a term S denoting a set, a parameter declaration
```f(x in S)
```
lets the evaluation of a function application f(a) abort if a not  in S.
• We may use the binary function `if` to define a function as
```fun f(x) = if(F, T);
```
If the condition F does not hold on the input arguments, the evaluation of the function is aborted with an error message.
The checking of constraints can be switched off by the command
```option check = false;
```
which may speed up the evaluation.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999