# William Stirton

Some facts about polymorphically typed combinatory logic

While this may be of interest mainly to people who have some interest in the polymorphically typed lambda calculus, the only knowledge I assume is, roughly, that you know what a polymorphic type is, plus some facts about the simply typed lambda calculus and the formulae-types correspondence (the Curry-Howard isomorphism). I do not assume you know what combinatory logic is. Model theory will not come into it. So if, like me, you find the model theory of the lambda calculus a bit scary, you need have no fear on that account.

The main new result I have to announce concerns a subsystem of polymorphically typed combinatory logic which is equivalent to Goedel's T. I have an answer to the question: how many reduction steps are needed to normalize a term within this subsystem? The answer is not surprising but I think it is at least new.