fix 20230505

Fix: Memoization and Fixed Points Made Easy

fix is an OCaml library that helps with various algorithmic constructions that involve memoization, recursion, and numbering.

Installation and Usage

Type opam install fix.

In your dune file, add (libraries fix) to the description of your library or executable.

Within your code, you may wish to declare open Fix. This allows you to access the submodules without the leading "Fix." qualifier.

Data Flow Analysis

The following submodules help solve systems of recursive monotone equations. In other words, they help implement data flow analyses.

• Fix.Fix This module offers support for computing the least solution of a set of monotone equations, as described in the unpublished paper Lazy Least Fixed Points in ML. 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 that has finite ascending chains. This function performs the fixed point computation on demand, in an incremental manner, and is memoizing. This is typically used to perform a backward data flow analysis over a directed graph. This algorithm performs dynamic dependency discovery, so there is no need for the user to explicitly describe dependencies between variables.
• Fix.DataFlow This module performs a forward data flow analysis over a (possibly cyclic) directed graph. Like Fix.Fix, it computes the least function of type variable -> property that satisfies a fixed point equation. It is less widely applicable than Fix.Fix, but, when it is applicable, it can be both easier to use and more efficient. It does not perform dynamic dependency discovery. The submodule Fix.DataFlow.ForCustomMaps is particularly tuned for performance.

The following submodules help construct the arguments required by the functors in Fix.Fix and Fix.DataFlow.

• Fix.Prop This module defines a few common partial orders, each of which satisfies the signature PROPERTY. These include Booleans, options, and sets.
• Fix.Glue This module contains glue code that helps use the functors provided by other modules. In particular, it helps build various implementations of association maps.

Numbering

The following submodules help generate unique numbers and assign unique numbers to objects.

• Fix.Gensym This module offers a simple facility for generating fresh integer identifiers.
• Fix.HashCons This module offers support for setting up a hash-consed data type, that is, a data type whose values carry unique integer identifiers.
• Fix.Numbering This module 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.
• Fix.GraphNumbering This module offers a facility for discovering and numbering the reachable vertices in a finite directed graph.
• Fix.Indexing This module offers a safe API for manipulating indices into fixed-size arrays.

Memoization and Tabulation

The following submodules help construct memoized or tabulated functions, both of which have the property that repeated computation is avoided.

• Fix.Memoize This module offers facilities for constructing a (possibly recursive) memoized function, that is, a function that lazily records its input/output graph, so as to avoid repeated computation.
• Fix.Tabulate This module 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 (near) constant time.

Minimization

The following submodules offer minimization algorithms.

• Fix.Minimize This module offers a minimization algorithm for deterministic finite automata (DFAs).

Data Structures

The following submodules offer data structures that can be of general interest.

• Fix.CompactQueue This module offers a minimalist mutable FIFO queue that is tuned for performance.
• Fix.Enum This module offers a few functions that help deal with enumerations.
• Fix.Partition This module offers a partition refinement data structure.