Talk:Phase semantics
(Preliminaries: relations and closures) |
(→LaTeX parsing: server update moved to old version of texvc) |
||
| (5 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
== Preliminaries: relations and closures == |
== Preliminaries: relations and closures == |
||
| + | |||
| + | ===References=== |
||
I think everything I write in the preliminaries can be found in Birkhoff, "Lattice theory". Can anyone check? (I don't think I have easy access to a copy. |
I think everything I write in the preliminaries can be found in Birkhoff, "Lattice theory". Can anyone check? (I don't think I have easy access to a copy. |
||
| Line 8: | Line 10: | ||
-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:22, 8 February 2009 (UTC) |
-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:22, 8 February 2009 (UTC) |
||
| + | |||
| + | |||
| + | |||
| + | ===Notation=== |
||
| + | |||
| + | The refinement calculus people use the relation in the reverse order: what I write <math>\langle R\rangle</math>, they write <math>\langle R^\sim\rangle</math>. (The same is true of <math>[R]</math>.) I find it confusing, and since this is hardly "standard" notation one way or the other, I don't think this is important... |
||
| + | |||
| + | -- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:27, 8 February 2009 (UTC) |
||
| + | |||
| + | == Phase semantics == |
||
| + | |||
| + | ===Realisability=== |
||
| + | |||
| + | I put the remark |
||
| + | |||
| + | :{{Remark| |
||
| + | :Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}} |
||
| + | |||
| + | at the end of the subsection "multiplicative connectives". |
||
| + | |||
| + | Has anybody heard the same about Tait proof and biorthogonal? |
||
| + | |||
| + | -- [[User:Pierre Hyvernat|Pierre Hyvernat]] 21:13, 8 February 2009 (UTC) |
||
Latest revision as of 08:13, 22 October 2011
Contents |
[edit] Preliminaries: relations and closures
[edit] References
I think everything I write in the preliminaries can be found in Birkhoff, "Lattice theory". Can anyone check? (I don't think I have easy access to a copy.
In particular, I think xR was written 
, with the relation R being implicit.
If so, we should add a reference to that.
-- Pierre Hyvernat 11:22, 8 February 2009 (UTC)
[edit] Notation
The refinement calculus people use the relation in the reverse order: what I write 
, they write 
. (The same is true of [R].) I find it confusing, and since this is hardly "standard" notation one way or the other, I don't think this is important...
-- Pierre Hyvernat 11:27, 8 February 2009 (UTC)
[edit] Phase semantics
[edit] Realisability
I put the remark
- Remark:
- Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...
at the end of the subsection "multiplicative connectives".
Has anybody heard the same about Tait proof and biorthogonal?
-- Pierre Hyvernat 21:13, 8 February 2009 (UTC)
