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 '18 at 14:36

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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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