Che tipo di lambda calcolo sarebbe Lisp vagamente essere un esempio di?

Question

Sto cercando di ottenere una migliore presa su come tipi entrano in gioco in lambda calcolo. Certo, un sacco di roba tipo teoria è sopra la mia testa. Lisp è un linguaggio tipizzato in modo dinamico, vorrei che corrispondono approssimativamente a non tipizzata lambda calcolo? O c'è una sorta di "lambda calcolo tipizzato in modo dinamico" che sono a conoscenza di?

Answer 1

  

Lisp è un linguaggio tipizzato in modo dinamico, sarebbe che corrispondono a circa lambda calcolo tipizzato?

Sì, ma solo in modo approssimativo. Nella "pura" lambda calcolo tipizzato, tutto è codificato come funzioni. (È possibile google per il popolare "Chiesa di codifica" e il meno popolare "encoding Scott".) Lisp ha dati non funzionali, come gli atomi e numeri e tale, quindi questo conterebbe come "senza tipo lambda calcolo esteso con costanti."

Un'altra importante differenza è in ordine di valutazione . Regole per la riduzione termini lambda-calcolo sono altamente non deterministico. (C'è un teorema, il teorema di Church-Rosser, che dice vagamente che, fintanto che le cose terminano, ordine di valutazione non importa.) In termini lambda pratica sono in genere ridotti utilizzando più a sinistra-esterno alias riduzione "normale-ordine", perché se qualsiasi termina strategici per la riduzione, che si fa. Questo è molto diverso da Lisp che valuta sempre argomenti di forma normale prima di fare un beta-riduzione. Questo ordine di valutazione è chiamato "chiamata per valore".

In sintesi, Lisp corrisponde a un tipizzato, chiamata per valore lambda calcolo esteso con costanti .

Answer 2

John McCarthy ha introdotto LISP in sua aprile 1960 di carta "funzioni ricorsive di espressioni simboliche e Il loro calcolo a macchina, Parte I ". Il seguente paragrafo è da pagina 6:

  

e. Funzioni e forme. E 'normale in matematica - al di fuori della logica matematica - ad usare la parola “funzione” impreciso e applicarlo a forme   come y ² + x. Perché avremo in seguito calcolare con le espressioni per le funzioni,   abbiamo bisogno di una distinzione tra le funzioni e le forme e una notazione per Express-   ing questa distinzione. Questa distinzione e una notazione per descrivere esso, dal   che deviamo banalmente, è data dalla Chiesa [3].   
...
  3. A. CHIESA, i calcoli di Lambda-Conversion (Princeton University   Press, Princeton, N. J., 1941).

Il articolo di Wikipedia sul lambda calcolo ha una storia di pubblicazioni della Chiesa. Il 1941 di carta a cui fa riferimento McCarthy sembra essere circa il tipizzato lambda calcolo, in contraddizione con l'introduzione del articolo di Wikipedia.

La parola chiave lambda in Lisp può essere inteso fare riferimento alla lambda-calcolo solo per analogia. Un Lisp espressione lambda è un tipo di funzione anonima .

Answer 3

Lisp non e 'un lambda calcolo', non so che cosa 'un lambda calcolo' è.

Se si desidera identificare lambda calcoli da lì sistema di tipo poi Lisp è proprio naturalmente. Il 'lambda' parola chiave in qualsiasi Lisp prima Scheme è sicuramente pretenzioso, e dopo Scheme c'è spazio anche per dire che è. Usando solo 'func' sarebbe stato più umile. Lisp è un processore lista soprattutto, non un 'lambda calcolo'

Ho anche scritto un piuttosto ampio articolo su questo una volta che tenta di dimostrare perché A: il termine 'programmazione funzionale' non ha senso e B: perché il parlare di 'un lambda calcolo', piuttosto che 'un sistema di tipo' è così troppo :

http://blog.nihilarchitect.net/archives/289/ on-funzionale-programmazione /

Inoltre, tenete a mente che in Lisp, tutte le funzioni sono in effetti solo argomento e può solo essere hanno list come i loro argomenti.