Semantically lifted programs integrate declarative ontologybased knowledge modelling into imperative programming. In this approach, each state of a program is mapped into an OWL knowledge base (KB) and enriched with user-de ned knowledge; the resulting KB can be accessed from the program using standard Semantic Web queries. The result of a query, however, should conform the type system of the program. We present a technique for checking type conformance statically, which is based on query containment over OWL KBs. We then discuss an approximation method for type checking, which exploits concept subsumption rather than containment and hence allows for an e cient implementation using existing tools. Finally, we describe our implementation of semantically lifted programs with static type checking in language SMOL.
Semantic lifting [
Semantic lifting is convenient when static expert domain knowledge in the
form of ontologies should tightly interact with the dynamic setting of a program's
1 class Platform(List<Server> serverList) ... end
2 class Server(List<Task> taskList) ... end
3 class Scheduler(List<Platform> platformList)
4 Unit reschedule()
5 List<Platform> l:=access("SELECT ?x WHERE {?x a Overloaded}");
6 this.adaptPlatforms(l);
7 end
8 end
runtime. In particular, as illustrated in Fig. 1, semantic lifting allows us to
integrate an external ontology into a program directly, without reimplementing
it. The SMOL program in this example models a scheduling mechanism for a
cloud system: a platform has a list of servers, each of which in turn have a list of
tasks, and a scheduler retrieves the list of all overloaded platforms by executing
a SPARQL query on its own state lifted to an OWL 2 DL [
The example in Fig. 1 also shows that the interaction between ontology reasoning and program states is challenging to handle for a type system. In particular, for type safety of the access assignment, one must verify that the query returns only instances of class Platform. However, since Overloaded is not de ned within the program itself, a system needs to analyse the interaction between the state lifting mechanism, the external ontology, and the query for such veri cation. Moreover, the situation can be more complicated if the query is parametrised by program expressions evaluated in the current state.
Type checking in SMOL of Kamburjan et al. [
Practical applicability of these results is limited by the lack of implemented
algorithms for query containment under expressive entailment regimes, such as
the OWL 2 regimes [
Our implementation of SMOL with a static type system based on our results is available at github.com/Edkamb/SemanticObjects.
Related Work. SMOL is an imperative programming language that uses SPARQL
and OWL as declarative sublanguages [
Description Logics (DLs) [
Query Answering. A conjunctive query (CQ ) Q(x) with answer variables x is an expression 9y: ', where the body ' is a conjunction of atoms C(t), d(t), P (t; t0) and (t = t0) with C 2 C, d 2 D, and P 2 R [ RD, while t; t0 either variables in x [ y or constants in I [ D. CQ Q(x) is unary if jxj = 1. CQ Q(x) may be written as just Q when x is immaterial. A tuple s of constants in I [ D is an answer to Q over an interpretation I if there is : x [ y ! I [ D such that (x) = sI and each atom in ' holds in I|that is, (t) 2 CI , (t) 2 dD, ( (t); (t0)) 2 P I , and (t) = (t0) for each C(t), d(t), P (t; t0), and (t = t0) in ', respectively. A tuple is a (certain) answer to Q over a KB K if it is an answer to q over each model of K.
RDF, OWL, and Entailment Regimes. As mentioned above, SROIQ(D)
KBs are in practice represented as OWL 2 DL ontologies in RDF format, where
both TBox and ABox are written as an RDF graph consisting of triples of IRIs,
literals (i.e., concrete datatype values), and blank nodes (i.e., named
placeholders). In turn, CQs can be translated to a core fragment of the RDF query
language SPARQL. Same as RDF, OWL and SPARQL are mature technologies
standardised by W3C, with e cient implementations of concept subsumption
checking and query answering, respectively. However, computing all certain
answers to CQs over KBs as de ned above has high computational complexity
(in fact, it is not even known whether the corresponding problem is decidable).
So, SPARQL engines instead realise so-called entailment regimes for query
answering over OWL ontologies. We refer to the literature for the speci cations
of existing entailment regimes [
In this section, we present the version of Semantic Micro Object Language SMOL
that extends the original SMOL of Kamburjan et al. [
Syntax First, we present the syntax of typed SMOL. In a nutshell, it is a core of standard Java with the only distinctive feature being access expression, which, as we will see later, allows us to query a SROIQ(D) KB exported from the current state of the program evaluation and extended with axioms de ned by a user. De nition 1 (Typed SMOL Surface Syntax). A CQ template is a CQ with some non-answer variables having special form %i with i 1. The syntax of SMOL is given in Fig. 2, where C ranges over class names, f over classes' elds, m over classes' method names, v over variables, Q over unary CQ templates, and n over (the literals representing the elements of ) D; the rst : : : denotes the datatypes in D besides Int, String and Unit, and the second the standard operations over the datatypes besides + and .1
A program consists of classes and a main block as the entry point for execution. A class declares lists of typed elds and methods, and may also extend another class. A method has a return type and a list of parameters. Besides classes and datatypes in D, types include lists, which, as we will see, are essentially
style generic types), which are inessential for this paper and omitted for brevity. Prog ::= Class main s end Class ::= class C extends C (T f) Met end Met ::= T m (T v) s end T ::= C j List<T> j Unit j Int j String j : : : s ::= [T] l:=rhs; j s s j if e then s else s end s
j while e do s end s j return e; j skip;
l ::= this.f j e.f j v rhs ::= e j new C(e) j e.m(e) j access(Q; e)
e ::= null j l j n j e + e j e e j : : :
Programs, classes
Methods, types
Statements
Locations, RHS
Expressions
classes with special structure parametrised by other types. The statements are
in an imperative language similar to standard WHILE-languages [
In essence, a con guration consists of three components: class de nitions CT, a list of objects ob with unique identi ers, and a stack of processes prc corresponding to nested method calls. Besides its unique identi er X, each object has the corresponding class name C and memory of elds. In turn, a process has an id i, the object identi er X to resolve this, the runtime statement rs that is executing, and memory of local variables. For the process on the top of the stack, the runtime statement is the currently executed normal statement; for all other processes, the runtime statement is of the form l stack, which denotes that location l is waiting for a return value from the next process on the stack.
As we will see below, SMOL semantics is such that the classes CT of each reachable con guration of a program Prog are always the same. In particular, CT includes all the classes of Prog as well as several implicit classes:
`process' for consistency with the previous work [
Thus, we call each con guration with such CT a con guration of Prog.
The evaluation of a program Prog starts in an initial con guration|that is, the con guration of Prog where the objects and processes are such that Entry is instantiated as an object with its only method initiating the only process in the stack, and Null as an object with identi er NULL to evaluate null expression. Further details of this con guration are standard and inessential for the paper.
As mentioned above, the operational semantics of SMOL is a set of conditional
rewrite rules describing transitions from one con guration into another. The
exact form of most of these rules is however immaterial to this paper. Thus, we
refrain from introducing them all of them in the de nition below, referring to
a technical report [
Second, Ans is a translation of CQ answers under an entailment regime into the structures of the runtime semantics. Formally, let s1; : : : ; sn be the answers to a unary CQ Q over a KB K under an entailment regime er in arbitrary order. Let the si have a common type T if either T is a datatype and all the si are its values, or T is the most speci c class such that all the si are object identi ers of objects of T. If the si have a common type T, then Anser(K; Q) is the pair (ob; Y1), where ob is the list of n new objects (List<T>; i)Yi , i = 1; : : : ; n, with each i(head) = si, and with i(tail) = Yi+1 if i < n and n(tail) = NULL (if n = 0 we take ob = ; and Y1 = NULL). Otherwise Anser(K; Q) is unde ned. De nition 3 (Transition System). The relevant rules of the SMOL transition system are given in Fig. 3, where Q v is the CQ obtained from a CQ template Q by substituting each variable %i in Q by element i of a list v, while TCT is a TBox constructed from a set of classes CT, Tuser is a user-de ned TBox, and AConf is an ABox constructed from con guration Conf; the construction is done via the semantic lifting mechanism, which is explained in Section 3.3. Recall also that the sets of classes in con gurations are always the same on the both sides of every transition rule. Thus, for readability, we mention CT over ! in the rules rather than in the con gurations on the sides of !.
Rule (e-av) assigns the evaluation of an expression to a local variable. In the rst premise, l is evaluated to a variable in the context of the object identi ed by X, the object of the current process. In the second, expression e is evaluated to a value v. In the conclusion, the assignment is consumed and object Y is updated JlKX ;ob = v
JeKX ;ob = v ob prc; (X; s; [v 7! v])i (acc-av)
JlKX ;ob = v ob prc; (X; l:=access(Q; e); s; )i | C{onzf
Anser (TCT [ Tuser; AConf); Q JeKX ;ob
CT ! }
= (ob0; Y) ob; ob0 prc; (X; s; [v 7! Y])i by setting f to v. Rule (acc-av) similarly assigns a list constructed by Ans from the CQ answers to a local variable (analogous rules (e-af) and (acc-af) assigning to a eld|that is, when the expression is evaluated to a identi er- eld pair|are omitted). Each rule applies only if the evaluation of its e or Ans is de ned.
A runtime con guration for which no rule is applicable is terminated. A
terminated runtime con guration with the empty stack is successfully terminated,
otherwise it is stuck. Thus, a program may get stuck in case of type mismatches
in assignments and expression evaluations, null access, and similar errors. The
semantics of (untyped) SMOL of Kamburjan et al. [
TBox TCT for classes CT consists of three parts: (1) the axioms describing the language primitives|that is, the structure of classes, elds, and methods, as well as relationships between them; (2) the axioms describing the runtime primitives|that is, the structure of objects, processes, and local variables, as well as relations between them;
(1) 9HasField :> v Class 9HasMethod :> v Class (2) 9RunsOnObj :> v Proc 9NextOnStack :> v Proc (3) 9HasField :> v Field 9HasMethod :> v Method 9RunsOnObj :> v Object 9NextOnStack :> v Proc funct(NextOnStack )
Class(aC); Var (av); HasField (aC; af); Field (af); HasMethod (aC; am); Method (am) for each class C in CT, and each eld f, method m and variable v in C
(3) the axioms describing the program itself|that is, the class hierarchy and the internal structure of classes, including elds, methods, and their local variables and statements, as well as relationships with the previous parts. Examples of axioms in all three parts is given in Fig. 4 (concept and role names are self-explanatory; some axioms are written as ABox assertions for readability, and they can be written as TBox inclusions between nominals as usual). Observe here, that only Part (3) depends on the program (and classes CT), while Parts (1) and (2) describe the SMOL syntax and semantics. Note also that TCT does not depend on a particular con guration; since CT does not change during execution, so does not TCT, and hence we can use TCT for static type checking in Section 4.
ABox AConf is constructed from a con guration Conf by mapping the objects ob and the stack prc of processes in Conf to a set of assertions. Example assertions of AConf are given in Fig. 4, where underlined individuals are evaluation-speci c.
Finally, the user-de ned Tuser can be an arbitrary TBox such that TCT [ Tuser
is in SROIQ(D) (as a side comment, note that TCT presented above does not use
the full functionality of SROIQ(D) and falls inside a weaker logic DLLiteA);
besides this, Tuser should be static|that is, can mention concepts, roles, and
individuals of TCT, but does not change throughout execution and hence does not use
the evaluation-speci c individuals of AConf. Our results in Section 4 require Tuser
to be consistent with the lifting mechanism|that is, the KB (TCT [ Tuser; AConf)
to be consistent for every CT and Conf. This requirement is reasonable since it
ensures meaningful CQ answering: if the KB is inconsistent, then each constant
is a certain answer to each unary CQ. It can be guaranteed, for example, by
ensuring that Tuser is a conservative extension of every TCT [
As mentioned above, the original formulation of SMOL [
Subject Reduction: If a well-typed con guration makes an execution step, then the resulting con guration is also well-typed.
Additionally, one needs to ensure that the initial con guration is well-typed.
We use well-typedness based on the following property of adherence. De nition 4. The typing function of a program Prog is the function mapping every location (i.e., a eld, variable, or parameter) of Prog to the type of its declaration in Prog. A con guration is well-typed if it adheres to |that is, if the value of each location l is a DE of type (l).
The goal of static type checking is to verify Local Progress and Subject
Reduction without running the program|that is, without applying the transition
system of De nition 3. Instead, much simpler type judgement rules are applied
to each of the program statements independently (which is sometimes called
`on the surface syntax'), and their applicability to each statement ensures type
safety of the program in the runtime. In the following De nition 5, we give type
judgement for access statements based on a standard data and knowledge base
property, namely query containment with respect to a TBox. We refrain form
giving these rules for all other cases, since they are standard [
So, as usual for static type checking using type judgement [
next straightforward theorem, which is the main result of this paper, shows that such applicability guarantees Local Progress and Subject Reduction for con gurations with access statements. Together with standard similar results for other statements, this implies type safety of programs with all statements labelled by appropriate type judgement rules.
Theorem 1. Let CT be class de nitions of a program Prog, be the typing function of Prog, and Tuser a TBox consistent with the lifting mechanism. Then, for each reachable con guration conf of Prog that adheres to and has statement l:=access(: : :) on top of the stack of processes such that `eTrCT[Tuser l:=access(. . . ) : Unit is derived by Rule ( acc-type), there exists a con guration conf0 of Prog that adheres to such that conf ! conf0 by Rule ( acc-av) in Fig. 3.
For example, consider the following access statement with a CQ template: List<C> l:=access("9%1: x = %1"), Obj);: Assuming that Obj is an object of class C' and C is also a class, type judgement of Rule (acc-type) for this statement boils down to checking containment 9%1: (x = %1) ^ ClassC'(%1) eTrCT[Tuser ClassC(x), which holds if and only if C' is a subclass of C (assuming that regime er takes atomic concept inclusions ClassC v ClassC0 in TCT into account).
Theorem 1 provide a ne-grained, but only su cient condition for type safety
of access statements, while necessity cannot be guaranteed since not all ABoxes
correspond to con gurations. Moreover, its applicability is limited in practice
since, as far as we are aware, there are no algorithms and tools for checking CQ
containment over SROIQ(D) under non-trivial entailment regimes. To
overcome this, we next present a stronger su cient condition, which is based on
concept subsumption rather than query containment under entailment regimes.
This approach is advantageous since concept subsumption is a main reasoning
task for DLs, and there are practical systems (e.g., HermiT [
The following straightforward theorem uses of an adaptation of concept subsumption to unary CQs: a unary CQ Q is subsumed by a concept C with respect to a KB (or a TBox) K, written Q vK C, if sI 2 CI for each certain answer s to Q over K and each model I of K. For brevity, the theorem is stated only for assigned locations of class (or list) types; the case of datatypes is analogous. Theorem 2. Theorem 1 holds if Rule ( acc-type) is replaced by Rule ( acc-approx-type), which is the same as Rule ( acc-type) except that the containment in the premise is replaced by existence of a concept C and two subsumptions Q0 vT C and C vT ClassT0 , where Q0 = 9y: ' ^ ST1 (%1) ^ ^ STn (%n) .
To apply this theorem and Rule (acc-approx-type) in practice, we can syntactically construct a concept C from the query Q0 using some technique that guarantees the rst subsumption to hold, and then check the second subsumption by a DL reasoner. A more speci c (with respect to vT ) concept C ensures more ne-grained su cient condition for type-safeness. However, unless Q0 is equivalent (with respect to vT ) to a concept, there is no most speci c such C. Thus, there may be many techniques for constructing C from the query.
A reasonable choice is to take a repetition-free unravelling of Q0; for
datatypefree queries, it is the concept equivalent, with respect to v;, to a maximal
constant-free query Q00 that is tree-shaped and has a homomorphism to Q0 that
does not identify atoms (cf. the rolling up of Horrocks and Tessaris [
Our SMOL implementation is available at github.com/Edkamb/SemanticObjects;
it provides an ability to generate full TBox TCT and ABox AConf, as well as to
link arbitrary Tuser. The language itself is implemented as an interpreter, using
ANTLR [
We have developed a method to ensure static type safety in semantically lifted programs. We have shown that the use of queries as an interface between the imperative and declarative parts of SMOL programs allows us to reduce type safety to query containment with respect to ontologies, which can in turn be approximated by concept subsumption. Due to lack of tools for such containment, our implementation of SMOL realises type checking using the approximating approach. We anticipate, however, that this new application of containment will initiate further theoretical and practice-oriented research in this direction. We emphasise that, for our application, we only need a special case of containment, where the containing query is always an instance query. For future work, we plan to design such containment algorithms, as well as to investigate how program accessibility modi ers (e.g., private) interact with semantic lifting. Acknowledgements. This work was supported by the Research Council of Norway via the PeTWIN project (Grant Nr. 294600).