Editing Combinatory logic (section)

===== CL<sub>K</sub> versus CL<sub>I</sub> calculus =====
A distinction must be made between the '''CL'''<sub>K</sub> as described in this article and the '''CL'''<sub>I</sub> calculus. The distinction corresponds to that between the λ<sub>K</sub> and the λ<sub>I</sub> calculus. Unlike the λ<sub>K</sub> calculus, the λ<sub>I</sub> calculus restricts abstractions to:
::''λx''.''E'' where ''x'' has at least one free occurrence in ''E''.
As a consequence, combinator '''K''' is not present in the λ<sub>I</sub> calculus nor in the '''CL'''<sub>I</sub> calculus. The constants of '''CL'''<sub>I</sub> are: '''I''', '''B''', '''C''' and '''S''', which form a basis from which all '''CL'''<sub>I</sub> terms can be composed (modulo equality). Every λ<sub>I</sub> term can be converted into an equal '''CL'''<sub>I</sub> combinator according to rules similar to those presented above for the conversion of λ<sub>K</sub> terms into '''CL'''<sub>K</sub> combinators. See chapter 9 in Barendregt (1984).