3

The $\lambda_I$-calculus is a restricted version of the usual $\lambda$-calculus. The set of expressions in this restricted calculus, $\Lambda_I$, can be defined inductively:

  1. If $x$ is a variable, then $x \in \Lambda_I$.
  2. If $M \in \Lambda_I$ and $x$ is a free variable in $M$, then $(\lambda x.M) \in \Lambda_I$.
  3. If $M, N\in\Lambda_I$, then $(MN)\in\Lambda_I$.

The restriction is the added requirement in the abstraction rule (rule $2$) that $x$ be a free variable in $M$. In particular, in the usual $\lambda$-calculus we have "constant" expressions like $\lambda y.x$; here we do not. However, with the usual definition of $I=\lambda x.x$, we see that by rule $2$, $I\in \Lambda_I$.

Recall that the Church numerals are usually defined as follows:

  • $C_0 := \lambda fx.x = \lambda f.I$
  • $C_1 := \lambda fx.fx$
  • $C_2 := \lambda fx.f(fx)$
  • $C_3 := \lambda fx.f(f(fx))$

and so on, with $C_{n+1} := \lambda fx.f(C_n f x)$. Clearly $C_n \in \Lambda_I$ for $n>0$, so we can just define $C_n^I=C_n$ for $n>0$. But $C_0 \not\in \Lambda_I$, so we are forced to use an alternate version:

  • $C_0^I := \lambda f x. f I I x$.

A theorem of Kleene says: a partial numeric function is $λ_I$-definable iff it is partial recursive. So there must be a $λ_I$-definable version of the Predecessor function, which satisfies ${\mathsf{Pred}} \;C^I_{n+1} = C^I_n$. Is there a construction of this function?

mjqxxxx
  • 41,358
André Batenburg
  • 39
  • I don't know what $\lambda I$ is, but wiki site on Church encoding has predecessor function encoded in untyped lambda, maybe it will help: https://en.wikipedia.org/wiki/Church_encoding – Przemek Nov 18 '23 at 16:14
  • Can you try to properly format your comment (which essentially defines the set $\Lambda_I$, right?) and add it to your question, rather than in a comment? This is essential context for getting a good answer to your question. If you don't know MathJax, do your best and someone may edit the question to help... but we can't edit comments. – mjqxxxx Nov 18 '23 at 17:26
  • This $\Lambda _I$ is a restricted class of $\Lambda$, defined by $x \epsilon \Lambda _I; M \epsilon \Lambda _I, x \epsilon FV(M) \Rightarrow ( \lambda x.M) \epsilon \Lambda _I; M, N \epsilon \Lambda _I \Rightarrow (MN) \epsilon \Lambda _I. $ $C _0 ^I = \lambda xy.xIIy$. The other numerals are just as in $\Lambda$. $C _0= \lambda fx.x $ is not in $\Lambda _I$. Because the Predecessor for church-numeral contains a constant $K= \lambda u.x$ I am not sure whether this Predecessor function is in $\lambda _I$. – André Batenburg Nov 18 '23 at 17:27
  • Is $I$ the identity function, the same as $\lambda x.x$? Or is it a primitive? – mjqxxxx Nov 18 '23 at 17:32
  • Yes. I=$\lambda$ x.x. I $\epsilon \Lambda _I$. – André Batenburg Nov 18 '23 at 18:04
  • I attempted to fill in all the relevant information in the question. Let me know (or make your own additional corrections) if I got anything wrong. I don't actually know the answer yet, though :). – mjqxxxx Nov 18 '23 at 19:12
  • Also I would be interested to know why (or if) that definition for $C_0^I$ makes intuitive sense. Is there a nice version of the successor function that also works for taking $C_0^I$ to $C_1$? – mjqxxxx Nov 18 '23 at 19:15
  • Thanks for your editions. $C_0^I$ is not very intuitive to me, but it has the application $c_0^I c_n^I c_m^I = c_n^I II c_m^I = I c_m^I = c_m^I$. So this approximates $c_0 c_n c_m = (\lambda xy.y) c_n c_m = c_m$. – André Batenburg Nov 19 '23 at 19:08

0 Answers0