8
$\begingroup$

Among models of $\lambda$-calculus, some like the Bohm tree model have the property that every element is a directed sup of definable elements, whereas others like the $D_\infty$ and $P(\omega)$ models contain "extra" elements (e.g. step functions) that are not sups of sets of $\lambda$-definable elements.

Among models of the real numbers, standard models have the property that every element is a sup of a set of rational (0,1,+,-,*,/-definable) points, whereas nonstandard models can contain "extra" elements like infinitesimals.

Does this property have a common name? A model is ___ if every element is a sup of a set of definable elements, for a give notion of definability.

Related properties of similar grammatical form:

  • separability of a metric space
  • algebraicity of a continuous lattice
  • completeness of a partial order or semilattice
  • standardness of a model of the reals
  • full-abstraction of model of a programming language
Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Why not just "definability"? These matters are related to the concept of "sequentiality" as well. This light article by Curien might help. $\endgroup$
    – Basil
    Commented Dec 24, 2014 at 11:27
  • $\begingroup$ People in higher-order computability also say "recursive in f, g..." for an element definable by abstractions, applications, initial functions and fixpoints over extra (e.g. parallel) elements f, g... $\endgroup$
    – Basil
    Commented Dec 24, 2014 at 11:38
  • $\begingroup$ @Basil Thanks for the reference. Here are three "definability"-like properties: a model is definable if it can be constructed in some language; a model is "definably inhabited" if each of its elements is definable (e.g. the rationals or the algebraic reals, depending on language); and a model is "definably compact" if each of its elements is a sup of definable elements (e.g. the standard reals or the Bohm tree model). It is this last property I am interested in. $\endgroup$
    – fritzo
    Commented Dec 24, 2014 at 17:31
  • 1
    $\begingroup$ You're asking that the finite or compact elements of the model be definable. This is one of the requirements for full abstraction; maybe Basil's suggested article by Curien might help you with this. Unfortunately, a lot of the theoretical computer scientists who might have answered this question have now left MathOverflow for another site. $\endgroup$
    – Paul Taylor
    Commented Dec 24, 2014 at 20:18
  • 1
    $\begingroup$ Besides containing a spelling mistake, your title is misleading about your question. $\endgroup$
    – Paul Taylor
    Commented Dec 24, 2014 at 20:19

0

Reset to default

You must log in to answer this question.