Stream: Coq users

Topic: presenting a language


view this post on Zulip Christian Williams (Aug 27 2021 at 22:00):

Hi, I'm interested in presenting languages in Coq. For example, the language of categories is given by sorts AA for arrows and OO for objects, constructors for source and target s,t:AOs,t :A\to O, with composition :t×sA\circ: t\times s\to A and identity i:OAi: O\to A, plus associativity and unitality equations. How can this presentation be given in Coq, so that we can reason in this language?

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:25):

where t \times s is really the pullback, right?

view this post on Zulip Christian Williams (Aug 27 2021 at 22:28):

yes

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:29):

For many languages the syntax can be described directly in Coq via inductives — but as usual, category theory is more challenging to formalize, e.g. this pullback is already trickier:

Inductive arrow : Set where
| identity : object -> arrow
| comp : arrow -> arrow -> arrow
with object : Set where
| src : arrow -> object
| dst : arrow -> object.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:31):

I hope somebody else has a smarter idea! It’d be nice to define this directly, but I think this would need induction-induction, which is not (yet) supported in Coq (?):

Inductive arrow : object -> object -> Set where

with object : Set where

view this post on Zulip Christian Williams (Aug 27 2021 at 22:32):

hm, yes I see. thanks

view this post on Zulip Christian Williams (Aug 27 2021 at 22:33):

I just noticed that someone asked the same question a few hours ago https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/New.20Stack.20Exchange.20question/near/250985540

view this post on Zulip Christian Williams (Aug 27 2021 at 22:34):

Record Category := {
  Ob : Type ;
  Hom : Ob -> Ob -> Type ;
  comp : forall {a b c}, Hom b c -> Hom a b -> Hom a c ;
  id : forall {x}, Hom x x ;
  Assoc :
    forall a b c d (f : Hom c d) (g : Hom b c) (h : Hom a b),
      comp f (comp g h) = comp (comp f g) h ;
  LeftId : forall a b (f : Hom a b), comp id f = f ;
  RightId : forall a b (f : Hom a b), comp f id = f ;
  Truncated : forall a b (f g : Hom a b) (p q : f = g), p = q
}.

view this post on Zulip Christian Williams (Aug 27 2021 at 22:35):

I suppose this method gets around the need for pullback? like the concept of generalized algebraic theory

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:35):

If that's relevant, I was probably mislead by "presenting a language"; I thought you wanted to reason about the syntax of words in the language?

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:35):

(this category theory library uses a similar approach: https://github.com/jwiegley/category-theory/blob/master/Theory/Category.v#L38)

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:38):

in these examples, values of type Category _are_ categories (or if you want, structures/models of that language); if that’s what you want, that’s alright

view this post on Zulip Christian Williams (Aug 27 2021 at 22:38):

yes, I'm looking for a way to present categories with structure, such as "Theory(Cat)" as a category with finite limits, in such a way that we can reason about morphisms (terms) in the internal language of such a category.

view this post on Zulip Christian Williams (Aug 27 2021 at 22:40):

well, for now I mainly care about the theory itself or the "free model". but yes, it would also be useful to reason about models as well.

view this post on Zulip Christian Williams (Aug 27 2021 at 22:40):

what would be any alternative to that? sorry I'm not yet seeing what distinction we're making.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:42):

Ah, the distinction is exactly the one between “free model” and “all models”.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:42):

And the records above lets you reason about “all models” without letting you reason about the free model.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:44):

While using inductive types gives an immediate way to build free theories, but does not (immediately) account for equations…

view this post on Zulip Christian Williams (Aug 27 2021 at 22:53):

hm, I see...

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:54):

okay, I can see an idea, tho I’m sure it’s not the simplest. How much Coq are you already familiar with?

view this post on Zulip Christian Williams (Aug 27 2021 at 22:54):

so you're saying inductive types are like free models, but they currently have limitations - no equations, no "forall", etc

view this post on Zulip Christian Williams (Aug 27 2021 at 22:54):

oh okay. not much, just beginning

view this post on Zulip Christian Williams (Aug 27 2021 at 22:54):

I just have a category theory background

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:55):

some “forall” is there, depending on what you mean, but equations are trickier.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 22:56):

On top of inductives, one can use quotients to encode equations, or reason “explicitly” about the equalities.

view this post on Zulip Christian Williams (Aug 27 2021 at 22:59):

okay

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:00):

For instance, after writing my first snippet, and something like (untested):

Inductive eq_arrow : arrow -> arrow -> Set where
| id_l : forall a, eq_arrow (comp identity a) a
| id_r : forall a, eq_arrow (comp a identity) a
| assoc : forall a b c, eq_arrow (comp (comp a b) c) (comp a (comp b c)).

then the type eq_arrow f g is a type containing the proofs (if any) that f and g are equal according to associativity and unitality.

view this post on Zulip Christian Williams (Aug 27 2021 at 23:02):

hm, I see. so in the first snippet, you made a multisorted theory by first saying "arrow" and then later saying "with object" to give the sorts that arrow depends on. is that right?

view this post on Zulip Christian Williams (Aug 27 2021 at 23:03):

then following that logic, we could also combine eq_arrow into that inductive type? eq_arrow depends on arrow depends on object

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:03):

  1. something like that

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:03):

  1. we don’t really need to combine eq_arrow into that (and it would fail)

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:04):

but Inductive does not exactly define “a theory”

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:04):

it defines the two sorts, then adds “constructors” and gives their sorts.

view this post on Zulip Christian Williams (Aug 27 2021 at 23:06):

alright, sure. so for some reasons it's good to keep the equational reasoning separate, okay.

view this post on Zulip Christian Williams (Aug 27 2021 at 23:07):

and then do we somehow quotient arrow by eq_arrow? or something to that effect

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:08):

This keeps them separate — there are ways, but trying to point you at them would be a didactic crime…

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:09):

at least this early — there are many subtle differences between inductives and multisorted theory, so what I started was just a hint…

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:09):

And as a technical correction, we need to add base elements:

Inductive arrow (A O : Set) : Set where
| base_arr : A -> arrow A O
| identity : object A O -> arrow A O
| comp : arrow A O -> arrow A O -> arrow A O
with object (A O : Set) : Set where
| base_ob : O -> Set
| src : arrow A O -> object A O
| dst : arrow A O -> object A O.

view this post on Zulip Christian Williams (Aug 27 2021 at 23:11):

base elements? like generators?

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:11):

yeah :-)

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:12):

However: to make sense of this, I must direct you at some Coq introduction first (say, https://softwarefoundations.cis.upenn.edu/lf-current/toc.html); at least you should get to the point where Inductive is presented.

view this post on Zulip Christian Williams (Aug 27 2021 at 23:12):

sure, thanks

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:12):

That book is more aimed at computer scientists than mathematicians or category theorists, but since you are interested in working with free models, that might be closer to what you need, and is a decent introduction to Coq anyway.

view this post on Zulip Christian Williams (Aug 27 2021 at 23:13):

great! I can look at this and get back to you later

view this post on Zulip Christian Williams (Aug 27 2021 at 23:13):

I appreciate your help.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 23:13):

FWIW, somebody else might have very different suggestions, and I’m curious about those :-)


Last updated: Feb 06 2023 at 13:03 UTC