Go backward to 2.3.4 Quantified Formulas Go up to 2.3 Predicate Logic |
The following are terms:
(let x = T: A) (A where x = T)
We omit the parentheses, if A, T, and S are unambiguous.
(let x = T: S) (S where x = T)
This definition shows that also terms (not only formulas) may be quantified.
Alternative Forms Various syntactic forms express local definitions.
let(x = T: A)
The last line denotes the input syntax for the Logic Evaluator.
Thus both operators let and where are just different syntactic forms for the same concept.
let y = 0: x <= yis false because 1 <= 0 does not hold.
The function f defined as
f(x) := s*x+s where s=x+1has the same meaning as if it were defined as
f(x) := (x+1)*x+(x+1).
is equivalent to
x | y /\ exists z: y | z where y=2x
x | 2x /\ exists z: 2x | zLikewise, the formula
is equivalent to
x | y /\ exists y: y | x where y=2x
x | 2x /\ exists y: y | xHowever, it is not equivalent to
x | 2x /\ exists y: 2x | xbecause 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.
(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:
The Java expressionpublic 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; } }
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=2Also the Logic Evaluator implements local definitions
with any number of quantified variables.let(x_0 = T_0, ..., x_n-1 = T_n-1: A)