previous up next
Go backward to A.2 Explicit Predicate Definitions
Go up to A Defining New Notions
Go forward to A.4 Implicit Function Definitions
RISC-Linz logo

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:

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

previous up next