Trivial Prolog Interpreter Written in Java

Preamble

I learned about Prolog from Byte magazine. I also learned how to programme in Prolog from Byte magazine. Some years ago I became interested in learning about the fundamentals of logic programming, and old Byte magazines were an invaluable source. But unification doesn’t map obviously to a machine based on registers, memory and an arithemetic unit. If Byte was still in existence I would never have needed to write my own Prolog interpreter — lacking a good explanation of how the interpreter actually achieves it ends, I was forced to write my own.

Of course, in the true spirit of logic programming, I invented a new and incompatible syntax for my interpreter. I also omitted all the useful bits, leaving only the core logic. ( You can’t even do arithmetic. )

In my thought experiments, I conceived of a way of writing an interpreter that only used one stack. Byte articles had hinted that two stacks were necessary, so I set out to prove otherwise. “C” would have been the natural language to write such an interpreter, as writing an interpreter that allocated all memory using “alloca” ( or GNU C dynamic arrays ) was the point of the whole exercise. However, the siren call of Java overwhelmed me.

I wanted to prototype my design in an kinder gentler environment than C. And I had been flirting with Java for some time. Despite being a compiled language (and despite not having had an IDE available), Java is quite good as a little language. Error messages are informative and the build system is easy to use. I don’t regret writing this in Java even though it completely obscures the code’s reason for being.

From the standpoint of a student of computer programming languages, Java is quite nice; the strong type system is well designed and inner classes and closures make it interesting to use. Only the cursed necessity of casting mars this language. Java needs STL. Certainly, advocates of strongly typed languages deserve something easier to use than C++.

Lastly, I had the opportunity of writing a simple GUI front end using Swing. The GUI barely does anything at all, but it allowed me explore every known way of deadlocking two concurrent threads. I am not sure, even now, whether the threading code is sound.

The Code and the Build System

This is the web formatted and coloured source for the tprologinjava package. The programme resides in the namespace “ca.draisey.free.tprolog” where it belongs. The ’t’ stands for trivial.

I used scons as the build system. I just pile all the source into one directory and let scons work out what to do. Scons reads the source to determine the dependency graph and rebuilds as necessary. It is very easy to use — here is the text of the entire build script — all two lines of it.

# SConstruct

Java('classdump', 'src')
Jar('tprolog.jar', ['Manifest.txt', 'classdump'], JARCHDIR='classdump')

And here is the manifest file.

Manifest-Version: 1.0
Name: ca.draisey.free.tprolog/Prolog
Specification-Title: Trivial Prolog Interpreter
Specification-Version: 1.0
Specification-Vendor: free.draisey.ca
Implementation-Title: tprolog.PrologNewGUI
Implementation-Version: build1
Implementation-Vendor: free.draisey.ca
Main-Class: ca/draisey/free/tprolog/PrologNewGUI

The Inheritance Hierarchy

Snippets

I put most of the documentation into the base abstract classes of the programme.

SuccessionDatabase.java
The rulebase for the interpreter. 
void queryDatabase(
    final Term goal,
    final Variables goals,
    final Successor success
)
{
    final java.util.Iterator i = matching( goal.getkey() );
    while( i.hasNext() ) {
        Sentence quantifiedRule = (Sentence) i.next();
        quantifiedRule.dequantifyClause().queryClause(
            goal,
            quantifiedRule.instantiateVariables(),
            goals,
            success
        );
    }
}
HornClause.java
We reason backward from effect to cause. Each HornClause node has consequent and antecedent fields. The queryClause method accepts a goal and implements our modus ponens rule --- if the consequent of a rule in the database would imply our goal we conditionally accept it and reason backwards from its antecedent as our new subgoal. 
final void queryClause(
    final Term goal,
    final Variables these,
    final Variables goals,
    final Successor success
)
{
    consequent.queryClause(
        goal,
        these,
        goals,
        success.succession().new SuccessionSuccessor() {
            void succeed()
            {
                succession().queryDatabase(
                    antecedent,
                    these,
                    success
                );
            }
        }
    );
}

private final Clause consequent;
private final Term antecedent;
Term.java
The unification of terms. The abstract base class of AtomTerm, PairTerm ( ConsTerms ) and VariTerm. 
final void queryClause(
    final Term goal,
    final Variables these,
    final Variables goals,
    final Successor success
)
{
        unifythrough( goal, these, goals, success );
}

protected abstract void unifythrough ... ;
protected void unifytoPair ... {}
protected void unifytoCons ... {}
protected void unifytoAtom ... {}

protected void unifytoUnboundVariable(
    final VariTerm that,
    final Variables these,
    final Variables those,
    final Successor success
)
{
    that.bindto( this, those, these, success );
}
PairTerm.java
The unification of terms. 
protected final void unifythrough(
    final Term that,
    final Variables these,
    final Variables those,
    final Successor success
)
{
    that.unifytoPair( this, those, these, success );
}

protected final void unifytoPair(
    final PairTerm that,
    final Variables these,
    final Variables those,
    final Successor success
)
{
    //System.out.print("P");
    left.unifythrough(
        that.left,
        these,
        those,
        success.succession().new SuccessionSuccessor() {
            void succeed()
            {
                right.unifythrough(
                    that.right,
                    these,
                    those,
                    success
                );
            }
        }
    );
}

private final Term left, right;
VariTerm.java
Terms that are variables. This class houses the bindto method which, despite being only five lines long, implements the unification algorithm. 
final void bindto(
        final Term that,
        final Variables these,
        final Variables those,
        final Successor success
)
{
    //System.out.print("V");
    these.ruleBindings[ index ] = that;
    these.instanceBindings[ index ] = those;
    success.succeed();
    these.ruleBindings[ index ] = null;
    these.instanceBindings[ index ] = null;
}

protected final void unifythrough(
    final Term that,
    final Variables these,
    final Variables those,
    final Successor success
)
{
    if( these.ruleBindings[ index ] == null )
        that.unifytoUnboundVariable( this, those, these, success );
    else
        these.ruleBindings[ index ].unifythrough(
            that,
            these.instanceBindings[ index ],
            those,
            success
        );
}

protected final void unifytoAtom(
    final AtomTerm that,
    final Variables these,
    final Variables those,
    final Successor success
)
{
    if( these.ruleBindings[ index ] == null )
        bindto( that, these, those, success );
    else
        these.ruleBindings[ index ].unifytoAtom(
            that,
            these.instanceBindings[ index ],
            those,
            success
        );
}
protected final void unifytoCons ...
protected final void unifytoPair ...
protected final void unifytoVari ...

protected final void unifytoUnboundVariable(
    final VariTerm that,
    final Variables these,
    final Variables those,
    final Successor success
)
{
    if( these.ruleBindings[ index ] == null ) {
        if( this == that && these == those ) success.succeed();
        else {
            if( randomGenerator.nextBoolean() )
                this.bindto( that, these, those, success );
            else
                that.bindto( this, those, these, success );
        }
    }
    else
        these.ruleBindings[ index ].unifytoUnboundVariable(
            that,
            these.instanceBindings[ index ],
            those,
            success
        );
}

protected final int index;