A system at the cross-roads of functional and logic programming

AbstractThe type-free λ-calculus is powerful enough to contain all the polymorphic and higher-order nature of functional programming and furthermore types could be constructed inside it. However, mixing the type-free λ-calculus with logic is not very straightforward (see Aczel [1] and Scott [15]). In this paper, a system that combines polymorphism and higher-order functions with logic is presented. The system is suitable for both the functional and the logical paradigms of programming as from the functional paradigm's point of view, the system enables one to have all the polymorphism and higher order that exist in functional languages and much more. In fact even the fixed point operator Y which is defined as λƒ.(λx.ƒ(xx)) (λx.ƒ(xx)) can be type-checked to ((α→α)→α)) where α is a variable type. (λx.xx)(λx.xx) can be type-checked too, something not allowed in functional languages. From the point of view of theorem proving, the system is expressive enough to allow self-referential sentences and those sentences that lead to Russell's and Curry's paradoxes. However, the paradoxes do not hold to the notion of circular types which contain the type of propositions. In fact both sentences λx.¬xx and λx.xx→⊥ are ill-typed according to the system, because their resulting types are circular. Hence the application of either sentence to itself will not result in a proposition. The system is implemented in Milner's ML and can be seen as extending ML in two important ways. First, it extends the part related to the functional paradigm in that it can type terms that could not be typed in ML, namely, the terms that contain self-application such as the Y term above. Second, our system extends ML by adding logic to it in a consistent way