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