# Are the $\lambda_I$-Calculus and the $\lambda_K$-Calculus equivalent?

I see here and there mention of the $\lambda_I$-Calculus (in which every variable must be used at least once) and the $\lambda_K$-Calculus (in which a variable can also be unused). Are they equivalent? Why has the latter kinda obscured the former?

EDIT

By equivalent, I mean they have the same expressive power, namely, being universal or Turing complete.

• Do you have references, to make the question more self-contained? Feb 17, 2013 at 8:58
• Might help to be more precise about what "equivalent" means here?
– usul
Feb 17, 2013 at 15:15

You've basically answered the question yourself.

$$\lambda K$$ is just another name for the standard, untyped lambda calculus.

$$\lambda I$$ is a strict subset of $$\lambda K$$.

$$\lambda I$$ doesn't allow terms where one abstracts over a variable but doesn't use it. So $$K = \lambda xy.x \in \lambda K$$ but $$K \not\in \lambda I$$

Thanks to this restriction, $$\lambda I$$ has some interesting properties, in particular if $$M$$ has a normal form then so do all its sub-terms.

Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics contains some notes about $$\lambda I$$, namely:

... the $$\lambda I$$ calculus is sufficient to define all recursive functions (since $$K_1 := \lambda xy . yIIx$$ satisfies $$K_1xc_n = x$$ for each of Church's numerals $$c_n := \lambda fz . f^n z$$ - it is also the case that for each finite set $$n$$ of nf's, we can find a "local $$K$$ for $$n$$" $$K_n$$ such that $$K_nMN = M$$ for each $$N$$ in $$n$$).

... The $$\lambda I$$ calculus corresponds to the combinatory logic with primitive combinators $$I$$, $$B$$, $$C$$, and $$S$$. ...

• Since the term recursive is abused, does he mean $\lambda_I$ is universal?
– day
Feb 17, 2013 at 15:58
• @plmday I'm not sure what you mean by universal. I extended the citation a bit. The statement means that in $\lambda I$ one can express all $\mu$-recursive functions. This means that any Turing machine can be simulated in $\lambda I$ (and of course in $\lambda K$ as well). See also Church-Turing thesis.
– Petr
Feb 17, 2013 at 19:45

I don't have much to add to the other answers, except that for termination behavior, it is sufficient to consider only the $\lambda_I$ version: see e.g. Strong Normalization from Weak Normalization by Translation into the Lambda-I-Calculus by Gortz, Reuss and Sorensen.

In effect, intuitively, by definition later one includes former one as a subset. Also observe that in the real world, unused variables are norm, unless compiler catches it up. Does that answer some part of your query?