Show newer

"If it walks like a duck and quacks like a duck, it's a duck" shows that in the type of birds, identity is determined by identity of movement and vocalisation

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:

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.

when I say several months I mean like. September

Show thread

First day in several months I've managed to get a "full night's sleep"... still too tired to do anything useful but maybe in the afternoon

huh sexy girlbots on fedi now too? and of course they're coming from lul

i'm beginning to think that universes of strict propositions have no redeeming features 🙃​

@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.

writing emails to professors like

"Dear Sir Prof. Dr. Dr. rer. nat. Lastname, it is with the utmost discomfort that I find the audacity to demand your invaluable attention for such a benign matter; unfortunately though, tackling this issue necessitates skill and experience far beyond the abilities of my humble self. Thus, I plead to your mercy and kindly ask for your assistance, if it is not too much trouble."

and getting replies like

"np here u go, cya"

was trying to get a full night sleep but i woke up at 1AM like a complete loser. hateful

Oh, I should probably look for hotels in Delft and Vienna ahead of time...

chasing after the elaborator into a dark alley and beating it unconscious to rifle through its unsolved constraints for loose partial elements

In a show of hubris that I'm sure the gods will punish me for, I've gone and merged the "boundary scavenging"/interaction point boundary PR.

I can barely wait for the first non-me person that uses this to immediately run into an IMPOSSIBLE or a garbled context or the like

As someone with no academic affiliation it's hard to understate how important sci-hub is for day-to-day work. Also fuck publishers but everyone knows that

If you want to opine on interaction point boundaries do it soon ( or forever hold your peace

... Or play around with it and submit issue reports, of course. I've tested it pretty extensively but I'm sure I'm missing something :D

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.