b"\n_START_ARTICLE_\nLambda calcolo\n_START_SECTION_\nTermini\n_START_PARAGRAPH_\nChiamiamo termine del lambda calcolo o, pi\xc3\xb9 brevemente, lambda termine o lambda espressione qualunque stringa ben formata a partire dalla seguente grammatica, in forma Backus-Naur:_NEWLINE_dove la metavariabile  denota una variabile appartenente a un insieme infinito numerabile di variabili._NEWLINE_Parafrasando la definizione formale, un lambda termine pu\xc3\xb2 essere, rispettivamente,_NEWLINE_un nome di variabile,_NEWLINE_l'astrazione di un termine rispetto ad una variabile,_NEWLINE_o l'applicazione di un termine come argomento (o parametro attuale) di un altro.\n_START_SECTION_\nEta conversione\n_START_PARAGRAPH_\n, se ._NEWLINE_Intuitivamente, l'importanza di questa regola risiede nel fatto che consente di dichiarare identici due lambda termini sulla base del principio che se essi si comportano allo stesso modo (una volta applicati ad un parametro) essi devono quindi essere considerati, per l'appunto, identici._NEWLINE_Quando diciamo che  e  si comportano allo stesso modo, intendiamo dire che per ogni : . In altre parole possiamo anche dire che la eta-conversione assiomatizza la dimostrabilit\xc3\xa0 dell'uguaglianza nel -calcolo estensionale (Barendregt, The Lambda Calculus).\n_START_SECTION_\nCodifiche\n_START_PARAGRAPH_\nAttraverso il \xce\xbb-calcolo sono state formulate diverse codifiche. Alcuni esempi sono la Codifica di Church, e quella di Mogensen-Scott. Esistono anche codifiche che usano il lambda calcolo tipato, come il Sistema F.\n_START_SECTION_\nNumerazione\n_START_PARAGRAPH_\nLa numerazione di Church pu\xc3\xb2 esprimere l'insieme dei numeri naturali  attraverso gli assiomi di Peano. Ogni numero viene espresso come il successivo del precedente, mentre lo zero \xc3\xa8 l'unico che non \xc3\xa8 il successivo di alcun numero._NEWLINE_Tutti i numeri appartenenti all'insieme dei naturali possono essere espressi analogamente.\n_START_SECTION_\nLogica di Boole\n_START_PARAGRAPH_\nLa logica booleana o algebra di Boole, \xc3\xa8 una formalizzazione della logica che si basa su due valori, cio\xc3\xa8 vero e falso, esprimibili come di seguito._NEWLINE_Da notarsi che la funzione  rappresenta sia il valore zero che falso.\n_START_SECTION_\nForme normali\n_START_PARAGRAPH_\nUn termine del lambda calcolo si trova in forma normale se esso non \xc3\xa8 riscrivibile per mezzo della regola di beta riduzione._NEWLINE_Se la beta riduzione rappresenta un passo di computazione di un lambda termine che descrive un programma, allora la sua chiusura transitiva ne rappresenta una qualsiasi computazione._NEWLINE_Quando una riduzione \xc3\xa8 finita e massimale, il termine ridotto in forma normale rappresenta il risultato finale della computazione._NEWLINE_Per esempio, supponiamo di arricchire il calcolo aggiungendovi i numeri naturali_NEWLINE_(semplicemente denotati come )_NEWLINE_e l'operazione di addizione binaria su di essi (scritta in forma prefissa come ),_NEWLINE_entrambi peraltro direttamente codificabili come lambda termini._NEWLINE_Consideriamo ora un termine che somma  al suo argomento, ovvero ,_NEWLINE_e passiamogli ._NEWLINE_Tale applicazione converge a forma normale , infatti:_NEWLINE_._NEWLINE_Non tutti i lambda termini hanno forma normale e la beta riduzione non ha sempre lunghezza finita._NEWLINE_Questo fenomeno rappresenta il fatto che il calcolo di un programma pu\xc3\xb2 procedere indefinitamente e divergere, e permette di rappresentare funzioni parziali._NEWLINE_L'esempio classico di divergenza \xc3\xa8 costruibile a partire dal termine duplicatore_NEWLINE_,_NEWLINE_che non fa altro che prendere un termine e restituirne due copie, l'una applicata all'altra._NEWLINE_Possiamo dunque definire il termine_NEWLINE_,_NEWLINE_e notare che esso riduce a se stesso_NEWLINE_."