Lambda calcolo: differenze tra le versioni

Versione delle 12:24, 24 mag 2006

Versione delle 16:52, 29 mag 2006

Riga 1:

Il '''lambda calcolo''' è un [[sistema di riscrittura]] definito formalmente dal matematico [[Alonzo Church]]. È stato sviluppato per analizzare formalmente le definizioni di [[Funzione (matematica)|funzioni]], le loro applicazioni ed è uno strumento interessante per studiare anche fenomeni di [[ricorsione]] . In quanto sistema di riscrittura, esso dà una descrizione dei ''termini ben formati'', che sono le sequenze di simboli riconosciute dal sistema e in grado di essere riscritti da esso. Il lambda calcolo, infatti, definisce un insieme di ''regole di riscrittura'' che determinano in maniera precisa come i termini stessi possono essere riscritti. In questo modo, il processo di riscrittura diventa un vero e proprio [[Calcolo (matematica)|calcolo]]. Per tale ragione, nel corso di questa descrizione ci si riferirà al lambda calcolo come ''il'' calcolo, quando non ci sia pericolo di ambiguità.

Il lambda calcolo affonda le proprie radici nel concetto di [[Funzione (matematica) | funzione]]. In matematica si definiscono ''funzioni'' particolari associazioni fra gli elementi di un insieme (''dominio'') e gli elementi di un altro insieme (''codominio''). Ad esempio, se chiamiamo ''radice'' la funzione che dato un numero restituisca la sua radice quadrata, scriviamo: