Is there any non-recursive term that is reset on the scotting list?

Question

Suppose I have scott-encoded , for example:

scott = (\ cn -> c 1 (\ cn -> c 2 (\ cn -> c 3 (\ cn -> n)))) 

I need a function that receives such a list and converts it to an actual list ( [1,2,3] ), except that such a function cannot be recursive. That is, it should be in normal et-beta form. Does this feature exist?

Answer 1

OK, I give him a chance. Feel free to correct me, because I am not an expert in this.

For arbitrary x and xs this should be such that toList (\cn -> cx xs) comes down to a term that can be converted to x : toList xs .

This is only possible if we reduce the left side to cx xs by applying (\cn -> cx xs) to some c and n . So, toList ~ (\f -> f ? ?) . (By the way, this is the part in which I could not come up with a good rigorous argument, I had some ideas, but I did not have anything good. I would be glad to hear advice).

Now it should be that cx xs ~ (x : toList xs) . But since x and xs are different universal variables, and they are the only variables on the right side, the equation is in a fragment of Miller’s template , and therefore c ~ (\x xs -> x : toList xs) is its most general solution .

So, toList should decrease to (\f -> f (\x xs -> x : toList xs) n) for some n . It is clear that toList cannot have a normal shape, since we can always expand a recursive entry.