define
The define
command creates a new definition in the current scope and a predicate which may be referred to by sentences in the current or children scopes.
Syntax
define [definition name]: [sentence definition];
define [definition name]([arg0], [arg1], ...): [sentence definition];
define [definition name];
define [definition name]([arg0], [arg1], ...);
dependent define [definition name];
dependent define [definition name]([arg0], [arg1], ...);
dependent define [definition name]([arg0], [arg1], ...): [sentence definition];
The command may optionally begin with the dependent
keyword before the define
keyword. The following identifier must be a valid predicate identifier. An optional list of object identifiers may follow the definition name. The ;
character may terminate the command, or :
marks the start of a ;
terminated sentence.
Behavior
The list of object identifiers is a list of unbound objects in the sentence definition, if present. The number of arguments the predicate depends on is the number of identifiers in the list of object identifiers. If no list of object identifiers is given, the predicate created depends on no arguments. If [sentence definition]
is present, then it is the sentence definition of the predicate created, otherwise the predicate has no sentence definition.
If the dependent
keyword is present or [sentence definition]
is not present, then the definition is added as a definition dependency. In these cases, the command must be called in a global scope or a dependent scope.
Examples
Suppose in
is a relation. Then consider the following commands:
object NATURALS;
define successor(A, B): *X(X in A -> X in B | X = B);
axiom successor_natural: *N*M(M in NATURALS & successor(N, M) -> N in NATURALS);
An object NATURALS
is created as well as a definition successor
. The sentence successor(A, B)
should be interpreted as “A
is the successor of B
.” Then the axiom successor_natural
says that the successor of a member of NATURALS
is a member of NATURALS
.
Now consider the following command:
dependent define related(A, B);
The command creates a definition related
which has two arguments but no sentence definition. When used in a program which is imported, it asserts that a definition with the identifier related
exists in the importing program, but does not enforce any requirements for such a definition. Such a command is useful when one wants to assert that a definition which behaves in a certain way (specified by axioms) exists but does not care how the definition is constructed.