Correct version of "Comments on Aaron and Clark's proposal"

[Silvio Ranise]

Dear All,

please, ignore my previous email!  I am away from my account
and I had difficulties in handling remotely my email.  So,
I messed up things and I sent an old message with a lot of things
that you were not supposed to read.
I apologize for this inconvinience.  Below, it follows the
correct message.

Best regards,

   Silvio.

-----------> COMMENTS ON AARON AND CLARK'S PROPOSAL <-----------

Dear Aaron and Clark,

thanks for your proposal. We think that it is a very good one
overall, and we strongly support it.
Nonetheless, we think that some clarifications are in order.  In
particular, we would like to put forward a more detailed proposal
about what should go in the restriction R to be attached to the
benchmarks.  The proposal follows below together with additional
comments.


Cesare & Silvio


>----------------------------------------------------------------------
>TITLE: Benchmark classes for SMT-LIB
>
>PROPOSAL: We propose that SMT-LIB be organized into different classes
>of problems, called benchmark classes, where each class is defined by:
>
>-- a signature Sigma, giving arities of function and predicate symbols,
>-- a Sigma-theory T, described either axiomatically or alebraically, and
>-- an (optional) syntactic restriction R on input Sigma-formulas.
>
We completely agree on this.


>A benchmark should then be a Sigma-formula satisfying the restriction R,
>together with a designation as to whether that formula is believed to be
>satisfiable or not in T (T-satisfiable).  A solver correctly runs
>the benchmark  iff it correctly indicates whether or not that
>benchmark is T-satisfiable.
>
>DISCUSSION:
>
>1. We agree with earlier proposals that all benchmark classes in
>SMT-LIB should use unsorted FOL-EQ as the underlying logic.  We
>resisted the temptation to include the underlying logic as part of the
>definition of benchmark classes (to allow things like constructive
>theories, of potential interest for program synthesis).
>
Of course, we agree here too.


>2. We included the signature as part of the definition of the
>benchmark class, because even in unsorted FOL-EQ, it is standard to
>have a signature giving the argument counts of symbols and indicating
>which are predicates and which are functions.  We also agree, however,
>that it is often convenient to have the signature inferred.  Thus, we
>propose that whenever the signature is not explicitly provided, it
>should be inferred to be the smallest signature which includes all the
>symbols in the theory and the benchmark (note that it would be easy to
>provide a tool to do this for solvers which require a signature).


To this we add the some details, following the Sparta group's
proposal.  No overloading of symbols within a benchmark class: a
symbol cannot have multiple arities and can only be a logical symbol,
a function symbol, or a predicate symbol.  The arity and the role of a
symbol are determined by the signature's specification or, in its
absence, by the first occurrence of the symbol in a benchmark.


>Signatures need not be finite, but they will presumablu be
>recursive.


We think that restricting to recursive signatures is quite a natural
requirement.  Relaxing such requirement would result in undecidable
languages (i.e. one cannot establish whether a given expression belong
to the language or not).


>3. Benchmark classes will be created in a grass-roots fashion, as
>people find benchmarks that do not fit into an existing benchmark
>class.  Judging by previous comments, the first benchmark classes to
>be created are likely to have restriction R on input formulas like
>"quantifier-free" or "conjunction of literals".


We agree with this.  For example, a new class of benchmarks is the one
needed to classify the "difference logic" benchmarks provided by
O. Strichman, S. Seshia, and S. Lahiri at CMU.  Such benchmarks are
already available from the local SMT-LIB node at CMU, which can be
visited at the following address:

      http://www-2.cs.cmu.edu/~ofers/smtlib-local

In a separate message we will send as an example a specification of
the difference logic benchmark class in the style you propose.

To make it easier to check the existence of a given class of
benchmarks, we propose to maintain a list of such classes in the
central web page of SMT-LIB.  Indeed, Each class in the list would be
specified in the format you suggest, possibly with the improvements we
propose later.  When setting up a local node of SMT-LIB, the
contributor should go and check the centralized list of benchmark
classes in order to avoid re-defining already existing classes,
thereby promoting reuse and sharing of common knowledge in the SMT-LIB
community.


>4. Another restriction on input formulas that we think may be useful
>is: "well-sorted with respect to a given sort system".  Note that this
>restriction does not require the solver to implement type-checking.
>It actually makes life easier for the solver, since it no longer has
>to worry about ill-sorted formulas.

We take it that, by adding a well-sorted restriction on inputs at the
meta level, you would like to recover some of the convenience of sorts
within the unsorted framework everyone seems to agree on adopting for
SMT-LIB.  This seems a useful device since often the designer of a
solver does not want to take into consideration ill-sorted expressions
(such as x + nil = 0).  Although useful, we would like to point out
that what you propose must be done carefully, since sorts have quite
substantial semantical implications.  To illustrate this, consider the
sorted theory T below:

- A and B are two sort symbols
- b1 and b2 are two constant symbols of sort B
- f is a function symbol of arity B -> B
- T = { \forall x,y:A. x=y,
        b = b, f(x) = f(x)   }

where the last two axioms, which are redundant, are added just for
illustrative purposes.  Now, since we are using an unsorted framework
we cannot use T as is as the background theory of a benchmark
class. So what theory do we use? Following your proposal of simply
stripping away the sort information from a benchmark once its
well-sortedness has been verified, we could think of doing the same
for the theory T itself. However, if we simply consider the following
unsorted theory

- T' = { \forall x,y. x=y,
         b = b, f(x) = f(x)   }

as the unsorted counterpart of T above, the problems begin.  For
example, it is easy to check that the formula

       b != f(b)

is satisfiable in (the sorted theory) T but unsatisfiable in (the
unsorted theory) T'.  So, if one has T in mind and uses a solver
implementing T', he will get unexpected results.

Most likely, you were thinking of a situation in which one has T in
mind and has also a solver that actually implements reasoning in T.
Although there are no problems in this case, we are still left with
the problem of how to correctly classify benchmarks for this solver in
the context of SMT-LIB.  We point out that using T' above and adding
well-sortedness restrictions on the input language will not solve the
problem in this case.  Of course, there is a correct way to translate
many-sorted logic to unsorted classical logic.  This goes under the
name of relativization of quantifiers.  For example, the sorted theory
T above would be translated into the following unsorted theory:

T'' = { \forall x,y.(A(x) /\ A(y) ==> x = y) },
        B(b), \forall x.(B(x) ==> B(f(x))) }

and the formula b != f(b) is satisfiable in T'' as it was in T.  All
we need to do is to introduce in the language as many unary predicates
as sort symbols, and to add axioms encoding what it means for a
term to be well-sorted.  More in general, any formula in the sorted
framework is satisfiable in T iff its relativization is satisfiable in
T''.

To cope with the problems described above, we propose the following.

PROPOSAL: each benchmark class is given a specification with four
sections/fields:

1) Signature:
   This section specifies a (possibly sorted) signature Sigma.
2) Theory:
   This section specifies a Sigma-theory T, either axiomatically
   or algebraically.
3) Input language:
   This section specifies the language of the benchmarks, together
   with whichever additional syntactic restrictions
   (in the sorted case, an example of such restrictions would be
   a well-sortedness requirement).
4) Semantics:
   This section specifies what it means for a benchmark to be
   T-satisfiable.

COMMENTS: sections 1,2, and 3 are as per your proposal. Section 4
takes care of semantic issues.  In the unsorted case, a benchmark will
typically be said to be T-satisfiable iff it is satisfied by a model
of T (the usual meaning of T-satisfiable).  In the sorted case, the
definition of T-satisfiability involves the relativization of
quantifiers. One can specify in the Semantics section that a benchmark
phi is T-satisfiable iff the relativization of phi is satisfiable, in
the usual sense, in the relativization of T. The relativization
process too is itself specified in the Semantics section.  For the
benefit of those in this list that are not familiar with
relativization of quantifiers, we sketch the process at the end of
this message. For semplicity, we consider there only the case of
(flat) many-sorted logic, with theories specified axiomatically.

RATIONALE: unsorted first-order logic is the underlying framework of
SMT-LIB with respect to which any semantical question should be
ultimately stated and solved.  Adding a Semantics section to a
benchmark class specification allows us to give a proper treatment of
sorted logics by means of the relativization process.  Note that
relativization, in addition to represent a semantical specification,
can also be used to automatically produce unsorted versions of the
benchmarks under consideration, allowing solvers working in unsorted
logic to process them as well.

The approach we propose would also help in bringing the surface some
intrinsic (and sometimes overlooked) difficulties in combining
many-sorted background theories.  In many cases, in fact, combining
two theories involves the sharing of (at least) one sort symbol on
which the two theories are supposed to agree.  To illustrate this with
an example, consider the combination of the sorted theory As of
arrays:

- sorts: ARRAY, ELEMENT, INDEX
- functions: select : ARRAY, INDEX --> ELEMENT
             store  : ARRAY, INDEX, ELEMENT --> ARRAY
- axioms:
   { \forall a:ARRAY, i:INDEX, e:ELEMENT.
        select(store(a,i,e),i)=e,
     \forall a:ARRAY, i,j:INDEX, e:ELEMENT.
       (i != j ==> select(store(a,i,e),i)=select(a,j)) }

with the following sorted theory Ns of natural numbers with an
ordering relation:

- sorts: NAT
- functions: 0 : NAT, s: NAT --> NAT
- predicates: >= : NAT, NAT
- axioms:
   { \forall x,y: NAT. x+s(y) = s(x+y),
     \forall x: NAT. x >= 0,
     \forall x: NAT. s(x) >= x,
     etc... }.

If the intended combined theory is that of arrays of natural numbers,
say, such a combination should identify the sort ELEMENT of As with
the sort NAT of Ns. This becomes even more evident when we translate
the two sorted theories into their unsorted counterparts.  In fact, if
we want to ensure that both ELEMENT and NAT are intepreted as the same
set in the combined theory, the relativization process must introduce
the same predicate symbol for both ELEMENT and NAT.  But this means
that the two unsorted theories that are the relativization of As and
Ns, respectively, end up sharing a predicate symbol, even if the
original theories were signature disjoint.  So, suppose that we have a
program that combines a solver for the sorted theory As and one for
the sorted theory Ns by using an implementation of the Nelson-Oppen
method, say. It is clear now that we cannot claim that our program is
correct simply as a consequence of the correctness of that
method. Nelson-Oppen applies to unsorted theories with disjoint
signatures, so it applies to neither As and Ns, which are sorted, nor
to their relativization, which have a predicate symbol in common!

We think that using the relativization process will have the
additional benefit of bringing these issues to light, exposing the
incorrectness of certain approaches and hopefully stimulating
further research on the matter.

As a final remark, we notice that this approach can be extended
further to handle more complex situations (such as the case of order
sorted logics or, more in general, logics with restricted quantifiers.

However, in those situations particular care must be taken to avoid
introducing inconsistencies.  So, at least for the moment, we suggest
to restrict the relativization process to handle (simple) many-sorted
logic, where it is simple and is well-understood.

>5. We are happy to include an if-then-else operator in the logic, as
>was suggested in previous proposals (so the logic might be called
>unsorted FOL-EQ-ITE).
>

We too are in favor of the ITE operator.  But we would like to press
again the case for adding a let construct as well. We are thinking of
something like:

let <hole> := <hformula> in <hformula>

where that <hole> is a class of variables (holes) disjoint from the
usual variables and <hformula> is the class of formulas with holes.

The meaning of let would be operationally the same as in lambda
calculus (with the same rules about scoping, binding and renaming):

let y := e in phi

would stand for the normal form of the term

((\lambda y. phi) e)

in lambda calculus. I.e., it would stand for the <hformula> obtained
by replacing all the free occurrences of y in phi by e.  A formula
would then be an hformula without free occurrences of holes.

Again the convenience of such a construct in the language is that it
lets one write more compactly formulas with a lot of same subformulas.

Of course, a similar let construct is also conceivable for terms. Some
more discussion is probably needed on whether we want two separate let
constructs, one for for formulas and one for terms, or a single
one. Either choice has its pros and cons in terms of the complexity of
the grammar and, correspondingly of a parser for its language.


>Transitioning to a unified suite of
>benchmarks might then be achieved by agreeing upon
>
>-- a concrete syntax for unsorted FOL-EQ-ITE signatures,
>-- a concrete syntax for unsorted FOL-EQ-ITE formulas,  -- a language for 
>describing the syntactic restrictions R.
>

We agree that we should agree on a concrete syntax for formulas, and
possibly for signatures too. This syntax should be defined formally in
BNF or similar formalism, so that users of the library can write their
own parsers/translators.

However, we do not think that it would be beneficial now to work on
devising a formal language for specifying syntactic restrictions. The
main reason is that we doubt that a benchmark provider would take the
pain of specifying the restrictions formally in language that we
designed.  We propose a more opportunistic approach in which the
benchmark provider specifies the restriction in whichever way he
choses. This specification should be rigorous, but it need not be
formal.  Some of us could work later, time and funds permitting, on a
specification language for restrictions and on hiring students for
translating the informal specifications given by the benchmark
provider into formal ones :)

>More flexibly, we could agree simply upon a concrete syntax for
>grammars defining the concrete syntax of signatures and formulas, and
>then write generic tools based on these grammars for things like
>
>-- translating between source and target languages
>-- checking that a formula satisfies a given syntactic restriction
>

Although this would be nice to have, we again believe that, within
this forum, we should just concentrate on agreeing on a concrete
syntax for signatures and formulas, let's call it the STM-LIB format.
We would leave the issues you mention above to the discretion of
anybody who decides to provide a general translator from or to the
STM-LIB format.


---------------------------------------------------------------------

APPENDIX ABOUT THE RELATIVIZATION PROCESS

For completeness, we add a brief description of the relativization
process Rel to translate the formulae in the benchmark to unsorted
logic:

- for any sort symbol S, add the theory a unary predicate symbol S;
- for any constant c of sort S, add the theory the following axiom:
      S(c);
- for any function symbol f of sort S_1, ..., S_n --> S_{n+1}, add the
  theory the following axiom:
  \forall x_1, ..., x_{n+1}.(S_1(x) /\ ... /\ S_n(x) ==> S_{n+1}(x_{n+1});
- Rel(\phi) := \phi
          IF \phi is an atom;
- Rel(\neg \phi) := \neg Rel(\phi);
- Rel(\phi \bowtie \psi) := Rel(\phi) \bowtie Rel(\psi)
          WHERE \bowtie is a boolean connective;
- Rel(\forall x:S. \phi) := \forall x.(S(x) ==> \phi);
- Rel(\exists x:S. \phi) := \exists x.(S(x) /\  \phi).

Note that the operator Rel is well-defined only for formulas with no
free variables. But there is no loss of generality in that because,
for satisfiability purposes, a formula phi with free variables x_1,
...., x_n of respective sort S_1, ..., S_n can always be treated as the
formula (\exists x_1:S_1, ..., x_n:S_n. phi).








_________________________________________________________________
MSN Search, le moteur de recherche qui pense comme vous ! 
http://search.msn.fr/worldwide.asp