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
    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
    Mar 18, 2018 at 9:16
  • $\begingroup$ See 14.3 (it is referred back to it at page 497). $\endgroup$
    – Mauro ALLEGRANZA
    Mar 21, 2018 at 11:02

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.