3 ms·
A cost model would give a proof of termination - require the output of each transform to be cheaper than the input. Confluence is less obvious.
by JonChesterfield 2y ago
A cost model would give a proof of termination - require the output of each transform to be cheaper than the input. Confluence is less obvious.
- mattalex 2y agoOnce you have strong normalization you can just check local confluence and use Newman's lemma to get strong confluence. That should be pretty easy: just build all n^2 pairs and run them to termination (which you have proven before). If those pairs are confluent, so is the full rewriting scheme.
- JonChesterfield 2y agoThat is a new one to me. Tracked the reference back to https://www.jstor.org/stable/1968867 https://www.jstor.org/stable/1968867 which looks excellent. Thank you!