Amélia Liao @amy@types.pl

Here is something that programming semanticists may find surprising and is not well known. And, as far as I know, hasn't been published.

Very few programming languages can be interpreted in the category of sets (types are sets, programs are functions). A notorious example where this *is* possible is Goedel's System T.

However, the set-theoretical model of System T is not fully abstract. A while ago a wrote a note explaining this, which gives credit to Kreisel:

https://www.cs.bham.ac.uk/~mhe/papers/tfullabs.pdf

Perhaps I should put this in the arxiv. I am not sure it is publishable, though, because, essentially, Kreisel did the work.

But it is worth noting that my exposition of the result uses the searchability of ℕ∞, the set of decreasing binary sequences, which, in topological models, is the one-point compactification of the discrete space of natural numbers.

Additionally, related to the above proof, the model of system T in which types are interpreted as compactly generated topological spaces and programs as continuous maps *is* fully abstract.

The proof of the failure uses that system T can detect non-continuity (using searchability) but everything definable in T is continuous.

The reason for the success is Kleene-Kreisel's density theorem, which implies that T can define a dense sequence of every topological space interpreting a type. We have to combine this with Hyland's characterization of the Kleene-Kreisel continuous functionals as maps of certain compactly generated spaces.

So the failure of full abstracttion of the domain theoretic model of PCF (which can be considered as an extension of T) has nothing to do with continuity.

@agdakx I think the most concise description of the SProp situation is: strengthening in the presence of SProp is undecidable because it depends on inhabitation.

Unification depends on strengthening in many places (e.g. occurrence checking) so we can't hope for completeness even in the simplest pattern fragment.

Registration is now open for HoTT/UF '23: https://hott-uf.github.io/2023/