The Knowledge Representation Library.
Introduction
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.
Knowledge Taxonomy
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.
Values
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.
Knowledge Base
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.
a value of class 'c = ('k,'s) cls
a slot holding a property 'p
of a class 'k
object.
an instance of the domain type class
an instance of the persistance type class
a set of possible conflicts
an opinion based fact of type 'a
objects cls
is a seqeuence of all objects of the class cls
.
val collect : ('a, 'p) slot -> 'a obj -> 'p t
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.
val require : ('a, 'p) slot -> 'a obj -> 'p t
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.
val provide : ('a, 'p) slot -> 'a obj -> 'p -> unit t
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.
val promise : ('a, 'p) slot -> ('a obj -> 'p t) -> unit
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_missing
.
val promising :
('a, 'p) slot ->
promise:('a obj -> 'p t) ->
(unit -> 's t) ->
's t
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_missing
.
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_missing
.
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_missing
.
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.
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
.
of_bigstring data
loads state from data
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
.
prints the state of the knowledge base.
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.
include Monads.Std.Monad.S with type 'a t := 'a t and module Syntax := Syntax
val void : 'a t -> unit t
void m
computes m
and discrards the result.
val sequence : unit t list -> unit t
sequence xs
computes a sequence of computations xs
in the left to right order.
val forever : 'a t -> 'b t
forever xs
creates a computationt that never returns.
Various function combinators lifted into the Kleisli category.
module Pair : sig ... end
The pair interface lifted into the monad.
The triple interface lifted into a monad.
module Lift : sig ... end
Lifts functions into the monad.
Interacting between monads and language exceptions
Lifts collection interface into the monad.
The Monad.Collection.S interface for lists
The Monad.Collection.S interface for sequences
include Monads.Std.Monad.Syntax.S with type 'a t := 'a t
val (>=>) : ('a -> 'b t) -> ('b -> 'c t) -> 'a -> 'c t
f >=> g
is fun x -> f x >>= g
val (!$) : ('a -> 'b) -> 'a t -> 'b t
val (!$$) : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val (!$$$) : ('a -> 'b -> 'c -> 'd) -> 'a t -> 'b t -> 'c t -> 'd t
val (!$$$$) :
('a -> 'b -> 'c -> 'd -> 'e) ->
'a t ->
'b t ->
'c t ->
'd t ->
'e t
!$$$$f
is Lift.quaternary f
val (!$$$$$) :
('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
'a t ->
'b t ->
'c t ->
'd t ->
'e t ->
'f t
!$$$$$f
is Lift.quinary f
include Monads.Std.Monad.Syntax.Let.S with type 'a t := 'a t
val let* : 'a t -> ('a -> 'b t) -> 'b t
let* r = f x in b
is f x >>= fun r -> b
val and* : 'a t -> 'b t -> ('a * 'b) t
val let+ : 'a t -> ('a -> 'b) -> 'b t
let+ r = f x in b
is f x >>| fun r -> b
val and+ : 'a t -> 'b t -> ('a * 'b) t
include Core_kernel.Monad.S with type 'a t := 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
t >>= f
returns a computation that sequences the computations represented by two monad elements. The resulting computation first does t
to yield a value v
, and then runs the computation returned by f v
.
val (>>|) : 'a t -> ('a -> 'b) -> 'b t
t >>| f
is t >>= (fun a -> return (f a))
.
val bind : 'a t -> f:('a -> 'b t) -> 'b t
return v
returns the (trivial) computation that returns v.
val map : 'a t -> f:('a -> 'b) -> 'b t
val join : 'a t t -> 'a t
join t
is t >>= (fun t' -> t')
.
val ignore_m : 'a t -> unit t
ignore_m t
is map t ~f:(fun _ -> ())
. ignore_m
used to be called ignore
, but we decided that was a bad name, because it shadowed the widely used Caml.ignore
. Some monads still do let ignore = ignore_m
for historical reasons.
val all : 'a t list -> 'a list t
val all_unit : unit t list -> unit t
Like all
, but ensures that every monadic value in the list produces a unit value, all of which are discarded rather than being collected into a list.
These are convenient to have in scope when programming with a monad:
Monadic operators, see Monad.Syntax.S for more.
include Monads.Std.Monad.Fail.S
with type 'a t := 'a t
and type 'a error = conflict
fail err
diverges the computation, possibly providing an extra information in a value of type _ error
.
val catch : 'a t -> (_ error -> 'a t) -> 'a t
catch m f
if m
diverges with some bottom value err
, the f err
is a result of the whole computation, otherwise returns m
.
module Order : sig ... end
Orders knowledge by its information content.
module Class : sig ... end
Class is a collection of sorts.
module Value : sig ... end
module Slot : sig ... end
A symbol is an object with a unique name.
module Agent : sig ... end
module Domain : sig ... end
Partially ordered sets with the least element.
module Name : sig ... end
module Enum : sig ... end
An extensible enumerated type.
the s-expression denoting the conflict.
module Rule : sig ... end
Online Knowledge documentation.