format.html

<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<link href="base-min.css" rel="stylesheet"/>
<link href="style.css" rel="stylesheet"/>
<title>TIP Format</title>
</head>
<body>
<div class="header">
<h1>TIP Format</h1>
</div>
<div class="content">
<p>This document contains the <a href="index.html">TIP</a> format, which is an extension of <a href="http://smt-lib.org">SMT-LIB</a> for expressing inductive problems. The grammar of the format can also be viewed as <a href="bnf.html">BNF</a>.</p>
<h3 id="scope-of-the-benchmark-suite">Scope of the benchmark suite</h3>
<p>The benchmark suite focuses exclusively on problems that need induction over datatypes. 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.</p>
<!--
### 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.
-->
<h3 id="differences-between-tip-and-smt-lib-2.6">Differences between TIP and SMT-LIB 2.6</h3>
<p>Our ambition is to keep TIP as close to SMT-LIB as possible. However, there are still a few incompatibilities:</p>
<ul>
<li>TIP allows polymorphism and type variables in function definitions. SMT-LIB only allows polymorphism in datatype definitions.</li>
<li>TIP allows higher-order functions, while SMT-LIB does not.</li>
<li>TIP allows partial functions. SMT-LIB does not.</li>
<li>For convenience, TIP has a special command <code>prove</code> for stating a goal to prove. This allows us to state several subgoals to be proved as separate proof attempts, in one file.</li>
<li>TIP uses a different syntax for annotations than SMT-LIB.</li>
</ul>
<p>The <a href="http://github.com/tip-org/tools">TIP tools</a> can convert TIP files not compatible with SMT-LIB 2.6 to valid SMT-LIB syntax (use the command <code>tip --smtlib myTIPfile.smt2</code>). This includes monomorphisation to remove type variables, removal of lambdas, completion of partial functions, removal of annotations and a translation pass which remove the <code>prove</code> statement and replaces them with valid SMT-LIB syntax using push/pop.</p>
<h3 id="datatypes-match-expressions-and-recursion">Datatypes, match-expressions and recursion</h3>
<p>This example specifies the commutativity of plus over natural numbers:</p>
<pre><code>(declare-datatype Nat ((Zero) (Succ (pred Nat))))
(define-fun-rec
  plus
  ((x Nat) (y Nat)) Nat
  (match x
    (((Succ n) (Succ (plus n y)))
     (_ y))))
(prove (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))</code></pre>
<p>The syntax should be familiar to users of SMT-LIB. Natural numbers are defined with <code>declare-datatype</code>, and the function is declared using <code>define-fun-rec</code>. Both are part of the <a href="http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf">SMT-LIB v2.6 standard</a>. We define <code>plus</code> rather than axiomatising it because, if the problem is from a functional program, we want to be explicit about which axioms are function definitions.</p>
<p>TIP has a <code>prove</code> construct which declares the goal, akin to <code>conjecture</code> in TPTP, or <code>goal</code> in Why3. It is not part of SMT-LIB. If the problem uses <code>prove</code> only once, then <code>(prove p)</code> means the same as <code>(assert (not p))</code>. If <code>prove</code> is used several times, it indicates that there are several goals which must all be proved.</p>
<ul>
<li>To convert a problem to standard SMT-LIB format, run <code>tip --smtlib</code>.</li>
<li>To replace <code>match</code> expressions with selector functions (e.g. <code>is-plus</code>), run <code>tip --remove-match</code>. You can combine this with conversion to SMT-LIB format with <code>tip --smtlib-no-match</code>.</li>
<li>To convert a problem to Why3 format, run <code>tip --why3</code>.</li>
</ul>
<h3 id="polymorphism">Polymorphism</h3>
<p>TIP also supports polymorphism. Here is an example showing the right identity of append over polymorphic lists:</p>
<pre><code>(declare-datatype
  list (par (a) ((nil) (cons (head a) (tail (list a))))))
(define-fun-rec
  append
  (par (a) (((xs (list a)) (ys (list a))) (list a)))
  (match xs
    ((nil (_ nil a))
     ((cons x zs) (cons x (append zs ys))))))
(prove
  (par (a) (forall ((xs (list a))) (= (append xs (_ nil a)) xs))))</code></pre>
<p>We allow polymorphic datatypes, declarations and assertions using the syntactic form <code>(par (A) ...)</code> to quantify over the type variable <code>A</code>. Only rank-1 polymorphism is supported. Note that TIP allows both polymorphic datatypes and polymorphic functions, unlike SMT-LIB 2.6, which only allows it in datatype definitions.</p>
<!--
suggested in @smtlam, which is currently waiting to be merged
into CVC4 (@cvc4parPR). This syntax uses the syntactic form
`(par (A) ...)` to quantify over the type variable `A`. Only rank-1
polymorphism is supported.
-->
<p>An underscore is used to instantiate a polymorphic function at a given type. In general, if <code>f</code> is a polymorphic function symbol having <code>n</code> type arguments, then <code>(_ f t1 ... tn)</code> applies <code>f</code> to the type arguments <code>t1 ... tn</code>. Explicit type arguments must be given whenever a function’s type cannot be inferred by looking at the types of its arguments. In the example above, this occurs with <code>(_ nil a)</code>.</p>
<!-- 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. -->
<ul>
<li>To eliminate polymorphism from a problem, run <code>tip --monomorphise</code>.</li>
</ul>
<h3 id="higher-order-functions">Higher-order functions</h3>
<p>This is an example property about mapping functions over lists:</p>
<pre><code>(declare-datatype
  list (par (a) ((nil) (cons (head a) (tail (list a))))))
(define-fun-rec
  map
  (par (a b) (((f (=&gt; a b)) (xs (list a))) (list b)))
  (match xs
    ((nil (_ nil b))
     ((cons y ys) (cons (@ f y) (map f ys))))))
(prove
  (par (a b c)
    (forall ((f (=&gt; b c)) (g (=&gt; a b)) (xs (list a)))
      (= (map (lambda ((x a)) (@ f (@ g x))) xs) (map f (map g xs))))))</code></pre>
<p>Lambdas are introduced much like lets in SMT-LIB, with an identifier list with explicit types. They are applied using ‘@’. Note that the function spaces are a family of types, with different arities. Thus, for some types <code>a</code>, <code>b</code> and <code>c</code>, there is a type <code>(=&gt; a b c)</code>, which is different from its curried version <code>(=&gt; a (=&gt; b c)</code>:</p>
<ul>
<li>To construct a value of type <code>(=&gt; a b c)</code>, write <code>lambda ((x a) (y b)) ...</code>. To apply it, write <code>(@ f x y)</code>.</li>
<li>To construct a value of type <code>(=&gt; a (=&gt; b c))</code>, write `<code>lambda ((x a)) (lambda ((y b)) ...)</code>. To apply it, write <code>(@ (@ f x) y)</code>.</li>
</ul>
<p>That is, if you want to partially apply a function, you must either write a lambda, or define it in a curried fashion in the problem.</p>
<ul>
<li>To eliminate lambdas from a problem, run <code>tip --axiomatize-lambdas</code>.</li>
</ul>
<h3 id="todo">TODO</h3>
<p>This document does not yet cover partial functions or annotations.</p>
</div>
</body>
</html>