Hello,

Here is the latest Caml Weekly News, week 20 to 27 May, 2003.

1) Theorem proving example code available
2) Data structures
3) Generating a call-graph

==============================================================================
1) Theorem proving example code available
------------------------------------------------------------------------------
John Harrison wrote:

I've made available some simple implementations of common automated
theorem proving methods. This code, intended to accompany a textbook on
theorem proving, is written in Objective CAML and covers quite a range
of techniques, e.g.

 * The Davis-Putnam procedure
 * Stalmarck's method
 * Binary decision diagrams
 * Tableaux
 * Resolution
 * Model elimination
 * Congruence closure
 * Rewriting
 * Knuth-Bendix completion
 * Brand's transformation
 * Paramodulation
 * Quantifier elimination over Z, C and R
 * Groebner bases
 * Geometry theorem proving
 * The Nelson-Oppen combination method
 * CTL and LTL model checking
 * Symbolic trajectory evaluation
 * Interactive LCF proof
 * Mizar-like proofs

For more details, and to browse or download the code, see:

  http://www.cl.cam.ac.uk/users/jrh/atp/index.html

The code is intended to illustrate the techniques described in the
simplest way I could think of, and *not* to be efficient or practically
useful. Part of my aim in making it available is to solicit ideas about
how it might be made simpler and clearer. Any suggestions will be
gratefully received at <johnh@ichips.intel.com>. I might mention two
notable features of the code as it stands:

 o The code is entirely functional (well, excluding various status
   messages that are emitted). In fact, I cheekily redefine the OCaml
   assignment operator ":=". On the whole, this seems fine, except for
   some messiness when threading BDD state (e.g. the files "bdd.ml" and
   "model.ml").

 o To represent sets, I use canonically ordered lists. This is
   questionable both on grounds of abstraction and efficiency, but
   there is a certain convenience in having an easy concrete syntax
   and being able to pick out elements by pattern matching.

==============================================================================
2) Data structures
------------------------------------------------------------------------------
Yamagata Yoriyuki asked and Diego Olivier Fernandez Pons answered:

> I'm looking for the Set/Map like data-structures which can efficiently
> add and remove large intervals over integers, and support
> intersections, unions and compliments.  Does anybody make such
> libraries?  Baire contains interval.ml[i] but misses these
> functionalities.  Is it easy to add them to Baire, or are Baire's
> intervals something different than I thought?

Baire's interval Set/Map data structure is based on Martin Erwig's
paper 'Diets for fat sets, Journal of Functional programming Vol 8,
N°6, 627-632, 1998'. It seems to be the data structure you are looking
for (that is an extension to usual sets and maps with a better support
for interval query, insertion, removal, ...)

Erwig's paper is available from his home page, there is also a version
by Olivier Andrieu.

There are interval data structures used in computational geometry
(interval tree, ...) but I don't think this is what you are refering
to, is it ?

Martin Erwig's paper presents the data structure and says that one
could easily add
- a balancing scheme
- the set operations (union, intersection, ...)

I did the first one longtime ago (should clean the data structure and
remove some bugs) but didn't have the courage to face the 23 cases of
interval respective positions needed to implement the 'difference'
operation over sets.  I also tried some generic implementation
(extending the 'partition' operation) but never ended that work.

> Failing that, is there Set/Map with order-related operations?  
> Actually I have one but if there is one actively developed, I would
> like to use it.

I dont understand exactly what do you mean by 'order-related
operations'. Anyway, if you have some code, it would be interesting to
release it.

> By the way, I have a library for arbitrary orders on (finite sets of)
> integers.  I think comparison of two integer is O(log n ^ 2)
> time. (n for the size of the finite set.)  Do you think it is worth to
> make public?

Yes. It could be included to one of the 'data structure projects'
being developed in Caml.

Oleg Trott wrote and Diego Olivier Fernandez Pons answered:

>> Baire has not even been released after 1 year of work,
>
> I understand that you are not designing new algorithms, but coding
> up ones that are well-known. If so, what is the limiting factor in
> your work : trying to anticipate what features users might and might
> not need ?

The first point is not absolutely true : Baire contains a useless
generalization of balancing schemes, a few operations on zippers,   
graph data structure based on ternary balanced trees (both inspired by
Gerard Huet's Zen library), lexical maps, there were dynamic optimal
trees (see the art of computer programming for the statical version)
based on Cartesian trees... But this is not the problem.

The main problems are :
- lack of knowledge
- lack of time
- lack of organization

And the worse is the last one.

I wanted to write a library of NP-hard approximation algorithms over
Baire's graph data structures. I soon understood I would need a  
LP-solver and an efficient branch-and-bound scheme.

I then experimented on branch-and-bound (huge trees) with two
techniques : continuations (simulated by exceptions) and zippers.
Wrote some code. I also experimented a few LP algorithms mostly on
Bender's decomposition to obtain a quasi-recursive scheme and to be
able to use a persistent data structure (sparse arrays). Wrote
some code.

The LP-algorithms had numerical unstability problems. I investigated
how to face this kind of problem (interval arithmetic, stochastic
arithmetic, regressive analysis). Chose CESTAC (stochastic arithmetic)
and wrote some code.

I also investigated a few tree traversal algorithms (classical
depth-first and best-first but also limited discrepancy search,
bounded-depth discrepancy seach, interleaved-discrepancy search, ...)

Tired of being rewriting trivial data structure (trees, heaps) because
I needed an immediate acces to X where X could be { the size, the
depth on the tree, the number of left segment in the path, ... } I
said to myself "wrong way...  automatic code generation is the only
truth".

Worked on automata (pda, lpda), attribute grammars and code
generation/specialisation. Wrote some code.

Result :
- a lot of pieces of unrelated code
- no library, not even a single line of code directly related to the
initial goal
- Baire hasn't been maintained and developed as it should have

This is the classical scheme of the 'library project disaster'.

==============================================================================
3) Generating a call-graph
------------------------------------------------------------------------------
Yaron Minsky asked and Xavier Leroy answered:

> Does anyone know a way of generating a call-graph from a set of ocaml
> sources?  What I want to do is, at a minimum, get a list of all the
> functions that could be called as a result of a given function invocation.

This requires a non-trivial static analysis called "control flow
analysis" in the literature; particular instances include Shivers'
0-CFA and k-CFA, Jagannathan and Wright's "polymorphic splitting",
etc.

The difficulty is that functions are first-class values, so the
function you're applying can be a parameter to another function, or a
member of a data structure.  (Objects raise similar issues.)
Thus, the control flow cannot be determined independently of the data
flow, and "control flow analysis" is really a data flow analysis that
tracks the flow of functional values.

I don't know of any implementation of control-flow analysis for the
whole OCaml language.

==============================================================================
Old cwn
------------------------------------------------------------------------------

If you happen to miss a cwn, you can send me a message
(alan.schmitt@inria.fr) and I'll mail it to you, or go take a look at
the archive (http://pauillac.inria.fr/~aschmitt/cwn/). If you also wish
to receive it every week by mail, just tell me so.

==============================================================================

Alan Schmitt