Legend:
Library
Module
Module type
Parameter
Class
Class type

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.FixThis 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.DataFlowThis 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.PropThis module defines a few common partial orders, each of which satisfies the signature PROPERTY. These include Booleans, options, and sets.

Fix.GlueThis 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.GensymThis module offers a simple facility for generating fresh integer identifiers.

Fix.HashConsThis module offers support for setting up a hash-consed data type, that is, a data type whose values carry unique integer identifiers.

Fix.NumberingThis 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.GraphNumberingThis module offers a facility for discovering and numbering the reachable vertices in a finite directed graph.

Fix.IndexingThis 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.MemoizeThis 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.TabulateThis 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.MinimizeThis 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.CompactQueueThis module offers a minimalist mutable FIFO queue that is tuned for performance.

Fix.EnumThis module offers a few functions that help deal with enumerations.

Fix.PartitionThis module offers a partition refinement data structure.