Finding a common factor in $\lambda$-terms that agree under certain substitutions

Question

Suppose that $\mathcal{L}$ is the language of a simply typed lambda calculus of two base types, $e$ and $t$, with infinitely many constants at each type.

A substitution $j$ is a mapping from constants of type $\sigma$ to arbitrary closed $\mathcal{L}$-terms of type $\sigma$. $j$ extends to a mapping on arbitrary closed terms of type $\sigma$ in the obvious way: $j\alpha$ is the result of substituting the constants in $\alpha$ with their $j$ counterparts.

Now suppose that for each constant $a:e$ there is a term $\phi^a: t$, and suppose moreover that:

• For any substitution, $j$, if $ja = jb$ then $j\phi^a =_{\eta\beta} j\phi^b$

Does it follow that there exists a closed term $\alpha:e\to t$ such that $\phi^a =_{\eta\beta} \alpha a$ for each constant $a$?

Answer 1

In case anyone is interested, I believe the following does it. I'm assuming, for simplicity, that $\phi^a$ is in $\eta\beta$ normal form.

Pick some constant $a$ arbitrarily, and let $b$ and $d$ be distinct constants that don't appear in $\phi^a$. Finally, let us write $x,y \mapsto z$ for the substitution that substitutes both $x$ and $y$ for $z$ and does nothing else.

Firstly we prove that for any constant $c\not= b$, $\phi^c$ does not contain $b$. Let $k=a,c\mapsto d$. Then $k\phi^a =_{\eta\beta} k\phi^c$ since $ka=kc = d$. Indeed $k\phi^a = k\phi^c$, since $\phi^a$ and $\phi^b$ are in normal form, and $k$ substitutes constants, so that $k\phi^a$ and $k\phi^c$ are in normal form too. $k\phi^a$ does not contain $b$, since $\phi^a$ does not contain $b$, and $k$ introduces only $d$. So $k\phi^c$ does not contain $b$, and thus $\phi^c$ does not contain $b$ since $k$ leaves $b$ alone.

Now $\phi^b$ can be decomposed into $\alpha b$ where $\alpha$ does not contain $b$ (let $\alpha = \lambda x \phi^b[x/b]$). Let $c$ be any constant, and let $i = b,c\mapsto c$. Since $ib=ic$, we know that $i\phi^c =_{\eta\beta} i\phi^b =_{\eta\beta} i(\alpha b) =_{\eta\beta} i(\alpha)ib = \alpha ib = \alpha c$. Secondly, $i\phi^c = \phi^c$ since, as we showed above, $b$ does not occur in $\phi^c$. Thus $\phi^c = \alpha c$ for arbitrary $c$.