9
$\begingroup$

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.

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

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ Since the term recursive is abused, does he mean $\lambda_I$ is universal? $\endgroup$ – day Feb 17 '13 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 '13 at 19:45
5
$\begingroup$

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.

Improve this answer
$\endgroup$
0
0
$\begingroup$

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?

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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