Theory
Logic theories, i.e. the knowledge bases of logic programs.
A theory is an ordered collection of clauses (see tuprolog.core.Clause):
- facts, stating what is true, e.g.
parent(abe, homer).; - rules, stating what is true provided that some conditions hold, e.g.
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).(the head holds if the body does); - directives, i.e. goals to execute when a theory is loaded, e.g.
:- dynamic(counter/1)..
A Prolog program is a theory, and solvers (see tuprolog.solve) answer queries against two of
them: a static knowledge base and a dynamic one, which assert/1 and retract/1 change.
Theories offer the usual Prolog operations on clauses: adding clauses at the beginning
(assert_a) or at the end (assert_z) of the theory, removing the first (retract) or every
(retract_all) clause unifying with a template, removing whole predicates (abolish), and
retrieving the clauses whose head may unify with a goal (theory[goal]). Clause order matters,
as Prolog tries clauses top-down.
Two independent choices distinguish theories, all sharing the Theory interface:
- immutable theories (
Theory, built bytheory) are persistent data structures: their operations return new theories, leaving the original one untouched; mutable ones (MutableTheory, built bymutable_theory) change in place, which is cheaper when clauses are asserted and retracted often; - indexed theories (the default) store clauses in a structure indexed by functor, arity and
first argument, making lookups fast at the cost of slower updates; listed ones (created by the
JVM factories, e.g.
Theory.listedOf) are plain lists of clauses.
Theories are mostly created by parsing Prolog text, see tuprolog.theory.parsing.
Examples:
>>> from tuprolog.core import indicator, struct, var
>>> from tuprolog.theory.parsing import parse_theory
>>> kb = parse_theory("parent(abe, homer). parent(homer, bart).")
>>> len(kb)
2
>>> list(kb[struct("parent", var("X"), "bart")])
[parent(homer, bart) :- true]
>>> indicator("parent", 2) in kb
True
>>> print(kb.assert_z(struct("parent", "bart", "maggie")).to_string(as_prolog_text=True))
parent(abe, homer) :- true.
parent(homer, bart) :- true.
parent(bart, maggie) :- true.
See Also
tuprolog.collections, for other collections of clauses; 2P-Kt's
clause database
explanation.
module-attribute
¶
Theory = _theory.Theory
An ordered collection of clauses, i.e. a logic program or knowledge base.
Plain theories are immutable: the operations "changing" them return new theories. Clauses must be
well-formed (e.g. their heads must be structures, not variables or numbers), or adding them raises
an IllegalArgumentException.
Python protocols (see tuprolog.theory._adapters):
- len(theory): the amount of clauses.
- item in theory: whether a clause is in the theory, any clause has the given head (a
tuprolog.core.Struct), or any clause has the given predicate indicator (e.g. parent/2).
- theory[key]: the clauses unifying with a clause, the rules whose head unifies with a
structure, or the rules of a predicate indicator, as a lazy iterable.
- theory + other: a theory with the clauses of other (a theory or a clause) appended.
- ==: the theories have equal clauses, in the same order; immutable theories are hashable.
Members
clauses,rules,directives: the (lazy) iterables of all clauses, of rules (facts included, as they are rules whose body istrue), and of directives.size,is_empty,is_non_empty,is_mutable: the amount of clauses, and flags.unificator,set_unificator(unificator): thetuprolog.unify.Unificatormatching clauses, and a copy of the theory using another one.assert_a(clause, ...),assert_z(clause, ...): the theory with clauses (or facts, from structures) added at its beginning or at its end.retract(clause, ...),retract_all(clause): theRetractResultof removing the first clause unifying with each template, or all of them.abolish(name, arity),abolish(indicator=...): the theory without the clauses of a predicate.to_mutable_theory(),to_immutable_theory(),clone(): conversions and copies.to_string(as_prolog_text=False): the theory as a string, or as Prolog source code.
Examples:
>>> from tuprolog.core import fact, struct, var
>>> from tuprolog.theory import theory
>>> kb = theory(fact(struct("f", "a")), fact(struct("f", "b")))
>>> kb.assert_a(struct("f", "c"))
IndexedTheory{ f(c) :- true. f(a) :- true. f(b) :- true }
>>> len(kb)
2
Note
Wraps 2P-Kt's it.unibo.tuprolog.theory.Theory interface, whose static factories (e.g.
Theory.empty(), Theory.indexedOf(unificator, clauses), Theory.listedOf(unificator,
clauses)) are available too.
module-attribute
¶
MutableTheory = _theory.MutableTheory
A Theory which changes in place.
assert_a, assert_z, retract, retract_all and abolish modify the theory itself (and
return it, or a RetractResult wrapping it), which is cheaper than building new theories when
clauses change often: every reference to the theory sees the changes. Mutable theories are not
hashable, as their equality depends on their changing clauses.
Examples:
>>> from tuprolog.core import struct
>>> from tuprolog.theory import mutable_theory
>>> kb = mutable_theory()
>>> _ = kb.assert_z(struct("f", "a"))
>>> len(kb)
1
Note
Wraps 2P-Kt's it.unibo.tuprolog.theory.MutableTheory interface.
module-attribute
¶
RetractResult = _theory.RetractResult
The outcome of retracting clauses from a Theory (see Theory.retract and
Theory.retract_all).
It is either a RetractResult.Success, if some clauses were removed, or a
RetractResult.Failure, if no clause matched.
Members
is_success,is_failure: which outcome it is.theory: the theory resulting from the operation (unchanged on failure).clauses: the removed clauses (None on failure).first_clause: the first removed clause (None on failure).
Examples:
>>> from tuprolog.core import struct, var
>>> from tuprolog.theory.parsing import parse_theory
>>> kb = parse_theory("f(a). f(b).")
>>> result = kb.retract(struct("f", var("X")))
>>> result.is_success, result.first_clause, len(result.theory)
(True, f(a) :- true, 1)
>>> kb.retract(struct("g", var("X"))).is_failure
True
Note
Wraps 2P-Kt's it.unibo.tuprolog.theory.RetractResult sealed class.
Creates an immutable, indexed theory containing the given clauses.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
*clauses
|
Clause | Iterable[Clause]
|
The clauses, in order, either as arguments or as one iterable. |
()
|
Returns:
| Type | Description |
|---|---|
Theory
|
The theory, whose clauses are matched by the default |
Raises:
| Type | Description |
|---|---|
IllegalArgumentException
|
If some clause is not well-formed (e.g. its head is a variable). |
Examples:
>>> from tuprolog.core import atom, fact, rule, struct, var
>>> X = var("X")
>>> theory(fact(struct("human", "socrates")), rule(struct("mortal", X), struct("human", X)))
IndexedTheory{ human(socrates) :- true. mortal(X_...) :- human(X_...) }
>>> len(theory([fact(atom("a")), fact(atom("b"))]))
2
>>> len(theory())
0
See Also
mutable_theory, and tuprolog.theory.parsing.parse_theory to parse theories.
Note
Wraps 2P-Kt's Theory.of.
mutable_theory(
*clauses: Clause | Iterable[Clause],
) -> MutableTheory
Creates a mutable, indexed theory containing the given clauses.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
*clauses
|
Clause | Iterable[Clause]
|
The clauses, in order, either as arguments or as one iterable. |
()
|
Returns:
| Type | Description |
|---|---|
MutableTheory
|
The mutable theory, whose clauses are matched by the default |
Raises:
| Type | Description |
|---|---|
IllegalArgumentException
|
If some clause is not well-formed. |
Examples:
>>> from tuprolog.core import fact, struct
>>> kb = mutable_theory(fact(struct("f", "a")))
>>> _ = kb.assert_z(fact(struct("f", "b")))
>>> kb
MutableIndexedTheory{ f(a) :- true. f(b) :- true }
See Also
theory, for immutable theories.
Note
Wraps 2P-Kt's MutableTheory.of.