Lambda calcolo programmazione funzionale al di fuori?

Question

Sono uno studente universitario, e stiamo attualmente studiando lambda calcolo. Tuttavia, ho ancora difficoltà a capire esattamente il motivo per cui questo è utile per me. Mi rendo conto che se si fa un sacco di programmazione funzionale potrebbe essere utile, ma mi sa che non è realmente necessario per l'apprendimento di programmazione funzionale, che ne pensi?

In secondo luogo, non v'è alcun uso per il lambda calcolo all'interno del regno di Computer Science, ma al di fuori di linguaggi di programmazione funzionale?

Answer 1

Il lambda calcolo è fondamentale nella logica, teoria delle categorie, teoria dei tipi, verifica formale, ... In sostanza, nulla a che fare con la programmazione semantica del linguaggio e della logica formale. Si tratta di un formalismo così fondamentale che le persone che lavorano in questi campi non hanno nemmeno in discussione il beneficio di esso.

Credo che sia estremamente utile per comprendere la programmazione funzionale perché ti dà l'essenza della programmazione funzionale. Funzioni, applicazione, sostituzione. Sulla base di questo si può costruire le vostre abilità nel ragionamento sui programmi funzionali e trasformazioni di loro. Funzioni di ordine superiore sono un gioco da ragazzi.

Certo si potrebbe imparare la programmazione funzionale senza il lambda calcolo, ma non avrebbe mai capito veramente programmazione funzionale senza di essa.

Answer 2

Stai chiedendo un esterno applicazione della scienza informatica e della logica. Che può essere facilmente trovato, per esempio in topologia algebrica è conveniente avere una categoria chiusa cartesiano degli spazi, vedere conveniente categoria degli spazi topologici su nLab. Il linguaggio formale che corrisponde a categorie chiuse cartesiani è proprio il $ \ lambda $ -calcolo. Permettetemi di illustrare con un esempio molto semplice come questo è utile.

In primo luogo, come un esercizio di riscaldamento, Supponiamo che qualcuno si chiede se la funzione $ f: \ mathbb {R} \ to \ mathbb {R} $ definito da $ f (x) = x ^ 2 e ^ x + \ log (1 + x ^ 2) $ è differenziabile. In realtà non è necessario dimostrare che è, basta osservare che si tratta di una composizione di funzioni differenziabili, quindi differenziabile. In altre parole, hai fatto una conclusione facile basata sulla forma di definizione.

Ora, per l'esempio reale. Supponiamo che qualcuno si chiede se la funzione $ f: \ mathbb {R} \ to \ mathbb {R} $ definito da $$ f (x) = \ left (. \ Lambda f: \ mathcal {C} (\ mathbb {R}) \ int _ {- x} ^ {x} f (1 + t ^ 2) dt \ right) ( \ lambda y:. \ mathbb {R} \ max (x, \ sin (y + 3)) $$ è continuo. Anche in questo caso, possiamo immediatamente rispondere "sì" perché la funzione è definita utilizzando la $ \ lambda $ -calcolo e partendo da mappe continue $ \ max $, $ \ int $, $ \ sin $, ecc.

Le varie estensioni del $ \ lambda $ -calcolo permettono di fare la stessa cosa in altri settori. Ad esempio, poiché un liscio topos è una categoria chiusa cartesiano, qualsiasi mappa che è definita secondo la $ \ lambda $ -calcolo, partendo da derivati ??e la struttura ad anello dei reali (e si può buttare in funzione esponenziale, se lo si desidera) viene automaticamente liscio. (In realtà, la spinta principale dei topos lisci è l'esistenza di infinitesimi nilpotenti che permettono di dire le cose come significato "noi disect un disco nel isosceli infinitamente sottili triangoli".)

Answer 3

Un modo di guardare a $ \ lambda $ -calcolo è come un semplice e laconico modello di programmi parametersing. È parametrizzare il codice in quasi qualsiasi linguaggio di programmazione che ha funzioni, procedure o metodi, e in qualsiasi lingua che ha i moduli o che vi permette di parametrizzare i tipi. Parametrizzazione è una forma di riutilizzo. Poiché $ \ lambda $ -calcolo è così semplice, i punti in comune tra molti linguaggi di programmazione che consentono di codice di parametrizzare, vengono alla ribalta soprattutto chiarezza.

E 'certamente possibile per essere un buon programmatore senza sapere circa $ \ lambda $ -calcolo, ma si sta perdendo su qualcosa di bello che è anche molto utile.

Answer 4

Microsoft LINQ (Language Integrated Query) innesta capacità di programmazione funzionali in lingue procedurali. Si avvale esteso e abbastanza diretto di $ \ lambda $ -calcolo dipendenze districare e porzioni segregare dell'albero di espressione che può essere delegata al server di database. Questa è un'applicazione estremamente pratico ad alto valore commerciale.

Ho scritto una piccola applicazione commerciale utilizzando un linguaggio funzionale e vi posso assicurare che, mentre ben la pena di accademici e ricercatori sono commercialmente meno utili rispetto ai loro cugini procedurali. In realtà si tratta di una questione di cavalli per i corsi, e più pratico di tutti è un linguaggio che può essere procedurale o funzionale, come richiesto. Di conseguenza, le capacità funzionali che sono state introdotte (a C #) a sostegno della LINQ, come $ \ lambda $ -expressions, ottenere un bel po 'di uso al di fuori del contesto di query di database.

Così, quando finalmente si ritrovi costretto a fare le cose icky perché vuoi essere pagato, si possono trovare $ \ lambda $ -calcolo più utile del previsto, anche se quasi certamente non si stia utilizzando un linguaggio funzionale.

Answer 5

Senza sapere di più su di esso, ho sentito che i linguisti stanno utilizzando lambda calcolo.

http://www.sfu.ca/~jeffpell/Ling406/LambdaAbstractionOH. pdf , https://files.nyu.edu/cb125/public/Lambda/