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: category theory

Topic: fully faithful doctrine extensions

Mike Shulman (May 06 2020 at 20:44):

Suppose $D_1$ and $D_2$ are "doctrines" in the informal sense of "structures that can be put on a category", like "having finite products", "having finite limits", "being closed symmetric monoidal", etc. Suppose furthermore that $D_1 \subseteq D_2$ in the sense that every $D_2$-category is a $D_1$-category, and that the resulting forgetful functor has a left adjoint assigning to every $D_1$-category the free $D_2$-category that it generates. Consider the property that the unit of this adjunction -- that is, the functor from an arbitrary $D_1$-category to the free $D_2$-category it generates -- is always fully faithful. What would you call this property, as a relation between $D_1$ and $D_2$?

Mike Shulman (May 06 2020 at 20:44):

In some literature this property is called something like "full completeness of $D_2$ over $D_1$" (I might have the prepositions wrong there). But this is not very evocative to me, aside from being somewhat grammatically awkward (my understanding is that the original term was that a particular model of $D_1$ was "fully complete" meaning that the map into it from the initial $D_1$-category is fully faithful), and it might not be too widespread yet to have any hope of being changed (at least among category theorists). Is there a better term?

Mike Shulman (May 06 2020 at 20:46):

I think it's a sort of "higher-dimensional conservativity" (in the logical sense of "conservative theory extension", which is unfortunately different from the category-theoretic meaning of "conservative functor"). Could we say something like "$D_2$ is a 2-conservative extension of $D_1$"?

Nathanael Arkor (May 06 2020 at 20:52):

Isn't full completeness a relation between syntax and semantics, rather than two syntaxes? (Taking doctrines here to be [higher] syntactic entities.)
Edit: I see you're suggesting this was the initial meaning, but not the current one. I haven't seen the meaning you suggest, though.

Nathanael Arkor (May 06 2020 at 20:52):

"2-conservative extension" seems sensible to me, though I would be tempted to drop the "2-".

Mike Shulman (May 06 2020 at 21:42):

Just "conservative" would work if it were clear from the names of $D_1$ and $D_2$ that their models are 1-categories rather than posets, n-categories, etc. But, for instance, "LEX" could refer to left exact n-categories for any n, while something like "IMLL" is sometimes used to refer to its 1-categorical models (CSMCs) and other times to its posetal models.

Mike Shulman (May 07 2020 at 01:02):

As for the use of "full completeness" for this, the only reference I can find at the moment is Hasegawa's Categorical Glueing and Logical Predicates for Models of Linear Logic (section 5). I thought I had seen it elsewhere too, but maybe I'm wrong.

Nathanael Arkor (May 07 2020 at 01:08):

Certainly Hasegawa suggests they were the one to adapt the term:

In their original use, full completeness means that any arrow of the semantic category is the denotation of a syntactic element; we adapt this for the case that the semantic category itself is syntactically defined as the term model of a type theory.)

Nathanael Arkor (May 07 2020 at 01:11):

Oh, I see: their full completeness is stronger than conservativity.

Mike Shulman (May 07 2020 at 01:58):

Yes, in that paper he seems to be using "conservativity" to mean that the functor in question is just faithful. That's not exactly what I would mean intuitively by "conservative" though.

Dan Doel (May 07 2020 at 02:45):

Does it really mean 'every arrow'? Even arrows between objects not in the image of the functor?

Mike Shulman (May 07 2020 at 13:31):

No, that's just a mistaken phrasing. The first part of the paragraph says

A much harder property to show is that the translation is full, i.e. if an expression of the target theory has types which are definable in the source theory, it is already definable in the source theory. Equivalently it amounts to the fullness of $\mathbb{I}$ . We say that a translation between type theories is fully complete if it is both conservative and full.

Amar Hadzihasanovic (May 07 2020 at 13:40):

I've seen “full completeness” indicate that there is an equivalence of categories, and not just a fully faithful functor. So that makes it even more confusing.

Amar Hadzihasanovic (May 07 2020 at 13:41):

(With the explicit explanation that “one does not want more contexts/probes in the semantics than in the syntax”, ie more objects to be the source of morphisms...)

Mike Shulman (May 07 2020 at 13:50):

Amar Hadzihasanovic said:

I've seen “full completeness” indicate that there is an equivalence of categories, and not just a fully faithful functor. So that makes it even more confusing.

Where?

Amar Hadzihasanovic (May 07 2020 at 14:04):

Umm, I think my recollection was based on this answer on stackexchange, and specifically the paragraph

So, if the semantic model or the target language has too many "contexts" then it will be able to poke our terms or semantic meanings in undesirable ways and spoil their equivalence. "Undesirable ways" means in ways that the programming language itself cannot poke them. So, to get full abstraction, we need to ensure that the "contexts" available in the semantic model or the target language do come from those in the source language in some form.

I interpreted this as requiring essential surjectiveness as well.

But the answer is a bit vague, and the one below by Martin Berger does identify full completeness with full faithfulness of a functor, so maybe either I misunderstood or the author was mistaken.

Amar Hadzihasanovic (May 07 2020 at 14:15):

In fact re-reading it, I'm pretty sure that they are using “contexts” in the sense of “terms with a hole” and not in the sense of “the context of term (e.g. in a typing judgement)”, so I must have misunderstood.

Mike Shulman (May 07 2020 at 14:42):

What a mess of terminology!

Dan Doel (May 07 2020 at 14:47):

Those are 'evaluation contexts'.

Amar Hadzihasanovic (May 07 2020 at 14:58):

I think the only issue with “conservative” may be that in logic it's mostly used in a language-specific way, so a theory extension may be conservative for certain formulas and not for others. With this in mind, I can see how in different circumstances one would think of conservative as meaning “the functor between free models is faithful”, for example if one only wants the truth of equality statements about terms of a type theory to be reflected, or “full and faithful”, if for example one wants also the provability relation to be reflected.

Amar Hadzihasanovic (May 07 2020 at 15:03):

I wonder if some made-up terminology on the lines of “exterior” or “outer” could work for the fully faithful case, suggesting that anything in $D_2$ that is not in $D_1$ must relate to some 'additional objects' outside the domain of $D_1$...

Mike Shulman (May 07 2020 at 15:32):

Amar Hadzihasanovic said:

I think the only issue with “conservative” may be that in logic it's mostly used in a language-specific way, so a theory extension may be conservative for certain formulas and not for others.

I don't know what you mean by "language-specific", or rather I don't know what it would mean for anything in logic to be not language-specific, since any theory is always formulated in some language. And I've never heard a usage of "conservative" that applies to some formulas but not others. For instance, I don't see any hint of it on wikipedia: conservative extension, where conservativity is just a property of a pair of theories. Can you give some references?

Mike Shulman (May 07 2020 at 15:32):

Amar Hadzihasanovic said:

With this in mind, I can see how in different circumstances one would think of conservative as meaning “the functor between free models is faithful”, for example if one only wants the truth of equality statements about terms of a type theory to be reflected, or “full and faithful”, if for example one wants also the provability relation to be reflected.

This is why I was suggesting to add the prefix "2-". More generally, we could say that a morphism of $n$-theories is $k$-conservative if the functor in question is full on $j$-morphisms for all $j\ge n-k+1$. Then a morphism of 2-theories (i.e. doctrines) would be 1-conservative if it is full on 2-morphisms, i.e. equalities, i.e. it is faithful, and it would be 2-conservative if it is also full on 1-morphisms. A 3-conservative morphism of 2-theories would be an equivalence. For ordinary 1-theories, 1-conservativity would mean fullness on 1-morphisms, i.e. equalities, which I think is the same as being conservative in the usual sense (as long as we are restricted to algebraic theories in which the only "propositions" are equalities -- we could generalize it to other theories by representing them with, say, FOLDS-signatures and asking for fullness on all sorts of appropriately bounded rank).

Mike Shulman (May 07 2020 at 15:34):

It would still be ambiguous if people use for instance "IMLL" to refer to both the 1-theory of closed symmetric monoidal posets and the 2-theory of closed symmetric monoidal categories. But that usage is arguably intrinsically confusing anyway...

Mike Shulman (May 07 2020 at 15:48):

I guess we could say "the inclusion from IMLL to MLL is a conservative morphism of 1-theories" or "...is a 2-conservative morphism of 2-theories".

Amar Hadzihasanovic (May 07 2020 at 15:49):

Mike Shulman said:

I don't know what you mean by "language-specific", or rather I don't know what it would mean for anything in logic to be not language-specific, since any theory is always formulated in some language. And I've never heard a usage of "conservative" that applies to some formulas but not others. For instance, I don't see any hint of it on wikipedia: conservative extension, where conservativity is just a property of a pair of theories. Can you give some references?

It's in the third paragraph of the wikipedia article, starting with “More generally, if $\Gamma$ is a set of formulas...”. The only way I've seen it used is with $\Gamma$ being all formulas in a restricted language. I've found a few hits googling “conservative with respect to formulas” or “conservative over formulas”, for example this paper by Visser.
A bit closer to home, in this paper with Benno van den Berg we considered some extension of a theory which was conservative only with respect to disjunction-free formulas.

Cody Roux (May 07 2020 at 15:49):

Mike Shulman said:

Amar Hadzihasanovic said:

I think the only issue with “conservative” may be that in logic it's mostly used in a language-specific way, so a theory extension may be conservative for certain formulas and not for others.

I don't know what you mean by "language-specific", or rather I don't know what it would mean for anything in logic to be not language-specific, since any theory is always formulated in some language. And I've never heard a usage of "conservative" that applies to some formulas but not others. For instance, I don't see any hint of it on wikipedia: conservative extension, where conservativity is just a property of a pair of theories. Can you give some references?

It's pretty common to say things like "Conservative over $\Pi^0_2$ formulas" or some such, which just means that $T_1\models \phi$ iff $T_2\models \phi$ for formulas in that class.

Mike Shulman (May 07 2020 at 15:53):

Thanks! I don't know how I missed that. But it certainly doesn't seem to be "mostly" used that way, since it only appears once in the article.

Mike Shulman (May 07 2020 at 15:54):

And anyway, I don't see how it could cause confusion, since if you don't specify a class of formulas, what could it mean except to consider all formulas?

Amar Hadzihasanovic (May 07 2020 at 16:05):

I meant “it is mostly accepted that 'conservative' can be relativised”, not that it is most frequently relativised :)

After your explanation of what you would mean by n-conservativity, I agree that it would not cause any confusion, after one specifies what 2-theories (or n-theories) are.

Mike Shulman (May 07 2020 at 16:37):

I'm still open to other suggestions for terminology...

Nathanael Arkor (May 07 2020 at 16:46):

Mike Shulman said:

As for the use of "full completeness" for this, the only reference I can find at the moment is Hasegawa's Categorical Glueing and Logical Predicates for Models of Linear Logic (section 5). I thought I had seen it elsewhere too, but maybe I'm wrong.

I found another reference: Fiore–Saville's Relative full completeness for bicategorical cartesian closed structure. After a conversation with @Philip Saville, I think I understand the nuances in the terminology better, so I'll summarise here in case this wasn't clear to others.

"Conservative extension" and "full completeness" technically mean the same thing, but they're used in different contexts, and come from different fields. Both are represented by full functors from initial models, but the intention is different. In a (model theoretic) conservative extension, we have two theories $T_1 \subset T_2$ and we take the canonical embedding $\mathrm{Syn}(T_1) \to \mathrm{Syn}(T_2)$. In (programming language semantic) full completeness, we have a single theory $T$ and we take the canonical embedding $\mathrm{Syn}(T) \to \mathcal C$, for models $\mathcal C$ of $T$. ("Relative full completeness" is used similarly to "full completness", but for free models rather than initial ones.)

There seems to be a slight ambiguity as to whether "conservative extension" in a categorical setting should mean "full" or "fully faithful", as the term originally comes from logic, where the distinction isn't apparent. I think using "proof-relevant" for faithful could be a reasonable compromise. For full completeness, you typically don't care about faithfulness.

Lastly, in model theory, an extension is an embedding into a supertheory. That's probably a distinction that's not important to carry over to categorical semantics, though maybe it could be reasonable to define an extension to be injective-on-objects (an isocofibration?).

Philip Saville (May 07 2020 at 16:53):

(just to add to what Nathanael said) Marcelo and I took the terminology from the Abramsky-Jagadeesan paper (https://doi.org/10.2307/2275407), which I believe is where it was first used. In that context you're looking to solve the full abstraction problem, and having a model in which every morphism between the interpretations of types is definable gets you a long way towards that. Girard uses "denotational completeness" to mean the same thing, I think.

Nathanael Arkor (May 07 2020 at 17:16):

Maybe worth noting as well that conservativity corresponds to completeness in the context of logic, so it stands to reason that conservativity should correspond to full completeness in the context of theories, which suggests fullness rather than full faithfulness.

Dan Doel (May 07 2020 at 17:16):

I think 'faithful' is not part of full completeness in PL semantics because that is called 'adequacy'. A denotational semantics is adequate if the denotation map is injective with respect to operational equivalence.

Nathanael Arkor (May 07 2020 at 17:28):

I wasn't quite ready to let go: I've found places where different authors use "conservative" to mean different things. Crole uses it to mean "full" (cf. On Fixpoint Objects and Gluing Constructions), while Curien uses it to mean "fully faithful" (cf. https://www.irif.fr/~curien/CIRM-2014.pdf). It'd definitely help to establish terminology to distinguish between these, then.

Mike Shulman (May 07 2020 at 18:01):

This is going to require more digestion, but from a categorical perspective, fullness without faithfulness is almost never a correct or interesting notion.

Mike Shulman (May 07 2020 at 18:04):

Are there examples of models that are actually full and not faithful?

Mike Shulman (May 07 2020 at 18:08):

If I were inventing names without regard to existing terminology, I would probably say that a particular model $C$ of a theory $T$ is "faithful", "full", "fully faithful", etc. when the functor $\mathrm{Syn}(T)\to C$ has those properties, and similarly that a map of theories $T_1 \to T_2$ is "faithful", "full", "fully faithful", etc. when the unit maps $C \to F C$ from a $T_1$-model to the free $T_2$-model it generates always has those properties.

Dan Doel (May 07 2020 at 18:30):

So, System F has a "trivial model" where it is interpreted as a second-order theory of the booleans. That isn't full, but perhaps it could be weakened to have a full model of constructive 'truth values' that is not faithful (since all terms of a type denote the same thing).

Wikipedia's writeup on terms in PL semantics indicates that full completeness is 'something else' you'd care about after the main properties like adequacy and full abstraction, though. So you might already be only considering faithful models before you worry about fullness.

vikraman (May 07 2020 at 18:37):

One example which comes to mind is STLC with weak sums vs strong sums, the translation of weak to strong is not bijective on equations. However, these things were studied many decades ago and don't use modern language, I think strong sums are the norm now and what you'd expect categorically.

Mike Shulman (May 07 2020 at 19:25):

@Dan Doel Which wikipedia article are you looking at?

Dan Doel (May 07 2020 at 19:26):

https://en.wikipedia.org/wiki/Denotational_semantics#Abstraction

Dan Doel (May 07 2020 at 19:29):

I don't know exactly how accurate that is to wider usage. I've never actually heard of "full completeness" in PL semantics before noticing it on that page.

Dan Doel (May 07 2020 at 19:33):

I guess that might suggest the premise that 'adequacy' and 'full abstraction' are taken as prerequisites, though, because I have heard of those elsewhere. (Full abstraction is kind of a given in your scenario, I think, because you'd already quotient by the 'operational' semantics.)

sarahzrf (May 07 2020 at 19:33):

ive seen "full abstraction" before definitely

Mike Shulman (May 07 2020 at 22:24):

Okay, so it looks like for particular models of one fixed doctrine, "fully abstract" means "is a model at all", "adequacy" means "the map from the initial model is faithful", and "(adequate and) fully complete" means "the map from the initial model is full(y faithful)".

Mike Shulman (May 07 2020 at 22:25):

But it seems confusing to re-use the same words when talking about something entirely different, namely the relationship between two different doctrines.

Mike Shulman (May 07 2020 at 22:27):

The intuitive meaning of the property I'm interested in is certainly consonant with "conservative" for logical theories, namely that you are free to use the constructs of the stronger theory when reasoning about the weaker one while remaining assured that anything you deduce could have been done entirely in the weaker theory.

Dan Doel (May 07 2020 at 22:28):

Yeah, I think "conservative" is the best name. It's just unfortunate that it's already taken for something else.

Mike Shulman (May 07 2020 at 22:28):

What specifically do you refer to?

Dan Doel (May 07 2020 at 22:29):

You said "conservative functor" already means something. Creates isomorphisms or something?

Mike Shulman (May 07 2020 at 22:30):

Ah, yes. Well, I'm not too worried about that, since here we're applying the adjective to a different kind of thing, so there isn't a huge potential for confusion.

Dan Doel (May 07 2020 at 22:31):

Oh okay.

Morgan Rogers (he/him) (May 08 2020 at 09:35):

Also any full and faithful functor is conservative in that sense anyway, so it would only be a one-way source of confusion :upside_down:

Lê Thành Dũng (Tito) Nguyễn (May 09 2020 at 12:50):

Mike Shulman said:

Okay, so it looks like for particular models of one fixed doctrine, "fully abstract" means "is a model at all",

Hm, I'm not sure that "full abstraction" makes sense in general categorical settings – I'd say that to speak of full abstraction you need observational equivalence, therefore you need to distinguish a type of observations, e.g. natural numbers in PCF – but in "concrete" PL theory it's far from a trivial property of models. A model merely has to send convertible terms to equal denotations, and two observationally equivalent terms are not convertible most of the time.
Actually the quest for a fully abstract model of PCF produced a lot of interesting theory as a side effect: stable domain theory, game semantics, arguably linear logic…

Lê Thành Dũng (Tito) Nguyễn (May 09 2020 at 12:58):

As for "full completeness" I believe it's used more in the context of logical calculi than for programming languages. For instance there are full completeness results for system F, linear logic, … in which the idea of quotienting by observational equivalence is perhaps not so interesting.
Fullness without faithfulness can be interesting: for instance if we had a fully complete, effective and finite (therefore necessarily non-faithful) model of the simply typed lambda-calculus, it would be easy to show that higher-order matching is decidable (whereas the only known proof, by Stirling, is very difficult technically and uses game semantics).

For PCF the constructions of fully abstract models actually rely on an approximate full completeness result, namely the definability of compact elements: see "Definability and full abstraction" by Curien. So there is definitely a relationship between the two notions, though it's not as simple as "one is a prerequisite for the other": in general fully complete models are not fully abstract and vice versa.

Mike Shulman (May 09 2020 at 13:37):

Nguyễn Lê Thành Dũng said:

Fullness without faithfulness can be interesting: for instance if we had a fully complete, effective and finite (therefore necessarily non-faithful) model of the simply typed lambda-calculus

But the operative word there is "if". The reason I don't think fullness without faithfulness is interesting is because it hardly ever happens. Do you have an example where it actually happens, as opposed to one where it would be nice if it did happen?

Lê Thành Dũng (Tito) Nguyễn (May 09 2020 at 15:15):

Melliès's fully complete model of propositional linear logic is not faithful, IIRC.

Mike Shulman (May 09 2020 at 17:00):

Reference?

Lê Thành Dũng (Tito) Nguyễn (May 09 2020 at 17:19):

The model I'm thinking of is described in a LICS 2005 paper:
https://www.irif.fr/~mellies/papers/Mellies05lics.pdf
I don't think the lack of injectivity is stated there, but it is mentioned at the end of Chapter 3 of Melliès's habilitation thesis (page 81):
https://www.irif.fr/~mellies//hdr-mellies.pdf

Lê Thành Dũng (Tito) Nguyễn (May 09 2020 at 17:30):

For another example (which I'm not familiar with at all, so I'm just repeating what the document says):
http://boole.stanford.edu/~dominic/papers/thesis/hughesthesis.pdf
The hypergame model of the polymorphic lambda-calculus apparently corresponds to quotienting the syntax by replacing all the types contained inside terms by their prenex normal forms. So it's almost faithful, but not entirely.

Philip Saville (May 11 2020 at 09:20):

one (perhaps somewhat contrived) place where fullness but not faithfulness can turn up is around definability. There you start with a semantic interpretation of a type theory and want to build a category making that interpretation full. Faithfulness is kind of a side issue: you only care that the interpretation you build doesn't identify too much more than the one you started with.

For the stlc you start with an interpretation $s[-]$ in a ccc $\mathcal{C}$ (which may not be faithful) and then use logical relations / glueing to build a ccc $\mathcal{K}$ and a strict ccc-preserving functor $\mathcal{K} \to \mathcal{C}$. Then the interpretation $\theta \mapsto (s[\theta], \mathrm{Def}_\theta)$ sending a base type $\theta$ to the pair consisting of its interpretation in $\mathcal{C}$ and the Kripke relation given by definability is full (because maps must preserve the relation) but, because the interpretation coincides with $s[-]$, it isn't faithful if $s[-]$ isn't. Good references for this with a categorical standpoint are the first part of Fiore's Semantic analysis of normalisation by evaluation or Alimohamed's A characterization of lambda definability in categorical models of implicit polymorphism.

As has already been pointed out, this kind of technique is interesting from a programming language perspective because it gets you closer to full abstraction. Beyond PCF I don't think it's been studied much but there is some very preliminary work along these lines due to Ohad Kammar and Shin-ya Katsumata (link), where they recast the fully-abstract O'Hearn-Riecke model for PCF more categorically. (Full disclaimer: I'm currently working with Ohad to flesh this out properly.)

Mike Shulman (May 12 2020 at 15:40):

Thanks both!

I think in my talk this week I'll use "(2-)conservative" but let it be known that I'm still open to better suggestions. It definitely seems less confusing if we restrict words like "full completeness" to the case of individual models rather than also lifting them to morphisms of theories; the terminology in the former case is already enough of a mess all by itself. (-: