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

is anf(x_{0}, ...,x_{n-1}) :=T

We callforallx_{0}, ...,x_{n-1}:f(x_{0}, ...,x_{n-1}) =T.

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 `x`_{0}, ..., `x`_{n-1}, `T`
has a single value).

The restriction that `f` must not occur in `T`
avoids contradictions like in

All free variables of the definiendum must occur in the definens in order to avoid a dependence on the current variable assignment, such as inf(x) := 1+f(x).

wheref(x) :=x+y

**Logic Evaluator** A function is explicitly defined by a statement

which is to be read asfunf(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

f(x_{0}, ...,x_{n-1}) :=T_{0},ifFT_{1},else(otherwise)

where the phrase (

f(x_{0}, ...,x_{n-1}) :=ifFthenT_{0}elseT_{1}

(is a term whose value is the value ofifFthenT_{0}elseT_{1})

is another form of writing

| x| := -x,ifx< 0x,else

|which denotes thex| :=ifx< 0then-xelsex

**Logic Evaluator** A conditional term is denoted as

which is to be read as (if(F,T_0,T_1)

**Constrained Function Domains**
In a definition
`f`(`x`_{0}, ..., `x`_{n-1}) := `T`,
the value of `T` may not be defined for
some `x`_{0}, ..., `x`_{n-1}, i.e., there is no knowledge
that relates this value to any other value.

We do not know anything aboutf(x) := 1/x.

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

f:A->Bf(x_{0}, ...,x_{n-1}) :=T

forallx_{0}, ...,x_{n-1},y:f(x_{0}, ...,x_{n-1}) =y<=> (<x_{0}, ...,x_{n-1}> inA/\y=T).

Above definition characterizes `f` uniquely.

Please note that, for every `x`_{0}, ..., `x`_{n-1},
we have to prove

<before we are allowed to deducex_{0}, ...,x_{n-1}> inA

f(x_{0}, ...,x_{n-1}) =T.

Furthermore, we still have to prove

(before we are allowed to assumeforallx_{0}, ...,x_{n-1}: <x_{0}, ...,x_{n-1}> inA=>TinB)

f(x_{0}, ...,x_{n-1}) inB.

where

| |: R->R_{ >= 0}| x| := -x,ifx< 0x,else

|However, the value of |a| =ifa< 0then-aelsea.

Furthermore, we can prove

because, for a realforallx: (ifx< 0then-xelsex) inR_{ >= 0}

| |: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

lets the evaluation of a function application`f`(`x`:`P`)`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

lets the evaluation of a function application`f`(`x`in`S`)`f`(`a`) abort if`a`not in`S`. - We may use the binary function
`if`

to define a function as

If the conditionfun

`f`(`x`) = if(`F`,`T`);`F`does not hold on the input arguments, the evaluation of the function is aborted with an error message.

which may speed up the evaluation.option check = false;

Author: Wolfgang Schreiner

Last Modification: October 4, 1999