Go backward to 2.3 Terms Go up to 2 Language Go forward to 2.5 Values

2.4 Miscellaneous

Formulas = [ Formula { , Formula } ]

A (possibly empty) sequence of formulas separated by commas.

pred areOrdered(a, b, c, d) <=>
  and(<=(a, b), <=(b, c), <=(c, d));
> predicate areOrdered/4.

Terms = [ Term { , Term } ]

A (possibly empty) sequence of formulas separated by commas.

fun sumSquares(a, b) =
  +(*(a, a), *(b, b)).
> function sumSquares/2.

IteratorVariables = [ IteratorVariable { , IteratorVariable }]

A (possibly empty) sequence of iterator variables separated by commas.

option universe = nat(1,10);
> universe of discourse set.
formula forall(x, y in nat(1, x), z = y: <=(y, z));
> true.

ConstrainedVariables = [ ConstrainedVariable { , ConstrainedVariable } ]

A (possibly empty) sequence of constrained variables separated by commas.

fun minus(x: Nat, y in nat(1, x)) = -(x, y);
> function minus/2.

BoundVariables = [ BoundVariable { , BoundVariable } ]

A (possibly empty) sequence of bound variables separated by commas.

term let(x = 1, y = 2: +(x, y));
> 3.

IteratorVariable = Variable | TypedVariable | BoundVariable

An iterator variable is a variable that iterates over a sequence of values: a plain variable (iterating over the universe of discourse), a typed variable (iterating over some domain), or a bound variable (iterating over a single value).

option universe = nat(1, 3);
> universe of discourse set.
term set(x, y in nat(1, x), p = tuple(x, y): true, p);
> > <1, 1>, <2, 1>, <2, 2>, <3, 1>, <3, 2>, <3, 3>.

ConstrainedVariable = Variable | TypedVariable | CheckedVariable

A constrained variable is a variable whose domain may be restricted: a plain variable (not constrained), a typed variable (constrained by a domain), or a checked variable (constrained by a predicate).

pred isMultiple(x: Nat, y in nat(1, x)) <=>
  exists(z in nat(1, x): =(x, *(y, z)));
> predicate isMultiple/2.

Variable = Name

A name represents a variable if it occurs in the scope of a corresponding variable declaration of some quantifier or if it is declared as a parameter in a predicate/function definition.

fun a = 0;
> function a/0.
formula forall(x in nat(2,10): not(=(a, -(x, 1))));
> true.
fun f(x) = x;
> fun f/1.

TypedVariable = Name in Term

A typed variable is a name whose value range is constrained by a domain (an interval or a set). It is an error to attempt to bind to the variable a value that is not from the specified domain (such an attempt is detected if parameter checking is switched on).

fun -1(x in nat(1, 100)) = -(x, 1);
> function -1/1.

BoundVariable = Name = Term

A bound variable receives its value from the denoted term. The token `=' should be surrounded by whitespace because it can be also part of a a name.

term let(x = 7: *(2, x));
> 14.
term let(x=7: *(2, x));
> ERROR: unexpected ':'.

CheckedVariable = Name : Name

A checked variable is a name whose value range is constrained by a predicate. The second name must denote a unary predicate; it is an error to attempt to bind a value to the variable that is not satisfy the predicate (such an attempt is detected if parameter checking is switched on).

pred isEven(n: Nat) <=>
  exists(m in nat(0, n): =(n, *(2, m)));
> predicate isEven/2.
fun half(n: isEven) =
  such(m in nat(0, n): =(n, *(2, m)));
> function half/2.

Name

A name is any sequence of non-whitespace characters that does not start with a decimal digit and that does not include any of the characters `(', `)', `,', `:', `;'.

term +3(xVal, f_0(y, #));