Canonical forms for initiality

Canonical forms for initiality

[Michael Shulman]

On Mon, Oct 16, 2017 at 8:00 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>> 1. Give bidirectional typing rules to ensure only beta-normal, eta-long
>>    terms are typeable.
>> 2. Hence, a conversion rule can be omitted, since all terms (including
>>    types) are in normal form.
>> 3. Prove a bunch of lemmas, eventually culminating in proofs of
>>    (a) hereditary substitution and (b) identity expansion. (This
>>    basically ends up making normalization part of the definition of
>>    substitution.)
>
> Yes, that's what I'm proposing.

Let me expand on that a little under a new subject line, since I've
played around with it some already and I think I have a fairly clear
picture of how it should go.

In a dependently typed bidirectional system, hereditary substitution
needs to be mutually defined along with the typing judgments.  In
principle it might be possible to do this inductive-recursively, but I
would want to instead define the graph of hereditary substitution
inductive-inductively and then afterwards prove it to be a total
function, since inductive-inductive types are easier to make sense of
homotopically and generally (in my experience) have a more useful
induction principle.  (To reply to Matt, I am not considering any kind
of impredicativity; the axiomatic version could be added later.)

However, when doing this intrinsically (which is the direct way to get
a useful induction principle) and without h-level restriction, I found
that there seems to be a new problem: you end up needing to substitute
hereditarily not just one term but a whole context morphism, and then
in defining the clauses for the graph of that hereditary substitution
you need to know already that it is associative.  So you add another
judgment for the graph of its associativity, but in defining its
clauses you need to know that the associativity is coherent, and so
on.  The result is an inductive-inductive definition with infinite
dependency, which we don't know how to make sense of internally.  But
if we can make sense of it (or make it finite by capping the h-level
somewhere), then this tower of dependent inductive-inductive types
ought to present the entire (semi)simplicial nerve of the syntactic
category of the type theory (probably in the form of something like a
"comprehension quasicategory").

The induction principle of this inductive-inductive definition should
then let us interpret it into an arbitrary sufficiently structured
quasicategory, or even an internally defined "complete Segal space" if
we do it in a homotopy type theory, such as the canonical universe,
thereby solving the autophagy problem.  On the other hand, since it
has no path-constructors, an encode-decode argument should prove that
it actually consists of h-sets, which should then allow us to
interpret untyped syntax into it.

Of course this is a VERY rough sketch and there are a lot of ways it
could go wrong, plenty of which I expect people will point out.  (-:

Mike

Re: [HoTT] Canonical forms for initiality

[Andrea Vezzosi]

On Mon, Oct 16, 2017 at 7:01 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> [...]
> However, when doing this intrinsically (which is the direct way to get
> a useful induction principle) and without h-level restriction, I found
> that there seems to be a new problem: you end up needing to substitute
> hereditarily not just one term but a whole context morphism, and then
> in defining the clauses for the graph of that hereditary substitution
> you need to know already that it is associative.  So you add another
> judgment for the graph of its associativity, but in defining its
> clauses you need to know that the associativity is coherent, and so
> on.

This is interesting but I can't quite see it, what would be the type
of the "graph of associativity" judgment?
And how would you use it in the term/type judgments?

> The result is an inductive-inductive definition with infinite
> dependency, which we don't know how to make sense of internally.  But
> if we can make sense of it (or make it finite by capping the h-level
> somewhere), then this tower of dependent inductive-inductive types
> ought to present the entire (semi)simplicial nerve of the syntactic
> category of the type theory (probably in the form of something like a
> "comprehension quasicategory").
>
> The induction principle of this inductive-inductive definition should
> then let us interpret it into an arbitrary sufficiently structured
> quasicategory, or even an internally defined "complete Segal space" if
> we do it in a homotopy type theory, such as the canonical universe,
> thereby solving the autophagy problem.  On the other hand, since it
> has no path-constructors, an encode-decode argument should prove that
> it actually consists of h-sets, which should then allow us to
> interpret untyped syntax into it.
>
> Of course this is a VERY rough sketch and there are a lot of ways it
> could go wrong, plenty of which I expect people will point out.  (-:
>
> Mike
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] Canonical forms for initiality

[Michael Shulman]

On Tue, Oct 17, 2017 at 12:33 AM, Andrea Vezzosi <sanz...@gmail.com> wrote:
> This is interesting but I can't quite see it, what would be the type
> of the "graph of associativity" judgment?

So there is a judgment for context morphisms

σ : Γ -> Δ

and a judgment for composites thereof (2-simplices)

s : σ2 ∘ σ1 = σ3

then one for the graph of hereditary substitution:

tσ : t1 [ σ ] = t2

and then for "associativity", or I suppose better "functoriality" of
that, which is a 2-simplex of some (semi-)simplicial set lying over
the (semi-)simplicial set of contexts and context morphisms:

ts : tσ2 ∘ tσ1 =( s ) tσ3

where

tσ1 : t1 [ σ1 ] = t2
tσ2 : t2 [ σ2 ] = t3
tσ3 : t1 [ σ3 ] = t3
s : σ2 ∘ σ1 = σ3

and so on

> And how would you use it in the term/type judgments?

In an intrinsic presentation of dependent type theory, the rules for
variables are kind of forced to be de Bruijn, with something like

------------------------------
(Γ , A) ⊢ pop : A [ πA ]

Γ ⊢ t : B
------------------------------
(Γ , A) ⊢ shift t : B [ πA ]

where π : (Γ , A) -> Γ is the weakening context morphism.  When you
try to define hereditary substitution into these, I think you end up
having to compose context morphisms, and then when you try to prove
functoriality for substitutions into these, you end up having to talk
about 3-simplices, and so on.

Re: Canonical forms for initiality

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 3988 bytes --]

Could you explain why you want to use normal forms and hereditary 
substitution--rather than more typical typing rules--if you expect to need 
an infinite tower of coherences anyway? Needing the coherence tower seems 
like it will make the definition dramatically more complicated, so wouldn't 
it be best to base it on the most simple and familiar typing rules?

Also, mightn't there be some clever way to "automatically" specify all the 
coherences by referring to the strict equational theory? From what little I 
read about higher operads, it seemed like they are doing that. If you need 
an infinite set of constructors, then it seems you need some strict "base 
language" to formalize the pattern. It should be able to use clever, 
indirect definitions.

On Monday, October 16, 2017 at 1:02:02 PM UTC-4, Michael Shulman wrote:
>
> On Mon, Oct 16, 2017 at 8:00 AM, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> >> 1. Give bidirectional typing rules to ensure only beta-normal, eta-long 
> >>    terms are typeable. 
> >> 2. Hence, a conversion rule can be omitted, since all terms (including 
> >>    types) are in normal form. 
> >> 3. Prove a bunch of lemmas, eventually culminating in proofs of 
> >>    (a) hereditary substitution and (b) identity expansion. (This 
> >>    basically ends up making normalization part of the definition of 
> >>    substitution.) 
> > 
> > Yes, that's what I'm proposing. 
>
> Let me expand on that a little under a new subject line, since I've 
> played around with it some already and I think I have a fairly clear 
> picture of how it should go. 
>
> In a dependently typed bidirectional system, hereditary substitution 
> needs to be mutually defined along with the typing judgments.  In 
> principle it might be possible to do this inductive-recursively, but I 
> would want to instead define the graph of hereditary substitution 
> inductive-inductively and then afterwards prove it to be a total 
> function, since inductive-inductive types are easier to make sense of 
> homotopically and generally (in my experience) have a more useful 
> induction principle.  (To reply to Matt, I am not considering any kind 
> of impredicativity; the axiomatic version could be added later.) 
>
> However, when doing this intrinsically (which is the direct way to get 
> a useful induction principle) and without h-level restriction, I found 
> that there seems to be a new problem: you end up needing to substitute 
> hereditarily not just one term but a whole context morphism, and then 
> in defining the clauses for the graph of that hereditary substitution 
> you need to know already that it is associative.  So you add another 
> judgment for the graph of its associativity, but in defining its 
> clauses you need to know that the associativity is coherent, and so 
> on.  The result is an inductive-inductive definition with infinite 
> dependency, which we don't know how to make sense of internally.  But 
> if we can make sense of it (or make it finite by capping the h-level 
> somewhere), then this tower of dependent inductive-inductive types 
> ought to present the entire (semi)simplicial nerve of the syntactic 
> category of the type theory (probably in the form of something like a 
> "comprehension quasicategory"). 
>
> The induction principle of this inductive-inductive definition should 
> then let us interpret it into an arbitrary sufficiently structured 
> quasicategory, or even an internally defined "complete Segal space" if 
> we do it in a homotopy type theory, such as the canonical universe, 
> thereby solving the autophagy problem.  On the other hand, since it 
> has no path-constructors, an encode-decode argument should prove that 
> it actually consists of h-sets, which should then allow us to 
> interpret untyped syntax into it. 
>
> Of course this is a VERY rough sketch and there are a lot of ways it 
> could go wrong, plenty of which I expect people will point out.  (-: 
>
> Mike 
>

[-- Attachment #1.2: Type: text/html, Size: 4590 bytes --]

Re: [HoTT] Re: Canonical forms for initiality

[Michael Shulman]

On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Could you explain why you want to use normal forms and hereditary
> substitution--rather than more typical typing rules--if you expect to need
> an infinite tower of coherences anyway? Needing the coherence tower seems
> like it will make the definition dramatically more complicated, so wouldn't
> it be best to base it on the most simple and familiar typing rules?

The advantage of canonical forms and hereditary substitution is that
the object-language judgmental equality automatically coincides with
the metatheoretic equality, and the inductive-inductive syntax should
simultaneously automatically form a set.  If we instead build a
coherence tower of judgmental equalities and higher judgmental
equalities, then we not only need to decide what that coherence
structure should be (whereas I think the coherence structure for
hereditary substitution should be fairly straightforward in
principle), but prove that it is "coherent" in some sense, in order to
enable the interpretation of raw syntax into inductive-inductive
syntax.

The rules of canonical-form type theory are the simple and familiar
ones, they're just annotated with "directionality" or "atomicity"
information.

Re: [HoTT] Re: Canonical forms for initiality

[Neel Krishnaswami]

Hi Mike,

Why do you prefer this style of definition to specifying the hereditary
substitution as a function (using an inductive-recursive definition)? It
seems like that would give you all the coherences you want since all
the substitution equations would hold judgmentally.[*]

I do want to see it worked out your way, now that you've told me about
it, but that's because doing the same thing two ways is usually
clarifying. However, the "obvious" way to generalize the simply-typed
presentation is with an inductive-recursive definition.

Best,
Neel

[*] I think?, since I haven't done the proofs.

On 19/10/17 20:07, Michael Shulman wrote:
> On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri <atm...@gmail.com> wrote:
>> Could you explain why you want to use normal forms and hereditary
>> substitution--rather than more typical typing rules--if you expect to need
>> an infinite tower of coherences anyway? Needing the coherence tower seems
>> like it will make the definition dramatically more complicated, so wouldn't
>> it be best to base it on the most simple and familiar typing rules?
> 
> The advantage of canonical forms and hereditary substitution is that
> the object-language judgmental equality automatically coincides with
> the metatheoretic equality, and the inductive-inductive syntax should
> simultaneously automatically form a set.  If we instead build a
> coherence tower of judgmental equalities and higher judgmental
> equalities, then we not only need to decide what that coherence
> structure should be (whereas I think the coherence structure for
> hereditary substitution should be fairly straightforward in
> principle), but prove that it is "coherent" in some sense, in order to
> enable the interpretation of raw syntax into inductive-inductive
> syntax.

Re: [HoTT] Re: Canonical forms for initiality

[Michael Shulman]

Good question!  I can think of three reasons:

1. We still don't know whether inductive-recursive definitions make
sense homotopically.
2. In my limited experience, inductive-inductive definitions generally
have more powerful induction principles than inductive-recursive ones.
In particular, it's much less clear to me that with an
inductive-recursive definition we could map out of it into any
(oo,1)-category.
3. I'm less confident than you that the inductive-recursive case would
be easier.  My experience with this sort of thing leads me to believe
that it's like playing whack-a-mole: if you think you solve the
coherence problem in one way then it pops up somewhere else.  But
someone should try it!

Mike

On Fri, Oct 20, 2017 at 3:57 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> Hi Mike,
>
> Why do you prefer this style of definition to specifying the hereditary
> substitution as a function (using an inductive-recursive definition)? It
> seems like that would give you all the coherences you want since all
> the substitution equations would hold judgmentally.[*]
>
> I do want to see it worked out your way, now that you've told me about
> it, but that's because doing the same thing two ways is usually
> clarifying. However, the "obvious" way to generalize the simply-typed
> presentation is with an inductive-recursive definition.
>
> Best,
> Neel
>
> [*] I think?, since I haven't done the proofs.
>
> On 19/10/17 20:07, Michael Shulman wrote:
>>
>> On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri <atm...@gmail.com> wrote:
>>>
>>> Could you explain why you want to use normal forms and hereditary
>>> substitution--rather than more typical typing rules--if you expect to
>>> need
>>> an infinite tower of coherences anyway? Needing the coherence tower seems
>>> like it will make the definition dramatically more complicated, so
>>> wouldn't
>>> it be best to base it on the most simple and familiar typing rules?
>>
>>
>> The advantage of canonical forms and hereditary substitution is that
>> the object-language judgmental equality automatically coincides with
>> the metatheoretic equality, and the inductive-inductive syntax should
>> simultaneously automatically form a set.  If we instead build a
>> coherence tower of judgmental equalities and higher judgmental
>> equalities, then we not only need to decide what that coherence
>> structure should be (whereas I think the coherence structure for
>> hereditary substitution should be fairly straightforward in
>> principle), but prove that it is "coherent" in some sense, in order to
>> enable the interpretation of raw syntax into inductive-inductive
>> syntax.
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] Re: Canonical forms for initiality

[Andrea Vezzosi]

To maybe add a third way: you can define the graph of hereditary
substition as a proposition if you have already proven judgmental
equality is decidable.

Let me write "Γ ⊢ e : A" for the typing judgment where Γ, e, and A are
not necessarily in normal form, and "(e , d) [[ σ ]]" for
type-preserving non-hereditary substitution for a typing derivation d.

Defining hereditary substitution mutually with the syntax seems like a
huge task to me because it involves a proof that your language is
normalizing, and I wouldn't want to convince any I-R schema that the
whole construction is well-founded.

However if one first proves that judg. equality is decidable for "Γ ⊢
e : A"[1], then we can define

t1 [ σ ] = t2 := isTrue (decideEq ((U-term t1) [[ U-subst σ ]]) (U-term t2))

where U is a function defined by I-R which converts normal form
judgments back into expressions and typing judgments; for both terms,
types, contexts and substitutions:

U-term : Γ ⊢ A → Σ (e : Expr). fst (U-cxt Γ) ⊢ e : fst (U-type A)

After the fact It should then be possible to show that the normal form
judgments are a set, and then define an actual substitution function.

However I don't know if this construction would still satisfy what we
want out of a type of normal forms? Would that be an initiality
theorem for a class of models? What class?

Best,
Andrea

[1] Like here https://github.com/mr-ohman/logrel-mltt , but I'd expect
a proof with intrinsic typing like https://arxiv.org/abs/1612.02462 to
also work.










[1] https://github.com/mr-ohman/logrel-mltt

On Fri, Oct 20, 2017 at 1:16 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> Good question!  I can think of three reasons:
>
> 1. We still don't know whether inductive-recursive definitions make
> sense homotopically.
> 2. In my limited experience, inductive-inductive definitions generally
> have more powerful induction principles than inductive-recursive ones.
> In particular, it's much less clear to me that with an
> inductive-recursive definition we could map out of it into any
> (oo,1)-category.
> 3. I'm less confident than you that the inductive-recursive case would
> be easier.  My experience with this sort of thing leads me to believe
> that it's like playing whack-a-mole: if you think you solve the
> coherence problem in one way then it pops up somewhere else.  But
> someone should try it!
>
> Mike
>
> On Fri, Oct 20, 2017 at 3:57 AM, Neel Krishnaswami
> <neelakantan....@gmail.com> wrote:
>> Hi Mike,
>>
>> Why do you prefer this style of definition to specifying the hereditary
>> substitution as a function (using an inductive-recursive definition)? It
>> seems like that would give you all the coherences you want since all
>> the substitution equations would hold judgmentally.[*]
>>
>> I do want to see it worked out your way, now that you've told me about
>> it, but that's because doing the same thing two ways is usually
>> clarifying. However, the "obvious" way to generalize the simply-typed
>> presentation is with an inductive-recursive definition.
>>
>> Best,
>> Neel
>>
>> [*] I think?, since I haven't done the proofs.
>>
>> On 19/10/17 20:07, Michael Shulman wrote:
>>>
>>> On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri <atm...@gmail.com> wrote:
>>>>
>>>> Could you explain why you want to use normal forms and hereditary
>>>> substitution--rather than more typical typing rules--if you expect to
>>>> need
>>>> an infinite tower of coherences anyway? Needing the coherence tower seems
>>>> like it will make the definition dramatically more complicated, so
>>>> wouldn't
>>>> it be best to base it on the most simple and familiar typing rules?
>>>
>>>
>>> The advantage of canonical forms and hereditary substitution is that
>>> the object-language judgmental equality automatically coincides with
>>> the metatheoretic equality, and the inductive-inductive syntax should
>>> simultaneously automatically form a set.  If we instead build a
>>> coherence tower of judgmental equalities and higher judgmental
>>> equalities, then we not only need to decide what that coherence
>>> structure should be (whereas I think the coherence structure for
>>> hereditary substitution should be fairly straightforward in
>>> principle), but prove that it is "coherent" in some sense, in order to
>>> enable the interpretation of raw syntax into inductive-inductive
>>> syntax.
>>
>>
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.