General notation for $\lambda x_1 … x_n.x_i$? Can it be called $\pi^n_i$?

In Lecture Notes on the Lambda Calculus by Peter Selinger, the notation for project is as follows:

• $\pi_1 = \lambda p.p(\lambda xy.x)$
• $\pi_2 = \lambda p.p(\lambda xy.y)$
• $\pi^n_i = \lambda p.p(\lambda x_1 … x_n.x_i)$

Is there a notation for the same thing without the leading $\lambda p.p$? So:

1. $\lambda x_1 x_2.x_1 = T$
2. $\lambda x_1 x_2.x_2 = F = \bar 0$
3. $\lambda x_1 … x_n.x_i$

I know 1. is also called $T$ for true and 2. is also called $F$ for false or $\bar 0$ for Church number $0$, but is there a general notation for 3.?

Solution 1:

As wikipedea reference showed your above notations for $T,F, \bar 0$ are commonly used in lambda calculus applications to model Booleans, arithmetic, data structure, etc. Your above $\pi^n_i$ is the standard notation for projection function of a n-tuple as one can easily verify $\pi_1, \pi_2$ are just its special case when the projection function only applies to a 2-tuple (a pair which can be written as $λz.zMN$ since in pure functional programming any data needs to be modeled as lambda function abstraction, not application). So $λxy.x$ without the leading $λp.p$ is like a kernel of the projection function $\pi_1$ (of a pair data structure), itself is not the whole projection function, you have to add back $λp.p$ to complete it. A quick verification shows $λp.p(λxy.x)(λz.zMN) →_β M$, but without the leading $λp.p$, we have $(λxy.x)(λz.zMN) →_β λyz.zMN$ which obviously doesn't do the job of projecting a pair to its first (inL) object.

But as its notation used in Booleans above, you already know $λxy.x$ can act as a projection of the application of 2 lambda terms $MN$ (not a data structure pair as above). So I'd say the answer for your question is both a kernel of a general projection function $\pi^n_i$ of n-tuple or can be a projection $\pi^n_i$ itself of the application of $n$ terms to filter our (project) its $i$th term, it all depends on your point of view.