Illogical, captain!

After the introductory blog posts on the importance of modeling, the concept of model queries (with OCL and EMF-IncQuery) and model evolution, I demonstrated the translation of OCL expressions into the graph pattern language of EMF-IncQuery, and outlined the general translation patterns in two consecutive posts.

The current post will place the language of EMF-IncQuery in a broader context, show aspects where it its expressive power superior to certain other approaches, and where the current implementation needs to be extended.

Propositions over models

The basic, elementary statements (so-called atomic formulas) that can be formulated in EMF-IncQuery (or most other query approaches) are the following:

• a given model element is of a certain type,
• there is a reference of a given type pointing from a given model element to another object, or to an attribute value,
• two model elements are different / the same.

There are examples to be found of all three kinds of elementary constraints in the following pattern:

pattern translated(cl: SchoolClass, s1: Student, s2: Student) = {
  SchoolClass.students(cl, s2);
  s1 != s2;
}

The trick is that query definitions can compose such atomic statements using so-called Boolean / logical connectives:

• conjunction / "and": all of the following is true,
• disjunction / "or": at least one of the following is true,
• negation / "not": it is not true that...

The previous sample pattern contained the conjunction of several pattern constraints - there is no special syntax to indicate the "and" connective. The following earlier example shows the usage of disjunction:

pattern namesInClass(self: SchoolClass, x:EString) = {
  SchoolClass.students.name(self, x);
} or {
  SchoolClass.homeroomTeacher.name(self, x);
}

While negation is exemplified by another one:

pattern nonHomeroomTeacher(self: SchoolClass, x: Teacher) = {
  SchoolClass.courses.teacher(self, x);
  neg {
    SchoolClass.homeroomTeacher(self, x);
  }
}

These types of connectives can express a certain range of composite formulas over the elementary statements discussed before, which corresponds to a famous level of expressive power called propositional calculus.

The language of EMF-IncQuery supports non-recursive pattern composition as well. It is a convenient and concise way of structuring and reusing queries. By itself, composition does not increase the expressive power, since any pattern composition can be "flattened", i.e. the called pattern copied into the calling one. For instance, the following form of the nameConflicts query...

pattern nameConflicts(clazz: SchoolClass, student1: Student, student2: Student, name: EString) = {
  find namedStudentOfClass(clazz, student1, name);
  find namedStudentOfClass(clazz, student2, name);
  student1 != student2;
} 
pattern namedStudentOfClass(clazz, student, name) = {  
  SchoolClass.students(clazz, student);
  Student.name(student, name);
}

... can be flattened into this single pattern:

pattern nameConflicts(clazz: SchoolClass, student1: Student, student2: Student, name: EString) = {
  SchoolClass.students(clazz, student1);
  SchoolClass.students(clazz, student2);
  student1 != student2;
  Student.name(student1, name);
  Student.name(student2, name);
}

The power of first order logic

There are many useful queries, however, that cannot be expressed using these language elements only. The addition of quantifiers allows us to express properties relating to all model elements, as opposed to single ones, resulting in the more expressive logic calculus first-order logic:

• quantification "exists"/"for all": it is possible / not possible to substitute model elements for the given variables so that the following is true/false

The language of EMF-IncQuery has two forms of quantification, the more important of the two is the ability to restrict the set of parameters of a pattern to a narrower set of variables. Take for example the following query :

pattern nonHomeroomTeacher2(self: SchoolClass, x: Teacher) = {
  SchoolClass.courses.teacher(self, x);
  neg find homeroomTeacher(x); 
}

pattern homeroomTeacher(x: Teacher) = {
    SchoolClass.homeroomTeacher(y, x);
}

The pattern "nonHomeroomTeacher2" expresses that teacher x lectures school class self , and is not the homeroom teacher of any classes (that's quantification!). Contrast with the pattern "nonHomeroomTeacher" shown earlier, which states that teacher x lectures school class self , and is not the homeroom teacher of the same class self.

The second form of quantification is basically just a notational shorthand with the same ultimate effect, without requiring us to modify the called pattern:

pattern nonHomeroomTeacher2(self: SchoolClass, x: Teacher) = {
  SchoolClass.courses.teacher(self, x);
  neg find homeroomTeacher(x, _); 
}
pattern homeroomTeacher(y:SchoolClass, x: Teacher) = {
    SchoolClass.homeroomTeacher(y, x);
}

Note there is a very wide range of formalisms, such as relational calculi, that have the expressiveness of first-order logic over a given set of atomic formulas - in this sense, the previousdly discussed elements of the graph pattern language are equivalent to many other languages used in computer science.

In particular, a large part of OCL - though not the entire language - can be expressed in first-order logic. The OCL to graph pattern translation shown in previous blog posts involved mostly, but not exclusively, these fragments of the language.

An interesting property of first-order logic is that even with all this expressive power, it is still manageable in some sense. For example, there are automated theorem provers that can check e.g. whether it is possible for a given query (first-order formula) to have results in any instance model. Note that this is a much harder task than finding the results of a query over a specified instance model, which is what query engines do.

Theories for attributes

In addition to the model structure of objects and their relationships, the domains of various attributes may introduce relations themselves, such as "addition" and "greather than" in case of integers, or "concatenation" in case of character strings. Many of these do not admit a practical and complete first order axiomatization, meaning that the aforementioned automated theorem provers cannot prove all theorems involving e.g. numerical equation systems. Fortunately, model querying does not have to involve the most difficult cases of equation solving, and theorem provers can be extended by so-called theories covering these domains.

As for EMF-IncQuery, statements about attributes can be made in check expressions:

pattern importantCourse(c: Course) = {
    Course.weight(c, weight);
    check(weight > 8)
}

OCL expressions also support such Boolean-valued data checks, and more: the result of such a computation can be the result of an OCL expression. Currently, the EMF-IncQuery tool does not implement this capability, but the corresponding eval language element has already been designed and published:

pattern courseTuitionFee(c: Course, fee) = {
    Course.weight(c, weight);
    fee == eval(weight * 50.0);
}

My colleagues Ágnes Barta, Ákos Horváth, Oszkár Semeráth, Zoltán Szatmári and Dániel Varró are currently investigating the translation of OCL into logic statements for which automated theorem proving can be applied. This is a follow-up of previous research on determining whether a given metamodel is satisfiable at all.

Beyond first order logic

EMF-IncQuery supports at least two additional features that are beyond the expressive power of first order logic, and cannot simply be added by "theories":

• Transitive closure
• Aggregation / accumulation

These have been covered in the preceding blog posts. Note that the current implementation of EMF-IncQuery provides partial support for the language proposal in both cases. Note also that OCL is more expressive in terms of collection accumulation.

Acknowledgement: this research was realized in the frames of TÁMOP 4.2.4. A/1-11-1-2012-0001 „National Excellence Program – Elaborating and operating an inland student and researcher personal support system”. The project was subsidized by the European Union and co-financed by the European Social Fund.