Dala Deduzione Naturale al lambda-mu calculus, e due macchine astratte

This work is part of a new research branch initiated by B. Accattoli concerning the study of time cost models for lambda-calculus, working in particular on the reasonable ones, that is, polynomially related to the one of Turing machines. This is achieved by means of abstract machines, that are implementation schemas for fixed evaluation strategies that are a compromise between theory and practice: they are concrete enough to provide a notion of machine, and abstract enough to avoid the many intricacies of actual implementations. Abstract machines can be used to prove that the number of ?beta-steps is a reasonable time cost model, i.e. a metric for time complexity. The study can then be reversed, exploring how to use this metric to study the relative complexity of abstract machines, that is, the complexity of the overhead of the machine with respect to the number of ?beta-steps. Such a study leads to a new quantitative theory of abstract machines, where machines can be compared and the value of different design choices can be measured. Actually, the thesis is divided in two different parts, each one ending with the study of an abstract machine. The first section is an introduction to lambda-calculus starting from natural deduction, an unusual way to handle this language, focusing on a proof-theoretic perspective. Then a didactic explanation of lambda mu-calculus is exhibited; this is an extension of lambda-calculus through the mu operator, introduced by Parigot. This extended language can express the principle of excluded middle, overcoming the intuitionistic range of usual lambda-calculus. An abstract machine corresponding to lambda mu-calculus (mu-MAM) is presented and for the first time its complexity is studied. The second part deals with the open call-by-need calculus: this evaluation strategy exploits the axiom of call-by-name and the substitution on demand of call-byvalue, allowing open terms. This strategy is based on a lambda-calculus redefined by means of Linear Substitution Calculus and is more performing based than the two mentioned. A new AM for open call-by-need, called We Need LOv, is presented and its reasonableness is proved. This achievement for the machine is obtained through a labelling of explicit substitutions and other features, whose combination in a single machine had never been presented before. In the last section its complexity is analysed.