TIP Format

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:

  1. 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.
  2. 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.
  3. 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.