The Read-back Problem in the Distributed Implementation of the Geometry of Interaction

Introduction and General Scheme In the last years all the scientists need ever more of the information technol- ogy. All the computer scientists, physicists, engineers, statisticians, chemists and biologists need ever more powerful machines for their discoveties, innovations and researches. But sometimes the processors are not enough. For this reason it was engineered the Distributed Implementation. The idea is summarized in this sen- tence: ”the union makes the power”; if we have a big problem (in a so called Principal Processor) we could divide it in several subproblems and to send them to many machines (called Hosting Processors), which solves them autonomously. Then, once all the computations result on the hosting processors terminate we ob- tain the final result by collecting the sequentially principal processor. The problem is that many subproblems must be solved sequentially and in these cases it is not possible to apply the parallelism. Therefore, firstly we have to check if a specific problem (or subproblem) is parallelizable and in case send it to another machine to be solved. The PELCR implementation (Parallel Environment for Optimal P1 P2 Pn P INPUT OUTPUT in in out out out in Principal Processor Hosting Processors Figure 1. How Distributed Implementation works Lambda-Calculus Reduction), originated by M.Pedicini and F.Quaglia and defined in Chapter 5, shows an important example of how an intrinsically sequential task, like the β-reduction of λ-calculus, can be finally implemented on parallel machines, after a deep theoretical study based on recent developments in mathematical logic. Analysing the Read-back problem we add a further step in this study. The goal of this thesis may be summarized as follows; see Figure 2. In Chapter 1 we define some basic concepts, usefull for arguments that we will present afterward. From the Natural Deduction we introduce either the λ-calculus, showing that every typed λ-term is strongly normalizable, or the sequent calculus, showing that in the Gentzen reduction the rule of cut is eliminable (Gentzen The- orem). Successively we define the System F as an extention of the simply typed λ-calculus, where the Normalization Theorem and the Church-Rosser property still hold. If a term contents both the Normalization Theorem and the Church-Rosser property means that exists its normal form and it is unique. Moreover, the System F is so big that we can define in it many data-types: Integers, Booleans, Lists and Trees the most importants. We see then the analogies between a proof of a sequent calculus and a proof of a λ-term in the proof-net structure. Thanks to the