Non-Atomic Variables

  var1: [t1 -> v1; t2 -> v2]

where var1 is the name of the variable, tx are timestamps, and vx are the values of the variable at those timestamps.

Note that t(n+1) must be greater than t(n)

Domains

Domains are separate spheres of execution. Each thread would have their own Domain, for instance.

Frontier

Domains have a frontier, which establishes which variables it can see at which timestamp.

  d1: [var1 -> t1; var2 -> t3; var3 -> t7]

where d1 is the name of the domain, varx are variable names, and tx are timestamps

Unification Algorithm

    type term =
    | Var of string
    | Term of string * term list

You either have a type variable with a name, or a type constructor with a name and a list of argument

Unification takes a list of term pairs which have to be made matching.

Unification returns a list of substitutions, where a substitution is a pair of a string and a term, aka the variable name that should be substituted with the term.

Steps for unifying two terms

Try to match