I reread some earlier comments on this subthread about (i) vs (ii). I think you’re right, and I misunderstood what Dan wants. It now seems to me like he might count natural families $\Pi X\,:\,Ob(C),\,(Hom(y X,Tm))_\bot$ as (i). And as far as I understand, this is essentially what you get from an element of $Tm_\bot$ constructed in the semantic logical framework without funny tricks.

]]>The partiality of (i) in $C$ is also external, so it doesn’t need a universe.

]]>Re #99: Thanks.

Re #100:

I’m not arguing for (i) over (ii), but I don’t see how (ii) in $[C^op,Set]$ is a way of talking about (i) in $C$. I don’t know what (i) in $C$ even means, since $C$ may not have a universe. There seems to be a serious misunderstanding about what (i) and (ii) are.

]]>What I’m saying is that whatever intuition you have that argues for (i) over (ii) (which I don’t think I share, but whatever) should be applied not to the presheaf category, but to $C$ itself, and that when this (i)-version in $C$ is translated into the presheaf category it looks like (ii) instead. So there’s no need to object to (ii) in the presheaf category, because it’s really just a way of talking about (i) in $C$, which is what we really care about.

]]>Re #95: The raw syntax is not defined internally.

]]>Re my own #96, I guess I should add what (i) *would* be, for the partial interpretation of types:

$[[T]]\,:\,((V \to Tm) \to Ty)_\bot$

But it doesn’t seem possible. $V$ itself is actually an argument before the partiality, but it’s not informative enough to determine whether the interpretation should be defined. The environment—the argument of type $(V \to Tm)$—*is* informative enough. It seems to be more informative than we need, since we only want to interpret well-typed types. *If* there were a semantic context argument, which the environment would be required to be an element of, then that would be pretty much the just-right amount of information.

Re #91:

I didn’t bring up semantic contexts, you did, I think, in #87, with the $SemCtx$ metatype. Is the confusion that #87 was taking place in $Set$, not $[C^op,Set]$? But that doesn’t seem to explain it, since then you were missing the argument for the semantic environment. I figured you were confusing contexts and environments.

That the partial interpretations of types and terms don’t involve semantic contexts was something I had said myself, in #89.

]]>Re #90:

Trying to translate Peter’s suggestion to our style, for the interpretation of raw types, you have:

$[[T]]\,:\,(V \to Tm_\bot) \to Ty_\bot$

Ours is:

$[[T]]\,:\,(V \to Tm) \to Ty_\bot$

But in both cases the “return value” is not a total function. So they’re (ii) style.

with (i), a piece of syntax is (classically) either interpretable in all semantic environments of the correct variable set, or none.

Not according to what Dan wrote in #86. “[…]”

I don’t see how that thing Dan wrote contradicts what I had written. But I realized that what I had written was misleading, because we *know* the semantic logical framework isn’t classical. But I still thought (i) and (ii) are generally different in the framework.

In light of #94, I see how confusing it was to talk about semantic contexts without clarification. I *was not* referring to the objects of $C$ that everything in the semantic logical framework (the internal language of the presheaf category) is implicitly parameterized by. Everything I was talking about was supposed to be taking place in the semantic logical framework, and not using any funny tricks to inspect the implicit object of $C$. There are not semantic contexts *explicitly* used by the partial interpretations of types and terms. And I didn’t think the partial interpretation was going to use tricks to inspect the implicit semantic context either. So far, it seems like everything before global totality can be done internally, without unusual axioms.

I’m going to back up and give some of my assumptions before making specific replies.

- The raw syntax is defined internally, without unusual axioms, so, for example, $RawTy$ and $RawTm$ are constant presheaves.
- The typing rules are also defined internally. Lots of constant presheaves.
- $Ty$ and $Tm$ are probably not constant presheaves, so when working with those, for all I know, there’s the possibility of funny tricks. But I was not proposing to use funny tricks, and I didn’t think we were planning to, anywhere.
- So the notion of partiality we’re using can be defined in extensional type theory with a universe, using the universe to imitate powersets: $A_\bot \coloneqq \{a_?\,:\,A \to Prop\,|\,\forall (a_1 \in a_?) (a_2 \in a_?),\,a_1 = a_2\}$.
- The essence of Dan’s distinction between (i) and (ii) is the difference between $(A \to B)_\bot$ and $(A \to B_\bot)$, respectively.
- $(A \rightharpoonup B) \coloneqq (A \to B_\bot)$
- So the difference between (i) and (ii) was not supposed to have anything to do with working internally/externally to the presheaf category.

Again, those are all things I assumed. Correct them as necessary. If all those assumptions are correct (you don’t actually need all of them), then Peter’s approach was (ii) style, and so is what we’re currently doing.

]]>Re #92: Oh, I see the confusion. This is what happens in the passage from a CwF $C$ to its presheaf category $[C^{op},Set]$. We start with style (i) relative to the category $C$ itself, so each term has a chance to get interpreted as a (total) morphism in $C$ (indeed, we don’t assume any structure on $C$ that would make the notion of “partial morphism” make sense therein). But “maybe having a morphism in $C$” is enough to define a *partial* morphism in the presheaf topos $[C^{op},Set]$. In the simplest case, a maybe-morphism $X\to Y$ induces a partial morphism $y X \to y Y$ between their Yoneda embeddings, whose domain is “all maps $U\to X$ such that the maybe-morphism exists” — in classical logic this is either all of $y X$ or empty.

Our situation is a bit more complicated because of the quantification over all possible interpretations of the domain and codomain. In terms of $C$ itself (refer to Peter’s original post), we say that for every term $T$, every object $X\in C$ (“semantic context”), every “environment over $X$” assigning to each variable of $T$ a semantic type over $X$ and a semantic term in that type (i.e. a display map $A\to X$ and a section of it), and every semantic type $Y$ over $X$ (since we are talking about checking judgments, we take the codomain as given), there *might* be given a section of $Y$ that is the interpretation of $T$ relative to all of these data.

I just reformulated this in terms of the presheaf category $[C^{op},Set]$ as follows. In natural-model style a CwF structure on $C$ is determined by a representable morphism of presheaves $Tm\to Ty$, where an element of the set $Ty(X)$ is a semantic type over $X$, and an element of $Tm(X)$ in the fiber over such a semantic type is a semantic term belonging to that type. Thus, if $V$ is the set of variables of $T$, then an “environment over $X$” as above is just an element of $Tm^V(X)$, and the semantic type $Y$ is just an element of $Ty(X)$. Thus, the description in the previous paragraph can be re-stated as “for every term $T$, every object $X\in C$, every element of $Tm^V(X)$, and every element $Y$ of $Ty(X)$, there might be given an element of $Tm(X)$ in the fiber over $Y$”. Now since $Tm(X)$ and $Ty(X)$ are just sets, this can be rewritten as “for every term $T$ and every object $X\in C$, a *partial function* $Tm^V(X) \times Ty(X) \rightharpoonup Tm(X)$ that (insofar as it is defined) lifts the projection $Tm^V(X) \times Ty(X) \to Ty(X)$”. Finally, since these partial functions are (insofar as they are defined) natural in $X$ (this is Peter’s point (8)), we can repackage them again into a “partial natural transformation” $Tm^V \times Tm\rightharpoonup Tm$., i.e. a partial morphism in $[C^{op},Set]$.

Does that help?

I think this is similar to the idea in #93: a presheaf on $C$ is sort of a “more categorically well-structured” version of a “set of objects of $C$”. I also agree with the sentiment in #93 that when packaged this way, the partial interpretation function should be a “fairly straightforward” inductive definition (although when you come down to it, the whole initiality theorem is *about* “packaging” things in just the right way so that we can apply induction).

One way that I like to think of it is that if we express the *raw* syntax in HOAS, so for instance we have $\Pi : ty \to (tm\to ty) \to ty$ and $\lambda : ty \to (tm\to ty) \to (tm \to tm) \to tm$ and so on, then it is just a collection of base types and axioms for simply typed $\lambda$-calculus, and the partial interpretation function is just an application of the *initiality theorem for simply typed $\lambda$-calculus* mapping from the syntactic CCC into the category whose objects are presheaves on $C$ and whose morphisms are *partial* morphisms of presheaves. There are some technicalities in making this precise, notably that the latter category is not actually a CCC but rather some kind of “closed relevance monoidal category”, and it also requires some translation to get to the usual CwF/natural model formulation of semantics using the fact that dependent products in a topos can be expressed as subobjects of partial function objects (given $C\to B\to A$, the dependent product $\Pi_B(C)$ embeds into $A\times Par(B,C)$, since each “element” of $\Pi_B(C)$ consists of an “element” $a\in A$ together with a partial section of $C\to B$ on the “fiber” of $B$ over $a$, and such a partial section is in particular a partial morphism $B\rightharpoonup C$). But I find it at least conceptulally helpful.

I’m still trying to wrap my head around how exactly the recursive partial interpretation works, so I’m wondering if the following would be a good way to formulate (or at least conceptualise) an interpretation strategy, inspired by a discussion I had with András Kovács.

Let $C$ be target model where we want to land. Define a “raw context” in $C$ to be a set of objects, a “raw type” to be a set of elements of $Ty$ (possibly over different objects), and so on. The various (essentially algebraic) operations of $C$ can be extended to (actually algebraic) operations on the “raw” level. Define the various validity relations on raw things of $C$. For example, given a raw context $\mathbf \Gamma$, and a raw type $\mathbf A$, we say that $\mathbf \Gamma \vdash \mathbf A$ if $\mathbf \Gamma$ is a singleton $\{\Gamma\}$, $\mathbf A$ is a singleton $\{A\}$, and $A$ is an element of $Ty(\Gamma)$.

Now from all these structures you get a (total!) interpretation function from the syntactic raw things to the corresponding raw things in $C$. This should be easy to define. And then it should also be easy to check that valid things get mapped to valid things. Both steps should be direct applications of an initiality principle for inductive definitions (i.e. they should be straightforward inductions). After that, one can trivially extract the desired interpretation function by inspecting the validity predicate of the outputs.

Using subsets basically corresponds to using multivalued functions instead of partial functions. But probably one could replace subsets with subsingletons and it seems everything works the same way.

Is this a valid description of any of the strategies that have been proposed? Am I overlooking some important points?

]]>Re #90: wait, I do think I agree with Matt here. The type of $interp$ that I had in mind for interpreting in a category $C$ is

$interp : \Pi X,Y : Ob(C). Tm \to (Hom_C(X,Y))_\bot$So the inputs $X$ and $Y$ before the partiality are in the sense of polymorphism, not in the sense of assuming elements of $X$ and $Y$.

That’s what I would call (i)-style.

What I had in mind for (ii)-style was something like

$interp : \Pi X,Y : Ob(C). Term \to X \to Y_\bot$Re #87, what is $SemTm$ here? If in this situation it’s like $Hom_C(X,Y)$, then it does seem to me like the partiality is in a different place in $Tm^V \to Tm_\bot$ (which is how I’m understanding your current text on the partial interpretation page, which seems like (ii) style) than in $(Tm^V \to Tm)_\bot$ (which would be (i)-style).

I.e. (i) is $A \to (B \to C)_\bot$ and (ii) is $A \to (B \to C_\bot)$, and (i) implies (ii) but not vice versa.

]]>I don’t understand why you are bringing in semantic contexts. In my sketch of the partial interpretation functions, the interpretation of a term is a partial morphism $Tm^V\rightharpoonup Tm$, where $Tm^V$ is a “semantic environment”, and I assumed this is what Dan was talking about when he said “a total interpretation of raw terms as partial morphisms”. The semantic contexts are only introduced later on, and end up being the domains of definition of these partial morphisms.

]]>I think Streicher does (i), insofar as I can see a difference. I don’t think there was every any intent to “use Streicher’s method” – we already made a bunch of changes inspired mainly by Peter’s suggestions. I was assuming that Peter’s original suggestion also counted as (i); is that not the case?

with (i), a piece of syntax is (classically) either interpretable in all semantic environments of the correct variable set, or none.

Not according to what Dan wrote in #86. “A partial function whose inputs are two objects X and Y and a term T” is different from “a partial function whose input is a term T and whose output is a (total) function whose input is two objects X and Y”.

]]>Come to think of it, this point makes me think that my mode-switch rule is wrong, and you can't do the partial interpretation (i)-style without semantic contexts. ]]>

At some point though, I imagine, we can't say anymore that we're using Streicher's method. I don't actually have Streicher's book, so I can't tell how central (ii) is for him. ]]>

I would say that my formulation as (ii) is just a reorganization of (i). Your partial interpretation as a partial function whose inputs are a semantic context (input), a semantic type (the output), and a syntactic term is

$SemCtx \times SemTy \times SynTm \to SemTm_\bot$where $(-)_\bot$ is the “partial elements” monad. I’m just currying this as

$SynTm \to (SemCtx \to SemTy \to SemTm_\bot).$ ]]>Putting this here since it’s sort of a reply to #71, but there has been related discussion on the Type Theory discussion page.

OK, I think the thing I’m confused about regarding the semantics is the difference between (i) a partial interpretation function taking syntax to total morphisms in the semantics, and (ii) a total interpretation of raw terms as partial morphisms. In keeping with my general proclivities that everything should be as typed as possible as soon as possible :-) my instinct would be to use (i) instead of (ii). This also seems slightly more precise, because (thinking of partiality as an effect) $A \to Partial(B \to C)$ implies $A \to B \to Partial(C)$ but not vice versa. Also, it seems like (ii) relies on being in a setting where there are enough monos in the semantics to talk about the domains of partial morphisms, whereas (i) moves the partiality into the meta-language. What I understand so far is that here that’s OK there are enough monos because Tm is valued in sets, so we can do subsets there.

Anyway, I’m definitely willing to be convinced that (ii) is necessary and/or more convenient and/or you all prefer it, but I thought just for the sake of discussion I’d write out how I envision (i) going for a very simple language just to show the pieces.

Suppose we have three raw types

$A ::= w \mid w' \mid i$of which $w$ and $w'$ (well-formed) are well-formed:

$\frac{} {w type} \quad \frac{} {w' type}$and $i$ (ill-formed) isn’t.

Term typing is $A \vdash T : B$, with the presuppositions that $A type$ and $B type$ (I’m thinking of this as a checking judgement with “context” $A$)

$\frac{A = B} {A \vdash id : B} \quad \frac{B \type \quad A \vdash T : B \quad B \vdash T' : C} {A \vdash T;_{B}T' : C}$ $\frac{} {w \vdash k' : w'} \frac{} {w' \vdash k : w}$(then term equality has identity and unit laws).

So there are ill-typed raw composites, like $k;_{w} k$ or $k;_{w} k'$.

We want to show this is the initial category generated by 2 objects $o$ and $o'$ (interpreting $w$ and $w'$) and two morphisms $h$ and $h'$ (interpreting $k$ and $k'$).

The partial interpretation of types is

$\begin{array}{l} [[ w ]] = o \\ [[ w' ]] = o' \\ [[ i ]] undefined \\ \end{array}$The partial interpretation of terms is a partial function whose inputs are two objects $X$ (the interpretations of the context) and $Y$ (the interpretation of the output, since I’m thinking of this as a checking judgement) and a term $T$. This is defined by

$interp(X,Y,k) = h$ if $X = o$ and $Y = o'$

$interp(X,Y,k') = h'$ if $X = o'$ and $Y = o$

$interp(X,Y,id) = id$ if $X = Y$

$interp(X,Z,(T ;_B T')) = f;g$ if $[[B]] = Y$ and $interp(X,Y,T) = f$ and $interp(Y,Z) = g$

(Personally, I think of this as a relation $interp_is(X,Y,T,f)$ with a funny syntax, but hopefully it’s acceptable as a partial function definition?)

Totality is:

(a) If $A type$ and $[[A]] = X$ and $B type$ and $[[B]] = Y$ and $A \vdash T : B$ then there exists $f : X \to Y$ such that $interp(X,Y,T) = f$.

Mutually (for when we add dependent types) with (b) If $A type$ then there exists an $X$ such that $interp(A) = X$.

For example, in the case for the typing rule for $T ;_B T'$, we are given $A type$ and $C type$ (the presuppositions of $A \vdash T;_B T' : C$), and $[[A]]= X$ and $[[C]] = Z$ (the “semantic validity” / definedness of the interpretation of the inputs), and $B type$ and $A \vdash T : B$ and $B \vdash T' : C$ as premises. By the IH part (b) on the subderivation of $B type$, there is some $Y$ such that $[[B]] = Y$. So we have the data needed to use the IH part (a) to get $interp(X,Y,T) = f$ and $interp(Y,Z,T') = g$, which is all enough to know that the interpretation is defined.

]]>I’m not talking about the difference between truncated and non. In the current situation it’s fine to have it truncated, since our only induction on derivations is to prove a proposition (totality). But I’ve always understood “$\mathcal{J}$ is derivable” to mean “there exists (in the truncated sense) a derivation tree of $\mathcal{J}$”, just as I’ve always understood “$P$ is provable” to mean “there exists a proof of $P$”. Certainly if I wanted to convince someone that $\mathcal{J}$ is derivable, I would do it by writing down a derivation tree, right?

]]>Thanks Paolo, that helps. I can see how that avoids an explicit mention of induction-induction. However, it’s more distant from the intuitive meaning of rules and derivations, namely that the derivable judgments are the ones you can obtain by building derivation trees out of the primitive rules.

I see. I guess I implicitly assumed that by writing things like:

$wellformedtype: \ldots \to Prop$(as in #61) the intention was to force the definition to yield predicates / relations, in the sense of $Prop$-valued families. A priori, derivations don’t give you relations, and it’s a theorem that you need to prove on a case by case basis. The impredicative definition I sketched essentially gives you the $(-1)$-truncation of that (i.e. the mere existence of a derivation).

If you really want to define derivations explicitly, then the inductive-inductive definition should be $Set$-valued, which means you can’t really use the impredicative encoding.

It didn’t even occur to me that derivation trees were to be taken as the intuitive meaning of inference rules. I’ve always thought of them as a structure on top of the actual validity predicate (a way to make it proof relevant). I assume you can’t avoid introducing them for certain proof-theoretic arguments, but for the sake of the initiality construction, why is it important to keep this extra proof relevance around?

]]>Thanks Paolo, that helps. I can see how that avoids an explicit mention of induction-induction. However, it’s more distant from the intuitive meaning of rules and derivations, namely that the derivable judgments are the ones you can obtain by building derivation trees out of the primitive rules. So I feel like if using that style as the definition, one ought to make a comparison to actual derivation trees, in which case one is back choosing between (2) and (3).

In fact I think that (2) already has this problem: how do you explain to someone, in terms of derivation trees that they can write down on a sheet of paper (or even create as data structures or execution traces in a computer), what it means for a judgment to be valid in style (2)? Of course there has to be a derivation tree of that judgment. But because of the presupposition on context validity, in order for such a derivation tree to imply (2)-validity, we need to know that the contexts appearing in that tree are valid, which means (inductively) that there must exist certain *other derivation trees*, and so on. In other words, the only way to explain (2) is to reduce it to (3): the “real notion of validity” can only mean (3)-validity *paired with* context-validity.

This is related to the reason I am unsatisfied with intrinsic inductive-inductive syntax for type theory: at the end of the day, what we write on a page (or type into a computer) is untyped, and that gap has to be bridged at *some* point.

Re #77:

one defines the set of “well-formed” terms as the intersection of all those subsets that are closed under the rules. Then there is no problem in having say context validity conditions as inputs to type validity rules

I don’t completely understand this. It’s not just one “set of well-formed terms” we are defining, we want to define the set of valid contexts, the set of valid types-in-context, and the set of valid typed-terms-in-context. Can you say more explicitly how you are thinking of expressing this?

I was thinking you consider say triples $(C, Ty, Tm)$ where $C$ is a set of raw contexts, $Ty$ is a set of pairs of an element of $C$ and a raw type, $Tm$ is a set of pairs of an element of $Ty$ and a raw term. One can define what it means for such a triple to be *closed* under the rules of the syntax. Then you take the intersection, over all such closed triples, of the $C$ sets (resp. $Ty$, $Tm$). So literally the syntax is the smallest set of raw “things” that is closed under the rules.

Okay, I think I see. That makes some sense.

Maybe we can put that idea on the back burner as something to try after this project is complete, and then compare the two? It does seem like that would involve double the work in one place, first defining the interpretation relation and then proving it single-valued, while with a recursively defined partial function both of those happen at once. But maybe an equivalent amount of work would pop up somewhere else, e.g. in the comparison between the two versions of syntax.

]]>Re 76: having done lots of things in Twelf a while ago (where this is the only way to define functions :) not only partial ones), I’d guess it wouldn’t be that bad. Say you define a relation interp(M,S) between syntax and semantics. Then the uniqueness is “for all M, if interp(M,S) and interp(M,S’) then S = S’”. Assuming there is only one constructor for interp for each term-generator (lam, app, etc.) (which will be true if you translate the function clauses as interp constructors), in each case you’ll get by the IHes that the interpretations of the sub-expressions are equal, and then some congruence will imply that S = S’. Maybe I’m missing something, but that’s my best guess.

]]>