Go up to 2 LanguageGo forward to 2.2 Formulas

## 2.1 Commands

The evaluator executes a sequence of commands:

{ [ `Command` ] `;` }

The input consists of a sequence of commands separated by one or more semicolons. The semicolon serves as a "boundary marker": in the case of a syntax error, the parser skips all input until it encounters the next semicolon.

```pred p(x,y) <=> <=(*(2, y), x);
> predicate p/2.
fun f(x, y) = if(p(x, y), x, y);
> function f/2.
term f(2 3);
> ERROR: unexpected '3'.
term f(2, 3);
> 3.
```

A `Command` is one of the following statements executed by the evaluator.

`pred` `Name` [ `(` `ConstrainedVariables` `)` ] [ `recursive` `Term` ] `<=>` `Formula`

Defines a predicate with a certain name and arity (number of parameters). Different predicates may have the same name if they have different arities. The symbol ``<=>`` should be surrounded by whitespace, because it can be also part of a name.

```pred isSubset(A: Set, B: Set) <=> // A is subset of B
forall(x in A: in(x, B));
> predicate isSubset/2.
pred positive(x: Nat)<=>>(x, 0);
> ERROR: unexpected '<=>>'.
```

If the `recursive` clause is given, the definition may refer to the function being defined. In this case, however, a termination term must be given that denotes a natural number which is decreased in every recursive invocation of the predicate (which is checked by the interpreter, if execution checking is switched on).

```pred <(m: Nat, n: Nat) recursive m =
if (=(m, 0), not(=(n, 0)),
and(not(=(n, 0)), <(-(m, 1), -(n, 1))));
> function </2.
```

`fun` `Name` [ `(` `ConstrainedVariables` `)` ] [ `recursive` `Term` ] `=` `Term`

Defines a function with a certain name and arity (number of parameters). Different functions may have the same name if they have different arities. The symbol `=` should be surrounded by whitespace, because it can be also part of a name.

```fun **(A: Set, B: Set) = // the intersection of A and B
set(x in A: in(x, B), x);
> function **/2.
fun inc(x: Nat)=+(x, 1);
> ERROR: unexpected '=+'.
```

If the `recursive` clause is given, the definition may refer to the function being defined. In this case, however, a termination term must be given that denotes a natural number which is decreased in every recursive invocation of the function (which is checked by the interpreter, if execution checking is switched on).

```fun sum(S: Set) recursive #(S) =
if (=(S, {}), 0,
let(e = element(S):
+(e, sum(-(S, {}(e))))));
> function sum/1.
```

`formula` `Formula`

Evaluates a formula to true or false.

```formula isSubset(**(A, B), A);
> true.
```

`term` `Term`

Evaluates a term to a value.

```term **(A, **(B, C));
> {1, 2, 3}.
```

`plot` `Term`

Plots a set of points. The value of the given term must be a set of tuples of length 2 which are interpreted as points in the plane. The elements of each tuple must be natural numbers that are interpreted as the horizontal respectively vertical coordinate of the point. The coordinate system has point (0,0) in the lower left corner and extends `swidth` units to the right and `sheight` units to the top. The values `swidth` and `sheight` are defined as startup parameters.

```plot set(x in nat(1,50), y in nat(1, x): <=(x,*(y,y)),
tuple(x, y));
> done.
```

`plots` `Term`

Plots a set of point sets. The value of the given term must be a set of point sets as described for the command `plot`. The point sets are printed in various colors.

```plots set(r in nat(1,50): true,
set(x in nat(1, r), y in nat(1, x): <=(x,*(y,y)),
tuple(x, y)));
> done.
```

`read` `Name`

Reads the file `Name``.txt` and executes the commands contained in the file.

```read theory/set;
> predicate Subset/2.
> function **/2.
```

`option` `Option`

Sets `Option` which can be one of the following:

`silent` `=` ( `true` | `false` )

Switches on respectively off the messages that are printed after the definition of every predicate respectively function (initially on). This is the only command to which the evaluator does not respond with a message:

```fun f(x) = x;
> function f/1.
set silent = true;
fun inc(x: Nat) = +(x, 1);
fun dec(x: Nat) = -(x, 1);
```

`check` `=` ( `true` | `false` )

Switches on respectively off the checking of guard formulas, parameter types, and termination terms in the evaluation of formulas and terms (initially on).

```fun f(x: Nat) = x;
> function f/1.
term f({});
> ERROR: value {} does not satisfy predicate Nat/1
for parameter x.
option check = false;
> execution checks are off.
term f({});
> {}.
```

`universe` `=` `Term`

Sets the universe of discourse to the domain denoted by the given term (initially undefined). The evaluation of this term must denote a domain (an interval or a set). All quantified variables without domain constraints are assumed to range over this domain.

```option universe = nat(1,100);
> universe of discourse set.
formula forall(x: <=(x, 1000));
> true.
```

`help`

Prints a short help message with a reference to the home page of the evaluator.

```help;
> commands (terminated by ';'):
>   pred <name>(<parameters>) <=> <formula>;
>   fun <name>(<parameters>) = <term>;
>   formula <formula>;
>   term <term>;
>   plot <term>;
>   plots <term>;