2
$\begingroup$

I'm reading the book 'The lambda calculus its syntax and semantics'. In part 5, chapter 19: Local structure of Models, more specifically 19.2 Local structure of $D_\infty$, the notation $D_\infty \vDash M \sqsubseteq N$ is used. This relation is used to proof that the theory of $D_\infty$ corresponds with the theory of $K^*$.

My question is that anyones knows where it stands for. I can't find the symbol in the index of symbols. I didn't came across the symbol (except when dealing in cpo's) in the context of terms. I can't figure out the meaning/definition it by reading the proofs.

The proofs where it is used, aren't fully worked out since it looks like that of the local structure of $P\omega$. But there the notation $\subseteq$ is used instead of $\sqsubseteq$. As $P\omega$ is is ordered by inclusion and $D_\infty$ is a CPO (ordered by $\sqsubseteq$), I would think that the notation comes from there, but then I don't see how a model derives the 'inclusion' since models (and theories) only deal with equality of terms (under their evaluation).

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ I don't have the book, but is there anything wrong with what seems to me the natural interpretation: $M$ and $N$ are two members of the domain $D_\infty$ and $M$ is below $N$ in the ordering of that domain? $\endgroup$
    – Andreas Blass
    Commented Mar 18, 2018 at 3:06
  • $\begingroup$ @AndreasBlass I don't think it is wrong and I also think that it should be that. But the problem for me is that there is only defined $D_\infty \vDash M=N \iff \llbracket M\rrbracket_\rho = \llbracket N\rrbracket_\rho$. En we can indeed as you suggest then write $D_\infty \vDash M\sqsubseteq N \iff \llbracket M\rrbracket_\rho \sqsubseteq \llbracket N\rrbracket_\rho$. But since it isn't defined I'm not sure about it. $\endgroup$
    – tpsp_lcs
    Commented Mar 18, 2018 at 9:16
  • $\begingroup$ See 14.3 (it is referred back to it at page 497). $\endgroup$
    – Mauro ALLEGRANZA
    Commented Mar 21, 2018 at 11:02

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .