<p>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.</p>

<p>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. </p>

<p>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. </p>

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

CC BY-SA 3.0
2017-09-30T01:20:47.957Z
2017-09-30T01:26:13.900Z
2017-09-30T01:26:13.900Z
Andrew Bacon
<p>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.</p>

<p>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.</p>

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

<ul>
<li>For any substitution, $j$, if  $ja = jb$ then $j\phi^a =_{\eta\beta} j\phi^b$</li>
</ul>

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

CC BY-SA 3.0
2017-09-28T18:06:52.980Z
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
CC BY-SA 3.0
2017-09-28T19:09:58.873Z
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
CC BY-SA 3.0
2017-09-28T19:10:28.730Z
Can you explain how it's an application of the Yoneda lemma? I'm finding it hard to see the connection!
Andrew Bacon
CC BY-SA 3.0
2017-09-28T20:23:08.127Z
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
CC BY-SA 3.0
2017-09-28T20:52:19.153Z
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
CC BY-SA 3.0
2017-09-28T21:34:35.577Z
I was thinking of $\phi$ as a function that respects $\alpha$-equivalence.
Max New
CC BY-SA 3.0
2017-09-28T21:41:45.930Z
Wouldn't it have to respect renaming of free variables as well? (I.e. trivialising $\phi$ so that $\phi^x = \phi^y$ for any $x$ and $y$.) Or am I misunderstanding something?
Andrew Bacon
CC BY-SA 3.0
2017-09-28T21:52:56.057Z
Right I'm treating all of the terms as only defined up to $\alpha$-equivalence, as they would be in the CCC term model.
Max New
CC BY-SA 3.0
2017-09-28T21:57:41.033Z
Let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/66365/discussion-between-andrew-bacon-and-max-new).
Andrew Bacon
<type-theory><lambda-calculus><typed-lambda-calculus>
Finding a common factor in $\lambda$-terms that agree under certain substitutions
Andrew Bacon
# Finding a common factor in $\lambda$-terms that agree under certain substitutions

(Asked by: username_0 on 2017-09-28)

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

**Tags:** type-theory, lambda-calculus, typed-lambda-calculus

> **Comments:**
> **username_1**: 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).  
> **username_0**: 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).  
> **username_0**: Can you explain how it's an application of the Yoneda lemma? I'm finding it hard to see the connection!  
> **username_1**: 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.  
> **username_0**: 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.  
> **username_1**: I was thinking of $\phi$ as a function that respects $\alpha$-equivalence.  
> **username_0**: Wouldn't it have to respect renaming of free variables as well? (I.e. trivialising $\phi$ so that $\phi^x = \phi^y$ for any $x$ and $y$.) Or am I misunderstanding something?  
> **username_1**: Right I'm treating all of the terms as only defined up to $\alpha$-equivalence, as they would be in the CCC term model.  
> **username_0**: Let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/66365/discussion-between-andrew-bacon-and-max-new).  

---

## 1 answers

### Answer by username_0 on 2017-09-30. Score: 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$.


---

