Module Fix.ForOrderedType

ForOrderedType is a special case of Make where it suffices to pass an ordered type T as an argument. A reference to a persistent map is used to hold the memoization table.


module T : sig ... end
module P : sig ... end


type variable = T.t

The type of variables.

type property =

The type of properties.

type valuation = variable -> property

A valuation is a mapping of variables to properties.

type rhs = valuation -> property

A right-hand side, when supplied with a valuation that gives meaning to its free variables, evaluates to a property. More precisely, a right-hand side is a monotone function of valuations to properties.

type equations = variable -> rhs

A system of equations is a mapping of variables to right-hand sides.

val lfp : equations -> valuation

lfp eqs produces the least solution of the system of monotone equations eqs.

It is guaranteed that, for each variable v, the application eqs v is performed at most once (whereas the right-hand side produced by this application is, in general, evaluated multiple times). This guarantee can be used to perform costly pre-computation, or memory allocation, when eqs is applied to its first argument.

When lfp is applied to a system of equations eqs, it performs no actual computation. It produces a valuation, get, which represents the least solution of the system of equations. The actual fixed point computation takes place, on demand, when get is applied.