domains

type AbstractLiteral ¶

type AbstractLiteral interface {
}

AbstractLiteral is the base interface for all concrete domain literals. Such literals are for example floats or strings. Abstract literals should be comparable and values from two different domains are never equal. That is checked in go automatically, from the specification:

"Interface values are comparable. Two interface values are equal if they have identical dynamic types and equal dynamic values or if both have value nil."

Source: https://golang.org/ref/spec#Comparison_operators

type BinaryEqualsRational ¶

type BinaryEqualsRational struct{}

func NewBinaryEqualsRational() BinaryEqualsRational

func (r BinaryEqualsRational) Arity() int

func (r BinaryEqualsRational) Relation(values ...AbstractLiteral) bool

func (r BinaryEqualsRational) String() string

type CDManager ¶

type CDManager struct {
	Domains  []ConcreteDomain
	Formulae []*TypedPredicateFormula
	// contains filtered or unexported fields
}

CDManager is used to store all concrete domains and the formulae (PredicateFormula) that exist within an ontology. It also stores a reference to the domain a formula was created for. It uses uints to identify the formulae, with indices from 0 to n-1 where n is the number of formulae. Thus it just stores TypedPredicateFormula instances. The Domains are normally fixed and contains all domains implemented. That is at the moment only the Rationals (ℚ). There also exists a mapping to get all formulae for a given domain.

Addming formulae is usually done with the build-in Add method, this will take care that the mapping from domain ↦ formulae of domain is kept in tact. Note that this method is not safe for concurrent use.

func NewCDManager() *CDManager

func (m *CDManager) Add(formula *TypedPredicateFormula) int

func (m *CDManager) AddDomain(d ConcreteDomain) int

func (m *CDManager) GetDomainByID(id ConcreteDomainEnumeration) ConcreteDomain

func (m *CDManager) GetFormulaByID(id uint) *TypedPredicateFormula

func (m *CDManager) GetFormulaeFor(id ConcreteDomainEnumeration) []*TypedPredicateFormula

type ConcreteDomain ¶

type ConcreteDomain interface {
	// Contains checks if an abstract literal is part of the concrete domain.
	// The concrete implementation must document this.
	Contains(l AbstractLiteral) bool
	// ConjSat must check if the conjuntion of all formulae is satisfiable.
	// Each formula consists of an id (the predicate as returned by GetPredicates)
	// and all the features (that become the variables in the first-order
	// formula).
	ConjSat(gamma ...*PredicateFormula) bool
	// Implies must check if the conjunction of formulae Γ implies the formula.
	Implies(formula *PredicateFormula, gamma ...*PredicateFormula) bool

	Name() string
}

ConcreteDomain is a concrete domain as defined in EL++. Thus it has a set Δ(D) and a set of extensions p(D). The set is of course not stored, for example ℚ is an infinite set. We cannot even store all predicates (for example predicate >q). A concrete domain will have methods to create new relations (for example for each q ∈ ℚ); and thus we construct them as needed.

A concrete domain must be able to answer conjunction queries (is a set of formulae Γ satisfiable) and answer implication queries (does a set of formulae Γ imply another formula).

As mentioned above relations for a concrete domain are created as need be - and these relations may here be used in formulae. The concrete domain must then understand each relation it has created. The details of that process are left to the concrete implementation. The functions should panic if they receive a predicate they don't understand.

It also has a function to determine if an abstract literal is part of the concrete domain. Concrete domains should document which values are considered part of the domain.

Concrete domains must be comparable via ==, that is two instances of a concrete domain must be considered equal and == should return false only if both sides are not the same concrete domain. See remark above about comparing interface values.

type ConcreteDomainEnumeration ¶

type ConcreteDomainEnumeration int

ConcreteDomainEnumeration is an enumeration of all concrete domains directly available in goel. Currently this is only the concrete domain of rationals.

const (
	Rationals ConcreteDomainEnumeration = iota
)

func (dom ConcreteDomainEnumeration) String() string

type EqualsRational ¶

type EqualsRational float64

func NewEqualsRational(q float64) EqualsRational

func (r EqualsRational) Arity() int

func (r EqualsRational) Relation(values ...AbstractLiteral) bool

func (r EqualsRational) String() string

type FeatureID ¶

type FeatureID int

FeatureID is used to represent different features (functions f1, ... fk) as defined in EL++.

func NewFeatureID(id int) FeatureID

func (id FeatureID) String() string

type GreaterRational ¶

type GreaterRational float64

func NewGreaterRational(q float64) GreaterRational

func (r GreaterRational) Arity() int

func (r GreaterRational) Relation(values ...AbstractLiteral) bool

func (r GreaterRational) String() string

type PlusRational ¶

type PlusRational float64

func NewPlusRational(q float64) PlusRational

func (r PlusRational) Arity() int

func (r PlusRational) Relation(values ...AbstractLiteral) bool

type Predicate ¶

type Predicate interface {
	Arity() int
	Relation(values ...AbstractLiteral) bool
}

Predicate is a predicate such as > for a concrete domain: It has an arity n > 0 and an extension (a realation with that arity). Enumerating all values is not possible (for example the smaller relation on ℚ), thus it is defined as a function that takes n arguments and returns true or false. A predicate relation may assume that it is only called with exactly n elements (n is returned by the Arity() function).

It may also assume that all values are indeed part of the concrete domain, see ConcreteDomain type for more details.

type PredicateFormula ¶

type PredicateFormula struct {
	Predicate Predicate
	Features  []FeatureID
}

PredicateFormula is a formula of the form p(f1, ..., fk).

func NewPredicateFormula(predicate Predicate, features ...FeatureID) *PredicateFormula

func (f *PredicateFormula) String() string

type RationalDomain ¶

type RationalDomain struct {
}

RationalDomain is the concrete domain for rational numbers (ℚ). Only elements of type float64 are considered part of this domain.

It has the following predicates:

(1) A unary predicate ⊤(ℚ) (contains all q ∈ ℚ)

(2) A unary predicate =(q) for all q ∈ ℚ (contains itself)

(3) A unary predicate >(q) for all q ∈ ℚ (contains all elements that are greater than q)

(4) A binary predicate +(q) for all q ∈ ℚ with the semantics { (q', q”) ∈ ℚ² | q' + q = q” }

Answering the logical queries is done by solving a linear program.

TODO in this domain: see my comment in Implies If this bug is still there it might be worth to try to reduce the actual cgo calls to a fixed value (like 500) see: https://groups.google.com/forum/#!topic/golang-nuts/_FYWG3oU6X8 we need a reasoner for this written in go...

Update: Problem still there, with new error: delete_lp: The stack of B&B levels was not empty (failed at 0 nodes) pretty sure it's something with lp_solve and golp

I've locked the complete domain when solving a linear program! That's totally not the way to go!

Update again: Even locking it with a mutex didn't help, some syscall crashes in golp (that's what I expect)

func NewRationalDomain() *RationalDomain

func (d RationalDomain) ConjSat(gamma ...*PredicateFormula) bool

func (d *RationalDomain) Contains(l AbstractLiteral) bool

func (d RationalDomain) FormulateLP(gamma ...*PredicateFormula) *golp.LP

func (d RationalDomain) Implies(formula *PredicateFormula, gamma ...*PredicateFormula) bool

func (d *RationalDomain) Name() string

type TrueRational ¶

type TrueRational struct{}

TrueRational implements the domain ⊤(ℚ).

func NewTrueRational() TrueRational

func (r TrueRational) Arity() int

func (r TrueRational) Relation(values ...AbstractLiteral) bool

func (r TrueRational) String() string

type TypedPredicateFormula ¶

type TypedPredicateFormula struct {
	Formula  *PredicateFormula
	DomainId ConcreteDomainEnumeration

	// id of the formula, this is required for the conversion to concepts
	// on create set to 0, but this must be set to the correct value!
	// thus when creating a formula and adding it use the Add function, that will
	// set this value correctly
	FormulaID uint
}

TypedPredicateFormula is a PredicateFormula that also has information about the domain a formula belongs to. Domains are identfied by an id, see CDManager for more information.

func NewTypedPredicateFormula(formula *PredicateFormula, domain ConcreteDomainEnumeration) *TypedPredicateFormula

func (formula *TypedPredicateFormula) String() string