UP Lambda-SKI cube

Type-free lambda logics (LambdaL)

Type-free lambda logics (LambdaL)

I don't know that these have ever been studied. I think its just a historical accident that the people who were interested in type-free systems worked with combinators rather than lambda abstraction.

However, if you want one of these then you could get one by adding lambda abstraction to one of the type free combinatory logics. Some care would be needed to ensure that this is just a mere notational extension or inconsistency might result.

An alternative that I have given some attention to is a classical type free theory of functions including lambda abstraction which is modelled on the kinds of function which appear in first order set theory. In such a system the constraint on abstraction in set theory which is reflected in the principle of separation would impose a constraint on the domains over which the function could be defined.

up home © RBJ created 1995/12/10 modified 1995/12/10