Integrating Logic Rules with Everything Else, Seamlessly

Integrated semantics, ensuring declarative semantics of rules.   In our overall language, the meaning of a rule set $\it rs$ is completely declarative, exactly following the standard least fixed-point semantics of rules [16, 38]:

• Given values of any set $\it s$ of base predicates in $\it rs$, the meaning of $\it rs$ is, for all derived predicates in $\it rs$ that fully depend on $\it s$, the least set of values that can be inferred, directly or indirectly, by using the given values and the rules in $\it rs$;

  for any derived predicate in $\it rs$ that does not fully depend on $\it s$, i.e., depends on any base predicate whose values are not given, its value is

  Definition 8.

  undefined.

  The operational semantics for the rest of the language ensures this declarative semantics of rules. The precise constructs for using rules with sets, functions, updates, and objects are described in Sections 2.3–2.6.

  2.3 Predicates as set-valued variables

  For rules to be easily used with everything else, our most basic principle in designing the language is to treat a predicate as a set-valued variable that holds the set of tuples that are true for the predicate, that is:

  • For any predicate $\it p$ over values $\it x_{1}$,$\it...$,$\it x_{a}$, assertion $\it p$($\it x_{1}$,$\it...$,$\it x_{a}$) is true—i.e., $\it p$($\it x_{1}$,$\it...$,$\it x_{a}$) is a fact—if and only if tuple ($\it x_{1}$,$\it...$,$\it x_{a}$) is in set $\it p$. Formally,

    $\vskip-4.30554pt\mbox{\footnotesize\tt\mbox{$\it p$}(\mbox{$\it x_{1}$},\mbox{$\it...$},\mbox{$\it x_{a}$})}~\Longleftrightarrow~\mbox{\footnotesize\tt(\mbox{$\it x_{1}$},\mbox{$\it...$},\mbox{$\it x_{a}$}) {\color[rgb]{0,0,1}in} \mbox{$\it p$}}$

  This means that, as variables, predicates in a rule set can be introduced in any scope—as global variables, object fields, or variables local to the rule set—and they can be written into and read from without needing any extra interface.

  Example 2.4.

  In rule set trans_rs in Figure 1, predicate edge is exactly a variable holding a set of pairs, such that edge($x$,$y$) is true iff ($x$,$y$) is in edge, and edge is local to trans_rs. In general, edge can be a global variable, an object field, or a local variable of trans_rs. Similarly for predicate path.

  Writing to predicates is discussed later under updates to predicates, but reading and using values of predicates can simply use all operations on sets. We use set expressions including the following:

  $\it exp$ in $\it sexp$	membership
  $\it exp$ not in $\it sexp$	negated membership
  $\it sexp_{1}$ + $\it sexp_{2}$	union
  {$\it exp$: $\it v_{1}$ in $\it sexp_{1}$,$\it...$,$\it v_{k}$ in $\it sexp_{k}$ | $\it bexp$}	comprehension
  $\it agg$ $\it sexp$,    where $\it agg$ is count, max, min, sum	aggregation
  some $\it v_{1}$ in $\it sexp_{1}$,$\it...$,$\it v_{k}$ in $\it sexp_{k}$ | $\it bexp$	existential quantification

  A comprehension returns the set of values of $\it exp$ for all combinations of values of variables that satisfy all membership clauses $\it v_{i}$ in $\it sexp_{i}$ and condition $\it bexp$. An aggregation returns the count, max, etc. of the set value of $\it sexp$. An existential quantification returns true iff for some combination of values of variables that satisfies all $\it v_{i}$ in $\it sexp$ clauses, condition $\it bexp$ holds. When an existential quantification returns true, variables $\it v_{1}$,…,$\it v_{k}$ are bound to a witness. Note that these set queries, as in [42], are more powerful than those in Python.

  Example 2.5.

  For computing the transitive closure T of a set E of edges, the following while loop with quantification can be used (we will see that we use objects and updates as in Python except for the syntax := for assignment in this paper):

  ⬇

  T := E.copy()

  while some (x,z) in T, (z,y) in E | (x,y) not in T:

  T.add((x,y))

  In the comprehension and aggregation forms, each $\it v_{i}$ can also be a tuple pattern that elements of the set value of $\it sexp_{i}$ must match [42]. A

  Definition 9.

  tuple pattern is a tuple in which each component is a non-variable expression, a variable possibly prefixed with =, a wildcard _, or recursively a tuple pattern. For a value to match a tuple pattern, it must have the corresponding tuple structure, with corresponding components equal the values of non-variable expressions and variables prefixed with =, and with corresponding components assigned to variables not prefixed with =; multiple occurrences of a variable must be assigned the same value; corresponding components of wildcard are ignored.

  Example 2.6.

  To return the set of second component of pairs in path whose first component equals the value of variable x, and where that second component is also the first component of pairs in edge whose second component is 1, one may use a set comprehension with tuple patterns:

  ⬇

  {y: (=x,y) in path, (y,1) in edge}

  Now that predicates in rules correspond to set-valued variables, instead of functions or procedures, we can further see that logic variables, i.e., variables in arguments of predicates in rules, are like pattern variables, i.e., variables not prefixed with = in patterns. These variables are used for relating values, through what is generally called unification; they do not hold values, unlike variables prefixed with = in patterns.

  2.4 Queries as calls to an inference function

  For inference and queries using rules, calls to a built-in inference function infer, of the following form, are used, with $\it query_{k}$’s and $\it p_{k}$=$\it sexp_{k}$’s being optional:

    infer($\it query_{1}$, $\it...$, $\it query_{j}$, $\it p_{1}$=$\it sexp_{1}$, $\it...$, $\it p_{i}$=$\it sexp_{i}$, rules=$\it rs$)
  

  $\it rs$ is the name of a rule set. Each $\it sexp_{k}$ is a set-valued expression. Each $\it p_{k}$ is a base predicate of $\it rs$ and is local to $\it rs$. Each $\it query_{k}$ is of the form $\it p$($\it arg_{1}$,$\it...$,$\it arg_{a}$), where $\it p$ is a derived predicate of $\it rs$, and each argument $\it arg_{k}$ is a constant, a variable possibly prefixed with =, or wildcard _. A variable prefixed with = indicates a bound variable whose value will be used as a constant when evaluating the query. So arguments of queries are patterns too. If all $\it arg_{k}$’s are _, the abbreviated form $\it p$ can be used.

  Function infer can be called implicitly by the language implementation or explicitly by the user. It is called automatically as needed and can be called explicitly when desired.

  Example 2.7.

  For inference using rule set trans_rs in Figure 1, where edge and path are local variables, infer can be called in many ways, including:

  ⬇

  infer(path, edge=RH, rules=trans_rs)

  infer(path(_,_), edge=RH, rules=trans_rs)

  infer(path(1,_), path(_,=R), edge=RH, rules=trans_rs)

  The first is as in Figure 1 (line 19). The first two calls are equivalent: path and path(_,_) both query the set of pairs of vertices having a path from the first vertex to the second vertex, following edges given by the value of variable RH. In the third call, path(1,_) queries the set of vertices having a path from vertex 1, and path(_,=R) queries the set of vertices having a path to the vertex that is the value of variable R.

  If edge or path is a global variable or an object field, one may call infer on trans_rs without assigning to edge or querying path, respectively.

  The operational semantics of a call to infer is exactly like other function calls, except for the special forms of arguments and return values, and of course the inference function performed inside:

  1. 1)

     For each value $\it k$ from 1 to $\it i$, assign the set value of expression $\it sexp_{k}$ to predicate $\it p_{k}$ that is a base predicate of rule set $\it rs$.

  2. 2)

     Perform inference using the rules in $\it rs$ and the given values of base predicates of $\it rs$ following the declarative semantics, including assigning to derived predicates that are not local.

  3. 3)

     For each value $\it k$ from 1 to $\it j$, return the result of query $\it query_{k}$ as the $\it k$th component of the return value. The result of a query with $l$ distinct variables not prefixed with = is a set of tuples of $l$ components, one for each of the distinct variables in their order of first occurrence in the query.

  Note that when there are no $\it p_{k}$=$\it sexp_{k}$’s, only defined values of base predicates that are not local to $\it rs$ are used; and when there are no $\it query_{k}$’s, only values of derived predicates that are not local to $\it rs$ may be inferred and no value is returned. This is the case for implicit calls to infer on $\it rs$.

  2.5 Updates to predicates

  Values of base predicates can be updated directly as for other set-valued variables, and values of derived predicates are updated by the inference function.

  Base predicates of a rule set $\it rs$ that are local to $\it rs$ are assigned values at calls to infer on $\it rs$, as described earlier. Base predicates that are not local can be updated by assignment statements or set update operations. We use

    $\it lexp$ := $\it exp$
  

  for assignments, where $\it lexp$ can also be a nested tuple of variables, and each variable is assigned the corresponding component of the value of $\it exp$.

  Derived predicates of a rule set $\it rs$ can be updated only by calls to the inference function on $\it rs$. The updates must ensure the declarative semantics of $\it rs$:

  • Whenever a base predicate of $\it rs$ is updated in the program, the values of the derived predicates in $\it rs$ are maintained according to the declarative semantics of $\it rs$ by calling infer on $\it rs$.

    Updates to derived predicates of $\it rs$ outside $\it rs$ are not allowed, and any violation will be detected and reported at compile time if possible and at runtime otherwise.

  Simply put, updates to base predicates trigger updates to derived predicates, and other updates to derived predicates are not allowed. This ensures the invariants that the derived predicates hold the values defined by the rule set based on values of the base predicates, as required by the declarative semantics. Note that this is the most straightforward semantics, but the implementation can avoid many inefficiencies with optimizations.

  Example 2.8.

  Consider rule set trans_rs in Figure 1. If edge is not local, one may assign a set of pairs to edge:

  ⬇

  edge := {(1,8),(2,9),(1,2)}

  If edge is local, the calls to infer in the example in Section 2.4 assign the value of RH to edge.

  If path is not local, then a call infer(edge=RH, rules=trans_rs) updates path, contrasting the first two calls to infer in the example in Section 2.4 that return the value of path.

  If path is local, the return value of infer can be assigned to variables. For example, for the third call to infer in the example in Section 2.4, this can be

  ⬇

  from1,toR := infer(path(1,_), path(_,=R), edge=RH, rules=trans_rs)

  If both edge and path are not local, then whenever edge is updated, an implicit call infer(rules=trans_rs) is made automatically to update path.

  For the RBAC example in Figure 1, different ways of using rules are possible, including (1) allloc: adding a rule path(x,x) if role(x,x) to the rule set, adding role=ROLES in the call to infer, and removing the union in function transRH, so all predicates are local variables; (2) nonloc: as in allloc, except to replace predicates edge, role, and path with RH, ROLES, and a new field transRH, respectively, replace call transRH() with field transRH, and remove function transRH; (3) union: as in Figure 1; and other combinations of aspects of (1)–(3).

  2.6 Using predicates and rules with objects and classes

  Predicates and rule sets can be object fields as well as global and local names, just as sets and functions can, as discussed in Section 2.2. This allows predicates and rule sets to be used seamlessly with objects in object-oriented programming.

  For other constructs than those described above, we use those in high-level object-oriented languages. We mostly use Python syntax (looping, branching, indentation for scoping, ‘:’ for elaboration, ‘#’ for comments, etc.) for succinctness, but with a few conventions from Java (keyword new for object creation, keyword extends for subclassing, and omission of self, the equivalent of this in Java, when there is no ambiguity) for ease of reading.

  Example 2.9.

  We use Role-Based Access Control (RBAC) to show the need of using rules with all of sets, functions, updates, and objects and classes.

  RBAC is a security policy framework for controlling user access to resources based on roles and is widely used in large organizations. The ANSI standard for RBAC [3] was approved in 2004 after several rounds of public review [59, 25, 15], building on much research during the preceding decade and earlier. High-level executable specifications were developed for the entire RBAC standard [37], where all queries are declarative except for computing the transitive role-hierarchy relation in Hierarchical RBAC, which extends Core RBAC.

  Core RBAC defines functionalities relating users, roles, permissions, and sessions. It includes the sets and update and query functions in class CoreRBAC in Figure 1, as in [37].¹¹ 1 Only a few selected sets and functions are included, and with small changes to names and syntax.

  Hierarchical RBAC adds support for a role hierarchy, RH, and update and query functions extended for RH. It includes the update and query functions in class HierRBAC in Figure 1, as in [37],¹ except that function transRH() in [37] computes the transitive closure of RH plus reflexive role pairs for all roles in ROLES by using a complex and inefficient while loop much worse than that in Section 2.3 (due to Python’s lack of some with witness) plus a union with the set of reflexive role pairs {(r,r): r in ROLES}, whereas function transRH() in Figure 1 simply calls infer and unions the result with reflexive role pairs.

  Note though, in the RBAC standard, a relation transRH is used in place of transRH(), intending to maintain the transitive role hierarchy incrementally while RH and ROLES change. It is believed that this is done for efficiency, because the result of transRH() is used continually, while RH and ROLES change infrequently. However, the maintenance was done inappropriately [37, 31] and warranted the use of transRH() to ensure correctness before efficiency.

  Overall, the RBAC specification relies extensively on all of updates, sets, functions, and objects and classes with inheritance, besides rules: (1) updates for setting up and updating the state of the RBAC system, (2) sets and set expressions for holding the system state and expressing set queries exactly as specified in the RBAC standard, (3) methods and functions for defining and invoking update and query operations, and (4) objects and classes for capturing different components—CoreRBAC, HierRBAC, constraint RBAC, their further refinement, extensions, and combinations, totaling 9 components, corresponding to 9 classes, including 5 subclasses of HierRBAC [3, 37].

  3 Compilation

  We describe our compilation framework for implementing Alda, by building on an object-oriented language that supports all features except rules and queries and on an efficient logic rule engine for queries using rules. Three main tasks are (1) compiling rule sets to generate rules accepted by the rule engine, (2) compiling queries using rules to generate queries accepted by the rule engine, together with automatic conversion of data and query results, and (3) compiling updates to predicates that require implicit automatic queries and updates of the query results. The compiler must appropriately handle scoping of rule sets and predicates for all three tasks. Besides that, task (1) is straightforward, task (2) is also straightforward but tedious, and task (3) requires the most analysis, so we focus on task (3) below.

  We first describe how to compile all possible updates to predicates, starting with the checks and actions needed to correctly handle updates for a single rule set with implicit and explicit calls to infer. We then describe how to implement the inference in infer. In B, we systematize powerful optimizations that can be added in the overall compilation framework; clearly separated handling of updates and queries in our compilation framework allows optimizations to be added in a modular fashion.

  3.1 Compiling updates to predicates

  The operational semantics to ensure the declarative semantics of a rule set $\it rs$ is conceptually simple, but for efficiency, the implementation required varies, depending on the kind of updates to base predicates of $\it rs$ outside $\it rs$. Note that inside $\it rs$ there are no updates to base predicates of $\it rs$, by definition of base predicate.

  1. 1)

     Local updates. Local variables of $\it rs$, i.e., predicates local to $\it rs$, can be assigned values only at explicit calls to infer on $\it rs$. Such a call passes in values of local variables that are base predicates of $\it rs$ before doing the inference. Values of local variables that are derived predicates of $\it rs$ can only be used in constructing answers to the queries in the call, and the answers are returned from the call.

     There are no updates outside $\it rs$ to local variables that are derived predicates of $\it rs$, by definition of local variables.

  2. 2)

     Non-local updates. For updates to non-local variables of $\it rs$, an implicit call to infer on $\it rs$ needs to be made only after every update to a base predicate of $\it rs$.

     Statements outside $\it rs$ that update derived predicates of $\it rs$ are identified and reported as errors.

     In languages or application programs where variables hold data values, such as in database languages and applications, these updates can be determined simply at compile time, e.g., if s holds a set value, then s := s+{x} updates the set value of s. This is also the case when logic rules are used in these languages and programs.

     In programs where variables may be references to data values, each update needs to check whether the updated variable may alias a predicate of $\it rs$, conservatively at compile-time if possible, and at runtime otherwise.

  To satisfy these requirements, the overall method for compiling an update to a variable v outside rule sets is:

  • –

    In languages or application programs where variables hold data values, report a compile-time error if v is a derived predicate of any rule set; otherwise, for each rule set $\it rs$ that contains v as a base predicate, insert code, after the update, that calls infer on $\it rs$ with no arguments for base predicates and no queries.

  • –

    Otherwise, if v may refer to a predicate in a rule set, insert code that does the following after the update: if v refers to a derived predicate of any rule set, report a runtime error and exit; otherwise for each rule set $\it rs$, if v refers to a base predicate of $\it rs$, call infer on $\it rs$ with no arguments for base predicates and no queries.

  Our method for compiling an explicit call to infer on a rule set directly follows the operational semantics of infer.

  In effect, function infer is called to implement a wide range of control: from inferring everything possible using all rule sets and values of all base predicates at every update, to answering specific queries using specific rules and specific sets of values of specific base predicates at explicit calls.

  Obviously, updates in different cases may have significant impact on program efficiency. Update analysis is needed to determine the case and generate correct code. Our compilation method above minimizes calls to infer in each case.

  3.2 Implementing inference and queries

  Any existing method can be used to implement the functionality inside infer. The inference and queries for a rule set can use either bottom-up or top-down evaluation [27, 65, 66], so long as they use the rule set and values of the base predicates according to the declarative semantics of rules

  The inference and queries can be either performed by using a general logic rule engine, e.g., XSB [57, 63], or compiled to specialized standalone executable code as in, e.g., [38, 53, 26], that is then executed. Our current implementation uses the former approach, by indeed using the well-known XSB system, as described in Section 4, because it allows easier extensions to support more kinds of rules and optimizations that are already supported in XSB. Other powerful logic rule engines, including efficient Answer Set Programming (ASP) systems such as Clingo [18], can certainly be used also.

  4 Implementation and experimental evaluation

  We have implemented a prototype compiler for Alda. The compiler generates executable code in Python. The generated code calls the XSB logic rule engine [57, 63] for inference using rules.

  We implemented Alda by extending the DistAlgo compiler [43, 42, 33]. DistAlgo is an extension of Python with high-level set queries as well as distributed processes. The compiler is implemented in Python 3, and uses the Python parser. So Python syntax is used in place of the ideal syntax presented in Section 2, allowing any user with Python to run Alda directly.

  The Alda implementation extends the DistAlgo compiler to support rule-set definitions, function infer, and maintenance of derived predicates at updates to non-local variables. It handles direct updates to variables used as predicates, not updates through aliasing, as we found this to be the only update case in all benchmarks and other examples we have seen; we think this is because using logic rules with updates is similar to using queries and updates in relational databases, with no need of updates through aliasing. Currently Datalog rules extended with unrestricted negation are supported, and well-founded semantics computed by XSB is used; extensions for more general rules can be handled similarly, and inference using XSB can remain the same. Calls to infer are automatically added at updates to non-local base predicates of rule sets.

  In particular, the following Python syntax is used for rule sets, where a rule can be either one of the two forms below, so the only restriction is that the name rules is reserved.

    def rules (name = $\it rsname$):
      $\it conclusion$, if_($\it hypothesis_{1}$, $\it hypothesis_{2}$, $\it...$, $\it hypothesis_{h}$)
      if ($\it hypothesis_{1}$, $\it hypothesis_{2}$, $\it...$, $\it hypothesis_{h}$): $\it conclusion$
      $\it...$
  

  Rule sets are translated into Prolog rules at compile time. The directive :- auto_table. is added for automatic tabling in XSB.

  For function infer, the implementation translates the values of predicates and the list of queries into facts and queries in standard Prolog syntax, and translates the query answers back to values of set variables. It invokes XSB using a command line in between, passing data through files; this external interface has an obvious overhead, but it has not affected Alda having generally good performance. infer automatically reads and writes non-local predicates used in a rule set.

  Note that the overhead of the external interface can be removed with an in-memory interface from Python to XSB, which is actively being developed by the XSB team.²² 2 A version for Unix, not yet Windows, has been released: passing data of size 100 million in memory took about 30 nanoseconds per element [63, release notes]. So even the largest data in our experiments, of size a few millions, would take 0.1–0.2 seconds to pass in memory, instead of 10–20 seconds with the current external interface. However, even with the overhead of the external interface, Alda is still faster or even drastically faster than half or more of the rule engines tested in OpenRuleBench [32] for all benchmarks measured except DBLP (even though OpenRuleBench uses the fastest manually optimized program for each problem for each rule engine), and than not using rules at all (without manually writing or adapting a drastically more complex, specialized algorithm implementation for each problem).

  Building on top of DistAlgo and XSB, the compiler consists of about 1100 lines of Python and about 50 lines of XSB. This is owing critically to the overall framework and comprehensive support, especially for high-level queries, already in the DistAlgo compiler and to the powerful query engine of XSB. The parser for the rule extension is about 270 lines, and update analysis and code generation for rules and inference are about 800 lines.

  The current compiler does not perform further optimizations, because they are orthogonal to the focus of this paper, and our experiments already showed generally good performance. Further optimizations can be implemented in either the Alda compiler to generate optimized rules and tabling and indexing directives, or in XSB. Incremental maintenance under updates can also be implemented in either one, with a slightly richer interface between the two.

  Benchmark      sets	Benchmarks	Variants  and timing	Problem kinds	Code/data size
  Open- RuleBench [32]	13 incl. LUBM, Mondial, DBLP, TC, WordNet, Wine	TCrev, TCda, TCpy, ORBtimer	many kinds of rules and queries, but missing aggregate queries	largest rule set: 967 rules, largest data size: 2.4M+
  RBAC as in Section 2.6	RBACallloc, RBACnonloc, RBACunion	RBACda, RBACpy, RBACtimer	interleaved object queries and updates with function and recursive rules	program size: 385–423, data size: 10K+
  Program Analysis	PA (on any prog.: numpy, pandas, matplot, pytorch, sympy, etc.)	PAopt, PAtimer	interleaved rules, aggregate and set queries, and recursive functions	program size: 55 XSB, 33 Alda, largest data size: 5.1M+

  We discuss our experiments on the benchmarks summarized in Table 1. Detailed description of the benchmarks are in [44, 45]. Just as the benchmarks selected, the experiments selected are also meant to show generally good performance even under the most extreme overhead penalties we have encountered—runs with large data (DBLP and PA), large query results (transitive closure TC), large rules (Wine), frequent switches among different ways of using rules and other features (RBAC and PA), and frequent external invocations of the rule engine (RBAC). Our extensive experiments with other uses of Alda have experienced minimum performance overhead.

  All measurements were taken on a machine with an Intel Xeon X5690 3.47 GHz CPU, 94 GB RAM, running 64-bit Ubuntu 16.04.7, Python 3.9.9, and XSB 4.0.0. For each experiment, the reported running times are CPU times averaged over 10 runs. Garbage collection in Python was disabled for smoother running times when calling XSB. Program sizes are numbers of lines excluding comments and empty lines. Data sizes are number of facts.

  We summarize the results from the experiments below. Detailed measurements and explanations are in [44, 45].

  • –

    Compared with XSB programs in OpenRuleBench, the corresponding Alda programs are much smaller, almost all by dozens or even hundreds of lines, because all benchmarking code is in a single shared 45-line ORBtimer, much easier in Python than XSB. Compilation times are all 0.6 seconds or less.

  • –

    Running times for all benchmarks and variants, except for PA, are as expected, e.g., TC is drastically faster than TCpy and TCda, and essentially as fast as XSB if not for the overhead of using external interface with XSB; and RBACnonloc is much faster than RBACallloc due to updates being much less frequent than queries. The overhead of using external interface is obvious: e.g., for TC, up to 5.9 seconds, out of 29.2, for graphs of 100K edges; for PA, 13.1 seconds, out of 15.2, on the largest program, SymPy; and worst for DBLP, 26.9 seconds, out of 30.6, on over 2.4M facts.

    However, even so, Alda is competitive, as described above, and the overhead is expected to be reduced to 1% of it with an in-memory Python-XSB interface.

  • –

    For PA, the corresponding XSB programs were all slower and even drastically slower than Alda programs, even 120 times slower on PyTorch. Significant effort was spent on performance debugging and manual optimization before we eventually created a version that is faster than Alda—5.1 vs. 15.2 seconds on SymPy.

  5 Related work and conclusion

  There has been extensive effort in design and implementation of languages to support programming with logic rules together with other programming paradigms, by extending logic languages, extending languages in other paradigms, or developing multi-paradigm or other standalone languages.

  A large variety of logic rule languages have been extended to support sets, functions, updates, and/or objects, etc. [27, 29]. For example, see Maier et al. [48] for Datalog and variants extended with sets, functions, objects, updates, higher-order extensions, and more. In particular, many Prolog variants support sets, functions, updates, objects, constraints, etc. For example, Prolog supports assert for updates, as well as cut and negation as failure that are imperative instead of declarative [62]; Flora [71, 28] builds on XSB and supports objects (F-logic), higher-order programming (HiLog), and updates (Transaction Logic); and Picat [72] builds on B-Prolog and supports updates, comprehensions, etc. Lambda Prolog [50] extends Prolog with simply typed lambda terms and higher-order programming. Functional logic languages, such as Mercury [61] and Curry [23], combine functional programming and logic programming. Some logic programming systems are driven by scripting externally, e.g., using Lua for IDP [8], and shell scripts for LogicBlox [4]. Additional examples of Datalog extensions include Flix [47, 46], which supports lattices and monotone functions, and DDlog [56], which supports incremental maintenance under updates to input relations. These languages and extensions do not support predicates as set-valued variables together with commonly-used updates and objects in a simple and direct way, or do not support them at all.

  Many languages in other programming paradigms, especially including imperative languages and object-oriented languages, have been extended to support rules by being a host language. This is generally through explicit library interfaces of the host languages to connect with a particular logic language, for example, a Java interface for XSB through InterProlog [11, 63], C++ and Python interfaces for answer-set programming systems dlvhex [51] and Potassco [5], a Python interface for IDP [68], Rust and other interfaces for DDlog [56], and many more, e.g., for miniKanren [9]. Hosting logic languages through explicit interfaces requires programmers to write extra wrapper code for going to the rule language and coming back—declare predicates and/or logic variables, wrap features in special objects, functions, macros, etc., and/or convert data to and from special representations. They are in the same spirit as interfaces such as JDBC [52] for using database systems from languages such as Java.

  Multi-paradigm languages and other standalone languages have also been developed. For example, the Mozart system for the Oz multi-paradigm programming language [55] supports logic, functional, and constraint as well as imperative and concurrent programming. However, it is similar to logic languages extended with other features, because it supports logic variables, but not state variables to be assigned to as in commonly-used imperative languages. Examples of other languages involving logic and constraints with updates and/or objects include LOGRES [10], which integrates object-oriented data modeling and updates with rules under inflationary semantics; TLA+ [30], a logic language for specifying actions; CLAIRE [12], an object-oriented language that supports functions, sets, and rules whose conclusions are actions; LINQ [49, 34], an extension of C# for SQL-like queries; IceDust [24], a Java-based language for querying data with path-based navigation and incremental computation; extended LogiQL in SolverBlox [7], for mathematical and logic programming on top of Datalog with updates and constraints; and other logic-based query languages, e.g., Datomic [2] and SOUL [14]. These are either logic languages lacking general imperative and objected-oriented programming constructs, or imperative and object-oriented languages lacking the power and full declarativeness of logic rules.

  In conclusion, Alda supports ease of programming with logic rules together with all of sets, functions, updates, and objects as seamlessly integrated built-ins, without extra interfaces or boiler-plate code. As a direction for future work, many optimizations can be added to improve the efficiency of implementations. This includes optimizing the logic rule engines used [38, 66], the interfaces and interactions with them, and using other efficient rule systems such as Clingo [18] and specialized rule implementations such as Souffle [26] to obtain the best possible performance.

  Acknowledgments

  We thank David S. Warren for an initial 28-line XSB program for interface to XSB, and Tuncay Tekle for help implementing some benchmarks and running some preliminary experiments. We also thank Thang Bui for additional applications in program analysis and optimization, and students in undergraduate and graduate courses for using Alda and its earlier versions, called DA-rules.

  References

  • Abiteboul et al. (1995) Abiteboul, S., Hull, R., and Vianu, V. 1995. Foundations of Databases: The Logical Level. Addison-Wesley.
  • Anderson et al. (2016) Anderson, J., Gaare, M., Holguín, J., Bailey, N., and Pratley, T. 2016. The Datomic database. In Professional Clojure. Wiley Online Library, Chapter 6, 169–215.
  • ANSI INCITS (2004) ANSI INCITS. 2004. Role-Based Access Control. ANSI INCITS 359-2004, American National Standards Institute, International Committee for Information Technology Standards.
  • Aref et al. (2015) Aref, M., ten Cate, B., Green, T. J., Kimelfeld, B., Olteanu, D., Pasalic, E., Veldhuizen, T. L., and Washburn, G. 2015. Design and implementation of the LogicBlox system. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data. 1371–1382. https://doi.org/10.1145/2723372.2742796.
  • Banbara et al. (2017) Banbara, M., Kaufmann, B., Ostrowski, M., and Schaub, T. 2017. Clingcon: The next generation. Theory and Practice of Logic Programming 17, 4, 408–461.
  • Bancilhon et al. (1986) Bancilhon, F., Maier, D., Sagiv, Y., and Ullman, J. D. 1986. Magic sets and other strange ways to implement logic programs. In Proceedings of the 5th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems. 1–16.
  • Borraz-Sánchez et al. (2018) Borraz-Sánchez, C., Klabjan, D., Pasalic, E., and Aref, M. 2018. SolverBlox: Algebraic modeling in Datalog. In Declarative Logic Programming: Theory, Systems, and Applications, M. Kifer and Y. A. Liu, Eds. ACM and Morgan & Claypool, Chapter 6, 331–356. https://doi.org/10.1145/3191315.3191322.
  • Bruynooghe et al. (2014) Bruynooghe, M., Blockeel, H., Bogaerts, B., De Cat, B., De Pooter, S., Jansen, J., Labarre, A., Ramon, J., Denecker, M., and Verwer, S. 2014. Predicate logic as a modeling language: Modeling and solving some machine learning and data mining problems with IDP3. Theory and Practice of Logic Programming 15, 6, 783–817. https://doi.org/10.1017/S147106841400009X.
  • Byrd (2009) Byrd, W. E. 2009. Relational programming in miniKanren: Techniques, applications, and implementations. Ph.D. thesis, Indiana University.
  • Cacace et al. (1990) Cacace, F., Ceri, S., Crespi-Reghizzi, S., Tanca, L., and Zicari, R. 1990. Integrating object-oriented data modelling with a rule-based programming paradigm. In Proceedings of the 1990 ACM SIGMOD international conference on Management of data. 225–236.
  • Calejo (2004) Calejo, M. 2004. InterProlog: Towards a declarative embedding of logic programming in Java. In Proceedings of the 9th European Conference on Logics in Artificial Intelligence. LNCS, vol. 3229. Springer, 714–717.
  • Caseau et al. (2002) Caseau, Y., Josset, F.-X., and Laburthe, F. 2002. Claire: Combining sets, search and rules to better express algorithms. Theory and Practice of Logic Programming 2, 6, 769–805.
  • Chen and Warren (1996) Chen, W. and Warren, D. S. 1996. Tabled evaluation with delaying for general logic programs. Journal of the ACM 43, 1, 20–74.
  • De Roover et al. (2011) De Roover, C., Noguera, C., Kellens, A., and Jonckers, V. 2011. The SOUL tool suite for querying programs in symbiosis with Eclipse. In Proceedings of the 9th International Conference on Principles and Practice of Programming in Java. 71–80.
  • Ferraiolo et al. (2001) Ferraiolo, D. F., Sandhu, R., Gavrila, S., Kuhn, D. R., and Chandramouli, R. 2001. Proposed NIST standard for role-based access control. ACM Transactions on Information and Systems Security 4, 3, 224–274.
  • Fitting (2002) Fitting, M. 2002. Fixpoint semantics for logic programming: A survey. Theoretical Computer Science 278, 1, 25–51.
  • Fong and Ullman (1976) Fong, A. C. and Ullman, J. D. 1976. Inductive variables in very high level languages. In Conference Record of the 3rd Annual ACM Symposium on Principles of Programming Languages. 104–112.
  • Gebser et al. (2019) Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T. 2019. Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming 19, 1, 27–82. https://doi.org/10.1017/S1471068418000054.
  • Geiger (1995) Geiger, K. 1995. Inside ODBC. Microsoft Press.
  • Gorbovitski et al. (2010) Gorbovitski, M., Liu, Y. A., Stoller, S. D., Rothamel, T., and Tekle, T. 2010. Alias analysis for optimization of dynamic languages. In Proceedings of the 6th Symposium on Dynamic Languages. ACM Press, 27–42. https://doi.org/10.1145/1869631.1869635.
  • Goyal (2005) Goyal, D. 2005. Transformational derivation of an improved alias analysis algorithm. Higher-Order and Symbolic Computation 18, 1–2, 15–49.
  • Gupta and Mumick (1999) Gupta, A. and Mumick, I. S. 1999. Maintenance of materialized views: Problems, techniques, and applications. In Materialized Views: Techniques, Implementations, and Applications. MIT Press, 145–157.
  • Hanus (2013) Hanus, M. 2013. Functional logic programming: From theory to Curry. In Programming Logics. Springer, 123–168.
  • Harkes et al. (2016) Harkes, D. C., Groenewegen, D. M., and Visser, E. 2016. IceDust: Incremental and eventual computation of derived values in persistent object graphs. In 30th European Conference on Object-Oriented Programming. LIPIcs, vol. 56. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 11:1–11:26.
  • Jaeger and Tidswell (2000) Jaeger, T. and Tidswell, J. 2000. Rebuttal to the NIST RBAC model proposal. In Proceedings of the 5th ACM Workshop on Role Based Access Control. 66.
  • Jordan et al. (2016) Jordan, H., Scholz, B., and Subotić, P. 2016. Soufflé: On synthesis of program analyzers. In Proceedings of the International Conference on Computer Aided Verification. Springer, 422–430.
  • Kifer and Liu (2018) Kifer, M. and Liu, Y. A., Eds. 2018. Declarative Logic Programming: Theory, Systems, and Applications. ACM and Morgan & Claypool.
  • Kifer et al. (2020) Kifer, M., Yang, G., Wan, H., and Zhao, C. 2020. Ergo Lite (a.k.a. Flora-2): User’s Manual Version 2.1. Stony Brook University. http://flora.sourceforge.net/. Accessed May 25, 2023.
  • Körner et al. (2022) Körner, P., Leuschel, M., Barbosa, J. a., Costa, V. S., Dahl, V., Hermenegildo, M. V., Morales, J. F., Wielemaker, J., Diaz, D., Abreu, S., and Ciatto, G. 2022. Fifty years of Prolog and beyond. Theory and Practice of Logic Programming 22, 6, 776–858. https://doi.org/10.1017/S1471068422000102.
  • Lamport (1994) Lamport, L. 1994. The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16, 3, 872–923.
  • Li et al. (2007) Li, N., Byun, J.-W., and Bertino, E. 2007. A critique of the ANSI standard on role-based access control. IEEE Security and Privacy 5, 6, 41–49.
  • Liang et al. (2009) Liang, S., Fodor, P., Wan, H., and Kifer, M. 2009. OpenRuleBench: An analysis of the performance of rule engines. In Proceedings of the 18th International Conference on World Wide Web. ACM Press, 601–610.
  • Lin and Liu (2022) Lin, B. and Liu, Y. A. 2014 (Latest update January 30, 2022). DistAlgo: A language for distributed algorithms. http://github.com/DistAlgo. Accessed May 25, 2023.
  • LINQ (2023) LINQ 2023. Language Integrated Query (LINQ). https://docs.microsoft.com/dotnet/csharp/linq. Accessed May 25, 2023.
  • Liu (2018) Liu, Y. A. 2018. Logic programming applications: What are the abstractions and implementations? In Declarative Logic Programming: Theory, Systems, and Applications, M. Kifer and Y. A. Liu, Eds. ACM and Morgan & Claypool, Chapter 10, 519–557. Also https://arxiv.org/abs/1802.07284.
  • Liu et al. (2016) Liu, Y. A., Brandvein, J., Stoller, S. D., and Lin, B. 2016. Demand-driven incremental object queries. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming. ACM Press, 228–241. https://doi.org/10.1145/2967973.2968610.
  • Liu and Stoller (2007) Liu, Y. A. and Stoller, S. D. 2007. Role-based access control: A corrected and simplified specification. In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats. Wiley, 425–439.
  • Liu and Stoller (2009) Liu, Y. A. and Stoller, S. D. 2009. From Datalog rules to efficient programs with time and space guarantees. ACM Transactions on Programming Languages and Systems 31, 6, 1–38. https://doi.org/10.1145/1552309.1552311.
  • Liu and Stoller (2020) Liu, Y. A. and Stoller, S. D. 2020. Founded semantics and constraint semantics of logic rules. Journal of Logic and Computation 30, 8 (Dec.), 1609–1638. Also http://arxiv.org/abs/1606.06269.
  • Liu and Stoller (2021) Liu, Y. A. and Stoller, S. D. 2021. Knowledge of uncertain worlds: Programming with logical constraints. Journal of Logic and Computation 31, 1 (Jan.), 193–212. Also https://arxiv.org/abs/1910.10346.
  • Liu and Stoller (2022) Liu, Y. A. and Stoller, S. D. 2022. Recursive rules with aggregation: A simple unified semantics. Journal of Logic and Computation 32, 8 (Dec.), 1659–1693. Also http://arxiv.org/abs/2007.13053.
  • Liu et al. (2017) Liu, Y. A., Stoller, S. D., and Lin, B. 2017. From clarity to efficiency for distributed algorithms. ACM Transactions on Programming Languages and Systems 39, 3 (May), 12:1–12:41. Also http://arxiv.org/abs/1412.8461.
  • Liu et al. (2012) Liu, Y. A., Stoller, S. D., Lin, B., and Gorbovitski, M. 2012. From clarity to efficiency for distributed algorithms. In Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications. 395–410. https://doi.org/10.1145/2384616.2384645.
  • Liu et al. (2022) Liu, Y. A., Stoller, S. D., Tong, Y., Lin, B., and Tekle, K. T. 2022. Programming with rules and everything else, seamlessly. Computing Research Repository arXiv:2205.15204 [cs.PL]. http://arxiv.org/abs/2205.15204.
  • Liu et al. (2023) Liu, Y. A., Stoller, S. D., Tong, Y., and Tekle, K. T. 2023. Benchmarking for integrating logic rules with everything else. In Proceedings of the 39th International Conference on Logic Programming (Technical Communications). Open Publishing Association.
  • Madsen and Lhoták (2020) Madsen, M. and Lhoták, O. 2020. Fixpoints for the masses: Programming with first-class Datalog constraints. Proceedings of the ACM on Programming Languages 4, OOPSLA, 1–28.
  • Madsen et al. (2016) Madsen, M., Yee, M.-H., and Lhoták, O. 2016. From Datalog to Flix: A declarative language for fixed points on lattices. ACM SIGPLAN Notices 51, 6, 194–208.
  • Maier et al. (2018) Maier, D., Tekle, K. T., Kifer, M., and Warren, D. S. 2018. Datalog: Concepts, history and outlook. In Declarative Logic Programming: Theory, Systems, and Applications, M. Kifer and Y. A. Liu, Eds. ACM and Morgan & Claypool, Chapter 1, 3–120.
  • Meijer et al. (2006) Meijer, E., Beckman, B., and Bierman, G. 2006. LINQ: reconciling object, relations and XML in the .NET framework. In Proceedings of the 2006 ACM SIGMOD international conference on Management of data. 706–706.
  • Miller and Nadathur (2012) Miller, D. and Nadathur, G. 2012. Programming with Higher-Order Logic. Cambridge University Press.
  • Redl (2016) Redl, C. 2016. The DLVHEX system for knowledge representation: Recent advances (system description). Theory and Practice of Logic Programming 16, 5-6, 866–883.
  • Reese (2000) Reese, G. 2000. Database Programming with JDBC and JAVA. O’Reilly Media, Inc.
  • Rothamel and Liu (2007) Rothamel, T. and Liu, Y. A. 2007. Efficient implementation of tuple pattern based retrieval. In Proceedings of the ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation. 81–90. https://doi.org/10.1145/1244381.1244394.
  • Rothamel and Liu (2008) Rothamel, T. and Liu, Y. A. 2008. Generating incremental implementations of object-set queries. In Proceedings of the 7th International Conference on Generative Programming and Component Engineering. ACM Press, 55–66. https://doi.org/10.1145/1449913.1449923.
  • Roy and Haridi (2004) Roy, P. V. and Haridi, S. 2004. Concepts, Techniques, and Models of Computer Programming. MIT Press.
  • Ryzhyk and Budiu (2019) Ryzhyk, L. and Budiu, M. 2019. Differential datalog. In Datalog 2.0, 3rd International Workshop on the Resurgence of Datalog in Academia and Industry. 56–67.
  • Sagonas et al. (1994) Sagonas, K., Swift, T., and Warren, D. S. 1994. XSB as an efficient deductive database engine. In Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data. ACM Press, 442–453.
  • Saha and Ramakrishnan (2003) Saha, D. and Ramakrishnan, C. R. 2003. Incremental evaluation of tabled logic programs. In Proceedings of the 19th International Conference on Logic Programming. Springer, 392–406. https://doi.org/10.1007/978-3-540-24599-5_27.
  • Sandhu et al. (2000) Sandhu, R., Ferraiolo, D., and Kuhn, R. 2000. The NIST model for role-based access control: Towards a unified standard. In Proceedings of the 5th ACM Workshop on Role-Based Access Control. 47–63.
  • Serbanuta et al. (2009) Serbanuta, T. F., Rosu, G., and Meseguer, J. 2009. A rewriting logic approach to operational semantics. Information and Computation 207, 305–340.
  • Somogyi et al. (1995) Somogyi, Z., Henderson, F. J., and Conway, T. C. 1995. Mercury, an efficient purely declarative logic programming language. Australian Computer Science Communications 17, 499–512.
  • Sterling and Shapiro (1994) Sterling, L. and Shapiro, E. 1994. The Art of Prolog, 2nd ed. MIT Press.
  • Swift et al. (2022) Swift, T., Warren, D. S., Sagonas, K., Freire, J., Rao, P., Cui, B., Johnson, E., de Castro, L., Marques, R. F., Saha, D., Dawson, S., and Kifer, M. 2022. The XSB System Version 5.0,x. http://xsb.sourceforge.net. Latest release May 12, 2022.
  • Tamaki and Sato (1986) Tamaki, H. and Sato, T. 1986. OLD resolution with tabulation. In Proceedings of the 3rd International Conference on Logic Programming. Springer, 84–98.
  • Tekle and Liu (2010) Tekle, K. T. and Liu, Y. A. 2010. Precise complexity analysis for efficient Datalog queries. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. 35–44. https://doi.org/10.1145/1836089.1836094.
  • Tekle and Liu (2011) Tekle, K. T. and Liu, Y. A. 2011. More efficient Datalog queries: Subsumptive tabling beats magic sets. In Proceedings of the 2011 ACM SIGMOD International Conference on Management of Data. 661–672. http://doi.acm.org/10.1145/1989323.1989393.
  • Tong et al. (2023) Tong, Y., Lin, B., Liu, Y. A., and Stoller, S. D. 2023. ALDA. http://github.com/DistAlgo/alda. Accessed May 25, 2023.
  • Vennekens (2017) Vennekens, J. 2017. Lowering the learning curve for declarative programming: A Python API for the IDP system. In Proceedings of 19th International Symposium on Practical Aspects of Declarative Languages. Springer, 86–102.
  • Warren and Liu (2017) Warren, D. S. and Liu, Y. A. 2017. AppLP: A dialogue on applications of logic programming. Computing Research Repository arXiv:1704.02375 [cs.PL]. http://arxiv.org/abs/1704.02375.
  • Wright and Felleisen (1994) Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Information and Computation 115, 38–94.
  • Yang and Kifer (2000) Yang, G. and Kifer, M. 2000. FLORA: Implementing an efficient DOOD system using a tabling logic engine. In Proceedings of the 1st International Conference on Computational Logic. Springer, 1078–1093. https://doi.org/10.1007/3-540-44957-4_72.
  • Zhou (2016) Zhou, N.-F. 2016. Programming in Picat. In Proceedings of the 10th International Symposium on Rule Technologies: Research, Tools, and Applications. Springer, 3–18.

  Appendix A Formal Semantics

  We give a complete abstract syntax and formal semantics for our language. The operational semantics is a reduction semantics with evaluation contexts [70, 60]. It builds on the standard least fixed-point semantics for Datalog [16] and the formal operational semantics for DistAlgo [42]. Relative to the latter, we removed the constructs specific to distributed algorithms, added an abstract syntax for rule sets and calls to infer, added a transition rule for calls to infer, extended the state with a stack that keeps track of rule sets whose results need to be maintained, extended several existing transition rules to perform automatic maintenance of the results of rule sets, and modified the semantics of existential quantifiers to bind the quantified variables to a witness when one exists. The removed DistAlgo constructs can easily be restored; we removed them simply to avoid repeating them.

  A.1 Abstract syntax

  The abstract syntax is defined in Figures 2–3. Tuples are immutable values, not mutable objects. Sets and sequences are mutable objects. They are instances of the predefined classes set and sequence, respectively. Methods of set include add, del, contains, size, and any (which returns an element of the set, if the set is non-empty, otherwise it returns None). Methods of sequence include add (which adds an element at the end of the sequence), contains, and length. For brevity, among the standard arithmetic operations, we include only one representative operation in the abstract syntax and semantics; others are handled similarly. All expressions are side-effect free. Object creation, comprehension, and infer are not expressions, because they all have the side-effect of creating one or more new objects. Semantically, the for loop copies the contents of a (mutable) set or sequence into an (immutable) tuple before iterating over it, to ensure that changes to the set or sequence by the loop body do not affect the iteration. whileSome and ifSome are similar to while and if, except that they always have an existential quantification as their condition, and they bind the variables in the pattern in the quantification to a witness, if one exists. We use some syntactic sugar in sample code, e.g., we use infix notation for some binary operators, such as is and and.

  We refer to rule sets defined in global scope and class scope as “global rule sets” and “class scope rule sets”, respectively.

  Note that method parameters are not variables and cannot be assigned to, and that methods do not have local variables. These choices simplify the semantics by eliminating the need for a call stack. The only local variables are local variables of rule sets. We refer to the other kinds of variables, namely global variables and instance variables, as non-local variables. For brevity, we use “variables” without a qualifier to refer to non-local variables.

  $\it Program$ ::= $\it Ruleset$* $\it Class$* $\it Statement$
  $\it Ruleset$ ::= rules $\it RulesetName$ $\it Rule$+
  $\it Rule$ ::= $\it DerivedPredicate$($\it PredicateArg$*) if $\it BasePredicate$($\it PredicateArg$*)*
  $\it DerivedPredicate$ ::=	$\it GlobalVariable$
  	self.$\it Field$
  	$\it LocalVariable$
  $\it BasePredicate$ ::=	$\it GlobalVariable$[.$\it Field$*]
  	self.$\it Field$+
  	$\it LocalVariable$
  $\it PredicateArg$ ::=	$\it LogicVariable$
  	$\it Literal$
  $\it Class$ ::= class $\it ClassName$ [extends $\it ClassName$] : $\it Ruleset$* $\it Method$*
  $\it Method$ ::=	def $\it MethodName$($\it Parameter$*) $\it Statement$
  	defun $\it MethodName$($\it Parameter$*) $\it Expression$
  $\it Statement$ ::=	$\it NonLocalVariable$ := $\it Expression$
  	$\it NonLocalVariable$ := new $\it ClassName$
  	$\it NonLocalVariable$ := { $\it Expression$ : $\it Iterator$* | $\it Expression$ }
  	$\it Statement$ ; $\it Statement$
  	if $\it Expression$ : $\it Statement$ else : $\it Statement$
  	for $\it Iterator$ : $\it Statement$
  	while $\it Expression$ : $\it Statement$
  	ifSome $\it Iterator$ | $\it Expression$ : $\it Statement$
  	whileSome $\it Iterator$ | $\it Expression$ : $\it Statement$
  	$\it Expression$.$\it MethodName$($\it Expression$*)
  	$\it NonLocalVariable$* := [$\it Expression$.]infer(	$\it Query$*, $\it KeywordArg$*,
  		rules=$\it RulesetName$)
  	skip
  $\it Expression$ ::=	$\it Literal$
  	$\it Parameter$
  	$\it NonLocalVariable$
  	$\it Tuple$
  	$\it UnaryOp$($\it Expression$)
  	$\it BinaryOp$($\it Expression$,$\it Expression$)
  	isinstance($\it Expression$,$\it ClassName$)
  	and($\it Expression$,$\it Expression$)	/ / conjunction (short-circuiting)
  	or($\it Expression$,$\it Expression$)	/ / disjunction (short-circuiting)
  	each $\it Iterator$ | $\it Expression$
  	some $\it Iterator$ | $\it Expression$
  	$\it Expression$.$\it MethodName$($\it Expression$*)

  $\it NonLocalVariable$ :=	$\it GlobalVariable$
  	$\it InstanceVariable$
  $\it InstanceVariable$ ::= $\it Expression$.$\it Field$
  $\it Literal$ ::=	None
  	Bool
  	Int
  	…
  Bool ::=	True
  	False
  Int ::= …
  $\it Iterator$ ::= $\it Pattern$ in $\it Expression$
  $\it Pattern$ ::=	$\it NonLocalVariable$
  	$\it TuplePattern$
  $\it TuplePattern$ ::= ($\it PatternElement$*)
  $\it PatternElement$ ::=	$\it Expression$
  	_
  	=$\it NonLocalVariable$
  $\it Query$ :=	$\it Predicate$[$\it TuplePattern$]
  $\it KeywordArg$ ::= $\it LocalVariable$ = $\it Expression$
  $\it Tuple$ ::= ($\it Expression$*)
  $\it UnaryOp$ ::=	not	/ / Boolean negation
  	isTuple	/ / test whether a value is a tuple
  	len	/ / length of a tuple
  $\it BinaryOp$ ::=	is	/ / identity-based equality
  	plus	/ / sum
  	select	/ / select($t$,$i$) returns the $i$’th component of tuple $t$

  Notation in the grammar.   A symbol in the grammar is a terminal symbol if it is in typewriter font or is a non-terminal symbol if it is in italics. In each production, alternatives are separated by a linebreak. Square brackets enclose optional clauses. * after a non-terminal means “0 or more occurrences”. + after a non-terminal means “1 or more occurrences”.

  Well-formedness requirements on programs.   In global rule sets, predicates cannot contain self. In class scope rule sets, derived predicates cannot be global variables. Each global variable appears as a derived predicate in at most one rule set in the program. In each class, for each field $f$, self.$f$ appears as a derived predicate in at most one rule set in that class. In each rule in each rule set, each logic variable that appears in the conclusion appears in a hypothesis. Within each rule set, all uses of the same predicate have the same number of arguments.

  In assignments with a call to infer on the right side of the assignment, the number of variables on the left of the assignment equals the number of queries, the predicates queried are derived predicates of the rule set used, and local variables in keyword arguments are base predicates of the rule set used.

  Invocations of methods defined using def appear only as statements. Invocations of methods defined using defun appear only as expressions; we also refer to these methods as “functions”. The program does not contain definitions of classes named set and sequence.

  Class names are unique; in other words, each class name is defined at most once. Method names are unique within the scope of each class. Rule set names are unique within each scope.

  A.1.1 Constructs whose semantics is given by translation

  Notation.   A (partial) function is represented as a set of mappings $x\mapsto y$. We represent substitutions as functions from parameters and variables to expressions. $t\,\theta$ denotes the result of applying substitution $\theta$ to $t$.

  Class scope rule set names.   The program is transformed so that rule set names are unique across all scopes. A straightforward way to do this is to prefix the name of every class scope rule set with the name of the enclosing class.

  Global variables.   Global variables are replaced with instance variables, and global rule sets are transformed to have the same form as class scope rule sets, by the following transformations. Choose an address $a_{\it gv}$ whose fields will be used to represent global variables. Everywhere except in global rule sets and in queries in calls to infer on global rule sets, replace each global variable $x$ with $a_{\it gv}.x$. Introduce a class name $C_{\it gv}$, put all global rule sets into this class, and replace each global variable $x$ with self.$x$ in those rule sets and in queries in calls to infer on those rule sets. Calls to infer on those rule sets are also transformed by prefixing $a_{\it gv}{\tt.}$ to the call, i.e., ${\color[rgb]{0,0,1}\tt infer}(\cdots)$ is replaced with $a_{\it gv}{\tt.}{\color[rgb]{0,0,1}\tt infer}{\tt(}\cdots{\tt)}$, so all calls to infer have a target object. The initial state of the program is defined so that an object of type $C_{\it gv}$ is at address $a_{\it gv}$. These transformations simplify the transition rules related to inference, by allowing global rule sets and class scope rule sets to be handled in a uniform way.

  Boolean operators.   The Boolean operators and and each are eliminated as follows: $e_{1}$ and $e_{2}$ is replaced with not(not($e_{1}$) or not($e_{2}$)), and each iter | $e$ is replaced with not(some iter | not($e$)).

  Non-variable expressions in tuple patterns.   Non-variable expressions in tuple patterns are replaced with variables prefixed by “=”. Specifically, for each expression $e$ in a tuple pattern that is not a variable, a variable prefixed with “=”, or wildcard, an assignment $v$ := $e$ to a fresh variable $v$ is inserted before the statement that contains the tuple pattern, and $e$ is replaced with =$v$ in the tuple pattern.

  Wildcards.   Wildcards are eliminated from tuple patterns in for loops, comprehensions, and quantifications (i.e., everywhere except as $\it Query$ in infer) by replacing each wildcard with a fresh variable.

  Tuple patterns in infer statements.   infer statements are transformed to eliminate tuple patterns in queries. After transformation, each query is simply the name of a predicate. Consider the statement $x_{1},\ldots,x_{n}$ := $[e.]$infer($p_{1}({\it pat}_{1}),$ $\ldots,$ $p_{n}(pat_{n}),{\it kwargs},$ rules=$rs$). Let $x_{i,1},$ $\ldots,$ $x_{i,k_{i}}$ be the components of ${\it pat}_{i}$, in order and without repetitions, that are variables not prefixed by “=”. Let $y_{1},\ldots,y_{n}$ be fresh variables. The above statement is transformed to:

  $y_{1},\ldots,y_{n}$ := $[e.]$infer($p_{1},\ldots,p_{n},{\it kwargs},$ rules=$rs$)
  $x_{1}$ := { ($x_{1,1},\ldots,x_{1,k_{1}}$) : ${\it pat}_{1}$ in $y_{1}$ | True }
  $\ldots$
  $x_{n}$ := { ($x_{n,1},\ldots,x_{n,k_{n}}$) : ${\it pat}_{n}$ in $y_{n}$ | True }
  

  ifSome statements.   ifSome is statically eliminated as follows. Consider the statement ifSome pat in $e$ | $b$ : $s$. Let $i_{1},\ldots,i_{k}$ be indices, in order of appearance from left to right, of elements of pat that are variables not prefixed by “=”. Let $x_{i_{1}},\ldots,x_{i_{k}}$ be those variables. Let foundOne and $x^{\prime}_{i_{1}},\ldots,x^{\prime}_{i_{k}}$ be fresh variables. Let substitution $\theta$ be $[x_{i_{1}}\mapsto x^{\prime}_{i_{1}},\ldots,x_{i_{k}}\mapsto x^{\prime}_{i_{k}}]$. Let ${\it pat}^{\prime}={\it pat}\,\theta$ and $b^{\prime}=b\,\theta$. The above ifSome statement is transformed to:

  foundOne := False
  for $pat^{\prime}$ in $e$:
    if $b^{\prime}$ and not foundOne:
      $x_{i_{1}}:=x^{\prime}_{i_{1}}$
      $\ldots$
      $x_{i_{k}}:=x^{\prime}_{i_{k}}$
      $s$
      foundOne := True
  

  whileSome statements.   whileSome is statically eliminated as follows. Consider the statement whileSome pat in $e$ | $b$ : $s$. Using the same definitions as in the previous item, this statement is transformed to:

  foundOne := True
  while foundOne:
    foundOne := False
    for $pat^{\prime}$ in $e$:
      if $b^{\prime}$ and not foundOne:
        $x_{i_{1}}:=x^{\prime}_{i_{1}}$
        $\ldots$
        $x_{i_{k}}:=x^{\prime}_{i_{k}}$
        $s$
        foundOne := True
  

  Comprehensions.   First, comprehensions are transformed to eliminate the use of variables prefixed with “=”. Specifically, for a variable $x$ prefixed with “=” in a comprehension, replace occurrences of =x in the comprehension with occurrences of a fresh variable $y$, and add the conjunct $y$ is $x$ to the Boolean condition. Second, all comprehensions are statically eliminated as follows. The comprehension $x$ := { $e$ | $pat_{1}$ in $e_{1}$, $\ldots$, $pat_{n}$ in $e_{n}$ | $b$ } is replaced with

  $x$ := new set
  for $pat_{1}$ in $e_{1}$:
    ...
      for $pat_{n}$ in $e_{n}$:
        if $b$:
          $x$.add($e$)
  

  Tuple patterns in iterators.   Iterators containing tuple patterns are rewritten as iterators without tuple patterns.

  Consider the existential quantification some ($e_{1},\ldots,e_{n}$) in $e$ | $b$. Let $x$ be a fresh variable. Let $\theta$ be the substitution that replaces $e_{i}$ with select($x$,$i$) for each $i$ such that $e_{i}$ is a variable not prefixed with “=”. Let $\{j_{1},\ldots,j_{m}\}$ contain the indices of the constants and the variables prefixed with “=” in ($e_{1},\ldots,e_{n}$). Let $\bar{e}_{j}$ denote $e_{j}$ after removing the “=” prefix, if any. The quantification is rewritten as some $x$ in $e$ | isTuple($x$) and len($x$) is $n$ and (select($x$,$j_{1}$), $\ldots$, select($x$,$j_{m}$)) is ($\bar{e}_{j_{1}}$, $\ldots$, $\bar{e}_{j_{m}}$) and $b\,\theta$.

  Consider the loop for ($e_{1},\ldots,e_{n}$) in $e$ : $s$. Let $x$ and $S$ be fresh variables. Let $\{i_{1},\ldots,i_{k}\}$ contain the indices in ($e_{1},\ldots,e_{n}$) of variables not prefixed with “=”. Let $\{j_{1},\ldots,j_{m}\}$ be as in the previous paragraph. Let $\bar{e}_{j}$ denote $e_{j}$ after removing the “=” prefix, if any. Note that $e$ may evaluate to a set or sequence, and duplicate bindings for the tuple of variables $(e_{i_{1}},\ldots,e_{i_{k}})$ are filtered out if $e$ evaluates to a set but not if $e$ evaluates to a sequence. The loop is rewritten as the code in Figure 4.

      $S$ := $e$
      if isinstance($S$,set):
        $S$ := { $x$ : $x$ in $S$ | isTuple($x$) and len($x$) is $n$
            and (select($x$,$j_{1}$), $\ldots$, select($x$,$j_{m}$))
               is ($\bar{e}_{j_{1}}$, $\ldots$, $\bar{e}_{j_{m}}$) }
        for $x$ in $S$:
          $e_{i_{1}}:={\color[rgb]{0,0,1}\tt select}(x,i_{1})$
          $\ldots$
          $e_{i_{k}}:={\color[rgb]{0,0,1}\tt select}(x,i_{k})$
          $s$
      else:  / / $S$ is a sequence
        for $x$ in $S$:
          if (isTuple($x$) and len($x$) is $n$
              and (select($x$,$j_{1}$), $\ldots$, select($x$,$j_{m}$))
                 is ($\bar{e}_{j_{1}}$, $\ldots$, $\bar{e}_{j_{m}}$):
            $e_{i_{1}}:={\color[rgb]{0,0,1}\tt select}(x,i_{1})$
            $\ldots$
            $e_{i_{k}}:={\color[rgb]{0,0,1}\tt select}(x,i_{k})$
            $s$
          else:
            skip
  

  A.2 Semantic domains

  The semantic domains are defined in Figure 5, using the following notation. $D^{*}$ is the set of finite sequences of values from domain $D$. ${\rm Set}(D)$ is the set of finite sets of values from domain $D$. $D_{1}\rightarrow D_{2}$ and $D_{1}\rightharpoonup D_{2}$ are the sets of (total) functions and partial functions, respectively, from $D_{1}$ to $D_{2}$. ${\it dom}(f)$ and ${\it range}(f)$ are the domain and range, respectively, of a partial function $f$, i.e., ${\it dom}(f)=\{x\;|\;\exists y:x\mapsto y\in f\}$ and ${\it range}(f)=\{y\;|\;\exists x:x\mapsto y\in f\}$.

  In a state $(s,h,ht)$, $s$ is the statement to be executed, $h$ is the heap that maps an address to the object at that address, and $ht$ is the heap type map that maps an address to the type of the object on the heap at that address.

  	$\displaystyle{\it Bool}$	$\displaystyle=$	$\displaystyle\{{\color[rgb]{0,0,1}\tt True},{\color[rgb]{0,0,1}\tt False}\}$
  	$\displaystyle{\it Int}$	$\displaystyle=$	$\displaystyle...$
  	$\it Address$	$\displaystyle=$	$\displaystyle...$
  	$\it Tuple$	$\displaystyle=$	$\displaystyle\mbox{$\it Val$}^{*}$
  	$\it Val$	$\displaystyle=$	$\displaystyle{\it Bool}\cup{\it Int}\cup{\mbox{$\it Address$}}\cup{\mbox{$\it Tuple$}}\cup\{{\color[rgb]{0,0,1}\tt None}\}$
  	$\displaystyle{\it Object}$	$\displaystyle=$	$\displaystyle({\mbox{$\it Field$}}\rightharpoonup{\mbox{$\it Val$}})\cup{\rm Set}({\mbox{$\it Val$}})\cup{\mbox{$\it Val$}}^{*}$
  	$\displaystyle{\it HeapType}$	$\displaystyle=$	$\displaystyle\mbox{$\it Address$}\rightharpoonup{\mbox{$\it ClassName$}}$
  	$\displaystyle{\it Heap}$	$\displaystyle=$	$\displaystyle\mbox{$\it Address$}\rightharpoonup{\it Object}$
  	$\displaystyle{\it State}$	$\displaystyle=$	$\displaystyle\mbox{$\it Statement$}\times{\it Heap}\times{\it HeapType}$

  A.3 Extended abstract syntax

  Section A.1 defines the abstract syntax of programs that can be written by the user. We extend the abstract syntax to include additional forms into which programs may evolve during evaluation. The new productions appear below. The statement for $v$ inTuple $t$: $s$ iterates over the elements of tuple $t$, in the obvious way.

  $\it Expression$ ::=	Address
  	Address.$\it Field$
  $\it Statement$ ::= for Variable inTuple $\it Tuple$: $\it Statement$

  A.4 Evaluation contexts

  Evaluation contexts, also called reduction contexts, are used to identify the next part of an expression or statement to be evaluated. An evaluation context is an expression or statement with a hole, denoted [ ], in place of the next sub-expression or sub-statement to be evaluated. Evaluation contexts are defined in Figure 6. Note that square brackets enclosing a clause indicate that the clause is optional; this is unrelated to the notation [ ] for the hole.

  For example, the definition of evaluation contexts for method calls (lines 3–4 of Figure 6) says that the expression denoting the target object is evaluated first to obtain an address (if the expression isn’t already an address); then, the arguments are evaluated from left to right. The left-to-right order holds because an argument can be evaluated only if the arguments to its left are values, as opposed to more complicated unevaluated expressions. The definition of evaluation contexts for infer implies that the expressions for the targets of the assignment are evaluated from left to right; then the expression for the target object, if any (i.e., if the call is for a rule set with class scope), is evaluated; and then the argument expressions are evaluated from left to right.

  $\it C$ ::=	[ ]
  	($\it Val$*, $\it C$, $\it Expression$*)
  	$\it C$.$\it MethodName$($\it Expression$*)
  	$\it Address$.$\it MethodName$($\it Val$*, $\it C$, $\it Expression$*)
  	$\it UnaryOp$($\it C$)
  	$\it BinaryOp$($\it C$, $\it Expression$)
  	$\it BinaryOp$($\it Val$, $\it C$)
  	isinstance($\it C$, $\it ClassName$)
  	or($\it C$, $\it Expression$)
  	some $\it Pattern$ in $\it C$ | $\it Expression$
  	$\it C$.$\it Field$ := $\it Expression$
  	$\it C$.$\it Field$ := new $\it ClassName$
  	$\it Address$.$\it Field$ := $\it C$
  	$\it C$ ; $\it Statement$
  	if $\it C$: $\it Statement$ else: $\it Statement$
  	for $\it InstanceVariable$ in $\it C$: $\it Statement$
  	for $\it InstanceVariable$ inTuple $\it Tuple$: $\it C$
  	($\it Address$.$\it Field$)*, $\it C$.$\it Field$, ($\it Expression$.$\it Field$)* :=
  	[$\it Expression$.]infer(	$\it Query$*, $\it KeywordArg$*,
  		rules=$\it RulesetName$)
  	($\it Address$.$\it Field$)* := $\it C$.infer(	$\it Query$*, $\it KeywordArg$*,
  		rules=$\it RulesetName$)
  	($\it Address$.$\it Field$)* :=
  	[$\it Address$.]infer($\it Query$*, ($\it Parameter$=$\it Val$)*,
  	$\it Parameter$=$\it C$, $\it KeywordArg$*, rules=$\it RulesetName$)

  A.5 Transition relations

  The transition relation for expressions has the form $h,ht\vdash e\rightarrow e^{\prime}$, where $e$ and $e^{\prime}$ are expressions, $h\in{\it Heap}$, and $ht\in{\it HeapType}$. The transition relation for statements has the form ${\it state}\rightarrow{\it state}^{\prime}$ where ${\it state}\in{\it State}$ and ${\it state}^{\prime}\in{\it State}$.

  Both transition relations, and some of the auxiliary functions defined below, are implicitly parameterized by the program, which is needed to look up method definitions, rule set definitions, etc. The transition relation for expressions is defined in Figure 7. The transition relation for statements is defined in Figures 9–10, using auxiliary functions defined in Figure 8. The context rules for expressions and statements at the top of Figure 9 allow the expression or statement in the evaluation context’s hole to take a transition, while the rest of the program, denoted by $C$, is carried along unchanged.

  $$\begin{array}[]{@{}l@{}}\mbox{/\,/\ field access}\\ h,ht\vdash a.f\rightarrow h(a)(f)\hskip 10.00002pt\mbox{if }ht(a)\not\in\{{\color[rgb]{0,0,1}\tt set},{\color[rgb]{0,0,1}\tt seq}\}\land f\in{\it dom}(h(a))\\ \\ \mbox{/\,/\ invoke function in user-defined class}\\ h,ht\vdash a{\tt.}m(v_{1},\ldots,v_{n})\rightarrow e[{\color[rgb]{0,0,1}\tt self}\mapsto a,x_{1}\mapsto v_{1},\ldots,x_{n}\mapsto v_{n}]\\ \hskip 7.5pt\mbox{if }{\it methodDef}(ht(a),m,{\color[rgb]{0,0,1}\tt defun}~m(x_{1},\ldots,x_{n})~e)\\ \\ \mbox{/\,/\ invoke function in pre-defined class (example)}\\ h,ht\vdash a{\tt.{\color[rgb]{0,0,1}any}()}\rightarrow v\hskip 10.00002pt\mbox{if }ht(a)={\color[rgb]{0,0,1}\tt set}\land v\in h(a)\\ h,ht\vdash a{\tt.{\color[rgb]{0,0,1}any}()}\rightarrow{\color[rgb]{0,0,1}\tt None}\hskip 10.00002pt\mbox{if }ht(a)={\color[rgb]{0,0,1}\tt set}\land h(a)=\emptyset\\ \\ \mbox{/\,/\ unary operations}\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}not}({\color[rgb]{0,0,1}True})}\rightarrow{\color[rgb]{0,0,1}\tt False}\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}not}({\color[rgb]{0,0,1}False})}\rightarrow{\color[rgb]{0,0,1}\tt True}\\ h,ht\vdash{\color[rgb]{0,0,1}\tt isTuple}{\tt(}v{\tt)}\rightarrow{\color[rgb]{0,0,1}\tt True}\hskip 10.00002pt\mbox{if $v$ is a tuple}\\ h,ht\vdash{\color[rgb]{0,0,1}\tt isTuple}{\tt(}v{\tt)}\rightarrow{\color[rgb]{0,0,1}\tt False}\hskip 10.00002pt\mbox{if $v$ is not a tuple}\\ h,ht\vdash{\color[rgb]{0,0,1}\tt len}{\tt(}v{\tt)}\rightarrow n\hskip 10.00002pt\mbox{if $v$ is a tuple with $n$ components}\\ \\ \mbox{/\,/\ binary operations}\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}is}(}v_{1},v_{2}{\tt)}\rightarrow{\color[rgb]{0,0,1}\tt True}\\ \hskip 7.5pt\mbox{if $v_{1}$ and $v_{2}$ are the same (identical) value}\\ \\ h,ht\vdash{\tt{\color[rgb]{0,0,1}plus}(}v_{1},v_{2}{\tt)}\rightarrow v_{3}\\ \hskip 7.5pt\mbox{if }v_{1}\in{\it Int}\land v_{2}\in{\it Int}\land v_{3}=v_{1}+v_{2}\\ \\ h,ht\vdash{\tt{\color[rgb]{0,0,1}select}(}v_{1},v_{2}{\tt)}\rightarrow v_{3}\\ \hskip 7.5pt\mbox{if }v_{2}\in{\it Int}\land v_{2}>0\land\mbox{($v_{1}$ is a tuple with length at least $v_{2}$)}\\ \hskip 7.5pt{}\land\mbox{($v_{3}$ is the $v_{2}$'th component of $v_{1}$)}\\ \\ \mbox{/\,/\ isinstance}\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}isinstance}(}a,c{\tt)}\rightarrow{\color[rgb]{0,0,1}\tt True}\hskip 10.00002pt\mbox{if }ht(a)=c\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}isinstance}(}a,c{\tt)}\rightarrow{\color[rgb]{0,0,1}\tt False}\hskip 10.00002pt\mbox{if }ht(a)\neq c\\ \\ \mbox{/\,/\ disjunction}\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}or}({\color[rgb]{0,0,1}True}},e{\tt)}\rightarrow{\color[rgb]{0,0,1}\tt True}\\ h,ht\vdash{\tt{\color[rgb]{0,0,1}or}({\color[rgb]{0,0,1}False}},e{\tt)}\rightarrow e\\ \\ \mbox{/\,/\ existential quantification}\\ h,ht\vdash{\color[rgb]{0,0,1}\tt some}~x~{\color[rgb]{0,0,1}\tt in}~a~|~e~~\rightarrow~~e[x\mapsto v_{1}]~{\tt{\color[rgb]{0,0,1}or}}~\cdots~{\color[rgb]{0,0,1}\tt or}~e[x\mapsto v_{n}]\\ \hskip 7.5pt\mbox{if }(ht(a)={\color[rgb]{0,0,1}\tt sequence}\land h(a)=\langle v_{1},\ldots,v_{n}\rangle)\\ \hskip 7.5pt{}\lor(ht(a)={\color[rgb]{0,0,1}\tt set}\land\langle v_{1},\ldots,v_{n}\rangle~\mbox{is a linearization of}~h(a))\end{array}$$

  $$\begin{array}[]{@{}l@{}}{\it deref}(h,a,F)=\begin{array}[t]{@{}l@{}}\mbox{if }a\not\in{\it dom}(h)\mbox{ then }\mathord{\perp}\\ \mbox{elif }{\it length}(F)=1\mbox{ then }(\mbox{if }F\in{\it dom}(h(a))\mbox{ then }h(a)(F)\mbox{ else }\mathord{\perp})\\ \mbox{else }{\it first}(F)\in{\it dom}(h(a))\mbox{ then }{\it deref}(h,h(a)({\it first}(F)),{\it rest}(path))\mbox{ else }\mathord{\perp}\\ \end{array}\\ \\ {\it allBaseAreSets}(h,ht)=\\ \hskip 7.5pt\begin{array}[t]{@{}l@{}}\forall a\in{\it dom}(h),{\it rs}\in{\it rulesets}(ht(a)),{\color[rgb]{0,0,1}\tt self}.F\in{\it nlBase}({\it rules}({\it rs})):\\ {\it deref}(h,a,F)=\mathord{\perp}\lor({\it deref}(h,a,F)\in{\mbox{$\it Address$}}\land ht({\it deref}(h,a,F))={\color[rgb]{0,0,1}\tt set})\end{array}\\ \\ {\it updateVar}(h,{\it rs},a.f,S)=\begin{array}[t]{@{}l@{}}\mbox{if }h(a)(f)\in{\mbox{$\it Address$}}\mbox{ then }\{h(a)(f)\mapsto S\}\\ \mbox{else }\{a\mapsto h(a)[f\mapsto{\it newAddr}({\it rs},a.f,h)],{\it newAddr}({\it rs},a.f,h)\mapsto S\}\end{array}\\ \\ {\it infUpdate}(h,{\it rs},a,{\it args})=\\ \hskip 7.5pt\begin{array}[]{@{}l@{}}\mbox{let }\begin{array}[t]{@{}l@{}}{\it facts}_{B}=\{a.F(v):{\color[rgb]{0,0,1}\tt self}.F\in{\it nlBase}({\it rules}({\it rs}))\land v\in{\it deref}(h,a,F)\}\\ {\it facts}_{L}=\{p(v):p\in{\it dom}({\it args})\land v\in h({\it args}(p))\}\\ {\it result}={\it evalRules}({\it rules}(rs)[{\color[rgb]{0,0,1}\tt self}\mapsto a]\cup{\it facts}_{B}\cup{\it facts}_{L})\\ \theta=\bigcup_{{\color[rgb]{0,0,1}\tt self}.f\in{\it nlDerived}({\it rules}({\it rs}))}{\it updateVar}(h,{\it rs},a.f,{\it result}(a.f))\end{array}\\ \mbox{in }(\theta,{\it result})\end{array}\\ \\ {\it maintain}(h,ht)=\begin{array}[t]{@{}l@{}}\mbox{let }\begin{array}[t]{@{}l@{}}\theta=\bigcup_{a\in{\it dom}(h),{\it rs}\in{\it rulesets}(ht(a))}\pi_{1}({\it infUpdate}(h,{\it rs},a,\{\}))\\ \theta_{T}=\{a\mapsto{\color[rgb]{0,0,1}\tt set}\;|\;a\in{\it dom}(\theta)\land\theta(a)\subseteq{\mbox{$\it Val$}}\})\\ (h^{\prime},ht^{\prime})=(h,ht)\sqcup(\theta,\theta_{T})\end{array}\\ \mbox{in if }(h^{\prime},ht^{\prime})=(h,ht)\mbox{ then }(h,ht)\mbox{ else }{\it maintain}(h^{\prime},ht^{\prime})\end{array}\end{array}$$

  Notation.   In the transition rules, $a$ matches an address, and $v$ matches a value (i.e., an element of $\it Val$).

  $f\cup g$ is the union of functions $f$ and $g$ with disjoint domains. For any functions $f$ and $g$, $f\sqcup g=\{x\mapsto f(x)\;|\;x\in{\it dom}(f)\setminus{\it dom}(g)\}\cup g$. For a function $f$, $f[x\mapsto y]=f\sqcup\{x\mapsto y\}$. When a function $\theta$ is intended to be used to compute an updated version $f\sqcup\theta$ of a function $f$, we refer to $\theta$ as an “update” to $f$.

  Sequences are denoted with angle brackets, e.g., $\langle 0,1,2\rangle\in{\it Int}^{*}$. $s@t$ is the concatenation of sequences $s$ and $t$. ${\it first}(s)$ is the first element of sequence $s$. ${\it rest}(s)$ is the sequence obtained by removing the first element of $s$. ${\it length}(s)$ is the length of sequence $s$.

  Auxiliary definitions.   ${\it new}(c)$ returns a new instance of class $c$, for $c\in{\mbox{$\it ClassName$}}$. When $c$ is the name of user-defined class, ${\it new}(c)$ returns an empty set representing the empty function.

  $$\begin{array}[]{@{}l@{}}{\it new}(c)=\mbox{if }c={\color[rgb]{0,0,1}\tt sequence}\mbox{ then }\langle\rangle\mbox{ else }\{\}\end{array}$$

  ${\it legalAssign}(ht,a,f)$ holds if assigning to field $f$ of the object with address $a$ is legal, in the sense that $a$ refers to an object with fields (not an instance of a pre-defined class without fields), and $a.f$ is not a derived predicate of any rule set. ${\it legalAssign}(ht,a,f)=ht(a)\not\in\{{\color[rgb]{0,0,1}\tt set},{\color[rgb]{0,0,1}\tt sequence}\}\land((a=a_{\it gv}\land a_{\it gv}.f\not\in{\it glblDerived})\lor(a\neq a_{\it gv}\land{\tt{\color[rgb]{0,0,1}self}.f}\not\in{\it nlDerived}(ht(a))))$.

  ${\it methodDef}(c,m,{\it def})$ holds iff $c$ is a user-defined class and either (1) $c$ defines method $m$, and def is the definition of $m$ in $c$, or (2) $c$ does not define $m$, and def is the definition of $m$ in the nearest ancestor of $c$ in the inheritance hierarchy that defines $m$.

  ${\it glblRulesets}$ is the set of names of global rule sets in the program. ${\it rulesets}(c)$ is the set of names of rule sets defined in class $c$ in the program. By definition, ${\it rulesets}(C_{\it gv})={\it glblRulesets}$, and for convenience, we also define ${\it rulesets}({\color[rgb]{0,0,1}\tt set})=\emptyset$ and ${\it rulesets}({\color[rgb]{0,0,1}\tt seq})=\emptyset$. For any rule set name ${\it rs}$ in the program, ${\it rules}({\it rs})$ is the set of rules in that rule set (recall from Section A.1.1 that rule set names have been transformed to be unique across all scopes).

  For a set of rules $R$, ${\it nlBase}(R)$ and ${\it nlDerived}(R)$ are the sets of non-local base predicates and non-local derived predicates, respectively, in $R$. For $c\in{\mbox{$\it ClassName$}}$, ${\it nlDerived}(c)$ is the set of non-local derived predicates in rule sets defined in class $c$. ${\it glblDerived}$ is the set of global variables that are derived predicates in any rule set.

  For a derived predicate $p$ of rule set ${\it rs}$, and heap $h$, ${\it newAddr}({\it rs},p,h)$ selects a fresh address for $p$ of ${\it rs}$; specifically, it returns an address that is not in ${\it dom}(h)$ and is different from ${\it newAddr}({\it rs}^{\prime},p^{\prime},h)$ whenever ${\it rs}\neq{\it rs}^{\prime}\lor p\neq p^{\prime}$. Using function ${\it newAddr}$ to select fresh addresses, instead of selecting them non-deterministically, is inessential but simplifies the definitions of auxiliary functions related to inference in Figure 8 and the transition rule for infer in Figure 10.

  The following five auxiliary functions and relation are defined in Figure 8.

  ${\it deref}(h,a,F)$ returns the value obtained by starting at address $a$ in heap $h$ and dereferencing the sequence $F$ of one or more fields. If $a$ is not an address in ${\it dom}(h)$, or if a field in $F$ is not in the domain of the appropriate object, then ${\it deref}$ returns $\mathord{\perp}$.

  ${\it allBaseAreSets}(h,ht)$ returns true if, in heap $h$ with heap type map $ht$, for each rule set, for each non-local base predicate of the rule set, either it is uninitialized (indicated by ${\it deref}$ returning $\mathord{\perp}$) or its value is a set.

  ${\it updateVar}(h,{\it rs},a.f,S)$ returns an update to the heap that makes variable $a.f$ to refer to a set with content $S$. If the value of $a.f$ is already an address $a^{\prime}$, a set with content $S$ is stored at $a^{\prime}$, otherwise $a.f$ is assigned a fresh address $a^{\prime}$, and a set with content $S$ is stored at $a^{\prime}$.

  ${\it infUpdate}(h,{\it rs},a,{\it args})$ computes an update expressing the result of inference for rule set ${\it rs}$ instantiated with ${\color[rgb]{0,0,1}\tt self}\mapsto a$, with heap $h$ and using ${\it args}$ to obtain values for local variables of $\rightarrow$. ${\it infUpdate}$ returns a pair containing the update to apply to the heap $h$ and a function ${\it result}$ that maps each defined derived predicate in the rule set to its value; a derived predicate is undefined after this inference if it depends on a local variable that is a base predicate whose value is not provided by ${\it args}$. For explicit calls to infer, ${\it args}$ contains values provided by keyword arguments; for automatic maintenance, ${\it args}$ is the empty function. Note that the condition $v\in{\it deref}(h,a,F)$ is false if ${\it deref}(h,a,F)$ is $\mathord{\perp}$; this has the effect that uninitialized base predicates are equivalent to empty sets. ${\it infUpdate}$ uses the auxiliary function ${\it evalRules}(R)$, which evaluates the set of rules $R$ and returns a function from the set of predicates that appear in the rules to their meanings, represented as sets of tuples.

  ${\it maintain}(\theta,\theta_{T},h,ht)$ returns a pair whose first and second components are updates to $h$ and $ht$, respectively, that express the result of automatic maintenance of all rule sets in heap $h$ and heap type map $ht$. For each set of rules that needs to be maintained, it calls ${\it infUpdate}$ to compute an update expressing the result of inference for that rule set, and uses function $\pi_{1}$, which select the first component of a tuple, to extract that update from the tuple returned by ${\it infUpdate}$. It combines the resulting updates using union, since the well-formedness restrictions on programs ensure that these updates have disjoint domains. ${\it maintain}$ uses recursion to repeatedly evaluate all rule sets until a fixed-point is reached.

  Notes.   The transition rules enforce the invariant that each non-local base predicate is either uninitialized or its value is a set. Inference treats uninitialized variables used as base predicates as empty sets. This is consistent with the semantics of Datalog and Prolog, which treats predicates for which no information has been supplied as false for all arguments. This principle is realized implicitly in the set comprehensions defining ${\it facts}_{B}$ and ${\it facts}_{L}$ in ${\it infUpdate}$: the resulting sets do not contain any facts for those base predicates. This principle applies whenever an uninitialized field is encountered in the sequence of field dereferences used to read the value of a base predicate.

  The transition rules include premises that check for run-time errors; in case of an error, the premise is false, and evaluation is stuck. Examples of such errors include trying to select a component from a value that is not a tuple, invoke a non-existent method of an object, read the value of a non-existent (uninitialized) field of an object, assign a value to a derived predicate using an assignment statement, or assign a non-set value to a base predicate. The transition rules check for this error at updates to fields of instances of all classes—not only classes that define rule sets—because base predicates may contain multiple field dereferences.

  Transition rules for methods of pre-defined classes set and sequence are similar in style, so only one representative example is given, for set.add. Note that ${\it maintain}$ needs to be called only in transition rules for methods of set that update the content of the set.

  The transition rule for invoking a method in a user-defined class executes a copy of the method body $s$ that has been instantiated by substituting argument values for parameters.

  The transition rule for an explicit call to infer on a rule set $rs$ with class scope instantiates $rs$ using the target object $a$ for self and values given by keyword arguments for local variables, calls ${\it infUpdate}$ to evaluate the instantiated rule set, and calls ${\it maintain}$ to determine the effects of automatic maintenance. Note that $\theta$ is an update to the heap that updates the values of non-local derived predicates of ${\it rs}$; ${\it result}$ maps each derived predicate of $R$ to its value; $\theta_{\it QNL}$ and $\theta_{\it QL}$ are updates to the heap that together update the values of $a_{1}.f_{1},\ldots,a_{n}.f_{n}$ to contain the query results, with the former handling queries of non-local derived predicates, and the latter handling queries of local derived predicates; and $\theta_{T}$ is an update to the heap type map that updates the types of addresses containing sets created by this call to infer.

  $$\begin{array}[]{@{}l@{}}\mbox{/\,/\ context rule for expressions}\\ \dfrac{h,ht\vdash e\rightarrow e^{\prime}}{(C[e],h,ht)\rightarrow(C[e^{\prime}],h,ht)}\\ \\ \mbox{/\,/\ context rule for statements}\\ \dfrac{(s,h,ht)\rightarrow(s^{\prime},h^{\prime},ht^{\prime})}{(C[s],h,ht)\rightarrow(C[s^{\prime}],h^{\prime},ht^{\prime})}\\ \\ \mbox{/\,/\ field assignment}\\ (a{\tt.}f\;{\tt:=}\;v,h,ht)\\ {}\rightarrow({\color[rgb]{0,0,1}\tt skip},h^{\prime}\sqcup\theta,ht\sqcup\theta_{T})\\ \hskip 7.5pt{}\mbox{if }{\it legalAssign}(ht,a,f)\land h^{\prime}=h[a\mapsto h(a)[f\mapsto v]]\land{\it allBaseAreSets}(h^{\prime},ht)\\ \hskip 7.5pt{}\land(\theta,\theta_{T})={\it maintain}(h^{\prime},ht)\\ \\ \mbox{/\,/\ object creation}\\ (a{\tt.}f\;{\tt:=}\;{\color[rgb]{0,0,1}\tt new}~c,h,ht)\\ {}\rightarrow({\color[rgb]{0,0,1}\tt skip},h^{\prime}\sqcup\theta,ht^{\prime}\sqcup\theta_{T})\\ \hskip 7.5pt\mbox{if }a^{\prime}\not\in{\it dom}(ht)\land a^{\prime}\in{\mbox{$\it Address$}}\land{\it legalAssign}(ht,a,f)\\ \hskip 7.5pt{}\land ht^{\prime}=ht\,[a^{\prime}\mapsto c]\land h^{\prime}=h[a\mapsto h(a)[f\mapsto a^{\prime}],a^{\prime}\mapsto{\it new}(c)]\land{\it allBaseAreSets}(h^{\prime},ht^{\prime})\\ \hskip 7.5pt{}\land(\theta,\theta_{T})={\it maintain}(h^{\prime},ht^{\prime})\\ \\ \mbox{/\,/\ sequential composition}\\ ({\tt{\color[rgb]{0,0,1}skip};}\,s,h,ht)\rightarrow(s,h,ht)\\ \\ \mbox{/\,/\ conditional statement}\\ ({\color[rgb]{0,0,1}\tt if}~{\tt{\color[rgb]{0,0,1}True}:}~s_{1}~{\tt{\color[rgb]{0,0,1}else}:}~s_{2},h,ht)\rightarrow(s_{1},h,ht)\\ \\ ({\color[rgb]{0,0,1}\tt if}~{\tt{\color[rgb]{0,0,1}False}:}~s_{1}~{\tt{\color[rgb]{0,0,1}else}:}~s_{2},h,ht)\rightarrow(s_{2},h,ht)\\ \\ \mbox{/\,/\ for loop}\\ ({\color[rgb]{0,0,1}\tt for}~x~{\color[rgb]{0,0,1}\tt in}~a{\tt:}~s,h,ht)\\ {}\rightarrow({\color[rgb]{0,0,1}\tt for}~x~{\color[rgb]{0,0,1}\tt inTuple}~{\tt(}v_{1},\ldots,v_{n}{\tt):}~s,h,ht)\\ \hskip 7.5pt\mbox{if }(ht(a)={\color[rgb]{0,0,1}\tt sequence}\land h(a)=\langle v_{1},\ldots,v_{n}\rangle)\\ \hskip 7.5pt{}\lor(ht(a)={\color[rgb]{0,0,1}\tt set}\land\langle v_{1},\ldots,v_{n}\rangle~\mbox{is a linearization of}~h(a))\\ \\ ({\color[rgb]{0,0,1}\tt for}~x~{\color[rgb]{0,0,1}\tt inTuple}~{\tt(}v_{1},\ldots,v_{n}{\tt):}~s,h,ht)\\ {}\rightarrow(s[x\mapsto v_{1}];{\color[rgb]{0,0,1}\tt for}~x~{\color[rgb]{0,0,1}\tt inTuple}~{\tt(}v_{2},\ldots,v_{n}{\tt):}~s,h,ht)\\ \\ ({\color[rgb]{0,0,1}\tt for}~x~{\color[rgb]{0,0,1}\tt inTuple}~{\tt():}~s,h,ht)\rightarrow({\color[rgb]{0,0,1}\tt skip},h,ht)\\ \\ \mbox{/\,/\ while loop}\\ ({\color[rgb]{0,0,1}\tt while}~e{\tt:}~s,h,ht)\\ {}\rightarrow({\color[rgb]{0,0,1}\tt if}~e{\tt:}~{\tt(}s{\tt;}~{\color[rgb]{0,0,1}\tt while}~e{\tt:}~s{\tt)}~{\tt{\color[rgb]{0,0,1}else}:}~{\color[rgb]{0,0,1}\tt skip},h,ht)\end{array}$$

  $$\begin{array}[]{@{}l@{}}\mbox{/\,/\ invoke method in pre-defined class (example)}\\ (a{\tt.add(}v_{1}{\tt)},h,ht)\rightarrow({\color[rgb]{0,0,1}\tt skip},h^{\prime}\sqcup\theta,ht\sqcup\theta_{T})\\ \hskip 7.5pt\mbox{if }ht(a)={\color[rgb]{0,0,1}\tt set}\land\nexists a_{\it gv}.f\in{\it glblDerived}:\;a=h(a_{\it gv})(f)\\ \hskip 7.5pt{}\land\nexists a^{\prime}\in{\it dom}(ht),{\color[rgb]{0,0,1}\tt self}.f\in{\it nlDerived}(ht(a^{\prime})):\;a=h(a^{\prime})(f)\\ \hskip 7.5pt{}\land h^{\prime}=h[a\mapsto h(a)\cup\{v_{1}\}]\land(\theta,\theta_{T})={\it maintain}(h^{\prime},ht)\\ \\ \mbox{/\,/\ invoke method in user-defined class}\\ (a{\tt.}m(v_{1},\ldots,v_{n}),h,ht)\\ {}\rightarrow(s[{\color[rgb]{0,0,1}\tt self}\mapsto a,x_{1}\mapsto v_{1},\ldots,x_{n}\mapsto v_{n}],h,ht)\\ \hskip 7.5pt\mbox{if }{\it methodDef}(ht(a),m,{\color[rgb]{0,0,1}\tt def}~m{\tt(}x_{1},\ldots,x_{n}{\tt)}~s)\\ \\ \mbox{/\,/\ invoke {\color[rgb]{0,0,1}\tt infer} on a rule set defined in class scope}\\ (a_{1}.f_{1},\ldots,a_{n}.f_{n}:=a{\tt.}{\color[rgb]{0,0,1}\tt infer(}q_{1},\ldots,q_{n},x_{1}=v_{1},\ldots,x_{k}=v_{k},{\color[rgb]{0,0,1}\tt rules}{\tt=}rs{\tt)},h,ht)\\ \hskip 7.5pt{}\rightarrow({\color[rgb]{0,0,1}\tt skip},h^{\prime}\sqcup\theta^{\prime},ht\sqcup\theta_{T}\sqcup\theta_{T}^{\prime})\\ \hskip 7.5pt\mbox{if }rs\in{\it rulesets}(ht(a))\\ \hskip 7.5pt\begin{array}[]{@{}l@{}}{}\land\forall i\in\{1..n\}:{\it legalAssign}(ht,a_{i},f_{i})\\ {}\land(\forall i\in\{1..k\}:v_{i}\in{\it dom}(ht)\land ht(v_{i})={\color[rgb]{0,0,1}\tt set})\\ {}\land{\it args}=\{x_{i}\mapsto v_{i}\;|\;i\in\{1..k\}\}\\ {}\land(\theta,{\it result})={\it infUpdate}(h,ht,{\it rs},a,{\it args})\\ {}\land\theta_{\it QNL}=\bigcup_{i\in\{1..n\}\mbox{ s.t. $q_{i}$ is a non-local predicate }{\color[rgb]{0,0,1}\tt self}.f}\{a_{i}\mapsto h(a_{i})[f_{i}\mapsto(h\sqcup\theta)(a)(f)]\}\\ {}\land\theta_{\it QL}=\bigcup_{i\in\{1..n\}\mbox{ s.t. $q_{i}$ is a local predicate}}\{\begin{array}[t]{@{}l@{}}a_{i}\mapsto h(a_{i})[f_{i}\mapsto{\it newAddr}({\it rs},q_{i},h)],\\ {\it newAddr}({\it rs},q_{i},h)\mapsto{\it result}(q_{i})\}\end{array}\\ {}\land\theta_{T}=\begin{array}[t]{@{}l@{}}\{a\mapsto{\color[rgb]{0,0,1}\tt set}\;|\;a\in{\it dom}(\theta)\land\theta(a)\subseteq{\mbox{$\it Val$}}\}\\ {}\cup\{a\mapsto{\color[rgb]{0,0,1}\tt set}\;|\;a\in{\it dom}(\theta_{\it QL})\land\theta_{\it QL}(a)\subseteq{\mbox{$\it Val$}}\}\end{array}\\ {}\land h^{\prime}=h\sqcup\theta\sqcup\theta_{\it QNL}\sqcup\theta_{\it QL}\sqcup\theta_{U}\\ {}\land{\it allBaseAreSets}(h^{\prime},ht\sqcup\theta_{T})\\ {}\land(\theta^{\prime},\theta_{T}^{\prime})={\it maintain}(h^{\prime},ht\sqcup\theta_{T})\end{array}\end{array}$$

  Executions.   An execution is a sequence of transitions $\sigma_{0}\rightarrow\sigma_{1}\rightarrow\sigma_{2}\rightarrow\cdots$ such that $\sigma_{0}$ is the initial state of the program, given by $\sigma_{0}=(s_{0},\{a_{\it gv}\mapsto\{\}\},\{a_{\it gv}\mapsto C_{\it gv}\})$, where $s_{0}$ is the top-level statement that appears in the program after the rule set definitions and class definitions, and $a_{\it gv}$ is the address of the object introduced by the transformation that eliminates global variables (see Section A.1.1).

  Execution of a program may eventually (1) terminate (i.e., the statement in the first component of the state becomes skip, meaning that there is nothing left to do), (2) get stuck (i.e., the statement is not skip, and the process has no enabled transitions, meaning an error in the program), or (3) run forever (due to an infinite loop or infinite recursion).

  Appendix B Powerful optimizations

  Efficient inference and queries using rules is well known to be challenging in general, and especially so if it is done repeatedly to ensure the declarative semantics of rules under updates to predicates. Addressing the challenges has produced an extensive literature in several main areas in computer science—database, logic programming, automated reasoning, and artificial intelligence in general—and is not the topic of this paper.

  Here, we describe how well-known analyses and optimizations can be used together to improve the implementation of the overall language as well as the rule language, giving a systemic perspective of all main optimizations for efficient implementations. There are two main areas of optimizations.

  The first area is for inference under updates to the predicates used. There are three main kinds of optimizations in this area: (1) reducing inference triggered by updates, (2) performing inference lazily only when the results are demanded, and (3) doing inference incrementally when updates must be handled to give results:

  Reducing update checks and inference.

  In the presence of aliasing, it can be extremely inefficient to check, for all rule sets after every update, that the update is not to a derived predicate of the rule set and whether a call to infer on the rule set is needed, not knowing statically whether the update affects a base predicate of the rule set. Alias analysis, e.g., [21, 20], can help reduce such checks by statically determining updates to variables that possibly alias a predicate of a rule set.

  Demand-driven inference.

  Calling infer after every update to a base predicate can be inefficient and wasteful, because updates can occur frequently while the maintained derived predicates are rarely used. To avoid this inefficiency, infer can be called on demand just before a derived predicate is used, e.g., [17, 54, 36], instead of immediately after updates to base predicates.

  Incremental inference.

  More fundamentally, even when derived predicates are frequently used, infer may be called repeatedly on slightly changed or even unchanged base predicates, in which case computing the results from scratch is extremely wasteful. Incremental computation can drastically reduce this inefficiency by maintaining the values of derived predicates incrementally, e.g., [22, 58].

  The second area is for efficient implementation of rules by themselves, without considering updates to the predicates used. There are two main groups of optimizations.

  Internal demand-driven and incremental inference.

  Even in a single call to infer, significant optimizations are needed.

  In top-down evaluation (which is already driven by the given query as demand), subqueries can be evaluated repeatedly, so tabling [64, 13] (a special kind of incremental computation by memoization) is critical for avoiding not only repeated evaluation of queries but also non-termination when there is recursion.

  In bottom-up evaluation (which is already incremental from the ground up), demand transformation [65, 66], which improves over magic sets [6, 1] exponentially, can transform rules to help avoid computations not needed to answer the given query.

  Ordering and indexing for inference.

  Other factors can also drastically affect the performance of logic queries in a single call to infer [48, 35].

  Most prominently, in dominant logic rule engines like XSB, changing the order of joining hypotheses in a rule can impact performance dramatically, e.g., for the transitive closure example, reversing the two hypotheses in the recursive rule can cause a linear factor performance difference. Reordering and indexing [38, 36] are needed to avoid such severe slowdowns.