basics of realizability #482
Conversation
New pages
Changed pages
|
plt-amy
force-pushed
the
aliao/realisability
branch
from
eb32396 to
cfd3865
Compare
plt-amy
force-pushed
the
aliao/realisability
branch
from
70eb62d to
0866ba8
Compare
| the information of whether the number is zero and its predecessor (if | ||
| any). These implementations are extensionally identical, in that they | ||
| both denote the same actual natural number, but for a concrete pca $\bA$, | ||
| they might genuinely be different --- we could imagine measuring the |
There was a problem hiding this comment.
I think we should add a bit here explaining why they could be different: EG, the source code is literally not the same.
| the only possible choice: we could, for example, invert the realisers, | ||
| and say that the value `true`{.Agda} is implemented by the *program* | ||
| $\tt{false}$ (and vice-versa). This results in a genuinely different | ||
| assembly over `Bool`{.Agda}, though with the same denotational data. |
There was a problem hiding this comment.
We should probably spend some more time here emphasizing that the realizability relation of an assembly views elements of the PCA as values, and not computations. IME this is where people start to get really confused; PCAs are untyped soup, so it's easy to get mislead into thinking about an element of a PCA as source code when you should think about it as a function and vice versa.
| ``` | ||
| --> | ||
|
|
||
| To understand the difference --- and similarity --- between the ordinary |
There was a problem hiding this comment.
Emphasizing the role of the propositional truncation is good, but we should probably do that after we define the maps and provide some intuition.
In particular, we should mention that maps of assemblies are "A-computable functions that preserve denotations", and that this is a place where we want to think about an element of the PCA as a computation instead of data.
| computable functions, since a realiser for $f : \nabla X \to (Y, | ||
| \Vdash)$ would have to choose realisers for $f(x)$ given no information | ||
| about $x$. Indeed, we can show that if there are non-constant maps | ||
| $\nabla \{0, 1\} \to \tt{2}$, then $\bA$ is [[trivial|trivial pca]]. |
There was a problem hiding this comment.
Would be good to call this out as a version of Rice's theorem, EG: there are no A-decidable properties of programs written inside of a non-trivia PCA A.
plt-amy
force-pushed
the
aliao/realisability
branch
from
0866ba8 to
97376da
Compare
plt-amy
force-pushed
the
aliao/realisability
branch
from
97376da to
9188d20
Compare
plt-amy
force-pushed
the
aliao/realisability
branch
from
9188d20 to
8044c32
Compare
plt-amy
force-pushed
the
aliao/realisability
branch
from
debe692 to
19c6dc3
Compare
No description provided.