Next: Relation Definitions, Previous: Type Declarations, Up: Programs [Contents][Index]

These comprise *predications*, *negated predications* and *meta-calls*.

These are atoms that are names of no argument defined relations or compound terms with functors that are the names of primitive or program defined relations with argument types consistent with the relation’s declared type. A compound term with a functor that is an expression of relation type consistent with the argument types of the compound term is also a predication, this includes the case where the functor is a variable. The compiler will also check that all varibles of any argument term of the predication that must be ground will have have been given ground values by the time the predication needs to be evaluated.

These have the form `not Cond`

where
`Cond`

is a predication. The compiler will check that any arguments of the predication `Cond`

that need to be ground will have ground bindings for all their variables before the `not`

is evaluated. All other arguments must also be ground values by the time the condition is evaluated, or
they must be anonymous underscore variables.

`not Cond`

is deemed to have been inferred if, and only if, a complete search of the tree of alternatve possible inferences of `Cond`

fails to find a proof. It is the so-called *negation-as-failure*. It is a sound rule of inference on certain assumptions regarding the completeness of the relation definitions used in the exploration of the possible proofs of `Cond`

and on the assumption that different data terms (after being normalised in the case os sets) denote different values.

These have the form `call Var`

where
`Var`

is of type `relcall`

.
`relcall`

is the system type comprising all terms that denote type correct calls to primitive or program defined relations. The meta call `call Var`

succeeds providing the relation call denoted by the `relcall`

value of `Var`

at the time of evaluation has all its input arguments ground and will succeed.

Negation. If `Predication`

is inferable then fail else succeed. At the time of call all
variables appearing in `Goal`

must be ground or underscore variables.

`relcall`

is the system type comprising all terms that are type correct calls to primitive or program defined relations. The functor of the predication must either be given or be a variable with known
moded type so that the compiler can check that the call is type correct and that any arguments that need to be ground will have ground bindings before the `not`

is evaluated. The only variables that need not already have ground bindings are underscore variables. None of these can be in `!`

argument positions of the called relation.

Find first solution to `SimpleConj`

and discard any alternative choices.
If `SimpleConj`

is just a predication the brackets are not needed.

`once`

cannot be used inside a `SimpleConj`

. It may only be used in an interpreter query or in the conjunctive body of a relation rule.

call `Call`

`relcall`

is the system type comprising all terms that are type correct calls to primitive or program defined relations. The functor of the predication must either be given or be a variable with known
moded type so that the compiler can check that the call is type correct and that any arguments that need to be ground will have ground bindings before the `call`

is evaluated.

`forall UVars (exists EVars1 SimpleConj1 => exists EVars2 SimpleConj2)`

If, for all bindings of variables in `UVars`

that make `exists EVars1 SimpleConj1`

inferable, ` exists EVars2 SimpleConj2`

is also inferable, then the `forall`

succeeds, otherwise it fails.

`UVars`

must be a collection of new variables and all free variables occurring in `SimpleConj1`

must be in `UVars`

, have a
ground value before the `forall`

is evaluated, or be an underscore variable.

`EVars1`

and `EVars2`

must also be collections of new variables,
all variables occurring in `SimpleConj1`

must be in `UVars`

or `EVars1`

and all variables occurring in `SimpleConj2`

must be in `UVars`

or `EVars2`

, have a
ground value before the `forall`

is evaluated, or be an underscore variable. `exists EVars1`

and `exists EVars2`

are optional.

`forall`

cannot be used inside a `SimpleConj`

. It may only be used in an interpreter query or in the conjunctive body of a relation rule.

Assuming we have a collection of `child_of(C, P)`

beliefs that associate a child `C`

with a parent `P`

, and a collection
of `person(Name, Gender, Age)`

beliefs, giving the gender and age of people. The following query will
return as an answer each parent who has at least one adult child.

child_of(_, P) & forall C (child_of(C,P) => exists A person(C,_,A) & A>20)

Note that `P`

will be given a value before the call on `forall`

and so there are no free variables in the body of `forall`

other
than `C`

and the underscore variable.

Also note that each quantified variable is not allowed to appear outside the quantification or in other quantifications.

Next: Relation Definitions, Previous: Type Declarations, Up: Programs [Contents][Index]