# Head variables of terms after application

We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\lambda y_1 y_2 \ldots y_n . y_i u_1 u_2 \ldots u_m$. In this case, we shall say that $i$ is the index of this term.

My question is, does every term of a type with multiple components (that is, $n$ is greater than $1$ in the example above) behave as a function with respect to indices? Namely, given two terms of the same index of type $A_1$ above, would both return terms of type $A_2\ldots\rightarrow A_n \rightarrow 0$ with the same index?

• I am confused about your question: are the terms assumed to be closed? Are the $A_i$ assumed to be distinct? Also: why is "Church-style" relevant?
– cody
Jan 24, 2018 at 14:36

$$\begin{array}{lcl} M & : & ((0 \to 0 \to 0) \to 0 \to 0 \to 0) \to 0 \to 0 \to 0 \\ M & = & \lambda\,f\,x\,y.\;f\;(\lambda\,a\,b.\;f\;(\lambda\,u\,v.\;u)\;a\;b)\;x\;y \end{array}$$
$$\begin{array}{lcl} N & = & \lambda\,p\,x\,y.\;p\;x\;y \\ N' & = & \lambda\,p\,x\,y.\;p\;y\;x \\ \end{array}$$
Now, $M\;N$ reduces to $\lambda\,x\,y.\;x$ (index 1) and $M\;N'$ reduces to $\lambda\,x\,y.\;y$ (index 2).