# 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? – Dave Clarke Feb 17 '13 at 8:58
Might help to be more precise about what "equivalent" means here? – usul Feb 17 '13 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 '13 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 Pudlák Feb 17 '13 at 19:45
Thanks a lot for the extension. Now it is clear. – day Feb 17 '13 at 23:36

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.

-
Thanks, cody, sounds like an interesting paper. – day Feb 20 '13 at 17:18

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?

-