Есть ли какой-нибудь нерекурсивный термин, который складывается над списком scott-encoded?

Question

Предположим, что у меня есть scott-encoded список таких как:

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

Я хочу функцию, которая получает такой вид списка и преобразует его в списке фактических ([1,2,3]), за исключением того, что такая функция не может быть рекурсивным. То есть, она должна быть в нормальной форме эта-бета. Существует ли эта функция?

Answer 1

Хорошо, я делаю снимок. Не стесняйтесь поправлять меня, потому что я не эксперт в этом.

Для произвольных x и xs, он должен быть так, что toList (\c n -> c x xs) сводится к термину, который способен переходить в x : toList xs.

Это возможно, только если мы уменьшим левую сторону до c x xs, применив (\c n -> c x xs) к некоторым c и n. Итак, toList ~ (\f -> f ? ?). (Кстати, это та часть, где я не мог придумать хороший строгий аргумент, у меня были некоторые идеи, но у меня не было ничего хорошего. Я был бы рад услышать подсказки).

Теперь это должно быть так, что c x xs ~ (x : toList xs). Но так как x и xs представляют собой различные универсальные переменные, и они являются единственными переменными, входящими в правую сторону, уравнение находится в Miller's pattern fragment, и поэтому c ~ (\x xs -> x : toList xs) является его наиболее общим решением.

Таким образом, toList должен уменьшиться до (\f -> f (\x xs -> x : toList xs) n) для некоторых n. Очевидно, что toList не может иметь нормальную форму, так как мы всегда можем развернуть рекурсивное возникновение.