bap-knowledge 2.5.0 · OCaml Package

Partially ordered sets with the least element.

The Domain is fundamental structure for the Knowledge representation as domains are used to represent property values. Basically, all information is represented with domains. Domains capture the idea of partial information or an approximation of information.

A domain is a set equipped with the partial order, which orders elements of this set by their information content, and the least element empty or bot, which is not greater than any other element of this set. The empty element indicates an absence of knowledge.

The resulting structure is not strictly a domain, the only missing element is the maximal element. The role of the is taken by values of type conflict, which denote the top element equipped with the diagnostic information. Therefore, type ('a,conflict) result is a directed-complete partial order, or a Scott-Ershov domain, or just a domain..

The domain structure is very general and the join operator is induced by the specified order. However, it is possible to upgrade the structure, used to represent a property, to lattice or lattice-like structure, by providing a custom join function.

type 'a t = 'a domain

val define : 
  ?inspect:('a -> Base.Sexp.t) ->
  ?join:('a -> 'a -> ('a, conflict) Core_kernel.result) ->
  empty:'a ->
  order:('a -> 'a -> Order.partial) ->
  string ->
  'a domain

define ~inspect ~empty ~order name defines a domain for the type 'a.

The empty value denotes the representation of an absence of information, or an undefined value, or the default value, or the least possible value in the chain, etc. It's only required that for all possible values x, empty <= x, where <= is the partial order defined by the order parameter

The order function defines the partial order for the given domain, such that

partial x y = LT iff x<=y && not(y <= x)
partial x y = EQ iff x <= y && y <= x
partial x y = GT iff not (x <= y) && (y <= x)
partial x y = NC iff not (x <= y) && not (y <= x).

The optional inspect function enables introspection, and may return any representation of the domain value.

The returned value is an instance of the domain type class that is used for declaration of a property. The instance is not nominal and is purely structural, the name argument is used only for introspection and better error messages.

val total : 
  ?inspect:('a -> Base.Sexp.t) ->
  ?join:('a -> 'a -> ('a, conflict) Core_kernel.result) ->
  empty:'a ->
  order:('a -> 'a -> int) ->
  string ->
  'a domain

total empty order name defines a domain from the total order.

Defines an ordinal domain, where the partial order is inferred from the total order, so that a <= b iff a < b.

The Hasse diagram of the ordinal domain:

val flat : 
  ?inspect:('a -> Base.Sexp.t) ->
  ?join:('a -> 'a -> ('a, conflict) Core_kernel.result) ->
  empty:'a ->
  equal:('a -> 'a -> bool) ->
  string ->
  'a domain

flat empty equal name defines a flat domain.

A flat domain has one element that is less than all other elements except itself and any other two elements that are not empty are non-comparable.

The Hasse diagram of the flat domain:

             x1 x2  ... xN
             o  o       o
             |  |       |
             +--+-+...--+
                  |
                  o
                 bot

val optional : 
  ?inspect:('a -> Base.Sexp.t) ->
  ?join:('a -> 'a -> ('a, conflict) Core_kernel.result) ->
  equal:('a -> 'a -> bool) ->
  string ->
  'a option domain

optional ~equal name a flat domain with None as bot.

Wrapping any data type into the option data type yields a flat domain. For example,

let tribool = optional ~equal:bool_equal "tribool"

is a tribool domain, where the property value could be either unknown (None), true (Some true), or false (Some false.

val mapping : 
  ('a, 'e) Core_kernel.Map.comparator ->
  ?inspect:('d -> Base.Sexp.t) ->
  ?join:('d -> 'd -> ('d, conflict) Core_kernel.result) ->
  equal:('d -> 'd -> bool) ->
  string ->
  ('a, 'd, 'e) Core_kernel.Map.t domain

mapping total_order ~equal ?join name a point-wise mapping domain.

Finite mapping naturally form domains, if every key in the mapping is considered an independent kind of information, and an absence of a key indicates the absence of that kind of information.

The upper bound of two mapping is the point-wise union of them, unless there is a key, which is present in both mapping with different values (combined with equal by default). In the latter case, the upper bound is the conflict.

The partial order between x and y is defined as follows:

EQ iff mappings are structurally equal;
LT iff y contains all bindings of x and x <> y;
GT iff x contains all bindings of y and x <> y;
NC iff neither of the above rules applicable.

since 2.5.0, the optional [join] parameter is made available.

By default, it returns Ok y when two elements x and y which share the same key are equal. Otherwise, it shall return the least upper bound of x and y, if it exists.

val powerset : 
  ('a, 'e) Core_kernel.Set.comparator ->
  ?inspect:('a -> Core_kernel.Sexp.t) ->
  string ->
  ('a, 'e) Core_kernel.Set.t domain

powerset total name defines a set of all subsets domain.

Sets ordered by inclusion is a natural domain. The join operator is the set union, and the order operator is the is_subset function.

val opinions : 
  ?inspect:('a -> Core_kernel.Sexp.t) ->
  empty:'a ->
  equal:('a -> 'a -> bool) ->
  string ->
  'a opinions domain

opinions empty equal name defines an opinionated domain.

In the opinionated domain, the order of elements is defined by the total reliability of agents that support this information. The more trustworthy the agent and the more agents support data, the higher the data will be in the chain.

See corresponding suggest, propose, and resolve operators.

val string : string domain

string is flat domain with an empty string at the bottom.

val bool : bool option domain

bool is the tribool domain.

val obj : ('a, _) cls -> 'a obj domain

obj is a flat domain with a null object at the bottom.

val empty : 'a t -> 'a

empty domain is the bottom of the domain.

val is_empty : 'a t -> 'a -> bool

is_empty domain x is true if x is empty domain.

val order : 'a t -> 'a -> 'a -> Order.partial

order domain x y orders x and y according to the domain order.

val join : 'a t -> 'a -> 'a -> ('a, conflict) Core_kernel.result

join domain x y is the upper bound of x and y.

val inspect : 'a t -> 'a -> Base.Sexp.t

inspect domain x introspects x.

val name : 'a t -> string

name domain is the domain name.

package bap-knowledge