Katja Example: Formulas

This example demonstrates the following additional Katja features:

  • Supports definition of lists and their subtype relation (called variants).
  • Supports the concept of term positions, i.e. the notion of location of a term contained in a much larger term.
  • Supports the navigation on terms using positions.
  • Supports the iteration over terms in pre- or post-order, using positions.
  • Supports to conveniently replace small pieces of data deeply embedded in a larger term by using positions.

Specification

The definition of first-order predicate logic formulas starts as usual:

specification Formulas

backend java {
    package Logic
    import java.lang.Integer
    import java.lang.String
}

The important difference to the first example is the root keyword, which defines a host of new sorts, representing (in this case) all possible term position in a Formula. The sorts are created by using the name of the corresponding term sort and appending the supplied suffix, in this case Pos:

root Formula Pos

external Integer
external String

Formula    ( Expression top )

Expression = False     ( )
           | Implies   ( Expression left, Expression right )
           | Not       ( Expression expr )
           | Predicate ( String name, Parameters vars )
           | Quantifier

Quantifier = Forall    ( Variable vari, Expression expr )
           | Exists    ( Variable vari, Expression expr )

Parameters * Variable

Variable   ( Integer index )

Also new is the explicit definition of a list and the definition of two variants. A variant is a supertype of the specified sorts. For convenience it is possible to define tuple sorts within the variant definition.

The specification is contained in the formula.katja. If you do not wish to compile the specification yourself you can download the library Formulas.jar and the common library katja.common.jar.

Sample Java Code

The example was part of a tool demo submitted to LDTA’05. Since then a lot of technical details have changed for Katja, but the general concept of Katja remained the same. So have in mind that some aspects of the details of the Java code have changed. (The changed are of course already incorporated into this example.)

The example source starts as usual:

import static Logic.Formulas.*;
import Logic.*;

public class Bindings {
    public static void main(String... args) {
        Formula formula = Formula(Implies(
            Exists(Variable(0), Forall(Variable(1),
                Predicate("p", Parameters(Variable(0), Variable(1))))),
            Forall(Variable(1), Exists(Variable(0),
                Predicate("p", Parameters(Variable(0), Variable(1)))))));

After creating an example formula, which would normally be an input to our program, e.g. created by a parser, we can now make the transition to term positions. We do this by using the a constructor for the specified root position sort:

        FormulaPos pos = FormulaPos(formula);

We are now able to navigate on the term, downwards as well as upwards, iterate over it, etc. We then pass it to an inspection method, which just prints out details of variable bindings:

        printAllBindings(pos);

        System.out.println();

To demonstrate manipulations of larger terms, we also call a normalization method, which rewrites the formula. Then we print the bindings again, to get a glimpse at the changes made:

        pos = normalize(pos);
        printAllBindings(pos);
    }

The boundTo method exploits the ability to walk upwards in a term, to determine the binding quantifier (if any) of the variable. Note that we can give the boundTo method a very expressive signature. It reflects that the parameter is the position of a variable in a larger term and that its result will be the position of a quantifier.

    public static QuantifierPos boundTo(VariablePos variablePos) {
        for(SortPos pos = variablePos; pos != null ; pos = pos.parent()) {
            if(pos instanceof QuantifierPos &&
                ((QuantifierPos) pos).vari().termEquals(variablePos))
                return (QuantifierPos) pos; // binding is found
        }
        return null; // unbound Variable
    }

The method uses the parent method to navigate upwards till we reach a matching quantifier or the root of the enclosing term is reached, in which case the variable is unbound.

The printAllBindings now uses the preOrder method to iterate over all positions in the formula and invokes boundTo whenever a variable is reached, which is not directly in a quantifier:

    public static void printAllBindings(FormulaPos formulaPos) {
        for(SortPos pos = formulaPos; pos != null; pos = pos.preOrder()) {
            if(!(pos instanceof VariablePos)) continue;
            if(pos.parent() instanceof QuantifierPos) continue;
            VariablePos v = (VariablePos) pos;
            System.out.println(pos + " is bound to " + boundTo(v));
        }
    }

Finally, the normalize method uses the replace method to replace the term at the current position with another one. Note that by using a post-order iteration this time, we apply the transformation bottom-up, such that a duplicated part of the formula is not normalized twice. The method normalizes existential quantifiers to universal ones:

    public static FormulaPos normalize(FormulaPos formulaPos) {
        SortPos last = null;
        for(SortPos pos = formulaPos.postOrderStart(); pos != null;
                last = pos, pos = pos.postOrder()) {
            if(pos instanceof ExistsPos) {
                Exists exists = ((ExistsPos) pos).term();
                pos = (SortPos) pos.replace(Implies(Forall(exists.vari(),
                        Implies(exists.expr(), False())), False()));
            }
        }
        return (FormulaPos) last;
    }
}

The listing of the program is found in the file Bindings.java. The output of the program is as follows (the dots mark parts which where cut out for readability):

Variable( 0 )@Formula.0.0.1.1.1.0 is bound to Exists( ... )@Formula.0.0
Variable( 1 )@Formula.0.0.1.1.1.1 is bound to Forall( ... )@Formula.0.0.1
Variable( 0 )@Formula.0.1.1.1.1.0 is bound to Exists( ... )@Formula.0.1.1
Variable( 1 )@Formula.0.1.1.1.1.1 is bound to Forall( ... )@Formula.0.1

Variable( 0 )@Formula.0.0.0.1.0.1.1.0 is bound to Forall( ... )@Formula.0.0.0
Variable( 1 )@Formula.0.0.0.1.0.1.1.1 is bound to Forall( ... )@Formula.0.0.0.1.0
Variable( 0 )@Formula.0.1.1.0.1.0.1.0 is bound to Forall( ... )@Formula.0.1.1.0
Variable( 1 )@Formula.0.1.1.0.1.0.1.1 is bound to Forall( ... )@Formula.0.1

There are two important things to note here:

  • A term position is only fully defined by its enclosing term and a selection path to it. The output Katja is doing on toString calls is printing the term as well as the name of the root sort and the selection path.
  • The effect of the normalization can be seen in the much longer selection paths and the absence of existential quantifiers.

Files of the Example

All links in one place: