Operator chart minification problem

There is a puzzle I've been knowing about a while now. I think it's an important problem to solve if I plan going on with the type-inferencer that I've been working on lately.

First some examples. The following program:

c = a + b
while (d < e) {
    c = c + e
}

Produces the chart:

a+b = c
d<e = f
e+c = c

And the following program:

a = 1 + b
c = d + (1 + 1.5)

Produces the chart:

Int + b = a
b + (Int|Rational) = c

And the following program:

f = a + b + c + d + e
u = a + b

Produces the chart:

a+b = g
g+c = h
h+d = i
i+e = f
a+b = u

Now some rules. We can collapse two expressions if we can prove that they have the same resolution. The resolution depends entirely on the input types.

For example, we can collapse a+b = g and a+b = u in the previous example, because they have same input flows. The chart shrinks to:

a+b = g&u
g+c = h
i+e = f

We rely on unique coercion on the rules. When resolving an operator, either side must be convertible to an another, but inverse must not be allowable.

Eg. If X -> Y and Y -> X, then we have a type error on X + Y, because there is no unique coercion to resolve that operation. In other hand if X -> Z, but not another way around, then X + Z can resolve to (+)::Z.

We can hoist every graph into set of input variable flows, for instance the second example can be rewritten as:

Int = x
Int|Rational = y
x + b = a
b + y = c

Now, the interesting questions related to this puzzle:

  1. Is it possible for us to know when some graph is minimal or irreducible to smaller format?
  2. Are there some other rules we can use for minifying the graph?
  3. Can an algorithm be written for minifying the graph, if the graph is internally in a flow-format?

Example of the flow-format with the first graph:

a --> x (+) [0]
b --> x (+) [1]
      x (+) [2] --> c

d --> y (<) [0]
e --> y (<) [1]
      y (<) [2] --> f

e --> z (+) [0]
c --> z (+) [1]
      z (+) [2] --> c

Similar posts