Timeline for Notation in 'The lambda calculus, its syntax and semantics' by H.P. Barendregt
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 21, 2018 at 11:02 | comment | added | Mauro ALLEGRANZA | See 14.3 (it is referred back to it at page 497). | |
| Mar 18, 2018 at 11:59 | history | edited | Peter LeFanu Lumsdaine |
Added tag lo.logic (all questions are supposed to have at least one top-level tag)
|
|
| Mar 18, 2018 at 9:16 | comment | added | tpsp_lcs | @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. | |
| Mar 18, 2018 at 3:06 | comment | added | Andreas Blass | 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? | |
| Mar 17, 2018 at 22:11 | review | First posts | |||
| Mar 17, 2018 at 22:25 | |||||
| Mar 17, 2018 at 22:09 | history | asked | tpsp_lcs | CC BY-SA 3.0 |