Predicates in this group are used to add and remove clauses from the predicate database dynamically. There are two types of databases in the Plang system: global and local.
The global database is shared between all parts of the Plang system and contains the following:
As an example, we consider a theorem prover for propositional logic. The prover needs simplification rules to convert complex logical expressions into simpler ones. Rather than fix the set of rules at compile time, the theorem prover allows the user to add new rules at runtime. To support this, we declare the simplify/2 predicate as dynamic and add the predefined rules as follows:
:- dynamic(simplify/2). add_rules() { assertz(simplify(in A && A, A)); assertz(simplify(in B || true, true)); ... }
To use the rules to simplify a logical expression, the application calls the simplify/2 predicate in the usual fashion:
simplify(Expr, Simplified);
When the user supplies a new rule, the application can call asserta/1 or assertz/1 to add the new rule to the start or end of the existing dynamic clause list. Rules that are no longer needed can be removed with retract/1.
In practice, theorem provers rarely implement a single theory of logic. We want our prover to be extensible from propositional logic to first order logic, higher order logic, and so on. Each logical theory will need its own simplification rules. We could define separate global predicates for each theory: prop_simplify/2, fo_simplify/2, etc. An alternative is to use local databases.
The application creates local databases with new_database/1 to store additional predicates that are generated at runtime. Each local database defines a separate scope - the same predicate name can have different purposes in different local databases.
Returning to our example, we will create a generic class to hold information about a logical theory. The constructor creates a new local database to hold the rules that make up the theory:
class theory { var rules; new() { new_database(Self.rules); } }
We can then create our theory object for propositional logic as follows:
new theory(Prop); assertz(simplify(in A && A, A), Prop.rules); assertz(simplify(in B || true, true), Prop.rules); ...
To use the simplification rules, we need to call the local predicate with call/2:
call(simplify(Expr, Simplified), Prop.rules);
The local predicate is executed in a context where the current database is set to Prop.rules
. If the local predicate calls other predicates, they will first be looked up in the local database, and then the global database.
abolish/1, abolish/2, abolish_database/1, asserta/1, asserta/2, assertz/1, assertz/2, clause/2, clause/3, new_database/1, retract/1, retract/2
instantiation_error
- one of Pred, Name, or Arity, is a variable. type_error(predicate_indicator, Pred)
- Pred does not have the form Name / Arity. type_error(integer, Arity)
- Arity is not an integer. type_error(atom, Name)
- Name is not an atom. domain_error(not_less_than_zero, Arity)
- Arity is less than zero. permission_error(modify, static_procedure, Pred)
- Pred is a builtin or compiled predicate.abolish(userdef/3) succeeds abolish(Pred) instantiation_error abolish(Name/3) instantiation_error abolish(userdef/Arity) instantiation_error abolish(1.5) type_error(predicate_indicator, 1.5) abolish(userdef/a) type_error(integer, a) abolish(1/a) type_error(integer, a) abolish(1/3) type_error(atom, 1) abolish(userdef/-3) domain_error(not_less_than_zero, -3) abolish(abolish/1) permission_error(modify, static_procedure, abolish/1)
instantiation_error
- Database is a variable. type_error(database, Database)
- Database is not a local database. instantiation_error
- one of Pred, Name, or Arity, is a variable. type_error(predicate_indicator, Pred)
- Pred does not have the form Name / Arity. type_error(integer, Arity)
- Arity is not an integer. type_error(atom, Name)
- Name is not an atom. domain_error(not_less_than_zero, Arity)
- Arity is less than zero.new_database(DB); assertz(userdef(a, b, c), DB); abolish(userdef/3, DB);
instantiation_error
- Database is a variable. type_error(database, Database)
- Database is not a local database.new_database(DB); assertz(userdef(a, b, c), DB); assertz(simplify(in A && A, A), DB); abolish_database(DB);
instantiation_error
- Clause or Head is a variable. type_error(callable, Head)
- Head is not a callable term (atom or functor). type_error(callable, Body)
- Body is not a callable term. In a departure from Standard Prolog, this error is thrown when the Body is executed, not when the Clause is asserted into the database. permission_error(modify, static_procedure, Pred)
- the predicate indicator Pred of Head refers to a builtin or compiled predicate.asserta(Clause) instantiation_error assertz((Head :- true)) instantiation_error asserta((1.5 :- true)) type_error(callable, 1.5) assertz((a :- true)) succeeds asserta((a(X) :- b(X,Y))) succeeds assertz(a(X)) succeeds asserta((det --> "the")) succeeds assertz((a :- X)) type_error(callable, X) when executed asserta(asserta(X)) permission_error(modify, static_procedure, asserta/1)
instantiation_error
- Database is a variable. type_error(database, Database)
- Database is not a local database. instantiation_error
- Clause or Head is a variable. type_error(callable, Head)
- Head is not a callable term (atom or functor). type_error(callable, Body)
- Body is not a callable term. In a departure from Standard Prolog, this error is thrown when the Body is executed, not when the Clause is asserted into the database. permission_error(modify, static_procedure, Pred)
- Pred is a builtin predicate in the global database that cannot be overridden by local databases.new_database(DB); assertz(userdef(a, b, c), DB);
:-
Body unifies with a clause in the predicate database. If there are multiple clauses that unify, then backtrack through the alternatives. Fails immediately if no clauses unify.instantiation_error
- Head is a variable. type_error(callable, Head)
- Head is not a callable term (atom or functor). permission_error(access, private_procedure, Pred)
- the predicate indicator Pred of Head refers to a predicate that is builtin or compiled.:-
Body unifies with a clause in the specified local predicate Database. If there are multiple clauses that unify, then backtrack through the alternatives. Fails immediately if no clauses unify.instantiation_error
- Database is a variable. type_error(database, Database)
- Database is not a local database. instantiation_error
- Head is a variable. type_error(callable, Head)
- Head is not a callable term (atom or functor).type_error(variable, Database)
- Database is not a variable.new_database(DB);
instantiation_error
- Clause or Head is a variable. type_error(callable, Head)
- Head is not a callable term (atom or functor). permission_error(modify, static_procedure, Pred)
- the predicate indicator Pred of Head refers to a builtin or compiled predicate.retract(Clause) instantiation_error retract((Head :- true)) instantiation_error retract((1.5 :- true)) type_error(callable, 1.5) retract((a(X) :- b(X, Y)) fails assertz((a(X) :- b(X, Y))); retract((a(X) :- b(X, Y))) succeeds retract(retract(X)) permission_error(modify, static_procedure, retract/1)
while [X, Y] (retract((a(X) :- b(X, Y)))) {}
instantiation_error
- Database is a variable. type_error(database, Database)
- Database is not a local database. instantiation_error
- Clause or Head is a variable. type_error(callable, Head)
- Head is not a callable term (atom or functor).new_database(DB); assertz(userdef(a, b, c), DB); retract(userdef(A, B, C), DB);