Termination of Polynomial Loops

on YouTube ↗19m

" summary

Decides termination for a concrete class: triangular weakly non-linear loops admit computable poly-exponential closed forms for variable values, substitution reduces non-termination to the existential first-order theory over the reals/real algebraic numbers, so termination is decidable over real algebraic numbers and non-termination is semi-decidable over Z and Q. Also gives a semi-decidable transformation from some non-twn to twn loops, and tight complexity: linear-update with real spectrum is Co-NP-complete for linear guards and forall-R-complete for non-linear guards.

AI-written summary · about

" chapters (11)

1. 0:00Polynomial loop intro
2. 0:20Termination decidability
3. 1:59Triangular weakly non-linear
4. 3:59Example triangular loop
5. 4:55Talk structure
6. 5:39Closed forms for updates
7. 8:28Termination to logic theory
8. 13:45Handling non-triangular weakly non-linear loops
9. 15:50Termination complexity linear
10. 17:41Complexity in triangular loops
11. 18:57Summary and future work