Si prega di spiegare nell'inglese più semplice e più gergale possibile, la "proprietà universale della piega"?

Question

Sto lavorando a "Real World Haskell", che ha portato a un PDF gratuito chiamato "A tutorial on the universality and expressiveness of fold". Rende il punto che una "piega" è "universale". Sto lottando con la sua definizione di "universale", e vorrei sentire il parere di coloro che hanno già investito del tempo a digerirlo: Per favore spiegate nell'inglese più semplice e più gergale possibile, la "proprietà universale della piega"? Cos'è questa "proprietà universale" e perché è importante?

Grazie.

Answer 1

(modalità gergo fuori :-)

La proprietà universale è solo un modo di dimostrare che due espressioni sono uguali. (Questo è ciò che si intende con il gergo "principio di prova"). La proprietà universale dice che se si è in grado di dimostrare queste due equazioni

g []  = v 
g (x:xs) = f x (g xs) 

allora si può concludere l'equazione aggiuntiva

g = fold f v 

Il contrario è anche vero, ma è banale da mostrare semplicemente espandendo la definizione di fold. La proprietà universale è una proprietà molto più profonda (che è un modo gergale per dire che è meno ovvio perché è vero)

Il motivo per cui è interessante fare questo è che ti permette di evitare prove per induzione, che è quasi sempre vale la pena di evitarlo.

Answer 2

carta definisce due proprietà:

g []  = v 
g (x : xs) = f x (g xs) 

e poi afferma che fold non è solo una funzione che soddisfa tali proprietà, ma è la funzione unico che soddisfa tali proprietà. che è unico al riguardo è ciò che lo rende "universale" nel senso in cui la carta sta usando.

Answer 3

La proprietà che fold ha è che è una funzione di ricorsività di lista, che è equivalente a tutte le altre funzioni di ricorsività dell'elenco, purché gli si forniscano i parametri corretti.

Ha questa proprietà, perché accetta come parametro, le funzioni che verranno applicate agli elementi nell'elenco.

Ad esempio, se abbiamo scritto una semplice funzione di somma:

sum []   = 0 
sum (head:tail) = head + (sum tail) 

allora potremmo effettivamente scrivere come una funzione di piegatura invece, passando l'operatore (+) che si vuole utilizzare per combinare la articoli:

sum list = foldl (+) 0 list 

Quindi qualsiasi funzione che agisce in modo semplice e ricorsivo su un elenco può essere riscritta come una funzione di piegatura. Quell'equivalenza è la proprietà che detiene. Credo che chiami la proprietà universale, perché funziona su tutti gli di questi algoritmi ricorsivi a elenco lineare, senza eccezioni.

E come spiega, la ragione per cui questa proprietà è così utile è che, poiché è possibile dimostrare che tutti questi altri algoritmi sono effettivamente equivalenti alla piegatura, provando qualcosa sulla piega, lo dimostriamo anche per tutti gli altri algoritmi.

Personalmente ho trovato la funzione di piegatura difficile da capire, così a volte ho usato la mia che assomiglia a questo:

-- forall - A kind of for next loop 
-- list is list of things to loop through 
-- f is function to perform on each thing 
-- c is the function which combines the results of f 
-- e is the thing to combine to when the end of the list is reached 
forall :: [a] -> (a->b) -> (b->b->b) -> b -> b 
forall [] f c e = e 
forall (x:xs) f c e = c (f x) (forall xs f c e) 

(Questo è in realtà un po 'più potente di foldl perché ha la caratteristica supplementare di applicare la funzione f per ogni elemento nell'elenco.)

Beh nessuno ha dimostrato nulla della mia funzione. Ma questo non ha importanza, perché posso dimostrare che la mia funzione è di fatto una funzione duplice:

forall l f c e = foldl c e (map fn l) 

e quindi tutte le cose che sono state rivelate su piega, sono anche dimostrato vero per la mia funzione forall, e tutti i suoi usi nel mio programma. (Nota non è necessario nemmeno considerare quale tipo di funzione c è fornita in ognuna delle diverse chiamate a forall e foldl, non importa!)

Answer 4

Ho appena trovato una nuova voce (per me) in Wikipedia, " Proprietà universale ". Fa un sacco di luce su questa domanda. Here's the link: Da esso, I (tenatively) concludono il seguente:

1. Anche se si potrebbe pensare di 100 modi diversi di camminare attraverso un elenco, di calcolo lungo la strada, e la produzione di un valore finale dalla lista, tutti e 100 i questi modi sono isomorfi (il che significa che alla fine sono uguali). C'è davvero solo un modo per ridurre una lista ad un valore, e questo è FOLD.
2. Fold è anche la "soluzione più efficiente" su come ridurre un elenco a un singolo valore. O si potrebbe dire, la soluzione più "fattorizzata" o più "semplificata".

Insieme, a quanto pare, quei 2 punti catturano il significato del termine "proprietà universale".

Answer 5

Sebbene possa essere un po 'difficile da seguire senza leggere i post precedenti della serie che spiegano le proprietà universali da un punto di vista categoriale, questo post fornisce una dettagliata spiegazione categoriale della proprietà universale della piega, oltre che della mappa e del filtro.

http://jeremykun.com/2013/09/30/the-universal-properties-of-map-fold-and-filter/

Anche se devo ancora scriverlo, il follow-up sarà generalizzare questo (e lo rendono molto più semplice da capire, anche se più astratto) di "fold-come" operazioni su strutture dati generali.

Vedi questo post per maggiori informazioni su ciò che una proprietà universale è: http://jeremykun.com/2013/05/24/universal-properties/

E qui per i link a tutti i messaggi nella serie: http://jeremykun.com/main-content/

In realtà, la risposta attualmente accettata è il modo più semplice per capire ciò che la proprietà universale sta dicendo di fold. Gli articoli collegati sopra semplicemente danno una descrizione tecnica più dettagliata attraverso la teoria delle categorie che è assente dal foglio in questione. Non sono d'accordo sull'affermazione nella risposta accettata, tuttavia, che la proprietà universale è una proprietà molto più profonda dell'affermazione priva di gergo. La proprietà universale della piega è esattamente la stessa affermazione, racchiusa nel linguaggio degli oggetti iniziali e finali secondo la natura dell'analisi delle cose con la teoria delle categorie. Questa analisi è preziosa proprio per le sue generalizzazioni naturali.