Is stratification too strict?

[lukaszlew]

You wrote "the abstract algorithm seems to work fine with, for example, general recursion, so stratification is too restrict". Do you have an example of a term that's not stratified, yet the abstract algorithm works?

[VictorTaelin]

Sorry for the delay, I really need to get those Github notifications.

My point is simply that the Y-combinator works fine, and it isn't stratified. An example would be:

( λf. (λx. f (x x)) (λx. f (x x)) 
  λr. λc. λn. c (λx. x) r
  λa. λb. a
  λx. x)

Here, the Y-combinator is used to produce a list of infinite ids, and then we get its head. The Haskell equivalent would be:

let r = (\x -> x) :: r in head r

That terms correctly reduces to identity on the abstract algorithm. Moreover, as far as I understand, not having an EAL-type assignment (because the Y-combinator never halts, and EAL is terminating). Thus, there are non-stratified terms on which the abstract algorithm works. Let me know if there is any mistake on my reasoning.

I do not know simpler examples.