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: practice: software

Topic: Metatheory.jl

Philip Zucker (Mar 11 2021 at 16:42):

Some promising approaches to automated equational reasoning for monoidal categories that I and others have been playing with https://www.philipzucker.com/metatheory-progress/

Nathanael Arkor (Mar 11 2021 at 17:13):

This is really interesting! I had intended to experiment using Z3 for verifying diagrammatic proofs, so it's good to see someone has already tried. What kind of structures does Metatheory.jl support natively? Am I right in understanding you're trying to encode GATs into those structures (with partial success)?

Philip Zucker (Mar 11 2021 at 17:22):

It is unclear to me exactly what Metatheory supports in theoretical terms. It does what it does. It's something like a rewrite system, something like the theory of uninterpreted functions. I put forward what a think is a correct method to encode GATs. but I am not 100% certain. I have not mechanized actually producing this encoding yet. I did it by hand.

Nathanael Arkor (Mar 11 2021 at 17:25):

I would have thought the "right" structure (at least from a theoretical point of view) would be generalised algebraic theories with rewrites, though I'm not sure if this translates across to e-graphs. You can encode structure like binding operators using generalised algebraic theories, which avoids having to describe more complex higher-order structures directly in e-graphs.

Philip Zucker (Mar 11 2021 at 17:25):

You can encode binding using GATs? How?

Philip Zucker (Mar 11 2021 at 17:25):

As in the point free formulation of binding? $\sum_i a(j,i) b(i,k)$ vs $A \cdot B$ Or something else?

Nathanael Arkor (Mar 11 2021 at 17:26):

You describe everything internally: so you have a type for "contexts", a type for "types", a type for "terms", etc. Then you have operations for extending contexts, etc. This is essentially the approach of "type-theory-in-type-theory", which uses quotient-inductive-inductive types (which are closely related to GATs).

Philip Zucker (Mar 11 2021 at 17:28):

I think I see. You explicilty hold bound terms before a turnstile?

Nathanael Arkor (Mar 11 2021 at 17:29):

A $\lambda$-abstraction operator would take a term in an extended context, for instance, and return a term in the non-extended context. E.g. something like $\Gamma : \mathsf{Ctx}, t : \mathsf{Tm}(\mathsf{ext}(\Gamma)) \vdash \mathsf{abs}(t) : \mathsf{Tm}(\Gamma)$ in an untyped setting.

Philip Zucker (Mar 11 2021 at 17:31):

That's very interesting. It does seem like a rather heavyweight encoding for automation to handle, but who knows.

Nathanael Arkor (Mar 11 2021 at 17:33):

Agreed: the disadvantage with describing everything internally is that the automation can't take advantage of knowing "what the constructions mean" for optimisation purposes (at least naïvely), but the advantage is that you can describe many more structures than you would be able to externally (because you don't need to invent new structures for describing more complex data types).

Nathanael Arkor (Mar 11 2021 at 17:34):

If you are even able to demonstrate viability of automation for equations involving categories, functors, and natural transformations, that will already be a huge step forwards, though.

Philip Zucker (Mar 11 2021 at 17:34):

That's the dream. Workin' on it

Nathanael Arkor (Mar 11 2021 at 17:34):

This is a problem I'm very interested in, and would be very happy to discuss in more detail at some point :)

Philip Zucker (Mar 11 2021 at 17:36):

The current set of discussion that I'm aware has been happening on the Julia zulip. I poke my head in over here very rarely because it is overwhelming.

Philip Zucker (Mar 11 2021 at 17:54):

But where does the variable go? Is everything de bruijn indexed?

Nathanael Arkor (Mar 11 2021 at 17:56):

Essentially, yes. You avoid variable names altogether.

Nathanael Arkor (Mar 11 2021 at 17:56):

(Though possibly a more principled approach to variable names, like nominal calculi, could also work as a GAT.)

Philip Zucker (Mar 11 2021 at 17:59):

I see. Manipulating de bruijn indices in the egraph is so far non obvious(to me) that one can do it, and non obvious if they even make sense. My intuition so far is that the egraph is a bit more than just a bag of syntax. The automated sharing and congruence closure can do some surprising things.

Philip Zucker (Mar 11 2021 at 18:00):

I emailed one of the egg authors https://egraphs-good.github.io/ about this and it seems it's still an open question from his perspective as well

Nathanael Arkor (Mar 11 2021 at 18:02):

It's not necessarily to think about de Bruijn indices explicitly, though: they're hidden in the structure of the GAT. If you can represent arbitrary GATs, you can represent de Bruijn indices.

Nathanael Arkor (Mar 11 2021 at 18:02):

Nathanael Arkor said:

A $\lambda$-abstraction operator would take a term in an extended context, for instance, and return a term in the non-extended context. E.g. something like $\Gamma : \mathsf{Ctx}, t : \mathsf{Tm}(\mathsf{ext}(\Gamma)) \vdash \mathsf{abs}(t) : \mathsf{Tm}(\Gamma)$ in an untyped setting.

Note that there are no explicit indices here.

Philip Zucker (Mar 11 2021 at 18:03):

This suggests to me that either de bruijn indices are fine or I'm not actually able to represent arbitrary GATs.

Philip Zucker (Mar 11 2021 at 18:03):

There are indices in t though?

Kenji Maillard (Mar 11 2021 at 18:04):

If I'm not wrong, F* uses de Bruijn indices in practice in its SMT encoding (but I don't think that's the most efficient part of the encoding)

Philip Zucker (Mar 11 2021 at 18:04):

Oh really? Fascinating.

Philip Zucker (Mar 11 2021 at 18:07):

Do they describe that in a paper or is it just internally in the code base?

Nathanael Arkor (Mar 11 2021 at 18:08):

Philip Zucker said:

There are indices in t though?

Where? You mean $\Gamma$ would be represented by an index?

Philip Zucker (Mar 11 2021 at 18:09):

I was assuming a term would be something like abs(var(0)) for id for example.

Nathanael Arkor (Mar 11 2021 at 18:11):

Actually you can represent a variable just by an operator $\mathsf{var}$ without an index; its index is captured by the context it is in. It's a little involved to describe exactly how this works, though.

Nathanael Arkor (Mar 11 2021 at 18:11):

This is what I meant by "Essentially, yes." Actually there are no explicit indices, and they are instead represented by the term structure itself.

Nathanael Arkor (Mar 11 2021 at 18:12):

(Probably the type-theory-in-type-theory literature contains an explicit worked example in this vein.)

Philip Zucker (Mar 11 2021 at 18:14):

So what would you write for id? Or is the question poorly formed?

Philip Zucker (Mar 11 2021 at 18:15):

And how would you write \x y -> x

Nathanael Arkor (Mar 11 2021 at 18:19):

The intuition is that you don't encode arbitrary higher-order operations: you encode structures that have higher-order operations (e.g. lambda-calculi). So whenever you want to describe a higher-order operation, you first need to describe contexts and terms.

Nathanael Arkor (Mar 11 2021 at 18:24):

Another way to describe it is that in a GAT, you have a first-order context. But you can encode higher-order contexts using GATs. So they if you have a higher-order structure, you can describe it internally with respect to the encoded higher-order context, rather than the "metatheoretical" first-order context of the GAT.

Philip Zucker (Mar 11 2021 at 18:58):

I'm afraid I don't follow without something more specific

Nathanael Arkor (Mar 11 2021 at 20:41):

I wanted to write up an explicit example at some point anyway, so when I get around to it, I'll let you know. Then I can figure out how best to present it :)

Alessandro (Mar 12 2021 at 10:01):

Hi everybody! Author of Metatheory.jl here

Nathanael Arkor (Mar 13 2021 at 20:02):

@Alessandro: hi! I would be interested to hear your thoughts on data structures for algebraic/symbol computation, especially in terms of what Metatheory.jl currently supports and what you have considered supporting in the future. Have you looked at generalised algebraic theories at all?

Alessandro (Mar 15 2021 at 19:50):

I have given a quick look at GATs. I'm not a mathematician sadly.

Alessandro (Mar 15 2021 at 19:51):

Nathanael Arkor said:

Alessandro: hi! I would be interested to hear your thoughts on data structures for algebraic/symbol computation, especially in terms of what Metatheory.jl currently supports and what you have considered supporting in the future. Have you looked at generalised algebraic theories at all?

Here are our current efforts:
https://github.com/0x0f0f0f/Metatheory.jl/blob/master/test/test_cat.jl
Simple equivalence proving in SMCs with explicit type tagging

@Philip Zucker 's blogpost
https://www.philipzucker.com/metatheory-progress/

Philip Zucker (Mar 21 2021 at 16:28):

I also made a version of the same rules that is compiled to the browser using the egg library (Metatheory and egg are related systems, one in Julia, one in Rust)
http://www.philipzucker.com/rust-category/