Gibt es einen nicht rekursiven Ausdruck, der sich über eine scott-codierte Liste faltet?

Question

Nehmen wir an, ich habe eine Liste scott-encoded wie:

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

möchte ich eine Funktion, die eine solche Art von Liste empfängt und wandelt es in einer aktuellen Liste ([1,2,3]), mit der Ausnahme, dass eine solche Funktion nicht rekursiv sein kann. Das heißt, es muss in der eta-beta-Normalform sein. Gibt es diese Funktion?

Answer 1

OK, ich gebe es eine Chance. Fühlen Sie sich frei, mich zu korrigieren, weil ich kein Experte darin bin.

Für beliebige x und xs muss es sein, dass toList (\c n -> c x xs) zu einer Laufzeit reduziert, die x : toList xs umwandelbar ist.

Dies ist nur möglich, wenn wir die linke Seite zu c x xs reduzieren, indem (\c n -> c x xs) einige c und n zu Anwendung. Also toList ~ (\f -> f ? ?). (Übrigens, das ist der Teil, an dem ich nicht an ein schönes strenges Argument denken konnte; ich hatte einige Ideen, aber keine sehr nette. Ich wäre glücklich, Tipps zu hören).

Jetzt muss es der Fall sein, dass c x xs ~ (x : toList xs). Aber da x und xs unterschiedliche universelle Variablen sind, und sie die einzigen Variablen sind, die auf der rechten Seite vorkommen, ist die Gleichung in Miller's pattern fragment und daher ist c ~ (\x xs -> x : toList xs) ihre allgemeinste Lösung.

So muss toList auf (\f -> f (\x xs -> x : toList xs) n) für einige n reduzieren. Natürlich kann toList keine normale Form haben, da wir das rekursive Vorkommen immer entfalten können.