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

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$?

• What exactly do you mean by "constant", just any closed term or uninterpreted constants? If you allow open terms you can apply $\phi$ to a variable (basically the Yoneda lemma). Otherwise I would think that it's probably false (I'll try to think of a counterexample). – Max New Sep 28 '17 at 18:06
• By constant I mean uninterpreted constant. I defined substitutions on constants rather than variables so I could have a simple definition on substitution (not every $j$ would extend to a mapping on arbitrary terms if I did it with variables: I would have to worry about free variables getting bound when substituted). – Andrew Bacon Sep 28 '17 at 19:09
• Can you explain how it's an application of the Yoneda lemma? I'm finding it hard to see the connection! – Andrew Bacon Sep 28 '17 at 19:10
• Yoneda lemma says if you have a map $\phi \forall \Gamma. Hom(\Gamma,A) \to Hom(\Gamma, B)$ that is natural in $\Gamma$, you can get a map $A \to B$ by picking $\Gamma = A$ and plugging in $\phi(id_A)$. In your scenario you have a function $\phi : (\cdot \vdash e) \to (\cdot \vdash t)$. If instead you let it be applied to open terms, you would be able to run $\phi$ on $x:e \vdash x : e$ which would give you a term $x:e \vdash \phi^x : t$ and then $\cdot \vdash \lambda x:e. \phi^x : e \to t$ would be the term you want. – Max New Sep 28 '17 at 20:23
• Thanks for clarifying! I'm not sure I completely follow: Am I supposed to be thinking in terms of the CCC for the open term model? $\phi^x$ might be different for different variables $x$, but $x: e \vdash x:e$ gets the same interpretation as $y: e\vdash y:e$ in the term model. So I'm not sure if we can think of $\phi = (x:e \vdash x:e) \mapsto (x:e\vdash \phi^x:t)$ as a well defined function once we've quotiented out by $\eta\beta$ equivalence. – Andrew Bacon Sep 28 '17 at 20:52

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