Cleaning the FGG

[davidweichiang]

means removing any nonterminal that does not yield a graph. This would be a purely grammatical operation, except that I think we also have to remove nonterminals that yield only graphs with weight zero.

A major complication is that what we call nonterminals are actually bundles of what Esparza et al call nonterminals. We could have a nonterminal whose sum product is a tensor with some zero entries. Presumably those zero entries make the system of equations not clean. What should we do about that?

• compute some kind of mask to exclude zero entries?
• invent a new way to guarantee converging to the least fixed point?

[davidweichiang]

I skimmed over the relevant sections of the Etessami and Younger paper (https://dl-acm-org.proxy.library.nd.edu/doi/10.1145/1462153.1462154, section 6-7), and it looks to me like the system of equations doesn't need to be "totally clean." Maybe it's enough that in every strongly connected component, there is at least one variable whose solution is positive? If that's true, then we have hope.

[davidweichiang]

I've read the E&Y paper a little more carefully and think that if (for Newton's method) if the "dirty" variables are still there, but the rows and columns of the Jacobian corresponding to "dirty" variables are all zero, it ought to be ok. Does that sound right?

[davidweichiang]

Commit dea0e31 adds test/test.json which demonstrates various kinds of uncleanness.

[davidweichiang]

• The nonterminal Unproductive should be removed during cleaning
• The nonterminal Unreachable can also safely be removed, though it doesn't (I think) affect convergence
• Nonterminal B is both productive and reachable; however, its first component is unreachable in the sense that fac1 has a zero weight in that component, and its second component is unproductive in the sense that fac3 has a zero weight in that component.

[davidweichiang]

It seems like cleanness is necessary for linear systems of equations too.

[kennethsible]

I am working on the cleaning algorithm now

[davidweichiang]

For the linear case, would it be correct to use torch.linalg.lstsq instead of torch.linalg.solve?

[kennethsible]

Can you elaborate on that? I am not seeing the connection. I am assuming that you would use torch.lingalg.lstsq to find the nearest solution, subject to some norm, for a linear system with no solution.

[davidweichiang]

If a linear system of equations is not clean, it is underdetermined and we want the least solution (under the ordering x ≤ y iff ∀ i. xᵢ ≤ yᵢ). According to its docs, torch.linalg.lstsq(Ax = b) computes A⁺ b, which in addition to being the nearest solution if there is none, is also the minimum-norm solution if there is more than one solution (https://en.wikipedia.org/wiki/Moore–Penrose_inverse#Minimum_norm_solution_to_a_linear_system).

Is it the case that the least solution is the same as the minimum-norm solution?

[davidweichiang]

I think so, right? We know that the least solution (under the ordering x ≤ y iff ∀ i. xᵢ ≤ yᵢ) exists, i.e., there exists z such that for any solution x, z ≤ x, and we also know that the minimum-norm solution exists, i.e., there exists z' such that for any solution x, ||z'|| ≤ ||x||. So 0 ≤ z ≤ z' and ||z'|| ≤ ||z|| which implies z = z'?

[kennethsible]

I think that must be correct because every term in the norm would be positive-definite.

[kennethsible]

How are you defining the least solution? x_i \leq y_i \forall x_i \in x and y_i \in y where |x| = |y|?

Edit: How can you guarantee that a least solution exists under that definition?

[davidweichiang]

(If I understand the theory correctly) it's the partial ordering x ≤ y iff ∀ i. xᵢ ≤ yᵢ, although I think it can be any partial ordering as long as x ≤ F(x) where F is the function we're finding the fixed-point of.

[davidweichiang]

How can you guarantee that a least solution exists under that definition?

Somehow it's guaranteed by Kleene's fixed-point theorem.

[davidweichiang]

torch.linalg.lstsq is not working, though -- it's returning a negative solution, which we don't want.

[davidweichiang]

torch_semiring_einsum fortunately works on Boolean tensors.

[davidweichiang]

@kennethsible How is this going?

[davidweichiang]

It really looks to me like semiring Newton's does not require cleaning (https://archive.model.in.tum.de/um/bibdb/kiefer/equations-lncs.pdf, appendix A.2-4), so I propose to close this issue.