Transcript algebra binds

Java Bytecode Compilation for
High-Performance, Platform-Independent
Logical Inference
Ashish Arte
Organization
 Designing
a reasoning system
 Reasoning systems in Java
• Java Logic Interpreter
• Logic-to-Java Compiler
• Logic-to-Bytecode Compiler
 Test
results and Evaluation
2
Reasoning
 Reasoning
is the process of drawing conclusions
from facts
• All men like donuts
• Homer is a man
• Homer likes donuts
 Automated
Reasoning
• Concerned with building computing systems that
automate reasoning
3
Automated Reasoning Systems
 Use
• Logic, Mathematics, Computer Science, Engineering
 Potential
Use
• Biological Sciences, Medicine, Commerce, etc.
 Impediments
• Computationally intensive
• Often have high performance requirements
• Not intuitive
• Do not learn from past experience
4
Solution
 Compensate
computational overhead
• Design systems that execute faster
• Introduce parallelization
 Java
supports both approaches
• Permits efficient reasoning
• Support for parallel and distributed computing
5
Designing A Reasoning System
 Problem
Representation
• General-purpose reasoning system
 Inference
Mechanism
 Efficient Reasoning
6
Simpson’s World
 Axioms:
• Homer is Lisa’s father
• Homer has a pet Santa
• Snowball is a cat
• Everybody in Springfield likes cats
• Anybody in Springfield who has a pet also likes cats
• Anybody who likes cats, will not kill a cat
• Either Homer or Curiosity killed the cat, Snowball
 Goal
• Did Curiosity kill the cat ?
7
First-Order Logic
 Constant
denotes an element in a domain
• homer, marge, lisa
• springfield, snowball, santa
 Predicates
capture relationships between elements
• father(homer, lisa)
• hasPet(homer, santa)
 Connectives
allow complex predicates
• father( homer, lisa)  mother( marge, lisa)
8
First-Order Logic
 Variables
are used to denote arbitrary elements
• Permit general statements about the domain
– father (X, Y)
– lives (X,springfield)
 Functions
describe mappings between elements
– mother (lisa)
 Constants,
variables, functions are collectively
identified as Terms
9
First-Order Logic Representation
abstract Term
Constant
Tuple
Variable
String value
Constant functor
Term[] body
String value
• homer, lisa
• zero, two
• mother(X)
• gt( successor(Y), Y)
•X
•Y
10
First-Order Logic Statements
sibling(lisa,brother(lisa))
sibling(brother(lisa), lisa)
Literal
Clause
Theory
boolean sign
Term term
Literal[] body
Clause[] clauses
11
Simpson’s World

Clause Set
1.
2.
3.
4.
5.
6.
7.

father(homer, lisa)
hasPet(homer, santa)
cat(snowball)
lives(X, springfield)  likesCats(X)
likesCat(X)  lives(X, springfield)  hasPet(X,Y)
kills(X,Y)  likesCats(X)  cat(Y)
kills(homer, snowball)  kills(curiosity, snowball)
Goal
G: kills(curiosity, snowball)
12
Designing A Reasoning System
 Language
Representation
 Inference Mechanism
• Model Elimination (Loveland)
– Goal-oriented
– Proof by contradiction
– Bottom-up construction of proof tree
 Efficient
Reasoning
13
Model Elimination Example
kills(curiosity, snowball)
kills(homer, snowball)
kills(curiosity, snowball)  kills(homer, snowball)
14
ME Extension

If a goal matches a complementary literal from a clause
• Extend the goal by attaching all other clause literals
• Attached literals considered as subgoals of original goal

Example
• kills(curiosity, snowball)
• kills(curiosity, snowball)  kills(homer, snowball)

Matching procedure is called Unification
15
ME Example
kills(curiosity, snowball)
kills(homer, snowball)
cat(snowball)
likesCats(homer)
kills( X, Y)  likesCats( X )  cat( Y )
16
Unification
 Pattern
matching via variable assignments
 Example
• kills( homer, snowball)
• kills( X, Y)  likesCats( X )  cat( Y )
• X/homer, Y/snowball
 Assignment
{X/homer} is called binding
 Binding, {X/likes(donuts,X)}, is not permitted
17
Dereferencing
 Process
of identifying a Term’s binding
 Constants and Tuples yield the respective
instances
 Variable yields
• The Variable instance if it is free
• The Term instance the variable is bound to
• X → Y → Z → homer
18
ME Example
kills(curiosity, snowball)
kills(homer, snowball)
cat(snowball)
cat(snowball)
likesCats(homer)
hasPet(homer, Y)
hasPet(homer, santa)
lives(homer, springfield)
likesCats(homer)
hasPet(homer,santa)
cat(snowball)
? )  likesCats(X)
likesCat( lives(
X )  X,
lives(
springfield
X, springfield
)  hasPet( X,Y)
19
ME Reduction

A subgoal can be reduced if
• It unifies with a complementary ancestor on its branch

Modeled as closing of the branch
20
ME Proof Procedure
kills(curiosity, snowball)
kills(homer, snowball)
cat(snowball)
cat(snowball)
likesCats(homer)
hasPet(homer, Y)
hasPet(homer, santa)
lives(homer, springfield)
likesCats(homer)
21
Java Logic Interpreter
Axioms
&
Goal
Preprocessor
Inference
Engine
Proof
22
Designing A Reasoning System
 Language
Representation
 Inference Mechanism
 Efficient Reasoning
• ME extension by compiled execution
23
Prolog
 Logic
programming language
 Proof by contradiction.
 Efficient proof procedure
• pre-compilation of unification steps
• compiled into executable abstract machine instructions
 Efficiency
at the expense of language
• Clauses restricted to definite clauses
• Definite clauses contain exactly one positive literal
– p  q  r  s
 ME
extension similar to Prolog’s inference step.
24
Contrapositive
 Set
of permutations with different literal as the first
literal each time.
 Logically equivalent to original clause.
 kills(homer,snowball)  kills(curiosity, snowball)
• (kills(homer,snowball)  kills(curiosity, snowball)
• (kills(curiosity,snowball)  kills(homer, snowball)
 Head:
first literal, body: other literals
• kills(homer,snowball)  kills(curiosity, snowball)
– Head: kills(homer,snowball)
– Body: kills(curiosity, snowball)
25
Logic-to-Java Compiler
FOL
Clauses
Rules
Preprocessor
Goal
Clause
Parser
Instances
Inference
Engine
Proof
Logic
Compiler
26
Rule Representation
Rule
Literal head
Literal[] body

Constructor
• Instructions to build the structure of
the contrapositive

applyRule method has:
• Pre-compiled instructions to unify a
Rule()
applyRule(Subgoal)
head term with any subgoal term.

Generated instructions are
embedded as Java code.
27
Rule: lives(X, springfield) Constructor
public class rule extends Rule{
Term constant_a;
Term variable_X;
Term tuple_t;
Term functor_f;
Literal head ;
public rule(){
constant_a = Constant.lookup( “springfield” );
variable_x = new Variable( “X” );
functor_f = Constant.lookup( “lives” );
Term[] body = {variable_X, constant_a};
tuple_t = new Tuple( functor_f, body );
head = new Literal( tuple_t );
// Constructs declared
// as member variables
// lookup instance of Constant
// create instance of Variable
// lookup functor
// array of Tuple’s parameters
// new Tuple
// Literal for head literal
}
}
28
Unification
Rule Head
Subgoal
p
a
p
q
W
1. Match functors p
2. Bind
UnifyWa to
& afirst parameter
q
3. Match
Unify q(X,Y)
functors
& qsecond parameter
X
Y
Z
s
4. Bind
1. Match
X to Zfunctors q
W
5. Bind
1. Bind
Y toXs(W)
to first parameter
p(a,q(X,Y))
1. Bind Y to second parameter
Unification as concurrent depth-first traversal of terms
29
Compiled Unification
Rule Head
Subgoal
p
applyRule(Subgoal s)
1. Match functors p
p
Term subgoal = subgoal.term ;
Tuple tuple = (Tuple)subgoal ;
a
q
W
q
if( tuple.functor == functor_p )
&& tuple.parameters == 2 ) {
X
Y
2. Unify a and first parameter
Z
s
Term param = tuple.body[0]
param = dereference ( param )
W
if( param != constant_a ) {
if ( param instanceof Variable ) {
variable = (Variable)param
variable.bind(constant_a)
}else {
return failure
}
} // Identical constants proceed
30
Compiled Unification
Rule Head
Subgoal
p
3. Unify q(X,Y) & second parameter
p
Term term = tuple.body[1]
term = dereference ( term )
a
q
X
W
Y
q
Z
if ( term instanceof Variable ) {
if( !occurs( term, term_q ) ) {
variable = (Variable) term ;
variable.bind(term_q);
}
s
}
W
31
Compiled Unification
Rule Head
Subgoal
p
else if ( term instanceOf Tuple ){
3.1 Match functors q
p
Tuple tuple = (Tuple)term;
if( tuple.functor == functor_q )
a
q
W
&& tuple.parameters == 2 ) {
q
3.2 Bind X to first parameter
Term param_1 = tuple.body[0]
X
Y
Z
variable_X.bind( param_1 )
s
3.3 Bind Y to second parameter
Term param_2 = tuple.body[1]
W
variable_Y.bind( param_2 )
}
}
else{
return failure
}
}
32
Logic-to-Java Compiler
FOL
Clauses
Parser
Rules
Preprocessor
Goal
Logic
Compiler
Rules As
Java Files
Inference
Engine
Proof
Java
Compiler
33
Bytecode Compilation
 Prolog’s
high efficiency
• Inference instructions precompiled for WAM
• Warren Abstract Machine instructions set optimized
for Prolog
• WAM & JVM have similar architectures
 JVM
instructions for logical deduction
• Standard Java compiler does not understand logical
deduction domain
• Specialized compiler generates bytecodes customized
for logical deduction.
34
Logic-to-Bytecode Compiler
FOL
Clauses
Parser
Rules
Preprocessor
Goal
Inference
Engine
Proof
Rules As
Logic
Compiler Binary Java Classes
35
JVM Instruction Set


Central focus is the operand stack
• Instructions transfer data between operand stack and local variables
Eg: a = b + c
• b, c and a stored in JVM’s local variables 2, 3, and 4
• Bytecodes generated to add these numbers:
–
–
–
–
–
–


9:
10:
11:
12:
14:
16:
iload_2
iload_3
iadd
istore 4
iload 4
ireturn
// Load b from local variable 2
// Load c from local variable 3
// Add the two integers
// Store the result in a, in local variable 4
// Load a from local variable 4
// Return the result
Stack-centric nature provides support for implementing JVM on broad
range of CPUs.
Compact design facilitates speedy transmission across networks.
36
Bytecode Logic Compiler

Input
• Set of clauses represented in Java

Output
• Binary Rule classes directly compiled using a library

Characteristics of bytecodes in applyRule
• Bytecodes perform a depth-first traversal similar to Logic-to•
•
•
•
Java Compiler.
Head term traversed by accessing the member variables
Subgoal term decomposed using method variables
Decomposition contains redundant operations
Redundancy because intermediate results are stored in variables.
37
Redundant Data Transfers
Load s_param
Tuple s_tuple = (Tuple)s_param
Cast Tuple
Store s_tuple
Load s_tuple
Term s_functor = s_tuple.functor
getField functor
Store s_functor
Load s_tuple
Term[] s_body = s_tuple.body
getField body
Store s_body
Load s_functor
if (functor_q equals s_functor)
Load functor_q
Compare
38
Stack-based Subgoal Decomposition
Rule Head
Subgoal
push p(W,q(Z,s(W))
dup
p
p
getField functor
getField functor_p
a
q
W
q
compare
getField body
X
Y
Z
s
dup
getField length
W
push 2
[2]
p
compare
p(W,q(Z,s(W)))
[2]
p
[W,q(Z,s(W))]
dup
p(W,q(Z,s(W)))
[W,q(Z,s(W))]
39
Stack-based Subgoal Decomposition
Rule Head
Subgoal
load 0
dereference
p
p
dup
getField constant_a
a
q
W
compare
q
checkCast Variable
X
Y
Z
s
getField constant_a
bind
load 1
W
…
a
W
a
compare functors
verfiy parameters
[Z,s(W)]
W
[W,q(Z,s(W))]
dup
q(Z,s(W))
[Z,s(W)]
[W,q(Z,s(W))]
…
40
Stack-based Subgoal Decomposition
Rule Head
Subgoal
load 0
dereference
p
p
getField variable_X
bind
q
a
W
load 1
q
dereference
X
Y
Z
s
getField variable_Y
bind
W
X
Y
Z
[Z,s(W)]
[Z,s(W)]
s(W)
41
Dereferencing Revisited
 Unification
binds variables
• X → Y → Z → homer
• Dereferencing traverses the chain of references
 Dereferencing implemented
while( term ) {
term = term.next
}
as a loop
42
Efficient Dereference Loop
Standard
26: aload 6
28: getfield <Field next>
31: aload 6
33: if acmpeq 46
36: aload 6
38: getfield <Field next>
41: astore 6
43: goto 26
Refined
<data on stack>
26: dup
27: getfield< Field next>
30: dup_x1
31: if_acmpne 25
34: dup
43
Evaluation
 Interpreted
versus Compiled
• Evaluate the performance of the system that performs
inference by executing compiled methods.
 Standard
compiled versus Custom compiled
• Evaluate the performance of the system executing the
refined inference methods.
44
Test Suite
 Test
Problems
• Five classes of problems
• Each class tailored to evaluate the effectiveness of
refinements.
 TPTP
problem library
• A large collection of problems from various domains
– Logic, Algebra, Geometry, Engineering, Planning
• Serves as a common suite for evaluation and
comparison of reasoning systems.
45
Interpreted v/s Compiled
Class
Class 1
Class 2
Class 3
Class 4
Class 5
Goal
Interpreted (secs)
Compiled(secs)
G11
20.227
10.793
G12
46.183
24.766
G13
106.68
57.646
G21
12.502
2.211
G22
30.999
13.787
G23
231.58
147.863
G31
11.391
8.032
G32
29.846
21.283
G33
84.805
60.981
G41
195.163
3.878
G42
239.347
6.904
G43
265.003
11.786
G51
7.249
6.904
G52
0.113
0.087
G53
0.18
0.133
46
Logic-to-Bytecode Compiler Configuration
Class
Class 1
Class 2
Class 3
Class 4
Class 5
Goal
Stack-Based(secs)
Dereference (secs)
Combined (secs)
G11
10.848
10.900
10.752
G12
24.912
24.941
24.571
G13
57.419
57.906
56.748
G21
2.211
2.223
2.178
G22
13.748
13.81
13.551
G23
147.631
148.958
145.747
G31
8.058
8.153
7.948
G32
20.331
21.67
21.140
G33
61.149
62.188
60.57
G41
3.911
3.888
3.866
G42
7.017
6.934
6.937
G43
11.772
11.708
11.740
G51
6.032
6.152
5.978
G52
0.086
0.087
0.087
G53
0.135
0.136
0.134
47
Standard Compiled v/s Bytecode Compiled
Class
Class 1
Class 2
Class 3
Class 4
Class 5
Goal
Logic-to-Java Compiler (secs)
Logic-to-Bytecode Compiler (secs)
G11
10.893
10.752
G12
24.766
24.571
G13
57.646
56.748
G21
2.221
2.178
G22
13.787
13.551
G23
147.863
145.747
G31
8.032
7.948
G32
21.283
21.140
G33
60.981
60.57
G41
3.878
3.866
G42
6.904
6.937
G43
11.786
11.740
G51
5.980
5.978
G52
0.087
0.087
G53
0.133
0.134
48
Conclusions



Pre-compiling inference steps into methods executable at
runtime is faster than runtime interpretation.
Using a special compiler, customized for an application
domain, provides ability to incorporate refinements that
improve performance.
Java platform provides extensive support to perform logical
reasoning efficiently.
49
Future Work



Introduce parallelization
• Reasoning in first-order logic offers various forms of
parallelism.
• Java platform provides supports several paradigms for
high-performance parallel and distributed computing.
Study other refinement techniques to implement an efficient
reasoning system.
Explore performance of the reasoning systems on a Java
processor tailored for the JVM.
50
Questions
51