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?

  • 1
    $\begingroup$ 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? $\endgroup$
    – cody
    Jan 24, 2018 at 14:36

1 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).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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