This document contains the TIP format, which is an extension of SMT-LIB for expression inductive problems. The grammar of the format can also be viewed as BNF.

### Scope of the benchmark suite

We want the benchmark suite to focus exclusively on problems that need induction. Functional programs that don't use inductive data types probably fit better elsewhere. Also, although we support higher-order functions and quantification over functions, problems that need a lot of higher-order reasoning (e.g. synthesis of functions) are probably better suited for THF.

### Criteria

When designing our language extensions, we had these criteria in mind:

- The problem format should not look like an encoding: features such as data types and pattern matching should be supported natively rather than encoded. We should preserve as much information as possible from the input problem in case it's useful to a prover.
- As far as possible, the syntax should be compatible with SMT-LIB. So we do not introduce new features just for the sake of it. We are however incompatible with SMT-LIB whenever it's needed to avoid breaking the first criterion.
- The format should be accessible: easy to understand and easy for other tools to use. We have written a tool which removes some of the advanced features (such as higher-order functions) from problems to help provers that don't support those features.

### Example: Datatypes, match-expressions and recursion

This example specifies the commutativity of plus over natural numbers:

```
(declare-datatypes () ((Nat (Zero) (Succ (pred Nat)))))
(define-fun-rec
plus
((x Nat) (y Nat)) Nat
(match x
(case Zero y)
(case (Succ n) (Succ (plus n y)))))
(assert-not (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))
(check-sat)
```

The syntax should be familiar to users of SMT-LIB. Natural numbers are defined with `declare-datatypes`

. This is not in the SMT-LIB standard, but is accepted by many SMT solvers, including Z3 and CVC4.

The function is declared using `define-funs-rec`

as proposed in the SMT-LIB v2.5 draft (Barrett, Stump, and Tinelli). We define `plus`

rather than axiomatising it because, if the problem is from a functional program, we want to be explicit about which axioms are function definitions.

The `match`

expression is our proposed extension for match-expressions. The first argument to match is the scrutinee, followed by a list of branches, all starting with the word `case`

(for ease of reading). The first argument to `case`

is the constructor and bound variables (their types are not indicated, as they are inferrable from the type of the scrutinee and the data type declarations).

TIP also allows the user to define their functions in a more traditional SMT-LIB syntax, using if-then-else with discriminator and projector functions (in this case `is-Nat`

and `pred`

). The TIP tool is able to translate between these syntaxes. Here is how the example above looks with match removed:

```
(declare-datatypes () ((Nat (Zero) (Succ (pred Nat)))))
(define-fun-rec
plus
((x Nat) (y Nat)) Nat (ite (is-Succ x) (Succ (plus (pred x) y)) y))
(assert-not (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))
(check-sat)
```

Match expressions can also have a default branch which matches all other pattern than those explicitly listed. This is sometimes useful when there are many constructors. However, in the example above, either of the patterns `Zero`

or `(Succ n)`

can be replaced with `default`

. As an example, this is how it looks with the `Succ`

case transformed:

```
(declare-datatypes () ((Nat (Zero) (Succ (pred Nat)))))
(define-fun-rec
plus
((x Nat) (y Nat)) Nat
(match x
(case default (Succ (plus (pred x) y)))
(case Zero y)))
(assert-not (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))
(check-sat)
```

Some provers like to distinguish between axioms and conjectures, and in many inductive problems we have a distinguished conjecture. Following our principle not to throw away information from the input problem, TIP has a `assert-not`

construct which identifies the goal, akin to `conjecture`

in TPTP, or `goal`

in Why3. The declaration `(assert-not p)`

means the same as `(assert (not p))`

, except that it marks `p`

as a goal. It can easily be removed by the TIP tool:

```
(declare-datatypes () ((Nat (Zero) (Succ (pred Nat)))))
(define-fun-rec
plus
((x Nat) (y Nat)) Nat
(match x
(case Zero y)
(case (Succ n) (Succ (plus n y)))))
(assert
(exists ((n Nat) (m Nat)) (distinct (plus n m) (plus m n))))
(check-sat)
```

The tool can also translate the example to Why3 syntax. It then looks like this:

```
module A
use HighOrd
use import int.Int
use import int.EuclideanDivision
type nat = Zero | Succ (nat)
function plus (x : nat) (y : nat) : nat =
match x with
| Zero -> y
| Succ n -> Succ (plus n y)
end
(* plus (Zero) y = y
plus (Succ n) y = Succ (plus n y) *)
goal x0 : forall n : nat, m : nat . (plus n m) = (plus m n)
end
```

### Example: Polymorphism

TIP also supports polymorphism. Here is an example showing the right identity of append over polymorphic lists:

```
(declare-datatypes (a)
((list (nil) (cons (head a) (tail (list a))))))
(define-fun-rec
(par (a)
(append
((xs (list a)) (ys (list a))) (list a)
(match xs
(case nil (as nil (list a)))
(case (cons x zs) (cons x (append zs ys)))))))
(assert-not
(par (a)
(forall ((xs (list a))) (= (append xs (as nil (list a))) xs))))
(check-sat)
```

We allow polymorphic datatypes, declarations and assertions using the syntax suggested in Bonichon, Déharbe, and Tavares (2014), which is currently waiting to be merged into CVC4 (Bobot). This syntax uses the syntactic form `(par (A) ...)`

to quantify over the type variable `A`

. Only rank-1 polymorphism is supported.

Expressions can be annotated with their type with the `as`

keyword. When the type of a function application is not fully specified by only looking the types of its arguments, the problem must use `as`

to specify the type.

Polymorphism can be removed by specialising the program at some ground types, but this is not necessarily complete. Another method is to encode typing information over monomorphic terms. We plan to add techniques for this to the TIP toolchain. For now, provers must natively support polymorphism if they want to solve polymorphic problems.

When translating `assert-not`

into `assert`

, any polymorphic type variables are Skolemised:

```
(declare-sort sk_a 0)
(declare-datatypes (a)
((list (nil) (cons (head a) (tail (list a))))))
(define-fun-rec
(par (a)
(append
((xs (list a)) (ys (list a))) (list a)
(match xs
(case nil (as nil (list a)))
(case (cons x zs) (cons x (append zs ys)))))))
(assert
(exists ((xs (list sk_a)))
(distinct (append xs (as nil (list sk_a))) xs)))
(check-sat)
```

Here is the same problem in Why3 syntax:

```
module A
use HighOrd
use import int.Int
use import int.EuclideanDivision
type list 'a = Nil2 | Cons2 'a (list 'a)
function append (xs : list 'a) (ys : list 'a) : list 'a =
match xs with
| Nil2 -> Nil2 : list 'a
| Cons2 x zs -> Cons2 x (append zs ys)
end
(* append (Nil2) ys = Nil2 : list 'a
append (Cons2 x zs) ys = Cons2 x (append zs ys) *)
goal x0 : forall xs : list 'a . (append xs (Nil2 : list 'a)) = xs
end
```

### Example: Higher-order functions

This is an example property about mapping functions over lists:

```
(declare-datatypes (a)
((list (nil) (cons (head a) (tail (list a))))))
(define-fun-rec
(par (a b)
(map2
((f (=> a b)) (xs (list a))) (list b)
(match xs
(case nil (as nil (list b)))
(case (cons y ys) (cons (@ f y) (map2 f ys)))))))
(assert-not
(par (a b c)
(forall ((f (=> b c)) (g (=> a b)) (xs (list a)))
(= (map2 (lambda ((x a)) (@ f (@ g x))) xs)
(map2 f (map2 g xs))))))
(check-sat)
```

Lambdas are introduced much like lets, with an identifier list with explicit types. Note that the function spaces are a family of types, with different arities. Thus, for some types `a`

, `b`

and `c`

, there is a type `(=> a b c)`

, which is different from its curried version `(=> a (=> b c)`

. Lambdas for the first type are constructed with `lambda ((x a) (y b)) ...`

, and for the second with `lambda ((x a)) (lambda ((y b)) ...)`

. To apply a lambda, you explicitly use the `@`

function, which also come at a family of types: `((=> a b) a) b`

, `((=> a b c) a b) c`

, and so on.

Partial application is not supported, i.e. if you have a function `f`

with type `(=> int int int)`

, the application `(f 1)`

is invalid, and should be written with an explicit lambda: `(lambda ((x int)) (f 1 x))`

. The reason why this is important is because SMT LIB supports polyvariadic functions, like `and`

, and `+`

. For example, if (implicit) partial application was allowed, the expression `(+ 1 2)`

could mean `3`

or `(lambda ((x int)) (+ 1 2 x))`

, or a function with higher arity.

In some cases, higher order functions can be removed with specialisation, like in the example above. They can always be removed by defunctionalisation, which is implemented in our tool chain. This pass transforms the above program into this:

```
(declare-sort fun1 2)
(declare-datatypes (a)
((list (nil) (cons (head a) (tail (list a))))))
(declare-fun (par (a b) (apply1 ((fun1 a b) a) b)))
(define-fun-rec
(par (a b)
(map2
((f (fun1 a b)) (xs (list a))) (list b)
(match xs
(case nil (as nil (list b)))
(case (cons y ys) (cons (apply1 f y) (map2 f ys)))))))
(define-fun
(par (a b c)
(lam
((f (fun1 b c)) (g (fun1 a b))) (=> a c)
(lambda ((x a)) (apply1 f (apply1 g x))))))
(assert-not
(par (a b c)
(forall ((f (fun1 b c)) (g (fun1 a b)) (xs (list a)))
(= (as (map2 (lam f g) xs) (list c)) (map2 f (map2 g xs))))))
(check-sat)
```

Here, `=>`

with one argument is replaced with `fun1`

, `@`

with one argument is replaced with `apply1`

. The lambda in the property has become a new function, `lam`

, which closes over the free variables `f`

and `g`

.

### TODO

This document does not yet cover mutual recusion (over data types or over functions), or partial branches and partiality.

### References

Barrett, Clark, Aaron Stump, and Cesare Tinelli. “The SMT-LIB Standard – Version 2.5 (Draft).” http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-draft.pdf.

Bobot, François. “[RFC] Add Adhoc Polymorphism.” https://github.com/CVC4/CVC4/pull/51.

Bonichon, Richard, David Déharbe, and Cláudia Tavares. 2014. “Extending SMT-LIB V2 with *λ*-Terms and Polymorphism.” In *12th International Workshop on Satisfiability Modulo Theories (SMT)*, edited by Philipp Rümmer and Christoph M. Wintersteiger, 53–62. CEUR Workshop Proceedings 1163. Aachen. http://ceur-ws.org/Vol-1163#paper-08.