Head variables of terms after application

Question

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?

Answer 1

Here's a counterexample to your conjecture.

$$ \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}$$

This beta-normal, eta-long with index 1. Now, consider the two following terms, both also of index 1:

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