Go up to 2 Language Go 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.
> file 'theory/set.txt' read.

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>;
>   read <name>;
>   option <name> = <value>;
>   help;
> see http://www.risc.uni-linz.ac.at/software/formal.