Explanations

This section clarifies particular topics.

Type checking

IDP-Z3 performs a static type check of the statements in each theory and structure block. It determines the type of each sub-expression, and checks that this type is expected where the sub-expression occurs.

Declaring a subset of integers can not be done as follows.

vocabulary V {
    type row
    c: -> row
}
theory { c() < 3. }
structure S1:V { row := {1..5}. }
structure S2:V { row := {A, B, C}. }

IDP-Z3 does not accept the theory because it cannot infer that c() is a number in c() < 3.. Indeed, it depends on whether S1 or S2 is used.

If row is intended to be a set of integers that can be used in arithmetic expressions, it should be declared in the vocabulary as a subset of Int:

row: Int -> Bool

At some point, we may decide that the elements of type row := {1..5} are identifiers that may not participate in arithmetic expressions.

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)).