Domain-specific Unification

Unification is the process of computing a substitution θ, a function from variables to terms, that unifies two terms s and t such that sθ = tθ. It is an essential ingredient of the proof procedure in logic programming (i.e., resolution). The domain-specific unification procedure complements the example-based interpretations of a template term.

Consider the following Java program and a logic query with a template term that exemplifies the prototypical implementation of a class with a getter method: 

class Person {
  private Integer age;  
  public Integer getAge() {  return this.age; }
  public Integer notGettingAge(Integer age) {  return age; }
}

if jtClassDeclaration(?c){
     class ?className {
       private ?fieldDeclarationType ?fieldName;
       ?modifierList ?returnType ?methodName(?parameterList) {
         return ?fieldName;
       }
     }
   }

The occurrences of ?fieldName on line 9 and line 11 substitute for the name of a field and the operand of a return-statement respectively. Through these occurrences, the template term exemplifies that the method must return the value of the field. Assume for a moment that the name of the field and the operand of the return statement are both reified as string constants. Using the general-purpose unification procedure, method notGettingAge(Integer) from above would be reported as a match for the template term. In this match, each occurrence of ?fieldName is bound to the same string.  This method is, however, not a getter method. The definition of the field is shadowed by the parameter of the method. Getter method getAge(), on the other hand, would not match under any interpretation. The reification of its operand (assumed to be the string 'this.age') does not unify with the reification of the field name (assumed to be the string 'age'). 

The domain-specific unification procedure therefore treats reified program elements different from other terms. Unifying two reified program elements can succeed where the general-purpose unification procedure fails. Implicit implementation variants (i.e., those implied by the semantics of the programming language) of the same pattern characteristic unify. To this end, the domain-specific procedure consults static analyses when unifying reified program elements. To determine whether an unqualified and fully qualified type should unify, for instance, a semantic analysis takes the import declarations into account of the compilation units in which they reside. A points-to analysis increases the amount of implementation variants that are recalled. When expressions are unified, for instance, syntactic deviations are allowed as long as they may evaluate to the same object at run-time. Users benefit from the results of these analyses without being exposed to their intricate details.