5
$\begingroup$

Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full functional submodel $M$ of $N$ such that $M\cap X=\emptyset$.

The union of any chain of functional submodels disjoint from $X$ is also a functional submodel disjoint from $X$, so by Zorn's lemma there's a maximal submodel with this property. My conjecture is that any such maximal functional submodel would be full, but I haven't been able to show this. Any pointers to relevant literature would also be welcome.

Note on terminology. Given some infinite set $N(o)$, $N(\cdot)$ is defined on complex types by identifying $N(\sigma\to\tau)$ with the set of all functions from $N(\sigma)$ to $N(\tau)$. Write $N$ for the union $\bigcup_\tau N(\tau)$. A submodel of $N$, as I am using the term, is a subset $M\subseteq N$ that is closed under application and contains the $S$ and $K$ combinators of $N$ (note in particular that it is not enough that a submodel merely contain and be closed under elements that behave like $S$ and $K$ relative to the submodel). Write $M(\sigma)$ for $M\cap N(\sigma)$, and interpret the application function $*: M(\sigma\to\tau) \to (M(\sigma)\to M(\tau))$ in the obvious way as the restriction of ordinary function application to $M$. Say that a submodel is additionally functional if $*$ is injective, and full if it is surjective.

$\endgroup$
  • $\begingroup$ I would feel more comfortable if you made it clear what rpecisely a model is. It looks like a mapping from types to sets (and presumably also from terms to elements), but when you write $M \cap X$ that's confusing. Is it supposed to be $M(o) \cap X$? $\endgroup$ – Andrej Bauer Jun 13 '16 at 14:13
  • $\begingroup$ Sorry, I was overloading the terminology a little bit: $N$ and $M$ simply denote certain sets of functions: functions which all belong to some fixed full model of type theory. By $N(\sigma)$ and $M(\sigma)$ I simply mean the subset of $N$ and $M$ respectively that corresponds to functions of that type. (This is well-defined assuming we're creating our full model using the standard function space construction, so that distinct types don't overlap etc.) $\endgroup$ – Andrew Bacon Jun 13 '16 at 14:47
  • $\begingroup$ It must be my well-typed brain that insists that $M \cap X$ makes no sense. Why would anybody want to compute the intersection of $M(o \to o)$ and $X \subseteq N(o)$? So, just to be sure. Does your question change if I say that $X \cap M(o) = \emptyset$ instead of $X \cap M = \emptyset$? In other words, are you tacitly assuming that $N(\tau)$ and $N(\sigma)$ are disjoint when $\tau \neq \sigma$? $\endgroup$ – Andrej Bauer Jun 13 '16 at 15:42
  • $\begingroup$ "In other words, are you tacitly assuming that N(τ) and N(σ) are disjoint when τ≠σ?" Yes: I'm assuming that functional types in $N$ are given by the set of all set theoretic functions (see the edit I made in response to your first question). As I emphasized at the end of my comment above, this implies that distinct types don't overlap. $\endgroup$ – Andrew Bacon Jun 13 '16 at 16:07
  • $\begingroup$ And yes: by definition $M(o) = N(o) \cap M$ so if $X\subset N(o)$ then $X\cap M(o) = X\cap M$. (The way I'm approaching the problem, using Zorn's lemma, makes this definition of a model quite natural. Provided you are working with subsets of a full model based on set theoretic functions it's fine. This sort of definition is sometimes used in the literature too -- I'm basically following Statman here: see e.g. link.springer.com/article/10.1007%2FBF02023009?LI=true.) $\endgroup$ – Andrew Bacon Jun 13 '16 at 16:21

Your Answer

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

Browse other questions tagged or ask your own question.