Il lambda-calcolo con la strategia Call-by-Value

Il lambda-calcolo è un sistema formale, ideato da Alonzo Church per studiare un ramo dell'informatica teorica, la teoria della calcolabilità, che studia quali siano le funzioni calcolabili. All'interno del documento viene introdotto il formalismo, in particolare ne vengono definite la sintassi e le regole di riduzione, e si osserva come il sistema sia non-deterministico. Per ovviare a questo problema, si rende necessario fissare una strategia di valutazione, che ci permette di operare in un ambiente deterministico. Una delle strategie di maggior rilevanza è la cosidetta Call-by-Value, una restrizione che consente di operare una riduzione soltanto nel caso in cui l'argomento della funzione sia un valore. Vengono quindi introdotte diverse presentazioni della strategia Call-by-Value, con delle osservazioni riguardo alcuni problemi semantici che si presentano con la strategia. Viene infine presentato il Value Substitution Calculus, un nuovo calcolo esteso che estende la sintassi del lambda-calcolo tradizionale attraverso le sostituzioni esplicite, e vengono mostrati alcuni dei più recenti sviluppi. L'elaborato vuole essere un punto di partenza per chi si approcci al lambda-calcolo e in particolare alla strategia Call-by-Value.