
\chapter{AIR Reasoner}

\section{Introduction}
When expressing a policy, one uses rules. A rule states that in certain circumstances, something applies. There are many ways of modeling this, but one of them is a rule language. 

The TAMI project\cite{TAMI} is a project for finding ways of keeping privacy in an increasingly connected world. One of the efforts of the project is finding ways to express and enforce policy. The AIR language\cite{air} is one such attempt. 

For building a policy language, a rule language similar to Notation3 rules
was thought of to be useful. However, justifications were thought
to be perhaps as important as the results. As a result, several different 
choices were made. 

The first major change is architectural. The RDF store is replaced
by a \emph{Truth Maintenance System} (TMS) \cite{doyle79}. 
The TMS provides considerable power in a very simple
mechanism; its primary cost is the memory required to record the
structure of a derivation.  Although the TMS technology was invented
in the 1970s, it is not well known outside the artificial intelligence
community, and consequently there are no uses of this technology in
policy systems of which we are aware.

The second major change is in syntax. In order to refer to
rules in a more clear way, it is useful to name them. This
makes rules take up more than one triple. Once this happens,
having a rules imply another rules requires special syntax.

Indeed, a rule can have any number of \qname{air:assert} clauses. However, unlike Notation3 rules which can imply the existence of other rules simply by having the other rule in the consequent, an AIR rule is a structure made of multiple triples. To allow for rules to be created with the data would allow for a set of triples created with separate rules to spontaneously become a rule. This would increase the complexity of the implementation. Therefore, a rule can have triples the have it as the subject, \qname{air:rule} as the predicate, and another rule as the object. This other rule, with the correct variable bindings, becomes active with the firing of the outer rule. 

A second problem is that a search can be either data directed or goal directed. However, both are wasteful. Pure goal direction, as in Prolog, will search for many facts which do not exist. Pure data direction, as in most production rule systems, will find many facts which are not interesting or wanted. To search from both ends, with goals and facts both directing the search, can be more efficient than either.

AMORD\cite{kleer77amord} is a production rule system like this. By writing rules to carefully manipulate goals, it is possible to cut down on search. As a production rule system, the rules are instructions to the system, and are not intended to have inherent logical meaning. 

A typical way of programming AMORD is to have facts themselves, and have goals of those facts. One can write rules to manipulate goals, and only generate facts when needed. In this way, AMORD can act like a hybrid of a forward and backward chainer.

AMORD also shows how this approach can lead to problems. Rules to manipulate goals that are not written carefully can loop backward forever like any backward chainer. Correctly writing rules that run efficiently is a subtle art.

In AIR, the TAMI project took this goal manipulation and made it part of the language. Having a pattern in a rule leads to that pattern being a goal. A {\bf goal rule} matches a set of triples, at least one of which is a goal. A goal rule will almost never create a fact --- few things are true simply because we want them to be. Typically, it has a sub-rule which is a normal rule, and is therefore controlled by the goal.

Therefore, AIR has a syntax that names rules. Every rule has a pattern, and some number of assertions. It can have some number of subrules, which assert a rule. It has its set of variables as a property, instead of as Notation3 variables, for historical reasons\footnote{The semantics for this are confusing at best. There is a reason why variables are a \emph{syntactic} property in Notation3}. A set of rules can belong to a \emph{policy} which is run by the reasoner. The AIR ontology has all of this, and more.

As an example, we will look at a rule to implement the \qname{rdfs:subPropertyOf} property. If a property $P1$ is a sub-property of $P2$, then 
\begin{equation}
\forall x,y . P1(x,y) \rightarrow P2(x,y)
\end{equation}
We can encode this as an AIR rule very easily. It looks like
\begin{verbatim}
:subProperty1 a air:Rule;
     air:variables :x, y, :P1, P2;
     air:pattern {?P1 rdfs:subPropertyOf ?P2 .
                  ?X ?P1 ?Y};
     air:assert {?X ?P2 ?Y} .
\end{verbatim}

Notice exactly how bad this rule is for AIR. The pattern \verb|?X ?P1 ?Y| creates the most general goal. Once this goal is created, the goal direction has essentially been bypassed. Therefore, more effort must be made in writing the rule. 

Simply encasing the rule in a goal rule would not work. The goal would be \verb|?X ?P2 ?Y|, which is also too general. 

The solution is to nest the rules, carefully controlling rules using goals and goals using rules. This would look like 
\begin{verbatim}
:subProperty2 a air:Rule;
     air:variables :x, y, :P1, P2;
     air:pattern {?P1 rdfs:subPropertyOf ?P2};
     air:goal-rule [ air:pattern {?X ?P2 ?Y};
                     air:rule [ air:pattern {?X ?P1 ?Y};
                                air:assert {?X ?P2 ?Y} ] ] .
\end{verbatim}
This is how the rule in \uri{http://dig.csail.mit.edu/TAMI/2007/amord/base-rules.ttl} is done. 

It is not always obvious what the correct way to write a rule is. That would depend on the interactions of the rules in the system. Perhaps this is a case where an optimizer written in software would be able to do a better job than the programmer.

%%% How much of the following needs to be kept/rewritten?

A Truth Maintenance System (TMS) \cite{doyle79} is a system to track
dependencies. By doing so, it figures out what results are based on 
what assumptions. One can easily add a satisfiability tester to
this, to find what is needed for something to be supported. One can 
assume and retract hypotheticals, to find out what results from 
various assumptions.

The main use of the TMS in AIR is to support the 
printing of justifications. It was deemed more interesting
to know why a particular decision was made, rather than
what was made. Given that the system will never have perfect
information, and at best it can be advisory towards people,
reasons are very important. 

TMS's have been used by others in RDF. The basic idea of using
a TMS to track derived facts, allowing for the removal of derived
facts if the base facts they depend on are removed, is used by \cite{Broekstra03inferencingand}.

As part of AIR rules, one can control the generation of dependencies.
In this way, the justification traces that are printed
can skip rules entirely, or classes of rules deemed to be not
interesting for whatever reasons. In particular, goal rules do
not manipulate any actual facts,
so should not appear in the
trace. 

The syntax for this allows for the matching of matched
graphs, and the building of TMS justifications out
of these. 

If no dependencies are given, then the rule to be used
for a rule is that everything that is created by the rule
depends on an \verb|AND| of everything that was used
to fire the rule --- the rule itself, and all
facts it matched. 

Other metadata can be given as properties to the rule. 
One that has been useful for human output is 
\qname{air:description}, which has in its range a list
of strings and RDF nodes. When the variables are substituted
into it, this is put into the justification output, forming
a human readable version.

In order to support a form of closed-world Negation-as-failure type reasoning, 
one can supply an \qname{air:alt} property to a rule.
This given what should be assumed if the rule
fails to fire. This is put into the TMS with a node
specifying exactly what was assumed that failed to 
fire the rule. In effect, it is making explicit the closed-world
assumption. This is easier to work with than \qname{log:includes},
though it runs into the problems of instability. 

An example of this instability is from a file reproduced in 
Appendix \ref{unstable.n3}. 

Running it through the current AIR reasoner fires exactly one
of the two rules, despite them being identical. Exactly what 
it should do in this case has yet to be determined. 
%%% @@@@ test me!!!! 

%===================================
\comment{
Justifications are required to explain reasoning results and usually
include the knowledge and rules used to infer these results. For
policy reasoners, this justification becomes especially important
because it provides important insights into the policy development and
enforcement process. Policy administrators use these justifications to
confirm the correctness of the policy and to check that the result is
as expected. Users, on the other hand, mainly utilize them to check
that the policy enforcement process works as it should and in the case
of failed queries to figure out what additional information is
required to get the correct result.

Our policy approach tracks dependencies during the reasoning process
in order to provide integrated justification support where policy
administrators are not required to handle or manipulate these
dependencies or justifications. We use a production rule system as a
reasoner and a Truth Maintenance System (TMS) as the
dependency-tracking mechanism. Our reasoner has additional features
for improved reasoning efficiency such as goal direction, which
controls how much inferencing the reasoner does. The reasoner also
supports the extraction of portions of explanations in order to
prevent the user from being overwhelmed by irrelevant data and
rules. As explanations are usually in the form of proof trees, we have
developed a graphical justification user interface, which presents the
explanation either in a Semantic Web rule language or in a graphical
layout that highlights the result of the reasoning and allows the
explanation to be explored.

Based on this approach, we propose a new policy language
\comment{amenable to efficient reasoning with dependency tracking in
  order to} aimed at meeting policy compliance requirements of open,
decentralized information infrastructures such as the World Wide Web
and large enterprise systems. \comment{Such environments have two
  unique requirements.  First, given the complexity of information
  usage rules, it is not always possible to completely evaluate rule
  compliance at the time an individual resource is accessed.  Rather,
  rule compliance can only be fully assessed by looking back over a
  chain of transactions.  Second, compliance may not be provable by an
  automated process, but only satisfied by the application of human
  judgment.  Hence, our system must be able to present a partial chain
  of justifications for a given action for evaluation by a human
  decision maker.  Finally, a mix of open and closed world reasoning
  is required.  Such challenging environments require a mix of open
  and closed world reasoning.}  The policy reasoner must be able to
search over a knowledge base as open as the Semantic Web, but must
also be able to assert closure over some set of facts in order to
reach a useful result.  These open environments point to the need for
flexible dependency tracking that gives users and administrators the
most complete possible view of the inference as well as efficient ways
of reasoning.

\section{Overview}

\subsection{Dependency Tracking}
\label{dependency-tracking}

A deductive reasoning system derives conclusions from previous
deductions or premises by the application of deductive rules.  For any
given conclusion, it is useful to know the specific set of premises
that it was derived from; this set is called the \emph{set of
  dependencies} for the conclusion.  \emph{Dependency tracking} is the
process of maintaining dependency sets for derived conclusions.

Some dependency-tracking mechanisms provide additional features.  For
example, a \emph{Truth Maintenance System} (TMS) \cite{doyle79} keeps
track of the logical structure of a derivation, which is an effective
explanation of the corresponding conclusion.  Another useful feature,
also provided by a TMS, is the ability to assume and retract
hypothetical premises.

There are several reasons why dependency tracking is useful for policy
systems:

\begin{itemize}

  \item The dependency set for a result provides a natural focus when
    trying to solve policy compliance problems.

  \item A dependency-tracking mechanism that tracks derivation
    structure can provide a concise explanation for a result.  This is
    essential for confirming that a policy is correctly modeled.  It
    can also help identify situations where a policy is having
    unanticipated or undesirable consequences.

  \item A dependency-tracking mechanism that supports hypothetical
    premises can simplify analysis and design of policies.  It can be
    used to test the response of a policy to a hypothetical situation.
    Or it can be used to construct an argument based on a supposed but
    as-yet unsupported belief.

\end{itemize}

We have chosen to use a TMS as the dependency-tracking mechanism for
our project.  The TMS provides considerable power in a very simple
mechanism; its primary cost is the memory required to record the
structure of a derivation.  Although the TMS technology was invented
in the 1970s, it is not well known outside the artificial intelligence
community, and consequently there are no uses of this technology in
policy systems of which we are aware.

One possible complaint about dependency tracking is that its use might
clutter the description of a policy, obscuring its meaning.  In
practice, this is not usually a problem since most of the information
needed to support dependency tracking can be inferred from the policy
description.  To see how this is done, we first need to define some
terms.

Our reasoner is a kind of \emph{production-rule system} in which the
\emph{condition} of a rule is a pattern to be matched against a set of
believed statements.  When the pattern matches, the rule's
\emph{action} is performed.  Typically the action asserts new beliefs,
causing them to be added to the set.

When something is added to the belief set, it is associated with a
\emph{justification} for its belief.  In the case of a simple
statement of fact, there is a trivial justification that the statement
is an assumption.  A derived statement has a justification based on
the inputs used to make the derivation.

In such a simple rule system, all of the dependency information is
implied by the rules themselves.  If a new belief is asserted by a rule's
action, then its justification is the set of statements that matched
the rule's pattern.  More precisely, we believe the asserted statement
if and only if we believe every one of the matched statements.
Additionally, the justification records an identifier for the rule;
this identifier together with the matched statements provide all the
relevant information about the particular deduction step just
performed.  Typically these deduction steps build on one another,
resulting in a tree-like justification structure for any given belief,
in which the belief is the trunk of the tree and the assumptions are
the leaves.  This tree structure is a complete explanation of the
support for the belief.

Our reasoner is not quite so simple.  It has additional features, such
as goal direction, for which the correct dependency structure is not
always inferrible from the rule.  To handle such situations, we
provide a means to write explicit justifications.  In practice, this
is used only occasionally, and has little impact on the overall
readability of a policy description.

Finally, one problem with this dependency-tracking mechanism is that
it can record \emph{too much} information.  It has no way to
distinguish between deductions that are interesting and that should
appear as part of an explanation, and those that should be omitted.
For example, suppose the statement ``Bob has a sister named Alice'' is
believed and that some rule has a pattern ``?X has a brother named
?Y''.  A rule can be written to deduce ``Alice has a brother named
Bob'' so the pattern can match, but that deduction step won't be very
interesting for most end users.

Our system provides a simple means for policy authors to elide
uninteresting deduction steps from explanations.  When writing a rule
that makes such a deduction step, the author declares it as
\emph{hidden}, and any deduction made by that rule will not appear in
the resulting explanation.  This distinction is under the control of
the policy author, so the consequent hiding can be tailored to the
users in the policy domain.

Let's reconsider our example to see how this works.  Assign the
following names:

\begin{itemize}
  \item{\(A\):} ``Bob has a sister named Alice''
  \item{\(B\):} ``Alice has a brother named Bob''
  \item{\(R_1\):} rule with pattern ``?X has a brother named ?Y''
  \item{\(R_2\):} rule that deduces \(B\) from \(A\)
\end{itemize}

In the absence of any hiding, the result of rule \(R_1\) will be shown
as derived from \(B\), and \(B\) in turn will be shown as derived from
\(A\) via \(R_2\).  However, if \(R_2\) is marked \emph{hidden}, then
the result of rule \(R_1\) will be shown as derived directly from
\(A\), while \(B\) won't be shown at all.  A person reading the
explanation will see that \(R_1\) was triggered by \(A\), which is
semantically obvious even though syntactically incorrect.

\subsection{AIR policy language}
\label{air}

AIR ({\bf A}ccountability {\bf I}n {\bf R}DF) is a policy language
that exploits our dependency tracking approach. The policies are
represented in Turtle \cite{beckett04turtle}, which is a human
readable syntax for RDF\@.  AIR constructs allow policy writers to
explicitly control how the reasoning happens by invoking rules
according to pattern matches and are based on AMORD constructs
\cite{kleer77amord}.  AMORD is a production-rule system that features
pattern matching, dependency tracking, nesting of rules, and goal
direction.  The combination of these features provides expressive
power (pattern matching and rule nesting), efficient execution (goal
direction), and integrated explanations (dependency tracking).

AIR consists of an ontology and a reasoner, which when given a set of
policies and data in Turtle, attempts to compute compliance of the
data with respect to the policies.  Each computed compliance result
has an associated explanation outlining the derivation of the result
from the inputs.

The AIR ontology comprises several classes and properties that are
used to define rule-based policies. Please refer to Figure
\ref{fig-air-ont} for an overview of the AIR classes, properties, and
their relationships.

\begin{figure}[tb]
  \centerline{\epsfig{file=images/air-ont.pdf, height=4in}}
  \caption{AIR ontology}
  \label{fig-air-ont}
\end{figure}

There are two top-level classes in AIR:
\airname{Abstract\dash{}action} and
\airname{Abstract\dash{}container}.  \airname{Policy} is a
subclass of \airname{Abstract\dash{}container}.  The
\airname{Abstract\dash{}container} class has properties for
defining variables, belief rules, goal rules, belief assertions, and
goal assertions that \airname{Policy} inherits.  Variables are scoped
to the container they appear in.  For example, in the following
declaration the scope of variable \lqname{REQ} is within
\lqname{DIGPolicy} and the rules it contains including \lqname{rule1}
and \lqname{rule2}.  The scope of variable \lqname{MEMBER} declared in
\lqname{rule1} is \lqname{rule1} and the scope of variable
\lqname{MEMBER} and \lqname{FOAF-REQ} declared in \lqname{rule2} is
\lqname{rule2}.  If \lqname{REQ} is bound before \lqname{rule1} or
\lqname{rule2} are invoked then it is passed as a value and not as a
variable.  (Variables do not have to be uppercase.)

\begin{verbatim}
:DIGPolicy a air:Policy;
   air:variable :REQ, :REQUESTER,
           :RESOURCE, :MEMBERLIST;
   air:rule :rule1, :rule2.

:rule1 a air:Belief-rule;
   air:variable :MEMBER.

:rule2 a air:Belief-rule;
   air:variable :MEMBER, :FOAF-REQ.
\end{verbatim}

An \airname{Abstract\dash{}rule} is a subclass of both
\airname{Abstract\dash{}container} and
\airname{Abstract\dash{}action} and its subclasses are
\airname{Goal\dash{}rule} and
\airname{Belief\dash{}rule}.  Instances of
\airname{Goal\dash{}rule} match statements that are asserted as
goals, and are used sparingly in typical applications.  The
\airname{rule} property applies to all
\airname{Abstract\dash{}containers} and is used to attach rules
to policies as shown in the example above.

A rule consists of a pattern, a matched-graph variable, a
justification, a label, and zero or more actions.  The matched-graph
variable, justification, and label are optional.  Omitting the
matched-graph variable means there's no direct reference for the
matched graph, which often isn't needed.  Omitting the justification
means a default justification is used, also the usual case.  For
example, the following belief rule declares a variable and has a
label and a pattern.

\begin{verbatim}
:rule1 a air:Belief-Rule;
   air:variable :MEMBER;
   air:label "Member access";
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
     :MEMBER a foaf:Person;
     foaf:openid :REQUESTER.
   }.
\end{verbatim}

Belief rules implement forward-chaining deduction, while goal rules
provide a means to limit the application of rules (and consequently
the amount of computation performed).  In the following example, a
belief rule \lqname{ruleB} has a nested goal rule \texttt{r1} that
controls the introduction of sub-class type inference. The outer rule
fires whenever a sub-class relationship is believed, causing
\texttt{r1} to be enabled.  \texttt{R1} is applied when there is a
goal to show that some resource is a member of the class \lqname{V2},
enabling the belief rule \texttt{r2}.  \texttt{R2} implements the
implication "if a resource is a member of a subclass \lqname{V3}, it's
also a member of the containing class \lqname{V2}".

\begin{verbatim}
:ruleB a air:Belief-rule;
   air:variable :V1, :V2, :V3, :V4;
   air:label "sub-class implication";
   air:pattern {
      :V3 rdfs:subClassOf :V2.
   };
   air:goal-rule [       # sub-rule r1
      air:pattern { :V1 a :V2. };
      air:rule [         # sub-rule r2
         air:pattern { :V1 a :V3. };
         air:assert { :V1 a :V2. };
      ];
   ].
\end{verbatim}

The purpose of the goal rule r1 is to limit the deductions made by the
system. If \lqname{ruleB} were rewritten as a belief rule, as below, it would
make all possible deductions of this kind, whether they were needed or
not. The use of a goal rule instead limits the deductions to those
actually asked for (specified as goals) rather than for every possible
deduction.

\begin{verbatim}
:ruleB a air:Belief-rule;
   air:variable :V1, :V2, :V3;
   air:label "sub-class implication";
   air:pattern {
      :V3 rdfs:subClassOf :V2.
      :V1 a :V3.
   };
   air:assert { :V1 a :V2. }.
\end{verbatim}

The action of a rule consists of a set of assertions and sub-rules.  A
sub-rule appearing in the action of a containing rule is initially
\emph{inactive}, meaning it is not eligible for matching.  When the
containing rule's pattern matches and its action is performed, the
sub-rule becomes \emph{active} and its pattern will be matched as
needed.

\begin{verbatim}
:SomePolicy a air:Policy;
  air:rule [
    air:label "containing rule";
    air:pattern { ... };
    air:rule [
      air:label "sub-rule";
      air:pattern  { ... };
      air:assert { ... };
      air:rule [
        air:label "sub-sub-rule";
        air:pattern { ... };
        air:assert { ... }
      ]
    ]
  ] .
\end{verbatim}

An assertion appearing in the action of a rule can be either a belief
or a goal. If it is a belief, the asserted
statement can be matched against belief rules and if it is a goal
the asserted statement can be matched against goal rules.  In
the following example, a belief assertion is associated with
\lqname{rule2}, so when the rule's pattern matches, the statement is asserted
as a belief.  Variables \lqname{MEMBERLIST}, \lqname{REQUESTER}, and
\lqname{DIG} are bound before the rule is invoked.

\begin{verbatim}
:rule2 a air:Belief-rule;
   air:variable :MEMBER;
   air:label "Member access";
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
     :MEMBER a foaf:Person;
       foaf:openid :REQUESTER.
   };
   air:assert {
     :MEMBER foaf:member :DIG
   } .
\end{verbatim}

AIR provides a small library that implements some simple
RDFS \cite{rdfs} and OWL \cite{owl} deduction rules.
For example, if a relation \(R\) is declared to be transitive,
and the belief set contains \(xRy\) and \(yRz\), the library
can deduce \(xRz\).  The library provides a number of generally
useful deductions, and will be augmented with new rules as the need
arises.
  
The properties dealing with policy compliance are
\airname{compliant\dash{}with} and
\airname{non\dash{}compliant\dash{}with}; they specify
that the subject is or is not compliant with the object policy.  For
example, the following policy has a single rule, which when matched
asserts that the request is compliant with the policy.

\begin{verbatim}
:rule6 a air:Belief-Rule;
   air:variable :MEMBER, :FOAF-REQ;
   air:label "Member referral access";
   air:pattern {
     :MEMBER air:in :MEMBERLIST.
     :MEMBER foaf:knows :FOAF-REQ.
     :FOAF-REQ foaf:openid :REQUESTER.
   };
   air:assert {
     :REQ air:compliant-with :DIGPolicy
   } .
\end{verbatim}
}

\section{RETE AIR Reasoner}
In needing to build a reasoner, several design decisions were
started with. First, I was going to write in Python \cite{python}. 
This is the language that I have experience programming in,
and whose libraries I know. Python has its own tradeoffs, 
which we will deal with in section \ref{python:tradoffs}

An RDF library was needed, and Cwm was chosen. The reason
for this was trivial; as Cwm's maintainer, I know that code and
can modify it to suit my needs. Much of the functionality needed
had been written or improved by me.

The first step of my work was to write a TMS. The TMS was based
on a \verb|tms.scm| written in scheme by Chris Hanson. Cwm was 
modified to use this TMS as the basis of the working store of things
it currently believes.

The rule engine I wrote is an implementation of RETE-UL \cite{reteul},
an advance of the original RETE algorithm by Forgy \cite{forgy82} by Robert Doorenbos. 
Work was done to adapt the algorithm into Cwm. 

The Cwm RDF store keeps eight indexes. These indexes correspond precisely
to the alpha nodes of a RETE network. The basic idea was to do just that;
make the existing indexes into alpha nodes. 

What quickly became clear was that these alpha nodes did not do enough
tests to be true alpha nodes. In particular, an alpha node must do all intra
statement tests, but the indexes had no way to test variable correctness. In 
particular, the patterns like \verb|?x :p ?x| must be handled correctly.

The solution was to split the alpha nodes into two. The initial indexes send
their data to alpha filters, which figure out the variable bindings and ensure
intra-statement correctness. These used the already existing unification
routines in Cwm.

In order to handle variables in facts, which must happen, variable renaming
had to be implemented. 

\label{rete-algorithm}
The beta network then simply tests for variable consistency, and passes
on the consistent ones. In following \cite{reteul}, there is a root node 
that is the start of every merge. It has as a child some number of 
merge nodes. Each merge node has a left parent, which is a beta node,
and a right parent, an alpha filter. When something is added to an
alpha filter, it call a corresponding method on all merge nodes
that are its children. Similarly, when something is added to
a beta node, it calls a corresponding method on all merge nodes
that are its children. When poked from one side, the merge node
searches through everything on the other side, and passes on to
its child beta node all consistent matches. 

The alternative was to have the 
top beta node have two alpha nodes as parents. The alternative, however,
does not handle zero- or one- triple patterns well, and is simply less
consistent. Also in following \cite{reteul}, the beta nodes were split
into beta memories, which store partial matches and have one parent,
and join nodes that have two parents and no memory.

When a join node queries its parents, it would be
possible to use heavy indexing on variable
bindings to reduce the cost of the search.
Pychinko \cite{pychinko} does this. The policy reasoner does not
do this. By a simple indirection in the API between nodes,
the API already supports this, if adding it in the future were found to be helpful. This is done by insuring
that instead of searching through the alpha filter directly, it calls
the \verb|AlphaFilter.getPossibles(bindings)| methods to get a
superset of matches consistent with the bindings. Note that the current
implementation simply returns the alpha filter itself --- it does nothing
with the information. Further, if this method was fully implemented,
the join nodes' test would be redundant. 

At the bottom of the beta node tree are production nodes. A production node has a single parent a beta node. A production node is handed a function to call on success, and a function to call on failure. In this way, the matcher knows nothing about what happens when the rule fires.

The structure \ref{retediag} shows one matcher built this way. The pattern is
\begin{verbatim}
?x a :Bar. ?y a :Bar .
?x :g :h . ?x :frob ?y
\end{verbatim}
 This pattern has four triples, so it will be a chain of four join nodes. These are on the left. Between the join nodes are beta memories, which store partial matches. It is the job of the join nodes to only pass on consistent partial matches.
 
 \begin{figure}[tb]
  \centerline{\epsfig{file=images/rete.pdf, height=4in}}
  \caption{Rete Structure for a single pattern}
  \label{retediag}
\end{figure}


Every join node, we see, has two parents. The left parent is a beta memory, or the single root node, which acts as a beta memory. The right parent is an alpha filter. There is therefore one alpha filter per triple in the pattern. 

The alpha filters get their data from the primary alpha nodes in the index of the formula. Actually, the diagram is a simplification. In the presence of variables in the facts, each alpha filter pulls data from up to eight alpha nodes, corresponding to variables in various positions in the fact. Nonetheless, we note that one primary alpha may be feeding multiple alpha filters, as both \verb|?x a :Bar.| and \verb|?y a :Bar.| have the same pattern to the index. 

To see how this works, let us say that the TMS supports the statement \verb|:ThreeChimneys a :Bar.|. This matches the alpha node \verb|(_ a :Bar)|. and is added. At that point, it is sent to the \verb|?x a :Bar.| and \verb|?y a :Bar.| alpha filters. It is consistent with both, generating the bindings \verb|{?x: ThreeChimneys}| and \verb|{?y: ThreeChimneys}| respectively. 

The \verb|?x| binding passes through, reaching its join node. That node merges the match with the empty one, passing it through to the beta memory. The beta memory passes it through to the next join node. This is now tested for consistency with the all of the statements in the next alpha filter. Because they have no variables in common, everything passes through to the next beta memory. In the meantime, the \verb|?y| binding is passed through its alpha filter. It is tested for consistency at the join node with everything in the beta memory, and for the same reason, every combination is passed through. 

All of those matches are then sent to the next join node. There, the bindings are tested for consistency with \verb|?x :g :h|. Essentially, if there is a statement \verb|:ThreeChimneys :g :h|, it is at this point passed through. 

To finish the example, if anything ever adds the last beta memory, it sends whatever it had straight through to the production node. The production node then notes it is nonempty, and calls the function it was given.

As notes already, CWM support built-in predicates for RDF. To
support this in a RETE, the alpha nodes must know they are built-ins
and return the appropriate matches. Nonetheless, for a RETE, several
difficulties present themselves. 

The first difficulty is one of location. Built-in predicates typically require that either the
subject, object, or both be already bound. These therefore must be placed low enough
in the RETE chain to insure this true. There are some built-ins, like \verb|math:inverse|
that given one of the subject and object, will return the other. Figuring out the correct
in the presence of these is non-trivial. 

The second problem is one of dynamically bound predicates. If the predicate of a pattern is a variable, it is possible that it will be bound to a built-in predicate. This is
easy enough to account for, but introduces another layer of complications in any
case.

Both other these problems with built-in predicates are in fact special cases of the \emph{ordering problem}. Given a pattern with multiple statements to match, what order should be used to try to match them? The general rule is to try to fail as quickly as possible, that things which will match the least should be used. This requires dynamic ordering, to order the match on the fly as matching.

On the other hand, a RETE has a fixed structure, which determines the match order. At the time the rule is built, the order of the beta nodes, and thus the order of the match, is predetermined.

\section{TREAT AIR Reasoner}
There are several ways that RETE is faster than a na\"\i{}ve matching algorithm. The first is the separation of alpha nodes and beta nodes, so a pattern is only matched against statements that could match it. The second is when a new statement is added, it is automatically matched against a statement in the pattern, with the match starting from there. Depending on where in the chain the statement is added, anything from no further work to the entire rest of the match may be added. It is in the hope that the added statement will be near the bottom that the structure of the RETE is maintained. Even in the worst case, however, this is better than a na\"\i{}ve matcher, which would rerun the entire search for things to match to the pattern once a single statement is added. 

Depending on the difficulty of a match, dynamic ordering can decrease the work of a pattern match by a great deal. It is argued in \cite{treat} that the cost of not being able to dynamically match in RETE is in fact greater than the savings from partial matches when new statements are added near the bottom. 

As an alternative, they present the TREAT algorithm. The alpha nodes remain as they were. However, instead of connecting to a chain of beta nodes, the alpha nodes are all connected to a single structure representing the match. This is as in \ref{treatdiag}. Any time an alpha filter adds something, it pokes all child match structures. These search all other parent alpha filters for a match consistent with the new statement, and pass it on. 

 \begin{figure}[tb]
  \centerline{\epsfig{file=images/treat.pdf, height=4in}}
  \caption{TREAT Structure for a single pattern}
  \label{treatdiag}
\end{figure}


The advantage of having this simplified structure is flexibility. While the property remains that each statement for each line of the pattern is only matched against the possibilities for the other statements once, nothing else in forced about the process. Therefore, a dynamic order to greedily try to minimize the search space is used. This greedy ordering is found to have good properties is practice \cite{owl-match}. 

\section{TMS}
Whichever way the match happens, it calls a function given to it with two arguments. The first argument is the list of statements that were matched against. The second argument is the bindings generated. In this way, the matcher has no dependencies on any other part of the reasoner. 

The function called is a method of the rule object. When called, it puts a thunk into the FIFO of things to do and returns. The thunk (a function called with no arguments) computes any assertions or subrules now supported by the firing of the rule, and adds those supports into the TMS.

We note that, in fact, so long as it was consistent with the rule we could add matches that contained unsupported statements into the TMS as well. The net result would be that the conclusion would also not be believed. The matcher is therefore simply insuring that the TMS contains what is necessary to support every true statement.

If everything worked, then the new assertion is supported. At that point, a function given to the TMS on its creation is called. This function, if given a rule node, builds the match structure for the rule. If given a statement, it adds the statement to the index for the matcher. This was, the matcher can run. The process is as in \ref{rulefire}

 \begin{figure}[tb]
  \centerline{\epsfig{file=images/rulefire.pdf, height=4in}}
  \caption{How a rule fires after a successful match}
  \label{rulefire}
\end{figure}

Goal direction adds a bit of complication to this process. Goal statements can be supported in the TMS just like regular statements. Typically, a goal statement is supported simply by existence of a rule. The goals are indexed separately. Therefore, a goal rule matches against a different index. This index must include both goal statements and fact statements. 


\section{Proof Generation}
The TMS is a graph structure. It contains multiple nodes for things that in presentation go together, and single nodes that should probably never be printed. It contains supports for things the user likely has no interest, and possibly support loops. It has large support structures for things that are not actually supported. Therefore, effort must be taken to print out a version of the TMS that is more viewable.

The transformation is done in stages. The first stage starts with the things we want to prove, the compliance statements, and recursively makes a table of the statements used to support them. When this is done, we have a representation of the subset of the TMS needed to prove what we want. We can then transform this to make the correct output.

The first of the transformations is to remove nodes that are truly redundant. A set of statements supports all statements inside of it, and is supported by all statements inside of it. Both of these facts are not necessary.

The second transformation is more involved. If a rule was marked as being a base rule, then it should not appear in the output. This transformation cannot always be applied, and subtle effects may result. 

Finally, the result is serialized as RDF. Multiple statements with the same reason are combined for brevity. 

\section{Performance}
AIR is designed to do work computing goals to avoid work computing facts.

The control structures in AIR can only do so much, however. Let us look at the behavior of the AIR reasoner on the ARL2 scenario file. The log is at \url{http://dig.csail.mit.edu/2008/ARL/log.n3}, and the policy is at \url{http://dig.csail.mit.edu/2008/ARL/udhr-policy.n3}. These are reproduced in Appendix \ref{arl2-scenario}. %%%@@@ really
The rules at  \uri{http://dig.csail.mit.edu/TAMI/2007/amord/base-rules.ttl} in appendix \ref{base-rules} are also run. These rules are trying to compute equality and RDF relations. They are very carefully written. 

I also created a version that does not have any goal rules or nested rules. Any goal processing by the reasoner is wasted. It is up to the reasoner to order things. We then have figure \ref{performance-air}

\begin{table}[tb]
\label{performance-air}
\caption{The time and things generated for ARL1 and Prox card  policies on sample data.}
{\small \input{goals_times} }
\end{table}

 \begin{figure}
  \centerline{\epsfig{file=images/goals_times.pdf, height=4in}}
  \caption{The things generated for ARL1 and Prox card  policies on sample data.}
  \label{performance-air-count-diag}
\end{figure}

For the ARL1 example, running the reasoner creates 60 goal rules, 310 rules, and 75 goals. This is in order to generate 51 facts, of which we are interested in less than ten. As noted in \cite{tmsbook}, we have used goals to gain some control of the generation of facts, but we don't have the same control over the generation of goals. The manipulation of goals to avoid creating facts seems to instead cause the creation of a great many rules.  In this case, there were a small enough number of facts that this hurt. By loading all ontologies for the files, we add many facts, all of which end up unnecessary. The goal manipulation here works, saving work. Still, it does not prevent hundreds of facts and rules being generated.

We note that with these rules TREAT actually outperforms RETE with enough facts. 


%% Running the reasoner creates 60 goal rules, 310 rules, and 75 goals. This is in order to generate 51 facts, of which we are interested in less than ten. As noted in \cite{tmsbook}, we have used goals to gain some control of the generation of facts, but we don't have the same control over the generation of goals. The manipulation of goals to avoid creating facts seems to instead cause the creation of a great many rules. At this point, it is important to look carefully at the scaling factors of the reasoner to figure out if goals or facts are more important. The RETE-UL algorithm which is implemented based of \cite{reteul} is designed to be able to handle cases with large numbers of rules very well.


\section{The Choice of Python}
\label{python:tradoffs}
The Python\cite{python} programming language is a dynamic typed language with everything being an object. The main implementation of Python is written in C, and a very high level virtual machine. Python's use of indentation to delineate blocks helps force code readability. Python has a good built in library, and is in general very pleasant to program in.

The implementation of Python has some performance limitations, however. There is a very large performance penalty for interpretation. Equivalent code in C might run 1000 times faster in some instances than Python. Multithreading was added on later, with the result that there is a Global Interpreter Lock (GIL) to protect the data structures of the interpreter. This insures that a single python process cannot run on multiple processors. This can be mitigated by running multiple interpreters, one per process, and using some IPC mechanism. 


\comment{
\section{Contributions}
\label{contributions}

Perhaps the most important aspect of this work is the assumptions
underlying its design.  First, that the complexity of modern data
systems, as typified by the web, requires the ability to do effective
reasoning in the presence of \emph{both} incompleteness and
inconsistency---and, as if that wasn't enough, to scale over many
orders of magnitude.  And second, that the widespread dissemination of
information is making access control decreasingly effective, requiring
the development of new complementary strategies.

Even so, our system brings some significant technical strengths to the
policy domain:

\begin{itemize}

\item{Explanations}

AIR is able to produce a concise explanation for \emph{any} result it
computes.  It is hard to overstate the importance of explanations: in
many cases, the explanation for a result is more important than the
result itself.  For example, to someone being arrested by a police
officer, an explanation is likely to be very important.  And later, a
detailed justification for the arrest may be crucial.

Good explanations are just one consequence of AIR's
dependency-tracking mechanism.  And because dependency tracking is
integrated into the language, it has little or no effect on the form
or expression of policies.

\item{Improved reasoning efficiency}

Conventional forward-chaining production rule systems suffer poor
efficiency and scalability.  AIR's goal direction mechanism provides
significantly better performance by restricting rules to make
deductions that support a specific goal, rather than making every
possible deduction over a set of beliefs.

This can make a huge difference in performance.  For example, consider
trying to determine whether objects \(a\) and \(b\) are related by a
transitive relation \(R\).  A conventional rule system answers this
question by computing the transitive closure of \(R\), which can
require deducing \(n^2\) statements from \(n\) initial references to
\(R\).  However, in AIR one can specify \(aRb\) as a goal, and the
appropriate goal rule then tries to deduce this statement, which at
most requires computing those parts of \(R\) that lie between \(a\)
and \(b\).  Typically this computation doesn't depend on the size of
\(R\), but only on the distance between \(a\) and \(b\), so in
addition to doing less work, it scales much better.




\end{itemize}


\section{Related Work}
\label{related-work}

As explanations are usually in the form of proof trees, which might be
incomprehensible to end users, we have developed a graphical
justification user interface in Tabulator \cite{berners06tabulator}, a
Semantic Web browser. This allows users to view the explanation
provided by the reasoner in different ways: (i) in a simple rule
language, N3 \cite{berners08n3}, and (ii) in a graphical layout that
highlights the result of the reasoning and allows the explanation to
be explored.  Please refer to Figure \ref{fig-ui} for a screen shot of
the explanation provided for the DIG policy scenario for a request
made by \textit{Alice}, a friend of one of DIG members for a protected
resource, \textit{http://dig.csail.mit.edu/proposal/nsf.tex}. The
different buttons {\bf Because} and {\bf Justify} provide a way for
the user to step through the proof starting from the most relevant
information (in this case facts that Alice is a friend of RRS who is a
member of the DIG group) and working backwards. We are still working
on improving the user interface to make it more intuitive to users.



The explanation framework in \cite{bonatti06advanced} provides natural
language explanations for questions about policy decisions including
explanations for failed results. The explanation generation process is
separate from the regular query process and uses abductive reasoning,
a method of inferring which hypothesis best explains the facts, to
obtain a proof. Parts of the proof language in the proof are then
substituted with natural language structures. Abductive reasoning is
known to produce incorrect results and as the proof generation process
is different from the query process it could infer an explanation that
is different from that inferred by the query process. Another problem
is that the explanation for failed policy results (e.g. why-not) ends
up being the list of all rules that the user did not match. This means
that the user has to sort through a lot of potentially irrelevant
information and the disclosure of these additional policy rules could
also be a privacy risk. In our approach, the proof generation happens
along with the inference and is not a separate process. We track the
rules and statements that were actually used to infer the statement
(policy decision). Also, by explicitly handling failed results or
unmatched cases using the \airname{alt} construct, it is possible to
provide explanations for failed (or incompliant) policy decisions
without revealing all unmatched rules.

Our proofs could be easily converted to generic proof representation
formats such as PML for display and analysis. PML is a general proof
language or "proof interlingua" that is used to describe proof steps
generated by different kinds of reasoning engines. Once written in PML
a user could Inference Web (IW) is a framework for displaying and
manipulating proofs defined in Proof Markup Language (PML)
\cite{mcguinness04iw}.  IW concentrates on displaying proofs whereas
our approach is mainly about generating these proofs.
}
\comment{Inference Web (IW) is a framework for displaying and
  manipulating proofs defined in Proof Markup Language (PML)
  \cite{mcguinness04iw}.  PML is a general proof language or ``proof
  interlingua'' that is used to describe proof steps generated by
  different kinds of reasoning engines. IW concentrates on displaying
  proofs whereas our approach is mainly about generating these
  proofs. Our proofs could be easily converted to PML so that we can
  use the IW set of tools.


Both WhyNot \cite{chalupsky02whynot} and the Know system
\cite{kapadia04know} focus explicitly on failed queries and try to
suggest changes to the knowledge base that will cause these queries to
succeed.  Our justification approach is more general and allows
failures to be captured in policies so explanations can be provided
for both successful and failed policy decisions.

}
\comment{\section{Conclusion and Future Work}
\label{future-work}

Having prototyped a number of different scenarios with AIR, we believe
that the language is expressive enough to support policy compliance in
a variety of environments. In the future, we plan to address the
engineering challenges of scalable, efficient reasoning over large,
distributed knowledge bases. We also see a number of UI and
HCI-related research challenges to be met including a higher-level
representation of the language to make authoring easier and UI designs
to help with rules authoring and presentation of dependency
relationships.  One of the benefits of the Semantic Web is the open
world assumption. Through our prototypes we have learned that some
subcultures, such as reasoning for legal adjudication, require the
ability to check when a certain premise does not exist, which is
impossible under open world semantics.  In future work, we will look
at mechanisms for creating closed world structures to derive
conclusions for discrete issues in those environments. Finally, we
will integrate policy aware capabilities into Semantic Web data
browsers.
}
