Explanations

This section clarifies particular topics.

Type inference in quantifications

It is often convenient to omit the type of variables in quantifications and aggregates, e.g.,

! p: 0 =< age(p).

It is also customary to use evocative names for variables, e.g., to use p for a variable ranging over persons, or col for a variable ranging over a set of columns. By extension, one would also consider p1, p2 as variables ranging over persons.

Therefore, we recommend knowledge engineers to declare variables in the vocabulary, e.g.,

var p in Person
var col in Column

This allows IDP-Z3 to properly infer the type of p in our example above. IDP-Z3 also uses the variable declaration to infer the type of variables p1, p2, …, e.g., in ? p1, p2: married(p1, p2). (the variable declaration in the vocabulary cannot end with a number)

Note that the variable declaration is only used when the type is not given in the quantification. In ! p in Column: ..., p ranges over the set of Columns, even if variable p is declared differently in the vocabulary.

Note also that ! p, c in Col: .. raises an error because p is ambiguous: is it a Person or a Col ?

Recursive datatypes

A recursive data type is a datatype whose constructor accepts arguments of the type being declared. An idiomatic example is a list of Int:

type List := constructed from {nil, cons(car:Int, cdr: List)}

Note that this List only contains Int. A different type declaration must be used for lists of other types (with different constructors).

A list [1, 2, 3] can be constructed as follows:

cons(1, cons(2, cons(3, nil)))

The length of the list can be computed using a recursive definition:

len: (List) -> Int // in vocabulary block


// in definition block
{ (recursive)
  len(nil) = 0.
  ! x in List: len(x) = len(cdr(x))+1 <- is_cons(x).
}

The (recursive) keyword is required to avoid non-terminating model search on satisfiable theories. Model search for an unsatisfiable theory with recursive definitions usually do not terminate, as the reasoning engine considers ever longer lists. This prevents the use of recursive datatypes for propagation and explanation problems, and thus in the Interactive Consultant.

Recursive datatypes and recursive definitions are natively supported by the Z3 solver that powers the IDP-Z3 reasoning engine.

Here is a definition of membership:

member: Int * List -> Bool // in vocabulary block

{ (recursive)
  ! x in Int, l in List: member(x,l) <- is_cons(l) & car(l)=x.
  ! x in Int, l in List: member(x,l) <- is_cons(l) & member(x, cdr(l)).
}

A definition can be used to express that the numbers in a list are positive.

positive: List -> Bool
l: () -> List

{ (recursive)
  ! x in List: positive(x) <- is_nil(x).
  ! x in List: positive(x) <- is_cons(x) & 0 < car(x) & positive(cdr(x)).
}
positive(l()).

(At some point, we might provide a generic List type, with quantification over the list: ! x in l(): 0 < x..)

Here is a complete code example, to find a list of 2 positive Integers that are in increasing order, and containing 1 and 2:

vocabulary V {
    type List1 := constructed from {nil1, cons1(car1:Int, cdr1: List1)}
    a: () -> List1
    len1: List1 -> Int
    increasing, positive: List1 -> Bool
    member: Int*List1 -> Bool
}

theory T:V {

    { (recursive)
      len1(nil1) = 0.
      ! x in List1: len1(x) = len1(cdr1(x))+1 <- is_cons1(x). }

    // between 1 and 2
    { (recursive)
      ! x in List1: positive(x) <- is_nil1(x).
      ! x in List1: positive(x) <- is_cons1(x) & 0<car1(x)<3 & positive(cdr1(x)).
    }

    { (recursive)
    ! l in List1, x in Int: member(x,l) <- is_cons1(l) & car1(l)=x.
      ! x in Int, l in List1: member(x,l) <- is_cons1(l) & member(x, cdr1(l)).
    }

    { (recursive)
    ! x in List1: increasing(x) <- x = nil1.
    ! x in List1: increasing(x) <- is_cons1(x) & is_nil1(cdr1(x)).
    ! x in List1: increasing(x) <- is_cons1(x) & increasing(cdr1(x))
            & is_cons1(cdr1(x)) & car1(x) < car1(cdr1(x)).}

    len1(a()) = 2.  //a() has 2 elements
    positive(a()).  // the elements in a() are positive
    increasing(a()). // the elements in a() are increasing
    member(1, a()) | member(2, a()).  // 1 and 2 are elements in a()
}

procedure main() {
    print(Theory(T).sexpr())
    pretty_print(model_expand(T, max=1, sort=True))
}

Its output is:

Model 1
==========
a := cons1(1, cons1(2, nil1)).