`Bap_knowledge.Knowledge`

The Knowledge Representation Library.

The library provides facilities for storing, accumulating, and computing knowledge. The knowledge could be represented indirectly, in the Knowledge Base, or directly as knowledge values. The library focuses on representing knowledge that is partial and provides mechanisms for knowledge accumulation and refinement. The knowledge representation library leverages the powerful type system of the OCaml language to facilitate development of complex knowledge representation and reasoning systems.

For a given knowledge system, the domain of discourse is a set of objects, optionally partitioned into sorts. Therefore, an *object* is fundamental building block of a knowledge system.

An object *class* defines a set of possible properties of that objects. A snapshot of all properties of an object is called *value*. A set of values belonging to a particular class could be partitioned into sorts, to facilitate the design of strongly typed interfaces.

Properties of objects and values are stored in *slots*. The data type of any property is required to be an instance of the *domain* structure, i.e., it should be a set with a special `empty`

value and the `order`

operation, that orders elements of this set by their informational content, so that `empty`

is the least element.

The knowledge could be represented directly as a value, or indirectly as a set of objects in a knowledge base.

A value is an ordered tuple of slots that holds all properties of an object with which this value is associated. Additionally, a value is attributed with a sort value, which is shared by all values belonging to that sort. The sort value could be a concrete value, holding some information that is common for all elements of the sort or it could be just a type index that witnesses that the value belongs to a certain set of values.

Properties of a value could be accessed using the `Value.get`

operator. A new value of a property could be put into the slot using the `Value.put`

operator.

Values are instances of the domain type class and therefore a property of an object or another value could also be a value.

The set of slots of a given value is defined by its class, and this set is extensible, i.e., it is possible to add more slots.

The knowledge base maintains a consistent set of facts about object properties. An object is a unit of identity. The value of an object is defined by its properties. However, the knowledge base doesn't provide the direct access to the object value.

Object properties could be accessed using the `collect`

operator and set using the `provide`

operator. The knowledge base maintains the consistency by disallowing changing an object property to a value that has less informational contents than the previous value, so that no information is never lost.

Object properties could also be computed on demand using the `promise`

operator, which effectively stores a procedure in the knowledge base. Several procedures could be provided for a property computation, and the procedures themselves could access other properties, including the property being computed. The knowledge base will ensure that the least fixed point of all procedures involved in the property computation is reached.

All Knowledge Base operators return a computation of type `'a knowledge`

which is a monad, that denotes a computation that is knowledge dependent, i.e., it either accesses the knowledge base, or modifies it, or both.

The knowledge computation may lead to an inconsistent state, in other words, it is not guaranteed that the computation will reach the normal form. A diverging computation will yield a value of type `conflict`

when run.

To prevent unnecessary conflicts, it is possible to represent object properties as opinions instead of facts. Opinions are facts that are attributed with the name of an agent that provided this fact. In case if mutiple agents provide conflicting opinions, the `resolve`

operator will compute the consensus, based on agents predefined trustworthiness. Opinions are introduced using the `suggest`

operator or promised using the `propose`

operator.

Finally, the knowledge base is partially persistent. It is possible to make some slots persistent, so that properties, stored in them are preserved between program runs.

`type 'a t = 'a knowledge`

a knowledge monad

`objects cls`

is a seqeuence of all objects of the class `cls`

.

`collect p x`

collects the value of the property `p`

.

If the object `x`

doesn't have a value for the property `p`

and there are promises registered in the knowledge system, to compute the property `p`

then they will be invoked, otherwise the empty value of the property domain is returned as the result.

`require p x`

collects the property `p`

and fails if it is empty.

When `require p x`

fails in the scope of a `promise`

, `proposal`

, or in the scope of `with_empty`

, then the scoped computation immediately returns the empty value.

`resolve p x`

resolves the multi-opinion property `p`

Finds a common resolution for the property `p`

using the current resolution strategy.

This function is the same as `collect`

except it collects a value from the opinions domain and computes the current consensus.

`provide p x v`

provides the value `v`

for the property `p`

.

If the object `x`

already had a value `v'`

then the provided value `v`

then the result value of `p`

is `join v v'`

provided such exists, where `join`

is `Domain.join (Slot.domain p)`

.

If `join v v'`

doesn't exist (i.e., it is `Error conflict`

) then `provide p x v`

diverges into a conflict.

`suggest a p x v`

suggests `v`

as the value for the property `p`

.

The same as `provide`

except the provided value is predicated by the agent identity.

`promise p f`

promises to compute the property `p`

.

If the property `p`

of `x`

is not provided, then `f x`

is invoked to provide the initial value, when `p`

is collected.

If there are more than one promises, then they all must provide a consistent answer. The function `f`

may refer to the property `p`

directly or indirectly. In that case the least fixed point solution of all functions `g`

involved in the property computation is computed.

and fails, the the whole promise immediately returns the empty value of the property domain, i.e., `f`

is wrapped into `with_empty`

.

`promising p ~promise f`

evaluates `f ()`

under `promise`

and retracts it after `f`

is evaluated.

The information provided by `promise`

is only available during evaluation of `f ()`

.

and fails, the the whole promise immediately returns the empty value of the property domain, i.e., `promise`

(not `f`

) wrapped into `with_empty`

.

`propose p f`

proposes the opinion computation.

The same as `promise`

except that it promises a value for an opinion-based property.

and fails, the the whole promise immediately returns the empty value of the property domain, i.e., `f`

is wrapped into `with_empty`

.

```
val proposing :
agent ->
('a, 'p opinions) slot ->
propose:('a obj -> 'p t) ->
(unit -> 's t) ->
's t
```

`proposing a p ~propose f`

a scope-limited proposal.

The proposal is active only during the evaluation of `f ()`

. The function is the same as `proposing`

except that it promises a value for an opinion-based property.

and fails, the the whole proposal immediately returns the empty value of the property domain, i.e., `propose`

(not `f`

) wrapped into `with_empty`

.

`observe property push`

calls `push`

when the `property`

changes.

Dual to `promise`

, `observe`

enables forward-chaining rules and propagates knowledge whenever `property`

value is refined.

Calls `push x v`

when the `property`

value of an object `x`

is refined to `v`

. It is guaranteed that `v`

is never empty.

```
val observing :
('a, 'p) slot ->
observe:('a obj -> 'p -> unit knowledge) ->
(unit -> 'r knowledge) ->
'r knowledge
```

`observing property ~observe:push scope`

observes the property in a `scope`

.

This operation is dual to `promising`

and it observes the property only during the time when the `scope`

computation is evaluate and removes the observer after that.

`with_empty ~missing f x`

evaluates `f ()`

and if it fails on an empty immediately evaluates to `return missing`

.

Inside of `with_empty`

it is possible to use the choice monad operations, like `reject`

, `guard`

, `on`

, and `unless`

, in addition to the knowledge specialized choice operators, such as `require`

and various `*?`

operators.

Note, that promised computations are invoked in the `with_empty`

scope.

`val reject : unit -> 'a t`

`reject ()`

rejects a promised computation.

When in the scope of the `with_empty`

function, e.g., in a promise or proposal, aborts the computation of the promise and immediately returns an empty value.

`val guard : bool -> unit t`

`guard cnd`

rejects the rest of compuation if `cnd`

is `false`

.

When in the scope of the `with_empty`

function, e.g., in a promise or proposal, aborts the computation of the promise and immediately returns an empty value.

`val proceed : unless:bool -> unit t`

`proceed ~unless:cnd`

rejects the computation unless `cnd`

holds.

Dual to `guard`

, this operator rejects a promise (or any other computation in the scope of the `with_empty`

operator) unless the `cnd`

holds, i.e., it is the same as `guard (not cnd)`

.

`on cnd x`

evaluates to `x`

if `cnd`

, otherwise rejects.

When in the scope of the `with_empty`

function, e.g., in a promise or proposal, aborts the computation of the promise and immediately returns an empty value if `cnd`

is `false`

. If it is not, then evaluates to `x`

.

`unless cnd x`

evaluates to `x`

if `not cnd`

, otherwise rejects.

When in the scope of the `with_empty`

function, e.g., in a promise or proposal, aborts the computation of the promise and immediately returns an empty value if `cnd`

is `true`

. If it is `false`

, then evaluates to `x`

.

`val empty : state`

state with no knowledge

`val of_bigstring : Core_kernel.Bigstring.t -> state`

`of_bigstring data`

loads state from `data`

`val to_bigstring : state -> Core_kernel.Bigstring.t`

`to_bigstring state`

serializes state into a binary representation.

`val load : string -> state`

`load path`

loads the knowledge base from the file at `path`

.

`val save : state -> string -> unit`

`save state path`

saves the knowledge base to the file at `path`

.

`module Context : sig ... end`

Context variables.

`val pp_state : Stdlib.Format.formatter -> state -> unit`

prints the state of the knowledge base.

```
val run :
('k, 's) cls ->
'k obj t ->
state ->
(('k, 's) cls value * state, conflict) Core_kernel.result
```

`run cls comp init`

computes the value of the object `obj`

given

Evaluates the knowledge dependent computation `comp`

using the initial set of facts `init`

.

The computation must evaluate to an object `p`

of the class `cls`

. The `run`

function computes all properties of `p`

, which will trigger all promises associated with the slots.

The result of evaluation is either a conflict, or a pair of value, which contains all properties of the object, and the knowledge accumulated during the computation.

`module Syntax : sig ... end`

`include Monads.Std.Monad.S with type 'a t := 'a t and module Syntax := Syntax`

`sequence xs`

computes a sequence of computations `xs`

in the left to right order.

`module Fn : sig ... end`

Various function combinators lifted into the Kleisli category.

`module Pair : sig ... end`

The pair interface lifted into the monad.

`module Triple : sig ... end`

The triple interface lifted into a monad.

`module Lift : sig ... end`

Lifts functions into the monad.

`module Exn : sig ... end`

Interacting between monads and language exceptions

`module Collection : sig ... end`

Lifts collection interface into the monad.

`module List : Collection.S with type 'a t := 'a list`

The Monad.Collection.S interface for lists

`module Seq : Collection.S with type 'a t := 'a Core_kernel.Sequence.t`

The Monad.Collection.S interface for sequences

`include Monads.Std.Monad.Syntax.S with type 'a t := 'a t`

`val (!!) : 'a -> 'a t`

`!!x`

is `return x`

`!$$$$f`

is `Lift.quaternary f`

`include Monads.Std.Monad.Syntax.Let.S with type 'a t := 'a t`

`include Core_kernel.Monad.S with type 'a t := 'a t`

`module Monad_infix : sig ... end`

`val return : 'a -> 'a t`

`module Let_syntax : sig ... end`

`module Let : Monads.Std.Monad.Syntax.Let.S with type 'a t := 'a t`

Monadic operators, see Monad.Syntax.S for more.

`module Order : sig ... end`

Orders knowledge by its information content.

`module Class : sig ... end`

Class is a collection of sorts.

`module Object : sig ... end`

Knowledge Base Objects.

`module Value : sig ... end`

Knowledge Values.

`module Slot : sig ... end`

Property accessor.

`module Symbol : sig ... end`

A symbol is an object with a unique name.

`module Agent : sig ... end`

An information provider.

`module Domain : sig ... end`

Partially ordered sets with the least element.

`module Persistent : sig ... end`

Persistence type class.

`module Conflict : sig ... end`

Conflicting information.

`module Name : sig ... end`

Fully qualified names.

`module Enum : sig ... end`

An extensible enumerated type.

`val sexp_of_conflict : conflict -> Core_kernel.Sexp.t`

the s-expression denoting the conflict.

`module Rule : sig ... end`

`module Documentation : sig ... end`

Online Knowledge documentation.