Go backward to 2.2 FormulasGo up to 2 LanguageGo forward to 2.4 Miscellaneous

## 2.3 Terms

A `Term` is one of the following phrases denoting a valuevalues:

`Variable`

A variable: the value of a variable is determined by the context in which the variable is evaluated.

```formula forall(x in Nat(1, 10): <=(x, 10));
> true.
fun f(x: Nat) = +(x, 1)
> function f/1.
```

`Name` [ `(` `Terms` `)` ]

A function application: the value of the application is the result of the function denoted by the given name and arity when applied to the values of the given argument terms.

```fun sumprod(x, y) = +(*(x, y), y);
> function sumprod/2.
term sumprod(2, 3);
> 9.
```

`if` `(` `Formula` `,` `Term` [ `,` `Term` ] `)`

A conditional term: if the formula (the guard) evaluates to true, the result is the value of the first term, otherwise it is the result of the second term. If the guard evaluates to false and the second term is not given, the result is undefined (evaluation aborts, if guard checking is switched on).

```term if(>(2, 3), {}, join(1, {}));
> {1}.
```

`let` `(` `BoundVariables` `:` `Term` `)`

A term with some locally bound variables: the value of this term is the value of the base term for the denoted variable bindings. The token ``=`' must be surrounded by whitespace because it can also appear as part of a name.

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

`such` `(` `IteratorVariables` `:` `Formula` `,` `Term` `)`

An implicit definition: the value of this term is the value of the base term for some binding of the quantified variables that satisfies the given formula.

```term such(x in nat(1, 10): =(12, *(2, x)), x);
> 6.
term such(x in nat(1, 10): =(24, *(2, x)), x);
> ERROR: no such value.
```

`0`-`9`{`0`-`9`}

A natural number is represented by a non-empty sequence of decimal digits.

```term 17;
> 17.
```

`set` `(` `IteratorVariables` `:` `Formula` `,` `Term` `)`

The set of values of the base term for all bindings of the quantified variables that satisfy the given formula.

```term set(x in nat(1, 6), y in nat(1, 6): =(6, +(x, y)),
tuple(x,y));
> {<1, 5>, <2, 4>, <3, 3>, <4, 2>, <5, 1>}.
```

`reduce` `(` `Name` `,` `Term` `,` `Term` `)`

The reduction of a set by a binary function. The name must denote a binary function f which is applied to each element of the set s denoted by the first term and the base value b of the last term such that

`reduce(f, {}, b)` = b
`reduce(f, v union s, b)` = f(v, reduce(f, s, b))

where v is an element not contained in s. An application `reduce`(f, s, b) only yields a unique result if f(p0, f(p1, ..., f(pn-1, b))) denotes the same value for every permutation p of the elements of s.

```term reduce(+, nat(1, 6), 0);
> 21.
term reduce(join, nat(1, 6), {});
> {1, 2, 3, 4, 5, 6}.
```

`tuple` `(` `Terms` `)`

A tuple, i.e., a sequence of values.

```term tuple(2, 3, 4);
> <2, 3, 4>.
```

`.``Number` `(` `Term` `)`

The element at the denoted position in the denoted tuple; `Number` is a natural number in the interval 0 to the length of the tuple minus one.

```term let(t = tuple(2, 3): +(.0(t), .1(t)));
> 5.
```

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