bap-knowledge 2.5.0 · OCaml Package

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.

type 'a t = 'a knowledge

a knowledge monad

type (+'k, +'s) cls

a sort 's of class 'k.

type +'k obj

an object of class 'k

type +'c value

a value of class 'c = ('k,'s) cls

type (+'k, 'p) slot

a slot holding a property 'p of a class 'k object.

type 'p domain

an instance of the domain type class

type 'a persistent

an instance of the persistance type class

type state

the knowledge base state

type conflict = ..

a set of possible conflicts

type agent

an information provider

type 'a opinions

an opinion based fact of type 'a

type name

a fully qualified name

val objects : ('a, _) cls -> 'a obj Core_kernel.Sequence.t t

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

since 2.2.0

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.

since 2.4.0

val resolve : ('a, 'p opinions) slot -> 'a obj -> 'p t

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.

val suggest : agent -> ('a, 'p opinions) slot -> 'a obj -> 'p -> unit t

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.

since 2.4.0 if [require] is called in the scope of the promise

and fails, the the whole promise immediately returns the empty value of the property domain, i.e., f is wrapped into with_empty.

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 ().

since 2.2.0

since 2.4.0 if [require] is called in the scope of the promise

and fails, the the whole promise immediately returns the empty value of the property domain, i.e., promise (not f) wrapped into with_empty.

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

propose p f proposes the opinion computation.

The same as promise except that it promises a value for an opinion-based property.

since 2.4.0 if [require] is called in the scope of the promise

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.

since 2.2.0

since 2.4.0 if [require] are called in the scope of the proposal

and fails, the the whole proposal immediately returns the empty value of the property domain, i.e., propose (not f) wrapped into with_empty.

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

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.

since 2.4.0

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.

since 2.4.0

val with_empty : missing:'r -> (unit -> 'r knowledge) -> 'r knowledge

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.

since 2.4.0

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.

since 2.5.0

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.

since 2.5.0

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).

since 2.5.0

val on : bool -> unit t -> unit t

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.

since 2.5.0

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

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.

since 2.5.0

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.

since 2.2.0

val save : state -> string -> unit

save state path saves the knowledge base to the file at path.

since 2.2.0

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

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.

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 -> 'b t) -> ('b -> 'c t) -> 'a -> 'c t

f >=> g is fun x -> f x >>= g

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

!!x is return x

val (!$) : ('a -> 'b) -> 'a t -> 'b t

!$f is Lift.unary f

val (!$$) : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t

!$$f is Lift.binary f

val (!$$$) : ('a -> 'b -> 'c -> 'd) -> 'a t -> 'b t -> 'c t -> 'd t

!$$$f is Lift.ternary f

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

monoidal product

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

monoidal product

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)).

module Monad_infix : sig ... end

val bind : 'a t -> f:('a -> 'b t) -> 'b t

bind t ~f = t >>= f

val return : 'a -> 'a t

return v returns the (trivial) computation that returns v.

val map : 'a t -> f:('a -> 'b) -> 'b t

map t ~f is t >>| f.

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.

module Let_syntax : sig ... end

These are convenient to have in scope when programming with a monad:

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

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

type 'a error = conflict

a type of error

val fail : _ error -> 'a t

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 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.

package bap-knowledge

Introduction

Knowledge Taxonomy

Values

Knowledge Base