Rule-based semantics for an extended lambda-calculus

Abstract

Many implementation techniques proposed for functional languages in the literature are based on lambda-calculus and the theory of combinators [5, 12, 14]. The main advantage of functional languages over the more conventional programming languages is their lack of side-effects which makes their semantics much simpler [2]. This paper presents a λ-calculus dialect with list-handling extensions that can be used for defining an operational semantics for functional programs. This semantics is based on a set of elementary α-rules and β-rules which collectively implement the substitution operation without explicitly using it [10]. Two extra reduction rules, called γ-rules, have been added to the system for list manipulations [11]. Combining λ-calculus with list-handling capabilities makes an efficient vectorization of λ-calculus possible. This way we obtain a very elegant treatment of mutual recursion in our system. The reduction rules described in this paper represent, in fact, an operational semantics for our extended λ-notation. An interpreter program for this extended λ-calculus has been developed by a direct implementation of the reduction rules which makes the correctness proof of the interpreter very easy. The notion of controlled reduction is introduced here to guarantee the existence of a normal form for λ-expressions representing recursively defined functions using the Y combinator.