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

A.4 Implicit Function Definitions

Let f(x₀, ..., x_n-1) be a y such that F.

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

f(x₀, ..., x_n-1) := such y: F

(such x: F)

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

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),

Consequently, we have for a function definition

f(x₀, ..., x_n-1) := such y: F

(forall x0, ..., xn-1: (exists y: F) => (forall y: y = f(x0, ..., xn-1) => F)),

Therefore, for given x₀, ..., x_n-1, we first have to prove

exists y: F.

x/y := such q: q*y = x.

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

p(x, y) : <=> F.

f(x) := such y: p(x, y).

G[y <- f(x)]

(forall y: p(x, y) => G)

lim(s) := such a: s converges to a.

lim(s+t) = lim(s)+lim(t)

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)

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.

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)

such(x_0  in~ T_0, ..., x_n-1  in~ T_n-1: F, T)

(let

t = such t that

(exists x0 in T0, ..., xn-1 in Tn-1: t=<x0, ..., xn-1> /\  F)

x0 = t0,

...

xn-1 = tn-1:

T)

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.

Let f(x) be a y such that y | x.

f(x) := such y: y | x

Frequently, however an implicit definition is given in the form

let f(x₀, ..., x_n-1) be the y such that F

This is equivalent to stating, in addition to

f(x0, ..., xn-1) := such y: F,

(forall x0, ..., xn-1, y: F => y = f(x0, ..., xn-1)).

Let f(x) be the y such that y | x.

However, we may define

Let x/y be the q such that q*y = x.