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?


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

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

3 Answers 3


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$. ...

  • $\begingroup$ Since the term recursive is abused, does he mean $\lambda_I$ is universal? $\endgroup$
    – day
    Feb 17, 2013 at 15:58
  • $\begingroup$ @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. $\endgroup$
    – Petr
    Feb 17, 2013 at 19:45
  • $\begingroup$ In To mock a mockingbird the author claims that Neither theory can be said to be "better" than the other; each has applications which the other does not. Was he wrong? (I've asked here, but haven't got a satisfying answer.) $\endgroup$
    – Enlico
    Mar 10, 2023 at 7:43

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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.