>It's possible (due to the Halting Problem) that we keep getting applications no matter how much we try to simplify, in which case we've hit an infinite loop wh

>It's possible (due to the Halting Problem) that we keep getting applications no matter how much we try to simplify, in which case we've hit an infinite loop while trying to calculate "t", and hence we can never reach the point where we can apply it to "s". But note that the _order_ of the reductions doesn't matter, as long as they're valid reductions. We always get the same result or it never halts like you said. https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem The Church-Rosser theorem probably deserves its own blog post.