sjm.engine
Interface Term

All Known Subinterfaces:

ArithmeticTerm, BooleanTerm, ComparisonTerm

All Known Implementing Classes:

Structure

public interface Term

The Term interface defines the core elements of the logic engine.

Terms are the central objects in the logic programming data model, which is basically as follows:

• A Program is a collection of Rules.
• A Rule is a series of Structures.
• A Structure is an Object associated with a collection of Terms.
• Structures and Variables are Terms.

The statement that "Structures and Variables are Terms" has both a loose meaning and a literal meaning. Loosely, the statement means that the contents of a structure are other structures and variables. For example, the terms of plays(jim, Game) are the structure jim and the variable Game. The literal meaning is that class Structure and class Variable implement the interface Term.

In addition to residing at the core of the data model, the Term interface also defines unification. Unification is a kind of matching, and is the basic step in the execution of a logic program. Roughly speaking, two structures can unify if their variables can take on values to make the structures equal. To prove itself against a program, a Structure:

• Unifies with the head of a Rule.
• Asks the Rule to prove its remaining structures.

This simple algorithm is the execution model of a logic engine. A structure can unify with another structure if their functors are equal, and if their terms can unify. An uninstantiated variable unifies with a term by instantiating to it. An instantiated variable can unify with another term if its instantiation can unify with the term.

The other methods declared by the Term interface define behavior that must exist in all terms, whether they are structures or variables. This behavior includes a method for creating provable version of a term, and a method for returning the value of term in a function.

Method Summary

Term	copyForProof(AxiomSource as, Scope scope) Returns a copy of the term for use in a proof.
java.lang.Object	eval() The value that this term should present to an evaluating function.
boolean	isList() Return true, if this term is a list
java.lang.String	listTailString() Returns a string representation of this listTailTerm.
Unification	unify(Structure s) Returns a collection of variables that allow this term to unify with a structure.
Unification	unify(Term t) Returns a set of variable instantiations that allow two terms to unify.
Unification	unify(Variable v) Returns a collection of variables that allow this term to unify with a variable.
Unification	variables() Returns the variables associated with this term.

Method Detail

copyForProof

public Term copyForProof(AxiomSource as,
                         Scope scope)

Returns a copy of the term for use in a proof.

When a structure proves itself against a program, it unifies with the head of a rule in the program, and then asks the remaining structures in that rule to prove themselves. For this to work, the rule has to provide a proving copy, which has a new Scope. To provide a proving copy, a rule needs proving copies of its structures, and ultimately every term needs to be able to produce such a copy.

Parameters:

PosultateSource - where the term can look for rules

Scope - variables for the provable rule copy

Returns:

a provable copy of this Term, that will use the supplied axiom source and scope

eval

public java.lang.Object eval()

The value that this term should present to an evaluating function.

Returns:

the value that this term should present to an evaluating function, such as an ArithmeticOperator.

isList

public boolean isList()

Return true, if this term is a list

Returns:

true, if this term is a list

listTailString

public java.lang.String listTailString()

Returns a string representation of this listTailTerm. That is, return a string representation of this term, given that it is the tail of a list.

Returns:

a string representation of this listTailTerm

unify

public Unification unify(Structure s)

Returns a collection of variables that allow this term to unify with a structure.

Parameters:

Structure - the structure to unify with

Returns:

a collection of variables that allow this term to unify with a structure

unify

public Unification unify(Term t)

Returns a set of variable instantiations that allow two terms to unify.

When a term unifies with another term, the necessary behavior can be different depending on whether the objects involved are structures or variables. To allow the right behavior to occur, the Term interface defines two unify methods. This allows an implementing class to use a "double dispatching" scheme to get the right behavior for unification.

Structure.unify(Term t) employs double dispatching by returning t.unify(this). This is a call to an implementation of unify(Structure s), which is a different method from than unify(Term t). The receiver thus knows it is unifying with a Structure and can act accordingly.

Structure implements unify(Structure s) to provide the unification of two structures. That is, it returns the combined unification of its terms with the other structure's terms, provided both have the same functor.

Variable implements both its unify() methods the same way. If the variable is uninstantiated, is instantiates to the supplied term. If the variable is already instantiated, it returns the unification of its instantiation with the supplied term.

Unification of an uninstantiated variable always succeeds. If a variable is instantiated, its success at unification depends on its instantiation. Unification of two structures succeeds if the structures have equal functors, the same number of terms, and if all their terms unify successfully. When unification fails, the unify methods return null.

Parameters:

Term - a term to unify with

Returns:

Unification a collection of variable assignments that allow the unification to succeed

unify

public Unification unify(Variable v)

Returns a collection of variables that allow this term to unify with a variable.

Parameters:

Variable - the variable to unify with

Returns:

a collection of variables that allow this term to unify with a variable

variables

public Unification variables()

Returns the variables associated with this term.

For a variable, this method returns a unification that contains just the variable itself. For a structure, this method returns a collection of the variables from each of its terms. For example, the variables in

     address(street(Street), city(City), state(State))
 

are Street, City, State.

Returns:

the variables associated with this term