<p>You've basically answered the question yourself.</p>
<p><span class="math-container">$\lambda K$</span> is just another name for the standard, untyped lambda calculus.</p>
<p><span class="math-container">$\lambda I$</span> is a strict subset of <span class="math-container">$\lambda K$</span>.</p>
<p><span class="math-container">$\lambda I$</span> doesn't allow terms where one abstracts over a variable but doesn't use it. So
<span class="math-container">$$K = \lambda xy.x \in \lambda K$$</span>
but
<span class="math-container">$$ K \not\in \lambda I$$</span></p>
<p>Thanks to this restriction, <span class="math-container">$\lambda I$</span> has some interesting properties, in particular if <span class="math-container">$M$</span> has a normal form then so do all its sub-terms.</p>
<p><a href="http://mathgate.info/cebrown/notes/barendregt.php" rel="noreferrer">Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics</a> contains some notes about <span class="math-container">$\lambda I$</span>, namely:</p>
<blockquote>
<p>... the <span class="math-container">$\lambda I$</span> calculus is sufficient to define all recursive functions  (since <span class="math-container">$K_1 := \lambda xy . yIIx$</span> satisfies <span class="math-container">$K_1xc_n = x$</span> for each of Church's numerals <span class="math-container">$c_n := \lambda fz . f^n z$</span> - it is also the case that for each finite set <span class="math-container">$n$</span> of nf's, we can find a &quot;local <span class="math-container">$K$</span> for <span class="math-container">$n$</span>&quot; <span class="math-container">$K_n$</span> such that <span class="math-container">$K_nMN = M$</span> for each <span class="math-container">$N$</span> in <span class="math-container">$n$</span>).</p>
<p>... The <span class="math-container">$\lambda I$</span> calculus corresponds to the combinatory logic with primitive combinators <span class="math-container">$I$</span>, <span class="math-container">$B$</span>, <span class="math-container">$C$</span>, and <span class="math-container">$S$</span>. ...</p>
</blockquote>

CC BY-SA 3.0
2013-02-17T15:58:12.513Z
Since the term *recursive* is abused, does he mean $\lambda_I$ is universal?
day
CC BY-SA 3.0
2013-02-17T19:45:14.360Z
@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](http://en.wikipedia.org/wiki/%CE%9C-recursive_function). 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](http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis).
Petr
CC BY-SA 4.0
2023-03-10T07:43:02.663Z
In [To mock a mockingbird](https://en.wikipedia.org/wiki/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](https://math.stackexchange.com/questions/4164233/doesnt-lambda-k-calculus-include-lambda-i-calculus), but haven't got a satisfying answer.)
Enlico
CC BY-SA 3.0
2013-02-17T12:27:11.103Z
2013-02-17T19:41:20.510Z
2020-06-17T09:38:08.363Z
Petr
<p>I don't have much to add to the other answers, except that for <strong>termination behavior</strong>, it is sufficient to consider only the $\lambda_I$ version: see e.g. <a href="http://link.springer.com/article/10.1023/A:1025693307470">Strong Normalization from Weak Normalization by Translation into the Lambda-I-Calculus</a> by Gortz, Reuss and Sorensen.</p>

CC BY-SA 3.0
2013-02-19T20:29:26.120Z
2013-02-19T20:29:26.120Z
cody
<p>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?</p>

CC BY-SA 3.0
2013-02-17T05:00:05.640Z
2013-02-17T05:00:05.640Z
Noga
<p>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?</p>

<p><em>EDIT</em></p>

<p>By <em>equivalent</em>, I mean they have the same expressive power, namely, being <em>universal</em> or <em>Turing complete</em>.</p>

CC BY-SA 3.0
2013-02-17T08:58:39.090Z
Do you have references, to make the question more self-contained?
Dave Clarke
CC BY-SA 3.0
2013-02-17T15:15:47.653Z
Might help to be more precise about what "equivalent" means here?
usul
<lambda-calculus>
Are the $\lambda_I$-Calculus and the $\lambda_K$-Calculus equivalent?
day
# Are the $\lambda_I$-Calculus and the $\lambda_K$-Calculus equivalent?

(Asked by: username_0 on 2013-02-16)

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

**Tags:** lambda-calculus

> **Comments:**
> **username_1**: Do you have references, to make the question more self-contained?  
> **username_2**: Might help to be more precise about what "equivalent" means here?  

---

## 3 answers

### Answer by username_3 on 2013-02-17. Score: 12 | Accepted answer

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](http://mathgate.info/cebrown/notes/barendregt.php) 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$. ...

> **Comments:**
> **username_0**: Since the term *recursive* is abused, does he mean $\lambda_I$ is universal?  
> **username_3**: @plmusername_0 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](http://en.wikipedia.org/wiki/%CE%9C-recursive_function). 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](http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis).  
> **username_4**: In [To mock a mockingbird](https://en.wikipedia.org/wiki/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](https://math.stackexchange.com/questions/4164233/doesnt-lambda-k-calculus-include-lambda-i-calculus), but haven't got a satisfying answer.)  

---

### Answer by username_5 on 2013-02-19. Score: 5

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](http://link.springer.com/article/10.1023/A:1025693307470) by Gortz, Reuss and Sorensen.


---

### Answer by username_6 on 2013-02-17. Score: 0

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?


---

