previous up next
Go backward to 2.3.4 Quantified Formulas
Go up to 2.3 Predicate Logic
 RISC-Linz logo

2.3.5 Local Definitions

Apart from universal and existential quantification of formulas, there exist several other frequently occurring quantifiers, most notably quantifiers for introducing local definitions.

Proposition 17 (Local Definitions) Let x be a variable, T and S be terms, and A be a formula. Then the following are formulas with bound variable x:
(let x = T: A)
(A where x = T)
The following are terms:
(let x = T: S)
(S where x = T)
We omit the parentheses, if A, T, and S are unambiguous.

This definition shows that also terms (not only formulas) may be quantified.

Alternative Forms  Various syntactic forms express local definitions.

The last line denotes the input syntax for the Logic Evaluator.

Proposition 18 (Semantics of Local Definitions) Let x be a variable, A be a formula, and T and S be terms. Under a given assignment in a domain,

Thus both operators let and where are just different syntactic forms for the same concept.

Example  Take the domain of natural numbers and assignment [x |-> 1]. Then the proposition
let y = 0: x <= y
is false because 1 <= 0 does not hold.

The function f defined as

f(x) := s*x+s where s=x+1
has the same meaning as if it were defined as
f(x) := (x+1)*x+(x+1).
The last example shows that local definitions are just convenient forms for structuring formulas by giving names to values. We can always remove the quantifier by replacing any free occurrence of the quantified variable x by its defining term T.

Example  The formula
x | y /\  exists z: y | z
   where y=2x
is equivalent to
x | 2x /\  exists z: 2x | z
Likewise, the formula
x | y /\  exists y: y | x
   where y=2x
is equivalent to
x | 2x /\  exists y: y | x
However, it is not equivalent to
x | 2x /\  exists y: 2x | x
because the second occurrence of y is within the scope of another quantifier that binds this variable.

Actually, local definitions can be replaced by existential respectively universal quantifiers.

Proposition 19 (Replacement of Local Definitions) Let x be a variable, T be a term, and A be a formula. Then we have
(let x = T: A) iff (forall x = T: A)
(let x = T: A) iff (exists x = T: A) 

The universal/existential formulas in above proposition are the previously introduced shortcuts for (forall x: x = T => A) and (exists x: x = T /\  A). The proposition is true, because for every term T there exists exactly one x such that x = T.

In the Logic Evaluator, local definitions are implemented for formulas as well as for terms as shown below:

Operational Interpretation  A term with a local definition is implemented in the evaluator by an object of the following Java class: 

public final class LetTerm implements Term
{
  private String variable;
  private Term term;
  private Term body;

  public LetTerm(String _variable, Term _term, Term _body)
  {
    variable = _variable;
    term = _term;
    body = _body;
  }

  public Value eval() throws EvalException
  {
    Context.begin(variable, term.eval());
    Value result = body.eval();
    Context.end();
    return result;
  }  
}
The Java expression new LetTerm(x, T, S) thus evaluates to the meaning of let x=T: S. As one can see, we construct a new context in which x is bound to the value of T and evaluate S in this context.

Formulas with local definitions are implemented analogously.

Convention  We merge multiple local definitions, i.e., instead of writing (let x=1: let y=2: (x+y)*(x-y)), we usually write

let x=1, y=2: (x+y)*(x-y)
or correspondingly
(x+y)*(x-y) where x=1, y=2
Also the Logic Evaluator implements local definitions 
let(x_0 = T_0, ..., x_n-1 = T_n-1: A)
with any number of quantified variables.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999
previous up next