Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorAli Caglayan
   • CommentTimeNov 29th 2018
   • (edited Nov 29th 2018)
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexI have seen judgements like $\Gamma \vdash A \mathrm{Type}$ and $A \mathrm{Type}$. I always thought of judgements as your basic statements in a formal theory, and contexts where something that was added on later. Should every judgement be in context? For example well-formed contexts are usually written like $\Gamma \ctx$ however I guess one could also write it like $\Delta \vdash \Gamma \ctx$. This would make defining contexts a lot easier too as every judgement would be of the form $\Gamma \vdash \Dec$ where $\Dec$ is what I will call a decleration. It can be a typing decleration, assertion that a context is well formed, assertion that something is a type etc. That way contexts would simply be lists of declerations.

   I have seen judgements like $\Gamma \vdash A \mathrm{Type}$ and $A \mathrm{Type}$. I always thought of judgements as your basic statements in a formal theory, and contexts where something that was added on later. Should every judgement be in context?

   For example well-formed contexts are usually written like $\Gamma \ctx$ however I guess one could also write it like $\Delta \vdash \Gamma \ctx$. This would make defining contexts a lot easier too as every judgement would be of the form $\Gamma \vdash \Dec$ where $\Dec$ is what I will call a decleration. It can be a typing decleration, assertion that a context is well formed, assertion that something is a type etc. That way contexts would simply be lists of declerations.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeNov 29th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexJudgments are indeed basic statements in a formal theory, but such a statement can *include* something called a "context". Sometimes in formal theories where all judgments include a "context" of the same sort, people are sloppy and omit mentioning the context when talking about the judgment, but formally speaking it's part of the judgment. Contexts do *usually* behave a bit specially in terms of how we formulate rules for judgments with contexts, but at a formal level I believe what I said above is true. Bob Harper's book [[PFPL]] has a discussion of this in chapter 3; in particular, after discussing derivability and admissibility, he says > a hypothetical inductive definition is to be regarded as an ordinary inductive definition of a *formal derivability judgment* $\Gamma\vdash J$ consisting of a finite set of basic judgments $\Gamma$ and a basic judgment $J$. In other words, the judgment is all of $\Gamma\vdash J$, even if it's usually put together from smaller "pieces" that one might call "basic judgments" (perhaps related to what you referred to as a declaration).

   Judgments are indeed basic statements in a formal theory, but such a statement can include something called a “context”. Sometimes in formal theories where all judgments include a “context” of the same sort, people are sloppy and omit mentioning the context when talking about the judgment, but formally speaking it’s part of the judgment.

   Contexts do usually behave a bit specially in terms of how we formulate rules for judgments with contexts, but at a formal level I believe what I said above is true. Bob Harper’s book PFPL has a discussion of this in chapter 3; in particular, after discussing derivability and admissibility, he says

   a hypothetical inductive definition is to be regarded as an ordinary inductive definition of a formal derivability judgment $\Gamma\vdash J$ consisting of a finite set of basic judgments $\Gamma$ and a basic judgment $J$.

   In other words, the judgment is all of $\Gamma\vdash J$, even if it’s usually put together from smaller “pieces” that one might call “basic judgments” (perhaps related to what you referred to as a declaration).

3. • CommentRowNumber3.
   • CommentAuthoratmacen
   • CommentTimeNov 29th 2018
   • PermaLink
   Author: atmacen
   Format: MarkdownItexIn proof theory, it seems more common than elsewhere for the context entries to be "basic judgments" with the informal expectation that the main subjects of those basic judgments are fresh variables. This style comes from [[natural deduction]], rather than [[sequent calculi]]. It's not necessarily sloppiness, since you can say precisely how to "sequentize" it, or alternatively, directly formalize what these higher-order derivations are. On the categories [[computational trinitarianism|corner]], I think it corresponds to using the (covariant) Yoneda lemma. On the programming corner, it corresponds to focusing on closed programs, with the meaning of open programs determined by their closed instances. In dependent type theory, it's a bit odd to have any basic judgment as a context entry: would that mean you have equality entries? Type variable entries? With judgments-as-types in [[Twelf]], I think they let you use any basic judgments to form judgments, but then you can use a "world" to express the form of legitimate contexts.

   In proof theory, it seems more common than elsewhere for the context entries to be “basic judgments” with the informal expectation that the main subjects of those basic judgments are fresh variables. This style comes from natural deduction, rather than sequent calculi. It’s not necessarily sloppiness, since you can say precisely how to “sequentize” it, or alternatively, directly formalize what these higher-order derivations are.

   On the categories corner, I think it corresponds to using the (covariant) Yoneda lemma. On the programming corner, it corresponds to focusing on closed programs, with the meaning of open programs determined by their closed instances.

   In dependent type theory, it’s a bit odd to have any basic judgment as a context entry: would that mean you have equality entries? Type variable entries? With judgments-as-types in Twelf, I think they let you use any basic judgments to form judgments, but then you can use a “world” to express the form of legitimate contexts.

4. • CommentRowNumber4.
   • CommentAuthorAli Caglayan
   • CommentTimeNov 30th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexatmacen If by equality you mean definitional (judgemental) equality then yes, I think this would be a very sensible thing to have in context. Type variable entries would also be very sensible. It would mean that formation rules would need the context to have something being a type too. In fact if one has universes it would be the same thing.

   atmacen

   If by equality you mean definitional (judgemental) equality then yes, I think this would be a very sensible thing to have in context. Type variable entries would also be very sensible. It would mean that formation rules would need the context to have something being a type too. In fact if one has universes it would be the same thing.

5. • CommentRowNumber5.
   • CommentAuthoratmacen
   • CommentTimeNov 30th 2018
   • PermaLink
   Author: atmacen
   Format: TextType variables would not be quite the same as having a universe, since the universe itself would be a type. I’m not saying there’s any big semantic problem with allowing those extras in the context, but it’s a difference from usual Martin-Löf type theory, where context entries are all assuming elements of types.

   Type variables would not be quite the same as having a universe, since the universe itself would be a type. I’m not saying there’s any big semantic problem with allowing those extras in the context, but it’s a difference from usual Martin-Löf type theory, where context entries are all assuming elements of types.
6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeNov 30th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI believe that allowing judgmental equalities in the context opens a big can of worms syntactically, akin to that opened by equality reflection: if you can hypothesize in the context that $\mathbb{N} \equiv (\mathbb{N}\to\mathbb{N})$, then the term $App(3,2)$ becomes well-typed in that context, and among other things you have to start annotating your applications with the relevant $\Pi$-type since you can't trust any more that $\Pi$ is injective. Semantically, one can interpret Twelf-style judgments-as-types in a presheaf model, so I believe any sort of context can be at least sort of made sense of. However, it gets progressively farther away from the category one is actually interested in.

   I believe that allowing judgmental equalities in the context opens a big can of worms syntactically, akin to that opened by equality reflection: if you can hypothesize in the context that $\mathbb{N} \equiv (\mathbb{N}\to\mathbb{N})$, then the term $App(3,2)$ becomes well-typed in that context, and among other things you have to start annotating your applications with the relevant $\Pi$-type since you can’t trust any more that $\Pi$ is injective.

   Semantically, one can interpret Twelf-style judgments-as-types in a presheaf model, so I believe any sort of context can be at least sort of made sense of. However, it gets progressively farther away from the category one is actually interested in.

7. • CommentRowNumber7.
   • CommentAuthoratmacen
   • CommentTimeNov 30th 2018
   • PermaLink
   Author: atmacen
   Format: MarkdownItex> and among other things you have to start annotating your applications with the relevant $\Pi$-type since you can't trust any more that $\Pi$ is injective. Well we were doing that anyway, in preparation for equality reflection, as you know. But if you just want ITT, an alternative would be to embrace the absurdity of badly-behaved type equations. Judgmental equality doesn't need to correspond to the categorical model.

   and among other things you have to start annotating your applications with the relevant $\Pi$-type since you can’t trust any more that $\Pi$ is injective.

   Well we were doing that anyway, in preparation for equality reflection, as you know.

   But if you just want ITT, an alternative would be to embrace the absurdity of badly-behaved type equations. Judgmental equality doesn’t need to correspond to the categorical model.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeNov 30th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> Well we were doing that anyway, in preparation for equality reflection, as you know. In the initiality project, yes, but this is not an initiality project thread.

   Well we were doing that anyway, in preparation for equality reflection, as you know.

   In the initiality project, yes, but this is not an initiality project thread.

9. • CommentRowNumber9.
   • CommentAuthorAli Caglayan
   • CommentTimeNov 30th 2018
   • (edited Nov 30th 2018)
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexI have been reading Harper recently and I quite like his book. It's probably the best type theory book I have ever read so far to be honest. He is very precise and doesn't abstract things away unless he needs to. I haven't gotten to what he has to say about Judgements yet, but from what Mike has said I think it will clear up my confusion.

   I have been reading Harper recently and I quite like his book. It’s probably the best type theory book I have ever read so far to be honest. He is very precise and doesn’t abstract things away unless he needs to. I haven’t gotten to what he has to say about Judgements yet, but from what Mike has said I think it will clear up my confusion.