[Compilers] Lattices


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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.