Non-commutative Newton - Githubissues

mschlund / FPsolve

FPsolve: solver for polynomial equations over omega-continuous semirings

BSD 2-Clause "Simplified" License

11 stars 5 forks source link

Non-commutative Newton #8

Open mschlund opened 11 years ago

mschlund commented 11 years ago

Requires (these are sketchy thoughts...) :

From a (system of) polynomial(s), obtain its unfolding (=again a (system of) polys with additional variables).
Define how to solve linear non-commutative equations (perhaps the semiring can specify that?) OR (similar to what we do in the comm. case with the Jacobian and the FreeSR): solve the linear equations symbolically (once) over the semiring of contexts (foo [box] bar).
- The symbolic solution then gives rise to an iteration scheme, which is basically a function of type (context -> context)
- e.g. for finite SRs we can either solve the linear equations by Kleene-iteration (in each Newton-step), or directly work with the symbolic context-representation of the solution (if this can be done in a meaningful way)

timvieira commented 2 years ago

I'm very curious about this 'context semiring' (#11): could you provide a reference (or sketch of how it works)? Is that like 3.4.4 of your dissertation?

mschlund commented 2 years ago

Yeah exactly! (as you mentioned my thesis: just as a reference for any readers https://d-nb.info/109842865X/34) The definite reference is the "Handbook of Weighted Automata" (M. Droste, W. Kuich, H. Vogler, 2009) where the things are called "contexts" I think (effectively linear grammars imho). What this Newton-stuff then just shows is that you can approximate any CFG with an (infinite) sequence of linear grammars. I think the practical value is limited however :) -- you simply have a different notation for a linear CFG as this "expression-with-numbered-holes". I think it may be a kind of "weaseling-out" of the question of how to actually "solve" the linear system of equations :)

timvieira commented 2 years ago

Awesome, thanks. I think that I see the connection to linear CFGs, but my worry is that linear-CFGs aren't closed under the operations needed to solve a system (addition: ok, multiplication, no, star: no). Maybe contexts are closed because they are actually weighted tree automata... which maybe are sufficiently closed to shove through a Gaussian elimination variant?

mschlund commented 2 years ago

Yeah maybe I was really sloppy :) In my naive understanding "rational tree expressions"/"contexts" were essentially linear grammars but this is false of course :)

timvieira commented 2 years ago

Haha, no worries, still a helpful connection!

The connection to linear CFGs is also in this paper. They appear to have a (rather expensive sounding) workaround for non-commutative semirings which lift the product operation into a Kronecker product... I haven't had time to get into the details yet (there is a talk recording)

mschlund commented 2 years ago

Yeah the relationship does not run back and forth :) but rational tree expressions still suffice to represent the solution ... however I don't really know what to do with them then (and also the question of convergence in finite time remains of course). (also btw: the Kronecker-Product-Construction they use for the predicate-abstractions is also described in my thesis for matrices over commutative semirings)

timvieira commented 2 years ago

(and also the question of convergence in finite time remains of course).

Oh, is it an open question?

(also btw: the Kronecker-Product-Construction they use for the predicate-abstractions is also described in my thesis for matrices over commutative semirings)

I thought it looked familiar 😉.

I am slowly working my way through your thesis. It's definitely the best resource on semiring Newton. (I am using Newton's method in a chapter of my thesis to execute our programming language Dyna https://arxiv.org/abs/2109.06966)