Go backward to 2.3 TermsGo up to 2 LanguageGo 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, #));
```

Maintained by: Wolfgang Schreiner
Last Modification: September 16, 2004