Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: DCPOs

John Baez (May 08 2020 at 17:52):

But go on, you seem to be explaining this stuff.

sarahzrf (May 08 2020 at 17:54):

now, if you have a very simple language—say terms are either numerals or else a term plus another term—then giving semantics is very simple: say the semantics of a term is a natural number; for literals it's the number corresponding to the numeral; for t + u, it's the sum of the semantics for t and the semantics for u

sarahzrf (May 08 2020 at 17:54):

so you can read "(3 + 4) + 5" as having a denotation of 12

sarahzrf (May 08 2020 at 17:55):

you can do something similar for the simply-typed lambda calculus into any cartesian closed category; you may have seen or heard of this

John Baez (May 08 2020 at 17:56):

You're talking about the most basic obvious way to give that lambda-calculus a semantics in CCC's, right? Then I know it.

sarahzrf (May 08 2020 at 17:56):

yep!

John Baez (May 08 2020 at 17:56):

So far no dcpos...

sarahzrf (May 08 2020 at 17:56):

about to get there :)

sarahzrf (May 08 2020 at 17:56):

so now say we, as mentioned, allow arbitrary recursion

John Baez (May 08 2020 at 17:57):

(Just making sure they hadn't slipped by already. Go ahead.)

sarahzrf (May 08 2020 at 17:58):

keep it simple: we take the STLC and add a rec operator which you use like rec x.e, with reduction rule rec x.e ↦ e[rec x.e/x]

sarahzrf (May 08 2020 at 17:59):

so a definition like f(z) = ... which uses f can be implemented as rec f. λz. ...

sarahzrf (May 08 2020 at 18:01):

the typing rule is

$\frac{\Gamma, x : \tau \vdash e : \tau}{\Gamma \vdash \operatorname{rec} x.e : \tau}$

John Baez (May 08 2020 at 18:01):

Hold on, this will take me time to absorb.

sarahzrf (May 08 2020 at 18:01):

:thumbs_up:

John Baez (May 08 2020 at 18:02):

Where did the f go in that typing rule? Did it turn into $\tau$, or $e$, or...

John Baez (May 08 2020 at 18:02):

You pulled the rug out from under me, notationally. :upside_down:

sarahzrf (May 08 2020 at 18:02):

oops!

sarahzrf (May 08 2020 at 18:02):

there, now x is not being used for 2 things

sarahzrf (May 08 2020 at 18:03):

so i can tell you that the f up there is the x in the rule

John Baez (May 08 2020 at 18:05):

Okay, let me see if I can even understand the "informal" explanation

rec x.e ↦ e[rec x.e/x]

sarahzrf (May 08 2020 at 18:05):

that's not informal! it's just operational

sarahzrf (May 08 2020 at 18:05):

it's the reduction rule as opposed to the typing rule

John Baez (May 08 2020 at 18:05):

Okay.

sarahzrf (May 08 2020 at 18:05):

it tells you how the thing computes, not how to tell when it's well-formed

John Baez (May 08 2020 at 18:05):

It was something I was supposed to understand first.

sarahzrf (May 08 2020 at 18:06):

well, this is all kind of a tangent anyway, so we can drop the typing rule :sweat_smile:

John Baez (May 08 2020 at 18:06):

I have no idea what it means except you said the word "recursion" so it's supposed to be about something being recursively defined and plugged into itself.

sarahzrf (May 08 2020 at 18:06):

yeah

John Baez (May 08 2020 at 18:06):

I cling to English words...

sarahzrf (May 08 2020 at 18:06):

sorry! let me clarify

sarahzrf (May 08 2020 at 18:06):

i forget that not everyone does PL :sob:

John Baez (May 08 2020 at 18:07):

Yes, there's a dwindling band of people who don't.

sarahzrf (May 08 2020 at 18:07):

and has its core concepts/conventions worked into their brain

John Baez (May 08 2020 at 18:07):

I can't even remember if e/x means "substitute e into x" or the other way around...

sarahzrf (May 08 2020 at 18:08):

depends on the source :sob: i meant it as substitute e for x

John Baez (May 08 2020 at 18:08):

Wow, so people don't even agree! Okay, substitute e into x.

sarahzrf (May 08 2020 at 18:08):

for x—but into the thing preceding the square brackets

John Baez (May 08 2020 at 18:08):

Could you read "rec x.e ↦ e[rec x.e/x]" translated into something more like English?

sarahzrf (May 08 2020 at 18:09):

yeah

sarahzrf (May 08 2020 at 18:09):

well, first: read rec x.e as an "inline recursive definition" much like λ is an "inline function"

John Baez (May 08 2020 at 18:09):

Okay, I'll read that except for the word "inline".

sarahzrf (May 08 2020 at 18:09):

so just as you can turn f(x) = e followed by a reference to f, into λx.e
so you can turn x = e, with x mentioned in e, followed by a reference to x, into just rec x.e

John Baez (May 08 2020 at 18:10):

Let me do an example.

sarahzrf (May 08 2020 at 18:11):

:thumbs_up:

sarahzrf (May 08 2020 at 18:11):

"do" as in you want to come up with one, or i should give you one?

John Baez (May 08 2020 at 18:11):

If x = sqrt(1+x) and I want to refer to the solution of this equation, I say

John Baez (May 08 2020 at 18:11):

rec x.sqrt(1+x)

sarahzrf (May 08 2020 at 18:11):

yeah

John Baez (May 08 2020 at 18:12):

Okay, I think I got it.

John Baez (May 08 2020 at 18:13):

That's cool, but at this rate you may give up on teaching me stuff about dcpos... I hope it's not far from here to there.

sarahzrf (May 08 2020 at 18:14):

we're getting there!

John Baez (May 08 2020 at 18:14):

So, probably something like "you can interpret a language with such a recursion operator in a dcpo..."

sarahzrf (May 08 2020 at 18:14):

yup!

sarahzrf (May 08 2020 at 18:14):

if you squint back at the reduction rule i wrote down, you'll see that the operational semantics of the expression you wrote is

sarahzrf (May 08 2020 at 18:15):

rec x.sqrt(1 + x) ↦ sqrt(1 + rec x.sqrt(1 + x)) ↦ sqrt(1 + sqrt(1 + rec x.sqrt(1 + x))) ↦ ...

sarahzrf (May 08 2020 at 18:16):

or rather: it depends on what the operational semantics of sqrt and + and so on are. if they're strict—they force their arguments to be some kind of final result before they make use of them—then you'll get what i just wrote

John Baez (May 08 2020 at 18:16):

Right.

sarahzrf (May 08 2020 at 18:17):

but if they start to compute an approximation based on partial info somehow, then you might be able to actually realize some kind of banach fixed point computation of an approximation of a fixed point using this

Daniel Geisler (May 08 2020 at 18:17):

Aren't you looking as a fixed point in this case?

sarahzrf (May 08 2020 at 18:18):

um, sorry, i can't juggle two ppl at once on this topic daniel :sweat_smile:

John Baez (May 08 2020 at 18:18):

(I'm gonna just talk to Sarah right now, since it's working.)

Right.

sarahzrf (May 08 2020 at 18:18):

but anyway, the reduction rule i wrote down above makes good sense as something that produces an ongoing process of computation that hopefully terminates

John Baez (May 08 2020 at 18:19):

I was gonna say: that Banach space fixed point stuff and approximations and such involve the metric on R, but I guess the point of dcpos is to sidestep all that.

sarahzrf (May 08 2020 at 18:19):

but in the context of math, where we don't usually view mathematical objects as such things, arbitrary recursion is generally not something you can do in your expression

sarahzrf (May 08 2020 at 18:20):

so if i say rec x.e, and i interpret e as some morphism in my CCC, then, well, it's not really clear from here what to do with that morphism to get a denotation for the whole term

sarahzrf (May 08 2020 at 18:20):

tons of morphisms don't have fixed points!

John Baez (May 08 2020 at 18:21):

Right. Is rec x.e the same as fix x.e?

sarahzrf (May 08 2020 at 18:21):

yeah

John Baez (May 08 2020 at 18:21):

Never mind.

sarahzrf (May 08 2020 at 18:22):

generally you want the denotation of a term to be the same as the denotation of anything it reduces to, or else things are weird

John Baez (May 08 2020 at 18:22):

Yes, I get it. So I bet you (or Scott or someone) is going to create a make-believe universe where everything has a fixed point.

sarahzrf (May 08 2020 at 18:22):

yup!

Dan Doel (May 08 2020 at 18:22):

(Some people do use (ultra)metric spaces for this, too.)

sarahzrf (May 08 2020 at 18:22):

but there's good reason for dcpos to model this kind of thing, and for why they're good for fixed points

sarahzrf (May 08 2020 at 18:23):

oh, but re:

generally you want the denotation of a term to be the same as the denotation of anything it reduces to, or else things are weird

sarahzrf (May 08 2020 at 18:23):

since rec x.e reduces to e[rec x.e/x], they should have the same denotation, so that's a fixed point of the denotation of e

John Baez (May 08 2020 at 18:23):

Right.

sarahzrf (May 08 2020 at 18:24):

anyway—

sarahzrf (May 08 2020 at 18:24):

the idea is roughly something like:

sarahzrf (May 08 2020 at 18:24):

you enrich your universe to contain undefined or partially-undefined objects

sarahzrf (May 08 2020 at 18:25):

then there is a partial order of "extends the information content of"

sarahzrf (May 08 2020 at 18:26):

so for example, if f, f' : X → Y, and f ≤ f', then whenever f(x) is defined, so is f'(x), among other things

John Baez (May 08 2020 at 18:26):

And they're equal I assume...

sarahzrf (May 08 2020 at 18:26):

well, no, it's the pointwise order

John Baez (May 08 2020 at 18:27):

Oh, sorry, Y is some sort of ordered set?

sarahzrf (May 08 2020 at 18:27):

but if the codomain is flat, they'd have to be equal

sarahzrf (May 08 2020 at 18:27):

err, sorry, "flat" as in

John Baez (May 08 2020 at 18:27):

I thought $\le$ was some purely "extends the information content of" order.

sarahzrf (May 08 2020 at 18:28):

if you have any set X, the "flat domain" on it is the poset X + 1 which extends X with a unique ⊥ and otherwise everything is incomparable

John Baez (May 08 2020 at 18:28):

Okay.

sarahzrf (May 08 2020 at 18:28):

i was perhaps misleading with my phrasing

John Baez (May 08 2020 at 18:28):

So all our objects are gonna be posets of some nice sort?

sarahzrf (May 08 2020 at 18:28):

yeah—dcpos with least element, generally

John Baez (May 08 2020 at 18:29):

I see, and you can take a mere set and turn it into a poset as you just described, where I guess $\bot$ means 'undefined'.

sarahzrf (May 08 2020 at 18:29):

yup!

John Baez (May 08 2020 at 18:29):

And that's a dcpo with least element...

sarahzrf (May 08 2020 at 18:29):

:wink:

sarahzrf (May 08 2020 at 18:29):

so if the codomain is flat, then if f(x) and f'(x) are both "defined" as in non-⊥, they must be equal, yeah

sarahzrf (May 08 2020 at 18:30):

but if the codomain is richer, we only need f(x) ≤ f'(x)

John Baez (May 08 2020 at 18:30):

Okay, good.

sarahzrf (May 08 2020 at 18:30):

but that's still "extends info content", because that's what the order on the codomain should mean too!

sarahzrf (May 08 2020 at 18:31):

now:

John Baez (May 08 2020 at 18:31):

So like if X and Y are mere sets, and we dcpo-ize them, their internal hom in dcpos will not be the dcpo-ization of a mere set.

sarahzrf (May 08 2020 at 18:31):

nope!

sarahzrf (May 08 2020 at 18:31):

er, i mean: you're correct that it will not be!

John Baez (May 08 2020 at 18:32):

That's pronounced "yeah - no!"

sarahzrf (May 08 2020 at 18:32):

:)

John Baez (May 08 2020 at 18:32):

I'm just guessing the category of dcpo's you're talking about is cartesian closed because if it weren't who'd ever want to think about it?

sarahzrf (May 08 2020 at 18:33):

iirc it is

John Baez (May 08 2020 at 18:33):

Okay, go ahead, though I think I'm getting the idea. I'm still not sure why it's so good to limit ourselves to d cpos instead of those with more general colimits.

sarahzrf (May 08 2020 at 18:33):

however i don't remember the details

sarahzrf (May 08 2020 at 18:34):

i'll circle back around to that in a minute!

sarahzrf (May 08 2020 at 18:35):

anyway: we can view the previously-described "ongoing process of computation" as a gradual enrichment of information content—a sequence of approximations to a final result

sarahzrf (May 08 2020 at 18:36):

so to give this semantics, you collect all of those approximations ahead of time in your platonic math-world, and the denotation is the thing they converge to—the sup

John Baez (May 08 2020 at 18:37):

Nice!

John Baez (May 08 2020 at 18:37):

Yes, you set it up so that part is obviously the goal.

sarahzrf (May 08 2020 at 18:38):

indeed, the kleene fixed-point theorem states that for a dcpo with least element, every scott-continuous endomorphism f has a least fixed point, which you can compute as the sup of the kleene chain ⊥, f(⊥), f(f(⊥))...

John Baez (May 08 2020 at 18:38):

Nice. I know that kind of idea from my studies of large countable ordinals. (Not research, just learning.)

sarahzrf (May 08 2020 at 18:39):

this is the depleted version of the theorem about initial algebras of finitary functors :)

John Baez (May 08 2020 at 18:39):

I don't really know the undepleted version, though I should.

John Baez (May 08 2020 at 18:39):

So I'm just sorta puzzled that "time" in this story is directed. That makes sense if you can only do one reduction rule at each step in a computation, so there's no branching.

sarahzrf (May 08 2020 at 18:40):

well...

sarahzrf (May 08 2020 at 18:40):

there may be generalizations of this story to other kinds of completeness!

Daniel Geisler (May 08 2020 at 18:40):

@John Baez said

So I bet you (or Scott or someone) is going to create a make-believe universe where everything has a fixed point.

This is exactly my plan! Is there a problem?

sarahzrf (May 08 2020 at 18:40):

and, i mean, it doesn't mean that exactly, just that they have to come back together later—i.e., church-rosser or something

sarahzrf (May 08 2020 at 18:41):

but yeah, i see what you mean, that might be unfortunate for non-deterministic stuff

sarahzrf (May 08 2020 at 18:41):

but the basic idea is like

John Baez (May 08 2020 at 18:41):

Okay, I can believe a lot of people would be content to study situations with confluence.

sarahzrf (May 08 2020 at 18:41):

if the ordering is supposed to be "enrichment of information content"—

sarahzrf (May 08 2020 at 18:42):

then if you have two incomparable things—

sarahzrf (May 08 2020 at 18:42):

what does it mean to take their join?

John Baez (May 08 2020 at 18:42):

Is that a rhetorical question?

Dan Doel (May 08 2020 at 18:42):

Some denotational semantics is done with lattices, too.

sarahzrf (May 08 2020 at 18:42):

yeah, but if you have an answer, you could give it :)

John Baez (May 08 2020 at 18:43):

I might know x = 2 and you might know y = 3 ; these are incomprable, but someone smarter than both of us might know both x = 2 and y = 3.

sarahzrf (May 08 2020 at 18:43):

i don't think it's a question without an answer, necessarily, but i do think it's a question that requires a delicate answer

sarahzrf (May 08 2020 at 18:43):

oops!

sarahzrf (May 08 2020 at 18:43):

i misspoke

sarahzrf (May 08 2020 at 18:43):

you're right, there's no issue with joins of incomparable things per se

John Baez (May 08 2020 at 18:44):

Whew!

sarahzrf (May 08 2020 at 18:44):

i just had a very specific example in mind of things that were incomparable

sarahzrf (May 08 2020 at 18:44):

which should have a problem

sarahzrf (May 08 2020 at 18:44):

namely: things which disagree

sarahzrf (May 08 2020 at 18:45):

if we want to interpret the type nat as a poset of things ordered by info content, and we have a semantics for the numeral 3 and for the numeral 5, then what on earth should their join be?

John Baez (May 08 2020 at 18:46):

That's a toughie.

John Baez (May 08 2020 at 18:46):

8? :stuck_out_tongue:

sarahzrf (May 08 2020 at 18:46):

:thinking:

sarahzrf (May 08 2020 at 18:46):

dcpos for this kind of purpose don't necessarily fail to have all joins which aren't directed, just that there are plenty of non-directed joins they shouldn't be expected to have

John Baez (May 08 2020 at 18:46):

Right, I see.

sarahzrf (May 08 2020 at 18:47):

directedness happens to be a good condition for talking about "coherence of approximations"

John Baez (May 08 2020 at 18:49):

I see. It's interesting that "incomparability" includes "facts that could never be reconciled" and also just "different partial views that could be reconciled".

sarahzrf (May 08 2020 at 18:50):

i seem to recall @Gershom's talk mentioning something about "lattices with conflict" or some such

sarahzrf (May 08 2020 at 18:50):

i imagine that might be extra structure to distinguish those

John Baez (May 08 2020 at 18:50):

In restricting to sups of directed sets you're throwing out the latter ("different partial views that could be reconciled"), seemingly, but I guess somehow they sneak back in.

sarahzrf (May 08 2020 at 18:50):

given that the context was concurrency, where nondeterminism is a big deal, that sounds useful

Dan Doel (May 08 2020 at 18:53):

Maybe something to think about is that DCPO is a relaxation of what someone might come up with first with is ωCPO, where you have sups of ω-chains.

sarahzrf (May 08 2020 at 18:54):

isn't it a strengthening, not a relaxation?

Dan Doel (May 08 2020 at 18:54):

Well, it's a relaxation of what you're required to give to get a sup.

sarahzrf (May 08 2020 at 18:55):

contravariance of swapping between abelard and eloise strikes again!!

sarahzrf (May 08 2020 at 18:56):

but yeah—worth keeping in mind that directed sups w/ finite indexing sets are always just the greatest element of the things youre taking a sup over

Dan Doel (May 08 2020 at 18:56):

Anyhow, we want to be able to do a limit of infinitely many approximations, and directed sets are nicer to work with than ω or something.

sarahzrf (May 08 2020 at 18:56):

so dcpos are really about the infinitary stuff

sarahzrf (May 08 2020 at 18:56):

ha, jinx

Dan Doel (May 08 2020 at 18:57):

I think in general ω might not be 'big' enough.

John Baez (May 08 2020 at 18:57):

Some people have bigger computers than others.

John Baez (May 08 2020 at 18:58):

Mine always runs for $\varepsilon_0$ steps before it gives up.

sarahzrf (May 08 2020 at 18:58):

just work in the effective topos

sarahzrf (May 08 2020 at 18:59):

haha, forgetting the var, classic mistake

John Baez (May 08 2020 at 18:59):

Yeah - that'd be bad. Anyway, thanks - I think I learned something!

sarahzrf (May 08 2020 at 18:59):

no problem! always happy 2 spread PL knowledge :halo:

John Baez (May 08 2020 at 19:00):

I think people could do well teaching "minicourses" like this here... but I really do think it works best one-on-one: if two or more questioners start pulling in different directions I think it's much much harder.

sarahzrf (May 08 2020 at 19:00):

yup :|

John Baez (May 08 2020 at 19:01):

So, if I see some dialogue going on here like this I will do my best to stay out of it except for some "yay!" emoticons.

sarahzrf (May 08 2020 at 19:01):

and THAT'S why i don't like giving talks nearly as much as i like chats

sarahzrf (May 08 2020 at 19:01):

not that i've, like, given more than about 2 talks ever, but

John Baez (May 08 2020 at 19:02):

I like giving talks because then I'm just talking to an idealized person who knows X and Y but not Z and W: I make up a plausible mental model and stick to it.

John Baez (May 08 2020 at 19:02):

And the advantage of this idealized person is that they don't interrupt much.

sarahzrf (May 08 2020 at 19:02):

hmm, i always work best in contexts w/ feedback

John Baez (May 08 2020 at 19:02):

But to really convey information well, it kinda has to be one-on-one.

sarahzrf (May 08 2020 at 19:03):

it's why i can focus better on programming than on reading about math, say

sarahzrf (May 08 2020 at 19:03):

probably an adhd thing

John Baez (May 08 2020 at 19:03):

I enjoy having the feedback be just me in my own head relentlessly criticizing all the slips where I assume knowledge of Z and W when I'd decided I wouldn't.

John Baez (May 08 2020 at 19:04):

That's enough to keep me quite busy in a talk even without annoying real people telling me what they don't understand. :upside_down:

sarahzrf (May 08 2020 at 19:04):

oh sure, but there's no substitute for someone who just actually doesn't know Z and W to catch those :upside_down:

John Baez (May 08 2020 at 19:05):

The trouble is that those people also forgot what they knew about X and Y. :upside_down:

sarahzrf (May 08 2020 at 19:05):

hmm.

sarahzrf (May 08 2020 at 19:05):

oh, i was gonna say another thing about directed stuff

sarahzrf (May 08 2020 at 19:05):

it has some relationships with compactness

sarahzrf (May 08 2020 at 19:05):

that's probably mediated by filters i guess

sarahzrf (May 08 2020 at 19:08):

e.g., maybe u know the characterization of compactness that every directed sup of opens producing the whole space must already include the whole space as one of the opens

sarahzrf (May 08 2020 at 19:09):

i posted a thread once on twitter where i twisted this a little further to characterize compactness as a commutation of modalities ^.^

John Baez (May 08 2020 at 19:12):

Hmm.

I'm not sure I knew that characterization of compactness, but I can use the axiom of choice to well-order any open cover $U_\alpha$ and then let

$V_\alpha = \bigcup_{\beta \le \alpha} U_\beta$

to replace it with an increasing sequence of open sets, so yes - it's true.

John Baez (May 08 2020 at 19:12):

Or, at least it follows from AC.

sarahzrf (May 08 2020 at 19:14):

well, there's a nicer way—

sarahzrf (May 08 2020 at 19:14):

take the sub-poset of opens in the cover, close it under finite unions, and that's directed

sarahzrf (May 08 2020 at 19:15):

so i guess that's the kind of thing that leads people to want to use directedness instead of, say, ordinal indexing

sarahzrf (May 08 2020 at 19:15):

no choice required!

sarahzrf (May 08 2020 at 19:27):

(for the record, here's the thread i mentioned https://twitter.com/sarah_zrf/status/1229089866551562242)

i saw https://math.stackexchange.com/q/579197 on someone's twitter (i'd quote tweet but can't re-find it) & i like the characterization of compactness & i bet there's a morally similar characterization in terms of some kind of commutation of modalities

- n-sarahzrf where n ≤ (1, 1) (@sarah_zrf)

John Baez (May 08 2020 at 19:45):

Believe it or not, I'd been confused about what "directed" meant all along today. I don't know why - I know perfectly well what it means. But somehow today I was thinking it meant "linearly ordered".

John Baez (May 08 2020 at 19:46):

Now I see this stuff I said was bullshit:

In restricting to sups of directed sets you're throwing out the latter ("different partial views that could be reconciled"), seemingly, but I guess somehow they sneak back in.

John Baez (May 08 2020 at 19:46):

"Different partial views that could be reconciled" was intended as a touchy-feely way of saying "incomparable elements in a poset that have some element greater than or equal to both".

John Baez (May 08 2020 at 19:47):

But in a directed set all pairs of elements have some element greater than equal to both.

Dan Doel (May 08 2020 at 19:47):

Oh okay, that makes more sense of what you were saying.

sarahzrf (May 08 2020 at 19:51):

no it wasnt bullshit

sarahzrf (May 08 2020 at 19:51):

remember, a dcpo isn't itself directed, it's directed-complete—the index set is what's directed

sarahzrf (May 08 2020 at 19:52):

oops

John Baez (May 08 2020 at 19:52):

Oh!

John Baez (May 08 2020 at 19:52):

So "directed" refers to "c", not "po".

sarahzrf (May 08 2020 at 19:52):

exactly

John Baez (May 08 2020 at 19:53):

Okay, but this makes even more sense. :upside_down:

Dan Doel (May 08 2020 at 19:53):

I don't know if this helps, but as I threw out earlier, the categorical language would be more like a DCPO is like a partial order with filtered colimits (I think).

sarahzrf (May 08 2020 at 19:53):

yeah

Dan Doel (May 08 2020 at 19:53):

Except the 'filtered' is de-categorified.

sarahzrf (May 08 2020 at 19:53):

honestly i don't think it has to be

Dan Doel (May 08 2020 at 19:54):

Yeah, maybe not.

John Baez (May 08 2020 at 19:54):

Well, a filtered category that's a poset is exactly the same thing as directed set.

sarahzrf (May 08 2020 at 19:54):

i think if you use a filtered category as an indexing diagram, then the diagram factors thru a directed set

sarahzrf (May 08 2020 at 19:54):

if the codomain is a proset

John Baez (May 08 2020 at 19:54):

Yes.

John Baez (May 08 2020 at 19:55):

Yes, and I meant "proset" above, not "poset": a filtered category that's a proset is exactly the same thing as directed set.

John Baez (May 08 2020 at 19:55):

(I think the good definition of directed set doesn't require it to be a poset, just a proset.)

John Baez (May 08 2020 at 19:59):

So now it all makes sense to me. In a dcpo we've got a bunch of "states of partial knowledge about the state of affairs", and if any two of them have the property that there's a state of partial knowledge that extends both, then there's a unique minimal state of partial knowledge extending all of them.

John Baez (May 08 2020 at 20:01):

Or in other words: in a DCPO where each element is actually one person's knowledge of the world, and we've got a bunch of people with the property that for all X and X' there's a person Y who knows everything X and X' do, then there's a (hypothetical) person who knows everything this bunch of people do.

John Baez (May 08 2020 at 20:02):

Nice!

sarahzrf (May 08 2020 at 20:02):

:)

sarahzrf (May 08 2020 at 20:03):

note the suspiciously similar phrasing to things that involve the word "compact"

sarahzrf (May 08 2020 at 20:03):

like ultraproducts/powers and the compactness theorem

John Baez (May 08 2020 at 20:03):

Right!

John Baez (May 08 2020 at 20:07):

A "compact" object is one s.t. homming out of it preserves filtered colimits.

sarahzrf (May 08 2020 at 20:08):

i was just tweeting about that :thinking:

John Baez (May 08 2020 at 20:08):

Didn't see it!

sarahzrf (May 08 2020 at 20:09):

the description on the nlab page gives an idea characterization that sounds a little like "if you map into a big union then your image lies fully in one of the things being unioned", but

sarahzrf (May 08 2020 at 20:09):

it occurred to me that that only works if the morphisms of the diagram are monic

sarahzrf (May 08 2020 at 20:09):

but like, if you take germs... that's also a filtered colimit, and the morphisms are far from monic usually

sarahzrf (May 08 2020 at 20:10):

and in that case, i worked out that preserving the filtered colimit is sort of like a tube lemma kind of thing o.o

John Baez (May 08 2020 at 20:10):

I had my moment of epiphany here:

https://twitter.com/johncarlosbaez/status/1136647587153338368

So, finite objects are often called "finitely presented" objects. Other people call them "compact" objects. Why? The poset of open sets of a topological space X is a category... and the space X itself is a finite object in this category iff X is compact! (cont)

- John Carlos Baez (@johncarlosbaez)

Dan Doel (May 08 2020 at 20:29):

Compact values of a domain form an important part when you get further into domain theory, too.

Dan Doel (May 08 2020 at 20:31):

E.G. you start considering domains where all values are generated as colimits of compact values (so, the compact values form a 'basis').

Dan Doel (May 08 2020 at 20:31):

However, per one of your earlier comments, my understanding is that the category of these sorts of domains is not Cartesian closed.

Dan Doel (May 08 2020 at 20:32):

(But DCPO is.)

sarahzrf (May 08 2020 at 20:45):

Dan Doel said:

E.G. you start considering domains where all values are generated as colimits of compact values (so, the compact values form a 'basis').

accessible category!

sarahzrf (May 08 2020 at 20:46):

@Jules Hedges hmmmmmmmm, interesting that you just retweeted this from yourself https://twitter.com/_julesh_/status/978928091157364738

Domain theory is (mostly) long dead but still sometimes a useful way of thinking. It would be really good to read a modern 'retrospective' treatment of it

- julesh (@_julesh_)

sarahzrf (May 08 2020 at 20:46):

do you have something to say 🤨

Jules Hedges (May 08 2020 at 20:47):

Yep, yay for converting people to domain theory

sarahzrf (May 08 2020 at 20:47):

have you heard about step-indexing & synthetic guarded domain theory?

Jules Hedges (May 08 2020 at 20:48):

Nope

sarahzrf (May 08 2020 at 20:48):

topos_of_trees.pdf

Jules Hedges (May 08 2020 at 20:49):

sarahzrf said:

do you have something to say 🤨

Also, I think the most important thing about DCPOs can be summarised like this: the cartesian monoidal structure on the category of DCPOs admits a trace operator

sarahzrf (May 08 2020 at 20:49):

:)

Jules Hedges (May 08 2020 at 20:50):

Ah, I do know a tiny bit about the topos of trees, just not the other words you used. Somewhere deep down my todo list is to try to apply it to repeated games

sarahzrf (May 08 2020 at 20:50):

sure, but that doesn't tell you much about what it is about dcpos that makes that true

sarahzrf (May 08 2020 at 20:51):

well, the idea about step-indexing is like

Jules Hedges (May 08 2020 at 20:52):

It's true. But I'd really like to see a book on domain theory that uses string diagrams (and I hope I don't have to write it myself, because it sounds like hard work)

sarahzrf (May 08 2020 at 20:53):

so you wanna make a recursive definition, but it's neither inductive nor coinductive, so you can't really make sense of it w/ a typical universal property

sarahzrf (May 08 2020 at 20:53):

er sorry to clarify i mean like it doesn't satisfy the kind of positivity constraint you need—like say you want to solve a fixed point of a functor C^op × C → C

Nathanael Arkor (May 08 2020 at 20:54):

I think domain theory is very much alive, cf. this POPL paper from last year, for instance.

sarahzrf (May 08 2020 at 20:54):

and okay okay i guess that's the kind of thing you often want ends/coends for, but,

sarahzrf (May 08 2020 at 20:54):

the step-indexing approach is like

sarahzrf (May 08 2020 at 20:55):

rather than trying to find a genuine fixed point—define a well-founded sequence of approximations to a fixed point, starting with something undefined and getting better and better

sarahzrf (May 08 2020 at 20:56):

so rather domain-theoretic in flavor

sarahzrf (May 08 2020 at 20:56):

and then you can interpret the recursive definition as defining each approximation in reference to the previous one[s]

sarahzrf (May 08 2020 at 20:58):

then you make your argument parameterized by the index into the sequence of approximations

sarahzrf (May 08 2020 at 20:58):

and show that it works for each of them

sarahzrf (May 08 2020 at 20:59):

and then you need to appeal to some kind of compactness property of your intended ultimate goal to say like

sarahzrf (May 08 2020 at 20:59):

for any given particular case, we only need to know that a finite approximation of the hypothetical fixed point is true

sarahzrf (May 08 2020 at 21:01):

as i understand it, the name "step-indexing" comes from using this for semantics of PLs, and then you do a thing where you're effectively decrementing the index whenever your program takes a step, so that you only have to prove things for runs up to a certain length, or something like that—so the sequence of approximations is indexed by how many steps you can take

sarahzrf (May 08 2020 at 21:02):

now, what's cool about the topos of trees is that it carries structure that lets you make most of what i just described synthetic

sarahzrf (May 08 2020 at 21:02):

when working internally

sarahzrf (May 08 2020 at 21:04):

anyway, i havent really gotten my hands dirty with step-indexing in practice, so beware that any or all of what i just said could be wrong :ghost:

Gershom (May 08 2020 at 22:29):

At some point I worked out the intuition, which I never fully checked, that a dcpo can often be thought of as simply "a distributive lattice plus an antichain" -- i.e. it is a distributive lattice with the top cut off. (there may be some finiteness around to make this description work). So this amounts to a set of "atoms" of knowledge, some depending on others, and generally you can freely join them, but at a certain point when two atoms become incompatible, you can no longer obtain their join, and consequently, the join of anything above them.

Reid Barton (May 08 2020 at 22:45):

By the way, it's true in general that {having/preserving} filtered colimits is equivalent to {having/preserving} directed colimits, not just in the situation of looking at colimits in preorders.

sarahzrf (May 08 2020 at 22:48):

oh, really?

Reid Barton (May 08 2020 at 22:49):

Let me find a reference

Nathanael Arkor (May 08 2020 at 22:52):

Direct limits and filtered colimits are strongly equivalent in all categories by Andréka–Németi has a proof.

Dan Doel (May 08 2020 at 22:53):

@Gershom Do you mean with an anti-chain subtracted from it?

John Baez (May 08 2020 at 22:53):

So just so everyone notices, Gershom suggested the following:

Conjecture: given a finite dcpo $X$, there is a distributive lattice $L$ and an embedding $X \subseteq L$ such that $X$ consists of all elements of $L$ that are less than all elements of some antichain $A \subseteq X$.

Gershom (May 08 2020 at 23:02):

yep, john stated my "general feeling" correctly.

Dan Doel (May 08 2020 at 23:02):

Okay.

Reid Barton (May 08 2020 at 23:04):

Nathanael Arkor said:

Direct limits and filtered colimits are strongly equivalent in all categories by Andréka–Németi has a proof.

Nice, maybe this is the original proof. Adamek-Rosicky has a proof, similar but probably shorter, though it is somewhat poorly formulated. They don't cite any reference nor is the paper you linked in the bibliography (though they cite some other papers by the same authors). https://stacks.math.columbia.edu/tag/0032 has what I think is a correct proof.

Gershom (May 08 2020 at 23:04):

Actually, I think we may want "strictly less than" rather less than or equal. I.e. the antichain gives the first level of conflicting information, not the last level of allowable information.

John Baez (May 08 2020 at 23:11):

Okay, I'll just fix that in my statement in case doesn't read down this far.

sarahzrf (May 08 2020 at 23:18):

hmm, statements involving "strictly less than" always feel wrong to me :\

Dan Doel (May 08 2020 at 23:29):

So what's the lattice look like for a flat dcpo, like the integers?

Dan Doel (May 08 2020 at 23:29):

It can't be 'just add top' because that's not distributive, right?

Dan Doel (May 08 2020 at 23:33):

Is it $P(ℤ)$ and the anti-chain is the two-element sets or something?

Dan Doel (May 08 2020 at 23:38):

I guess that works.

Jem (May 09 2020 at 12:31):

All finite posets are DCPOs, as if a finite subset is directed then it has a top element.
Doesn't that mean that this DCPO fails to arise from a lattice in that way, due to the pairs of incomparable elements not having meets? image.png

Jem (May 09 2020 at 13:59):

We do, however, have that every DCPO $D$ embeds cofinally into $\{f \in F \mid \exists a \in A. f \leq a\}$ for $F$ the opposite of a frame (hence a distributive lattice) and $A$ an antichain, assuming choice.
Let $F$ consist of the closed subsets of $D$ under the Scott topology (i.e. those downwards-closed subsets which are also directed-complete), and $A$ consist of the sets $\{a\}\downarrow$ for $a$ the maximal elements of $D$. Then the inclusion map $d \mapsto \{d\}\downarrow$ is injective (as long as we require that $D$ was a poset, and not merely preordered), monotone, and cofinal by construction.
(A map between postets is cofinal if every element of the codomain is bounded above by some element of the image. I don't know if that's widespread terminology.)

Jem (May 09 2020 at 14:43):

A map on functions can be given by taking image then downward closure, which makes it functorial, and in fact gives us that the family of embeddings is a natural transformation from Id.

sarahzrf (May 09 2020 at 14:57):

what about DCPOs with least element?

sarahzrf (May 09 2020 at 14:57):

in a finite poset w/ a least element, any two things are gonna have a meet, right?

Reid Barton (May 09 2020 at 14:57):

You can add a least element to the given example

Reid Barton (May 09 2020 at 14:58):

The top two guys have a common lower bound, but not a greatest one

sarahzrf (May 09 2020 at 14:58):

wait, duh lol

Jem (May 09 2020 at 14:58):

The other stuff stays the same if you replace "directed" with "directed or empty", too.

sarahzrf (May 09 2020 at 14:58):

obviously glb stands for least lower bound

sarahzrf (May 09 2020 at 15:00):

the closed subsets of $D$ under the Scott topology (i.e. those downwards-closed subsets which are also directed-complete)

hmm, the characterization i know of the scott topology is that the opens are the sets whose characteristic functions are scott-continuous—that's [classically] equivalent to this?

Reid Barton (May 09 2020 at 15:01):

What I think Gershom maybe noticed, and I don't know whether it is true but it seems plausible from a few examples, is that this sort of thing doesn't occur in the DCPOs you get from the denotations of types in Haskell for example.

Reid Barton (May 09 2020 at 15:02):

Another question one could ask is whether computable functions have to preserve meets that exist, or joins that exist.

Reid Barton (May 09 2020 at 15:03):

For some specific notion of "computable" at least.

sarahzrf (May 09 2020 at 15:03):

Reid Barton said:

What I think Gershom maybe noticed, and I don't know whether it is true but it seems plausible from a few examples, is that this sort of thing doesn't occur in the DCPOs you get from the denotations of types in Haskell for example.

i would imagine that's it :upside_down:

Reid Barton (May 09 2020 at 15:05):

For example "parallel OR" with both True || undefined = True and undefined || True = True is continuous, and it's computable in a model where you can interleave the computation of the two arguments, but you can't define it in (the pure fragment of) Haskell because in Haskell you have to commit to which argument you want to compute first. (For purposes of modelling in DCPOs, maybe assume the function is curried so it accepts a pair.) Maybe you can detect this difference as failing to preserve meets or joins.

Dan Doel (May 09 2020 at 15:10):

The parallel one doesn't preserve meets, I think.

sarahzrf (May 09 2020 at 15:11):

really? i thought the parallel one existed in dcpos and that was kind of a problem because it meant you didn't get full abstraction

Reid Barton (May 09 2020 at 15:11):

It does exist in DCPOs.

sarahzrf (May 09 2020 at 15:12):

er, wait, actually now i cant remember why that would break full abstraction, maybe i meant definability

Reid Barton (May 09 2020 at 15:12):

So the question is whether there's a smaller (and in particular, non-full) subcategory of DCPOs through which the semantics of Haskell programs also factors.

Reid Barton (May 09 2020 at 15:13):

I don't know what full abstraction is; is it trying to say the maps between semantic objects all arise from actual programs?

Dan Doel (May 09 2020 at 15:13):

I think they must preserve joins because e.g. {(true,⊥), (⊥,true), (true,true)} is directed, and they must be continuous.

sarahzrf (May 09 2020 at 15:14):

full abstraction means that observationally equivalent (i.e., operationally identically behaving) programs get mapped to equal denotations

sarahzrf (May 09 2020 at 15:15):

but like i said, i can't remember now why parallel or would break that, so maybe the property i was remembering was the thing you said

sarahzrf (May 09 2020 at 15:16):

that said, i do remember that the dcpo model of pcf fails to be fully abstract for some reason

Dan Doel (May 09 2020 at 15:16):

I guess that works in general? If you have a and b with a join in a DCPO, then {a,b,a∨b} is directed with sup a∨b, and so it must be preserved by continuous functions.

sarahzrf (May 09 2020 at 15:16):

because it was a major open problem for a long time to provide a fully abstract model without "cheating" by quotienting the syntax or something

sarahzrf (May 09 2020 at 15:17):

okay yeah see the last line here image.png

Reid Barton (May 09 2020 at 15:19):

Dan Doel said:

I guess that works in general? If you have a and b with a join in a DCPO, then {a,b,a∨b} is directed with sup a∨b, and so it must be preserved by continuous functions.

But all you learn is that {f(a), f(b), f(a∨b)} has sup f(a∨b), which you already knew because f is order preserving.

Dan Doel (May 09 2020 at 15:21):

Ah, right. So, it's an upper bound, but it might not be least.

sarahzrf (May 09 2020 at 15:26):

well, it'll be least, it just might not be least for f(a) and f(b) alone

Reid Barton (May 09 2020 at 15:29):

So if parallel or is needed for full abstraction, I guess it must be because it lets you operationally distinguish two terms you otherwise couldn't?

Nathanael Arkor (May 09 2020 at 15:34):

You can write a program that checks whether a function is the parallel-or operator, and then gate behaviour on whether the parallel-or operator has been passed in. Something like t_1 := if is_por { true } else { false} and t_2 := if is_por { false } else { false}. You can't distinguish between t_1 and t_2 operationally, because there's no syntax for parallel-or, but you can denotationally.

Nathanael Arkor (May 09 2020 at 15:39):

So really, distinguish denotationally rather than operationally.

Reid Barton (May 09 2020 at 15:41):

Now I'm confused. I thought that there was some fixed mapping from program syntax to denotations. If the denotational semantics fails to be fully abstract for PCF, it means there are two different programs with the same operational behavior but different denotations. If I extend the language by adding parallel or, I don't change the denotations of these programs. Right?

sarahzrf (May 09 2020 at 15:42):

right, but now they no longer have "the same operational behavior"

sarahzrf (May 09 2020 at 15:42):

to be a little more precise, observational equivalence is about distinguishability by the rest of the language

Reid Barton (May 09 2020 at 15:42):

Yes, because now there's some context (presumably involving parallel or) which distinguishes them

Reid Barton (May 09 2020 at 15:43):

OK, I see that t_1 and t_2 would be an example if I knew how to implement is_por.

Reid Barton (May 09 2020 at 15:45):

More specifically, is_por needs to send parallel or to True and anything definable without parallel or to False or undefined

Nathanael Arkor (May 09 2020 at 15:46):

image.png

Nathanael Arkor (May 09 2020 at 15:47):

$T_i$ acts similarly to t_i here, with is_por inlined.

Reid Barton (May 09 2020 at 15:47):

OK, right. For some reason I thought it would have to be more complicated.

Reid Barton (May 09 2020 at 15:50):

So informally, we could say that PCF has the ability to specify a function it cannot define

Nathanael Arkor (May 09 2020 at 15:51):

Yes, and that in the semantics it can be.

Reid Barton (May 09 2020 at 15:53):

But another way to fix this could be to adjust the denotational semantics to make the denotations of these programs equal, say by restricting the morphisms to ones which preserve meets.

Reid Barton (May 09 2020 at 15:53):

It seems obvious enough that it should have been tried already.

Reid Barton (May 09 2020 at 15:53):

So, probably there is a reason that it doesn't work...

Reid Barton (May 09 2020 at 15:53):

For example maybe it's not actually true that functions definable in PCF preserve meets.

Gershom (May 09 2020 at 16:42):

Let me answer @Jem with how it works in the case given, which is not a counterexample. You have a distributive lattice and an antichain, and what you want is every element not greater than or equal to the antichain (which is a bit different than what john wrote above) to be your DCPO.

image.png

Gershom (May 09 2020 at 16:45):

That's the bruns-lakser embedding of the non-lattice X (which maybe should be called the "confused poset") into a distributive lattice (omitting bottom). again, just the downsets of the join-irreducibles (which in this case is true of all elements). Now we can recover X by taking everything not >= the element "ab". So X is the distributive envelope of X minus the "conflicted" information when both a and b occur. We can read it as "you can get to c from a, and you can get to c from b, but you can't have a and b at once." and similarly for "d".

Gershom (May 09 2020 at 16:47):

With the converse statement, we can instead of course take everything that is >= ca or db -- i.e. instead of picking out the minimal conflicted elements we pick out the maximal consistent elements.

Jem (May 09 2020 at 16:57):

Even if you define distributive lattice to only require binary meets/joins, don't you still need to explicitly exclude the bottom element of the lattice, as well as elements which are at least the antichain? The pictured poset doesn't have a meet for ca and db.

Reid Barton (May 09 2020 at 16:57):

I don't understand how this is an embedding; what happened to the edge $a \le d$?

sarahzrf (May 09 2020 at 17:00):

yeah, i think your diagram is a bit mangled

Gershom (May 09 2020 at 17:00):

Damnit, let me redraw the diagram.

Gershom (May 09 2020 at 17:12):

yep its a real counterexample, and what i sketched is wrong. here's the right embedding (which coincides with dedekind macneillie in this case) and you can't "cut out" the bits you need with just an antichain.
IMG_3761.jpg

Gershom (May 09 2020 at 17:13):

Indeed the argument is simple enough -- since every finite poset is a dcpo then obviously not every finite poset is given by a distributive completion and an antichain. I wonder if I was thinking of something else I read, or just totally off base.

Gershom (May 09 2020 at 17:14):

In this case the interesting bit is "you can't have a and b together, unless they are "resolved" by either c or d. so things that are not compatible can be made compatible in multiple ways.

Gershom (May 09 2020 at 17:29):

Hrmm.. does what I sketched work for algebraic domains -- aka those where every element is the supremum of compact elements below it?

Dan Doel (May 09 2020 at 17:31):

Isn't this example an algebraic domain?

Dan Doel (May 09 2020 at 17:32):

I was trying to figure out if something like that ruled out this example, but it seems like it doesn't.

Jem (May 09 2020 at 17:34):

Isn't every finite poset an algebraic domain, because any directed subset has a top element, hence the join of a directed subset is in the directed subset?

Dan Doel (May 09 2020 at 17:37):

I think so. Every element of a finite poset is compact, so the whole poset is a compact basis for itself. Or something like that.

Gershom (May 09 2020 at 17:40):

ok now i'm more confused than ever. if the definition of "algebraic domain" is "every element is the supremum of compact elements below it", then in the original diagram, the compact elements below "c" are "a" and "b" and they don't have a supremum in X, right? or am i misunderstanding the definition?

Dan Doel (May 09 2020 at 17:41):

It's the elements 'way below' it. But compact elements are 'way below' themselves.

Dan Doel (May 09 2020 at 17:45):

The fact that it's written << doesn't help, though.

sarahzrf (May 09 2020 at 17:53):

whoaa i think the compactness theorem of FOL says that the proset of theories ordered by reverse semantic consequence—i.e., T ≤ T' iff T' ⊨ T—has a compact top element

sarahzrf (May 09 2020 at 17:55):

er, i mean, you have to do a little bit of work to establish the equivalence, but i think they're roughly equivalent statements

zigzag (May 10 2020 at 14:04):

Oh that's cute! Which version of FO compactness do you have in mind ? "If $T \vdash \bot$, then there is a finitely generated $T'$ s.t. $T' \vdash \bot$" ? (it seems a bit sad to me to restrict to deriving $\bot$)

sarahzrf (May 10 2020 at 14:14):

well, given that i phrased using ⊨, we'd have T ⊨ ⊥ instead, which is equivalent to not having a model

sarahzrf (May 10 2020 at 14:15):

without need for completeness

sarahzrf (May 10 2020 at 14:16):

er, to be clear, i'm understanding T ⊨ T' here to mean Mod(T) ⊆ Mod(T')

sarahzrf (May 10 2020 at 14:16):

so completeness is T ⊨ φ <-> T ⊢ φ

zigzag (May 10 2020 at 14:32):

Yes sorry, I am used to converting to the variant in terms of $\vdash$, and why that's called compactness is maybe less immediate from a formal pov :) For (classical/intuitionistic) FOL, I like to do away with models (so that I don't have to think about what notion my interlocutor is thinking of (Tarskian, Kripke, ...)) when I can and think of the statement proven directly "by induction over a proof-tree".

sarahzrf (May 10 2020 at 14:32):

yeah, me too ;)

Gershom (May 10 2020 at 20:22):

By the way, what I think I may have been thinking of is not DCPOs but the much more specialized gadgets of prime algebraic domains (since those come up in the event structure stuff i was looking at) https://www.cl.cam.ac.uk/~gw104/REPN-updated.pdf -- but again, given my track record here, who knows.

Hendrik Boom (Jun 02 2020 at 04:42):

sarahzrf said:

it's why i can focus better on programming than on reading about math, say

Yes, I think it's an ADD thing (I don't have the H). The computer keeps interacting with you, telling you interesting ways in which your code isn't right yet. It's a two-way conversation, not a monologue. Like a very abstract video game, one that interacts without pictures or natural language.

sarahzrf (Jun 02 2020 at 15:01):

i like to joke that coq is the world's greatest puzzle game

sarahzrf (Jun 02 2020 at 15:02):

i don't know that i specifically "have the H" either—i want to say that at some point they stopped bothering to keep track of the difference? i'm not sure though.

sarahzrf (Jun 02 2020 at 15:02):

(i guess it also depends on who "they" is)

Rich Hilliard (Jun 02 2020 at 16:59):

It's no joke. I like to learn languages by reading other folks' code. Every time I find a Coq file or library to study, I invariably run into a construct I've never seen before. So I look in the reference manual, the imported libraries, maybe I find it and in trying to understanding that construct, encounter 3-4 more I've never seen before. And so on. It's a massive, distributed puzzle..

sarahzrf (Jun 07 2020 at 16:29):

so i think explaining stuff in this topic is where it really clicked for me that like... operational semantics of PLs are basically describing how programs give rise to processes, and then a ton of the time, difficulties in finding denotational semantics stem basically from trying to cram process-nature into the math world

sarahzrf (Jun 07 2020 at 16:30):

and every time i explain something related, it just gets more and more cemented in my head

sarahzrf (Jun 07 2020 at 16:30):

i really like this pov

sarahzrf (Jun 07 2020 at 16:31):

i think it explains very well why brouwerian math applies so often

sarahzrf (Jun 07 2020 at 16:32):

and but so

sarahzrf (Jun 07 2020 at 16:33):

i stumbled on that one ncat cafe post again where @John Baez was bemoaning the apparent destruction of "computation" itself in quotienting together conversion classes of terms to form a CCC out of the simply-typed lambda calc

sarahzrf (Jun 07 2020 at 16:37):

& how reduction ought to be higher cells, etc, which ties in with some work these days on higher dimensional rewriting i think??

sarahzrf (Jun 07 2020 at 16:42):

so now i have some vague stuff buzzing around in my head like...

• if a bunch of constructions in pl theory are trying to cope with lack of process-nature in mathematical objects
• but higher categories bake in process-nature; then
• i wonder if there are many constructions in pl theory that are basically "colimits in Set"-style lower-category reflections of lax stuff that's more natural?

sarahzrf (Jun 07 2020 at 16:45):

i wonder if @Jonathan Sterling has any input on this

Jon Sterling (Jun 07 2020 at 19:36):

Be careful what you wish for! :)

The idea of reductions as higher cells instead of equations can play an important role in the study of computation; this approach, for instance, can be used in combination with homological tools to compute invariants of rewriting presentations of algebraic theories --- for instance, placing bounds on the number of axioms needed to present a given theory.

It is currently unclear whether, or to what degree, the higher dimensional perspective will benefit programming languages. I am optimistic, but I think that "every reduction is a higher cell" is going to be definitely too naive --- because some reductions are more "important" than others. Many reductions in programming languages are not interesting and are mere technical details, whereas some reductions are extremely important --- even so important that the "models" we use to study programming languages rarely validate these reductions. These reductions are called, in the field, "fold-unfold" reductions and have to do with recursive types and fixed points. A reasonable hypothesis is that _all other_ reductions should be treated as exact equations, but these fold-unfold reductions should be thought of in a different (perhaps higher dimensional) way --- but it is still super unclear how all this will shake out.

Some people like to say that even alpha renaming of variables is a "reduction" that should be a higher cell... My opinion is that this perspective is irrational, because the existence of alpha renaming is a consequence of a given formal encoding of a language and doesn't reflect any decisive aspects of the language. Therefore, I think the most important thing will be to study the input of higher dimensional ideas on programming languages in a way that is very conscious of the open problems in the discipline, and in a way that can be explained to experts in the discipline (who usually know very little, if any, mathematics). This seems to be necessary in order to tell apart the "cool but useless" and the "cool but decisive" ways to apply higher dimensional ideas to programming languages.

sarahzrf (Jun 07 2020 at 21:51):

hmm, that's interesting, but i'm not sure how much it bears on the particular POV i meant to ask about :thinking:

sarahzrf (Jun 07 2020 at 21:56):

or, well, let me rephrase: why would you say that "A reasonable hypothesis is that _all other_ reductions should be treated as exact equations"?

Dan Doel (Jun 07 2020 at 22:48):

Here's an argument: this is essentially the precedent set by intensional type theory. α, β and some η rules are exact and just happen automatically, because they are decidable, and that is convenient. The higher dimensional structure ('propositional equality') is there for things like undecidable reductions that you must prove by induction. When you move into homotopy/cubical stuff, the higher stuff gives computational evidence of other 'equations' that are hard/impossible to decide.

And if you want to change the precedent, what is gained by making people manually specify that 'x = y' by some β reduction, say? You might want higher-dimensional (directed) structure in your language because it's nice for modelling operational semantics of a language you're describing within it. But what is the benefit of making people write down the steps in the operational semantics of the meta language to prove an equation between terms, when the computer could figure it out?

sarahzrf (Jun 07 2020 at 22:51):

i don't think i suggested any such thing :mischievous:

sarahzrf (Jun 07 2020 at 22:53):

for one thing, i'm not talking about when you work internally to a system—i'm talking about when you give denotational semantics to an object language

Dan Doel (Jun 07 2020 at 22:53):

Okay, so there was no reason for bringing up the CCC thing?

sarahzrf (Jun 07 2020 at 22:53):

er, sorry, i meant i don't think i suggested any such thing as "making people write down" etc

Dan Doel (Jun 07 2020 at 23:05):

Anyhow, I was trying to answer what I thought the thing you quoted meant.

Dan Doel (Jun 07 2020 at 23:06):

Perhaps that confirms that it wasn't what you were talking about, unless Jon meant something else.

Dan Doel (Jun 07 2020 at 23:13):

For cases where you want to explicitly reason about operation, higher dimentional stuff also seems useful (and John Baez has a cool paper on it). I'm not sure I'd call it "denotational semantics" just because it's math, though.

sarahzrf (Jun 07 2020 at 23:15):

but it's denotation :thinking:

Dan Doel (Jun 07 2020 at 23:18):

https://arxiv.org/abs/1905.05636 There's the Baez paper, if you haven't seen it.

Dan Doel (Jun 07 2020 at 23:41):

So I guess an alternate question is: if you describe the stuff in an operational semantics as forming a higher dimensional category, why does it become 'denotational semantics'?

Jon Sterling (Jun 07 2020 at 23:55):

sarahzrf said:

or, well, let me rephrase: why would you say that "A reasonable hypothesis is that _all other_ reductions should be treated as exact equations"?

The reason I think this is a reasonable hypothesis is that we have found no interesting theorems about programming languages that hinge on the other equations holding only weakly, whereas much of modern PL hinges precisely on the fold-unfold equation being weak. It may of course turn out that it is best for everything to be weak, but at a time when we are so ignorant of the _conceptual_ aspects of PL, I find it safest to base my hypothesis on the data I currently have.

Jon Sterling (Jun 07 2020 at 23:57):

I should weaken or qualify my last remark --- there is plenty of interesting stuff to be said about a situation where everything is weak, and I think it's super cool. I just want to say that the last decade or two of PL research seems to point to this one class of non-equation being very important, and probably fundamental to whatever it is PL is studying.

Jon Sterling (Jun 08 2020 at 00:06):

Regarding "operational semantics" vs "denotational semantics", I feel this distinction is very old-fashioned (but unfortunately still current). It comes from a time when classical denotational semantics (like domain theory) had started to be recognized as suffering from severe limitations and obscurity, and a generation of PL researchers abandoned it and adopted what they started to call "operational semantics". With operational semantics, many amazing theorems about programming languages became possible to prove, but what was lost was the ethos of compositionality --- an entire generation of researchers basically abandoned the very notion of compositionality, with good intentions, but of course, suffering a loss of perspective as a result (IMO).

What is denotational semantics? It is just semantics period, and the word "denotational" is (in my opinion) quite redundant. The need to distinguish from operational semantics comes from the fact that most operational semantics is really operational non-semantics (to rip off the joke of Kontsevich). When operational semantics is made compositional (as in game semantics, as well as these cool higher dimensional things), then it is "denotational" in some sense, but I would just say that it has been turned into semantics, period.

Now, coming back to "non-semantics", it is not for nothing that practitioners have been doing "non-semantics" for so many years --- specifically, the old dogma that these fold-unfold situations (and other similar things) should be strict equations has made the semantics of such theories very awkward, and I think now that we are recognizing that these equations should be re-thought, we can also re-think the operational aspects of programming languages from an objective/semantical point of view.

(=_=) (Jun 08 2020 at 03:11):

sarahzrf said:

i stumbled on that one ncat cafe post again where John Baez was bemoaning the apparent destruction of "computation" itself in quotienting together conversion classes of terms to form a CCC out of the simply-typed lambda calc

This was the same concern I had with the Backprop as Functor paper, that they were quotienting out stuff just to get a SMC of "learners". As Jonathan Sterling pointed out with his history of semantics:

it is not for nothing that practitioners have been doing "non-semantics" for so many years --- specifically, the old dogma that these fold-unfold situations (and other similar things) should be strict equations has made the semantics of such theories very awkward [...]

I just hope that we've now learned enough not to head down the same path with ML.

(=_=) (Jun 08 2020 at 03:12):

Dan Doel said:

https://arxiv.org/abs/1905.05636 There's the Baez paper, if you haven't seen it.

The Baez-Williams paper. This looks like it could be part of Christian's thesis.

(=_=) (Jun 08 2020 at 03:13):

Jonathan Sterling said:

The need to distinguish from operational semantics comes from the fact that most operational semantics is really operational non-semantics (to rip off the joke of Kontsevich).

I'm curious: what was the original joke of Kontsevich?

John Baez (Jun 08 2020 at 05:21):

Rongmin Lu said:

Dan Doel said:

https://arxiv.org/abs/1905.05636 There's the Baez paper, if you haven't seen it.

The Baez-Williams paper. This looks like Christian's work.

We actually both worked on it!

(=_=) (Jun 08 2020 at 05:45):

John Baez said:

Rongmin Lu said:

Dan Doel said:

https://arxiv.org/abs/1905.05636 There's the Baez paper, if you haven't seen it.

The Baez-Williams paper. This looks like Christian's work.

We actually both worked on it!

Clearly! I just wanted to point out it's not "the Baez paper", but something that looked like it could be part of Christian's thesis. I should've kept the original wording, the edit made it worse! Sorry, John! :sweat_smile:

John Baez (Jun 08 2020 at 06:21):

I was just joking around. It's not a "Baez paper", nor is it "Christian's work" - we both put a lot of ourselves into it, and we were fleshing out and polishing some ideas of Mike Stay and Greg Meredith.

John Baez (Jun 08 2020 at 06:22):

Christian has been working a lot with them.

(=_=) (Jun 08 2020 at 06:45):

John Baez said:

It's not a "Baez paper", nor is it "Christian's work" - we both put a lot of ourselves into it, and we were fleshing out and polishing some ideas of Mike Stay and Greg Meredith.

Well, that's complicated... :thinking: :sweat_smile:
But complicated is awesome. Good to know how those ideas have been shepherded.

Jon Sterling (Jun 08 2020 at 12:38):

Rongmin Lu said:

Jonathan Sterling said:

The need to distinguish from operational semantics comes from the fact that most operational semantics is really operational non-semantics (to rip off the joke of Kontsevich).

I'm curious: what was the original joke of Kontsevich?

I am hearing it third-hand but the joke was that "non-commutative geometry" is really "non-commutative non-geometry" --- because important aspects of geometrical language do not extend to noncommutative rings. But I don't know enough to say whether the joke was funny in its original context ;-)

(=_=) (Jun 08 2020 at 12:47):

Jonathan Sterling said:

Rongmin Lu said:

I'm curious: what was the original joke of Kontsevich?

I am hearing it third-hand but the joke was that "non-commutative geometry" is really "non-commutative non-geometry" --- because important aspects of geometrical language do not extend to noncommutative rings. But I don't know enough to say whether the joke was funny in its original context ;-)

Lieven le Bruyn wrote in 2006 that Kontsevich had apparently mentioned "non-geometry" in a talk in Antwerp "a couple of years ago". I think I've also heard references to "point-less geometry" as well, but probably not from the same source.