how can we detect endless rewriting chain?

[yegor256]

Let's assume I have an expression that can't be rewritten, because its rewriting leads to endless recursion:

{⟦ m ↦ ⟦ x ↦ ξ.t, t ↦ ξ.x ⟧.x ⟧}

Is it possible, with the help of normalizer, to confirm that this expression is not normalizable?

[yegor256]

@fizruk @deemp please, help

[yegor256]

@fizruk Maybe we can do this (on our side): run normalizer with --chain --max-depth=100 and then count the number of lines it produces. If the number is 100, we can be more or less confident that it didn't finish with a normal form. How does this sound?