README.md 4 KB
Newer Older
POTTIER Francois's avatar
README.  
POTTIER Francois committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
# Fix: memoization and fixed points made easy

`fix` is an OCaml library that helps with various constructions
that involve memoization and recursion.

## Installation

Type `opam install fix`.

## Overview

At the top of an OCaml module, declare `open Fix`.
This gives you access to the following submodules:

POTTIER Francois's avatar
README.    
POTTIER Francois committed
15
16
* [`CompactQueue`](src/CompactQueue.mli) offers **a minimalist mutable
  FIFO queue** that is tuned for performance.
POTTIER Francois's avatar
README.    
POTTIER Francois committed
17

POTTIER Francois's avatar
POTTIER Francois committed
18
* [`DataFlow`](src/DataFlow.mli) performs a **forward data flow analysis**
POTTIER Francois's avatar
POTTIER Francois committed
19
20
21
22
  over a directed graph. Like [`Fix`](src/Core.mli), it computes the
  least function of type `variable -> property` that satisfies a fixed
  point equation. It is less widely applicable than `Fix`, but, when
  it is applicable, it is easier to use and more efficient than `Fix`.
POTTIER Francois's avatar
POTTIER Francois committed
23
  `DataFlow.ForCustomMaps` is particularly **tuned for performance**.
POTTIER Francois's avatar
POTTIER Francois committed
24

POTTIER Francois's avatar
README.  
POTTIER Francois committed
25
26
27
* [`Gensym`](src/Gensym.mli) offers a simple facility
  for **generating fresh integer identifiers**.

POTTIER Francois's avatar
README.    
POTTIER Francois committed
28
29
* [`Indexing`](src/Indexing.mli) offers **a safe API for manipulating indices
  into fixed-size arrays**.
POTTIER Francois's avatar
README.    
POTTIER Francois committed
30

POTTIER Francois's avatar
README.  
POTTIER Francois committed
31
32
33
34
35
36
37
38
39
40
* [`Memoize`](src/Memoize.mli) offers a number of combinators
  that help **construct possibly recursive memoizing functions**, that
  is, functions that lazily record their input/output graph,
  so as to avoid repeated computation.

* [`Tabulate`](src/Tabulate.mli) offers facilities
  for **tabulating a function**, that is, eagerly evaluating this function
  at every point in its domain, so as to obtain an equivalent
  function that can be queried in constant time.

POTTIER Francois's avatar
POTTIER Francois committed
41
42
43
44
* [`Numbering`](src/Numbering.mli) offers a facility for
  **assigning a unique number** to each value in a certain finite set
  and translating (both ways) between values and their numbers.

45
46
47
* [`GraphNumbering`](src/GraphNumbering.mli) offers a facility for
  **discovering and numbering the reachable vertices** in a finite directed graph.

POTTIER Francois's avatar
README.  
POTTIER Francois committed
48
49
50
51
52
53
54
* [`HashCons`](src/HashCons.mli) offers support for
  **setting up a hash-consed data type**, that is, a data type whose
  values carry unique integer identifiers.

* [`Fix`](src/Core.mli) offers support for **computing
  the least solution of a set of monotone equations**,
  as described in the unpublished paper
POTTIER Francois's avatar
POTTIER Francois committed
55
  [Lazy Least Fixed Points in ML](http://cambium.inria.fr/~fpottier/publis/fpottier-fix.pdf).
POTTIER Francois's avatar
README.  
POTTIER Francois committed
56
57
58
59
  In other words, it allows defining a recursive function of
  type `variable -> property`, where
  **cyclic dependencies** between variables are allowed,
  and properties must be equipped with a partial order.
POTTIER Francois's avatar
README.    
POTTIER Francois committed
60
61
62
  The function thus obtained performs the fixed point
  computation on demand, in an incremental manner,
  and is memoizing.
POTTIER Francois's avatar
POTTIER Francois committed
63
64
  This is typically used to perform a **backward data flow analysis**
  over a directed graph.
POTTIER Francois's avatar
README.  
POTTIER Francois committed
65
66
67
68
69
70
71
72
73
74
75
76
77

* `Prop` defines a few common partial orders, including
  [`Prop.Boolean`](src/Boolean.mli),
  [`Prop.Option`](src/Option.mli),
  [`Prop.Set`](src/Set.mli).

* [`Glue`](src/Glue.mli) contains glue code that helps
  build various implementations of association maps.

The signatures that appear in the above files,
such as `MEMOIZER`, `TABULATOR`, `SOLVER`, and so on,
are defined [here](src/Sigs.ml).

78
The [documentation of the latest released
POTTIER Francois's avatar
POTTIER Francois committed
79
version](http://cambium.inria.fr/~fpottier/fix/doc/fix/Fix/index.html)
80
81
is also available online.

POTTIER Francois's avatar
README.    
POTTIER Francois committed
82
83
84
85
86
87
## Demos

A few demos are provided:

* [`brz`](demos/brz) sets up a hash-consed representation of regular
  expressions and shows how to convert a regular expression to a deterministic
POTTIER Francois's avatar
README.    
POTTIER Francois committed
88
89
90
  finite-state automaton by Brzozowski's method. This demo exploits almost all
  of the submodules listed above, and is accompanied with
  [a commentary](misc/post.md).
POTTIER Francois's avatar
README.    
POTTIER Francois committed
91
92
93
94
95
96
97
98
99
100
101
102
103

* [`cyk`](demos/cyk) presents a CYK-style parsing algorithm as an instance of
  `Fix`.

* [`cfg`](demos/cfg) uses `Fix` to perform certain static analyses of a
  context-free grammar; this includes computing nullability information and
  FIRST sets.

* [`fib`](demos/fib) defines Fibonacci's function in several different ways
  using the fixed-point combinators offered by `Memoize` and `Fix`.

* [`hco`](demos/hco) sets up simple-minded hash-consed trees
  using `HashCons`.