Can an Equation Solver Handle Lattice Functions with Join and Meet Operators?

[Learner]

Hi,

I need some direction help. The problem I am facing is related to solutions of equations , where equations are montone functions over complete lattice , operators being meet and join and the solution set should range over elements of lattice.

Normally data flow analysis problems in compilers are modeled as above, where the solution to equations is calculated by fixpoint calculation.

I am looking for an equation solver, that takes equations over lattice values,with operators (join and meet, instead of + -), and can provide me a solution set.

Example.

Take X, Y as variables to be determined whose domains are complete lattice L.
U is join operator. ^ is a meet operator. a,b,c are constants , the values from lattice L

X = (X U Y ) ^ a; eq-1
Y = X^b; eq-2

Suppose the above equations are montone. Then using fixpoint iteration , we can solve these equations.


I want a tool that takes such equations and solves them.

 

[kakaz]

Take X, Y as variables to be determined whose domains are complete lattice L.
U is join operator. ^ is a meet operator. a,b,c are constants , the values from lattice L

X = (X U Y ) ^ a; eq-1
Y = X^b; eq-2

Suppose the above equations are montone. Then using fixpoint iteration , we can solve these equations.


I want a tool that takes such equations and solves them.

Structure You describe is very general, but it also is algebra. So probably You should ask for software which works in general algebra and finds ( construct is probably better word) solutions. I assume that You know some algorithms for solving equations You show? If Yes, You probably may implement them efficiently in Sage environment ( by means of GAP but not only).
I have hope I help You anyway.
Regards
Kazek