Go backward to A.3 Explicit Function DefinitionsGo up to A Defining New NotionsGo forward to A.5 Recursive Definitions

## A.4 Implicit Function Definitions

In some situations, it is more convenient to describe a function rather by a condition between the argument values and the result value than by a term that denotes the result value. Such an  implicit function definition (implizite Funktionsdefinition) is typically written in the form.
Let f(x0, ..., xn-1) be a y such that F.

However, this is just another way of writing an explicit definition

f(x0, ..., xn-1) := such y: F
where (such y: F) is a term in which f does not occur and with no other free variables than x0, ..., xn-1 (y is bound).

Definition 142 (Such Quantifier) For every variable x and formula F, the phrase
(such x: F)
is a term with bound variable x.

The value of this term is some x such that F holds (if such an x exists). We omit the parentheses if F is clear.

Frequently, we write

such x in S: F
to denote such x: x in S /\  F.

Reasoning  When reasoning about implicitly defined objects with have to take special care because the definition may be inconsistent (i.e., no object with the denoted property exists) or not unique (multiple objects satisfy the property).

All that we actually have is the knowledge

 (exists x: F) => (forall x: x = (such x: F) => F),
i.e., if an object with property F exists, then the object denoted by the "such term" satisfies F as well.

Consequently, we have for a function definition

f(x0, ..., xn-1) := such y: F
the knowledge
 (forall x0, ..., xn-1: (exists y: F) => (forall y: y = f(x0, ..., xn-1) => F)),
i.e., for any tuple of function arguments the result value satisfies F, provided that such a value indeed exists.

Therefore, for given x0, ..., xn-1, we first have to prove

exists y: F.
before we may assume that, for every y = f(x0, ..., xn-1), F holds.

Example  We define
x/y := such q: q*y = x.
Then 12/4 = 3 because 3*4 = 12.

Take a := 1/0. We must not assume that a*0 = 1, because we cannot prove exists q: q*0 = 1.

Such Terms and Predicates  An alternative to defining a function

 f(x) := such y: F
is always to define a predicate
 p(x, y) : <=> F.
Apparently, we then have the relationship
 f(x) := such y: p(x, y).
However, it may be easier to understand (and to reason about) statements that are formulated with the help of the predicate than with the corresponding "such" term: for every formula G, the statement
 G[y <- f(x)]
is equivalent to
 (forall y: p(x, y) => G)
which may be preferrable in some situations.

Example  We define in Section Sequences and Series the limit of a sequence s as
 lim(s) := such a: s converges to a.
We then wish to state that, for all sequences s and t,
 lim(s+t) = lim(s)+lim(t)
where, for every i in N, (s+t)i = si + ti.

Inserting the definition of "lim" gives us the statement

 (such a: s+t converges to a) = (such b: s converges to b) + (such c: t converges to c)
which is rather difficult to prove.

However, above statement can be also formulated as

 forall a, b, c: (s+t converges to a /\  s converges to b /\  t converges to c) => a = b+c.
which is much more amenable to a formal proof.

As the previous example shows, it may be advisable to "switch" from the formulation of a statement with "such terms" to a statement with corresponding predicates to understand the subtleties of the statement.

Logic Evaluator  We have a restricted form of the "such" quantifier that allows to express the value of the term (such x in S: F) as

```such(x in S: F, x)
```
In general, the quantifier binds multiple variables x0, ..., xn-1 and returns a value of term T where F holds:
```such(x_0  in~ T_0, ..., x_n-1  in~ T_n-1: F, T)
```
The value of this term can be expressed by the standard quantifier as
 (let t = such t that (exists x0 in T0, ..., xn-1 in Tn-1: t= /\  F) x0 = t0, ... xn-1 = tn-1: T)
where t is a variable that does not occur in T and F.

Operational Interpretation  A `such` expression is an instance of the Java class shown below.

```public final class SuchThat implements Term
{
private String variable;
private Term domain;
private Formula formula;
private Term term;

public SuchThat(String _variable, Term _domain,
Formula _formula, Term _term)
{
variable = _variable;
domain = _domain;
formula = _formula;
term = _term;
}

public Value eval() throws EvalException
{
Iterator iterator = Model.iterator(domain);
while (iterator.hasNext())
{
Value result = null;
Context.begin(variable, iterator.next());
if (formula.eval())
result = term.eval();
Context.end();
if (result != null) return result;
}
throw new EvalException("no such value");
}
}
```

The Java expression ```(new SuchThat(x, d, F, T)).eval()``` computes the value of let x = (such x in d: F): T. As one can see, we iterate over d and establish new contexts in which x is assigned each value of the domain in turn. In each context, we evaluate F. If the formula is true, we evaluate T and return its value.

Unique Implicit Function Definitions  The "such quanifier" does not necessarily determine a unique value, consequently an implicit function definition not always determines a function uniquely.

Example  We define
Let f(x) be a y such that y | x.
or, in other words,
f(x) := such y: y | x
where | denotes the predicate "divides". Then all we know is that f(12) | 12 (because exists y: y | 12), and consequently f(12) in {1, 2, 3, 4, 6, 12}.

Frequently, however an implicit definition is given in the form

let f(x0, ..., xn-1) be the y such that F
which implies that there exists at most one y that satisfies F for given x0, ..., xn-1.

This is equivalent to stating, in addition to

 f(x0, ..., xn-1) := such y: F,
also the condition (which has to be proved)
 (forall x0, ..., xn-1, y: F => y = f(x0, ..., xn-1)).

Example  It is wrong to write
Let f(x) be the y such that y | x.
because from 6|12 we must not conclude f(12) = 6.

However, we may define

Let x/y be the q such that q*y = x.
Since 3*4=12, we may conclude 12/4 = 3.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999