Relations

Reflexive: a R a, equal to itself…
Transitive: a R b ^ b R c –> a R c
Symmetric: a R b –> b R a
Anti-symmetric: a R b –> ㄱ(b R a) (causes to be not reflexive)
a R b ^ b R a –> a = b

Equivalence class: reflexive & transitive & symmetric
Partial order: reflexive & transitive & anti-symmetric, ex) <=

Least upper bound (lub): a <= c, b <= c, and all d in S.
a <= d ^ b <= d –> c <= d
Greatest lower bound (glb): c <= a, c <= b, and all d in S.
d <= a ^ d <= b –> d <= c

Worklist Algorithm using Lattices

Abstract Interpretation Ordering uses BOTTOM, Dataflow Analysis uses TOP

Try to define a global flow function F, which takes a map m as a parameter and returns a new map m’ in which individual local flow functions have been applied!

Always safe to use TOP, but hard to go down the lattice and gives less precise solution which is not favorable.
If F is monotonic and the lattice has a finite hight, it guarantees termination