COMPACT BRACKET ABSTRACTION IN COMBINATORY-LOGIC

Translations from Lambda calculi into combinatory logics can be used t o avoid some implementational problems of the former systems. However, this scheme can only be efficient if the translation produces short o utput with a small number of combinators, in order to reduce the time and;transient storage space spent during reduction of combinatory term s. In this paper we present a combinatory system and an abstraction al gorithm, based on the original bracket abstraction operator of Schonfi nkel [9]. The algorithm introduces at most one combinator for each abs traction in the initial Lambda term. This avoids explosive term growth during successive abstractions and makes the system suitable for prac tical applications. We prove the correctness of the algorithm and esta blish some relations between the combinatory system and the Lambda cal culus.