Investigations into the foundations of functional programming and an implementation of existential quantification on a lambda calculus based reduction machine
Klaus Berkling, Heinz Schluetter · 1987
This work originated with the task of integrating logic and functional programming in a function based reduction system by the addition of existential quantification and absolute set abstraction. The thesis is divided into two parts, the first and main one dealing with language aspects, and the second with (abstract) architectures. Since we think that it is important to understand the motivations behind ideas we give a detailed account of the early development of two of the three underlying calculi, the combinatory and the lambda calculus, and explore some relationships between them. Berkling's number variable extension of the lambda calculus, which forms the basis of the implementation, is presented in detail, as well as his scheme of headorder reduction; the concepts are then used to analyse the unification problem for combinatory terms. After a discussion of function languages and a logic language we will take a closer look at efforts which are trying to combine the two families of languages; the main part of this section will describe our own work in that direction and the difficulties encountered. Finally, the basic ideas underlying (abstract) function machines (with the G-machine as a prime example) will be described; the main emphasis, however, will be on the RED 1.5-machine, whose strengths and weaknesses will be thoroughly discussed.