Supponiamo che ho una lista scott-encoded come ad esempio:Esiste un termine non ricorsivo che si ripiega su un elenco codificato in scott?
scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))
Voglio una funzione che riceve questo tipo di lista e lo converte in un elenco effettivo ([1,2,3]), salvo che tale funzione non può essere ricorsiva. Cioè, deve essere nella forma normale eta-beta. Esiste quella funzione?
OK, ci provo. Sentiti libero di correggermi, perché non sono un esperto in questo.
Per arbitraria x e xs, deve essere il caso che toList (\c n -> c x xs) riduce ad un termine che è convertibile in x : toList xs.
Questo è possibile solo se riduciamo il lato sinistro a c x xs applicando (\c n -> c x xs) ad alcuni c e n. Quindi toList ~ (\f -> f ? ?). (A proposito, questa è la parte in cui non ho potuto pensare ad una discussione rigorosa, avevo alcune idee, ma nessuna molto carina, sarei felice di ricevere consigli).
Ora deve essere il caso che c x xs ~ (x : toList xs). Ma dal momento che x e xs sono variabili universali distinte, e sono le uniche variabili che si verificano nella parte destra, l'equazione è in Miller's pattern fragment, e quindi c ~ (\x xs -> x : toList xs) è la sua soluzione più generale.
Quindi, toList deve essere ridotto a (\f -> f (\x xs -> x : toList xs) n) per alcuni n. Chiaramente, toList non può avere una forma normale, dal momento che possiamo sempre spiegare l'occorrenza ricorsiva.
Non capisco la parte del frammento del modello di Miller, ma mi sembra molto corretta. – MaiaVictor
Disclaimer: Sono (ovviamente) non completamente sicuro che sia corretto. – MaiaVictor
Per quello specifico elenco, sì esiste. Ma tu intendi sicuramente una funzione che può prendere una qualsiasi lista, arbitrariamente lunga, e restituire una lista standard, giusto? – chi
Sì, questo è ciò che intendo. – MaiaVictor
Non dovrebbe essere '\ c n -> c 3 (\ c n -> n)' alla fine dell'elenco? –