7
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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). $\endgroup$ – Max New Sep 28 '17 at 18:06
  • $\begingroup$ 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). $\endgroup$ – Andrew Bacon Sep 28 '17 at 19:09
  • $\begingroup$ Can you explain how it's an application of the Yoneda lemma? I'm finding it hard to see the connection! $\endgroup$ – Andrew Bacon Sep 28 '17 at 19:10
  • $\begingroup$ 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. $\endgroup$ – Max New Sep 28 '17 at 20:23
  • $\begingroup$ 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. $\endgroup$ – Andrew Bacon Sep 28 '17 at 20:52
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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