README.md 3.48 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
POTTIER Francois committed
15
16
17
18
19
20
* [`DataFlow`](src/DataFlow.ml) performs a forward data flow analysis
  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
README.  
POTTIER Francois committed
21
22
23
24
25
26
27
28
29
30
31
32
33
* [`Gensym`](src/Gensym.mli) offers a simple facility
  for **generating fresh integer identifiers**.

* [`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
34
35
36
37
* [`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.

38
39
40
* [`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
41
42
43
44
45
46
47
* [`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
48
  [Lazy Least Fixed Points in ML](http://cambium.inria.fr/~fpottier/publis/fpottier-fix.pdf).
POTTIER Francois's avatar
README.  
POTTIER Francois committed
49
50
51
52
  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
53
54
55
  The function thus obtained performs the fixed point
  computation on demand, in an incremental manner,
  and is memoizing.
POTTIER Francois's avatar
README.  
POTTIER Francois committed
56
57
58
59
60
61
62
63
64
65
66
67
68

* `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).

POTTIER Francois's avatar
README.    
POTTIER Francois committed
69
70
71
72
73
74
## 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
75
76
77
  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
78
79
80
81
82
83
84
85
86
87
88
89
90

* [`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`.