Zulip Chat Archive

Stream: maths

Topic: groebner basis algorithm


view this post on Zulip Jalex Stark (May 11 2020 at 21:28):

I don't really know what a groebner basis algorithm is, except that

  1. it's a generalization of the ring tactic and

  2. sage has an implementation that is fast enough to be useful to people doing exploratory mathematics

question: does the grobner basis method produce small witnesses checkable by ring? if so, can we get ring++ in Lean by "just" shelling out to an oracle?

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 21:45):

Yes, this is possible but you need to understand what elements of the coefficients ring are equal to zero.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 21:47):

Coq has a per-field/ring set of tactics that deal with coefficients, and this set of tactics is used by ring, field, and groebner (not sure about exact names).

view this post on Zulip Alex J. Best (May 11 2020 at 21:49):

I've also had this thought, I think this is a really achievable goal, what's needed is enough of the theory to give Buchberger's criterion, this should be enough that lean can check the witness, then Sage or Singular can be called to produce a basis.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 21:51):

If all we want is a tactic that solves a goal P1(x1,,xn)=0,,Pk(x1,,xn)=0Q(x1,,xn)=0P_1(x_1, \dots, x_n) = 0, \dots, P_k(x_1, \dots, x_n)=0 \vdash Q(x_1, \dots, x_n)=0, then we don't need any theory to check the witness.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 21:54):

Because the witness has a form R(P1,,Pk)=QmR(P_1, \dots, P_k)=Q^m.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 21:55):

On the other hand, it would be nice to have a function that verifies is_groebner_basis predicate but this can be postponed.

view this post on Zulip Kevin Buzzard (May 11 2020 at 22:09):

Yes this is a job which would be perfect for an external solver like sage and it would not surprise me at all if @William Stein could help. @Rob Lewis set this up with Mathematica before, right?

view this post on Zulip Kevin Buzzard (May 11 2020 at 22:09):

The "normal"algebra package finds a relation and then ring formally checks it

view this post on Zulip Alex J. Best (May 11 2020 at 22:10):

@Gabriel Ebner's hammer project would also be a good template for calling an external program, parsing the result into lean and then doing something with it I think.

view this post on Zulip Alex J. Best (May 11 2020 at 22:15):

It would be great to have a Sage link, but I think for this purpose calling one of the underlying libraries of Sage to calculate groebner bases might be simpler (and faster) to begin with.

view this post on Zulip Anne Baanen (May 12 2020 at 08:30):

Some people at the VU have worked on Gröbner bases a while back, but I believe it's dormant now. I'll ask about the current state and see if they want to share the work in progress.

view this post on Zulip Kenny Lau (May 12 2020 at 08:32):

every project not PR'd into mathlib is lost in time

view this post on Zulip Kevin Buzzard (May 12 2020 at 08:59):

Do you know if they were actually implementing the algorithm in Lean? Because this is one of these situations where a result is far easier to check than to discover, the discovering might be best left to an external program

view this post on Zulip Rob Lewis (May 12 2020 at 09:02):

The project at the VU did implement the algorithm in Lean, but I think resurrecting it will be a big challenge.

view this post on Zulip Rob Lewis (May 12 2020 at 09:03):

Doing this with an external computation is totally reasonable. The problem is, how do we integrate that into mathlib? Do we make Sage a dependency for compiling the library?

view this post on Zulip Rob Lewis (May 12 2020 at 09:03):

Who wants to stay up to date on compatibility with different OSs, Python versions, Sage versions, ...?

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:04):

I guess this shouldn't be in mathlib?

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:04):

Or the tactic should just break if the dependency isn't there?

view this post on Zulip Rob Lewis (May 12 2020 at 09:04):

We don't need to leave calls to Sage in the library, so maybe it's not a requirement to compile. But there's still some presumption that if the tactic is available someone keeps it working.

view this post on Zulip Rob Lewis (May 12 2020 at 09:05):

It's similar to worries about #1083

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:06):

This is one of these tactics like library_search where you run it once and it says "type this instead" and whoever types this instead doesn't need sage

view this post on Zulip Rob Lewis (May 12 2020 at 09:07):

Right, but if you want to run it once, you do need Sage, so a lot of people are going to show up on this chat asking "why doesn't groebner work for me?"

view this post on Zulip Johan Commelin (May 12 2020 at 09:08):

Maybe if we call it groebner_sage we will get less of those questions?

view this post on Zulip Johan Commelin (May 12 2020 at 09:08):

Or sage.groebner

view this post on Zulip Rob Lewis (May 12 2020 at 09:09):

Again, it's the same situation as #1083 or sledgehammer or anything with external dependencies. I'm not saying don't do it. Just make sure it's worth the support costs.

view this post on Zulip Rob Lewis (May 12 2020 at 09:09):

/ know who's tasked with supporting it and what they're willing to help with.

view this post on Zulip Mario Carneiro (May 12 2020 at 09:15):

I think the first step is to write the ring ++ tactic that can be used as the target for these groebner calls

view this post on Zulip Mario Carneiro (May 12 2020 at 09:19):

I'm imagining an interface like ring [(x + y, h1), (z, <- h2)] which checks that if the goal is a = b and h1 : l1 = r1 and h2 : l2 = r2, then a - (x + y) * l1 - z * r2 = b - (x + y) * r1 - z * l2 is an equality in commutative rings

view this post on Zulip Mario Carneiro (May 12 2020 at 09:21):

Importantly, you don't need sage to use this tactic; in many instances it is perfectly within the ability of the user to come up with coefficients making the invocation work

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:24):

Wow, this looks like a much easier endeavour and Mario is absolutely right, in many cases the user will be able to solve for the coefficients by themselves. And in the manual it could say "if you are lazy and don't want to work out the coefficients of h1 and h2 yourself, then type "sage.ring_hint" and cut and paste the resulting code into sage, and then cut and paste the output of the sage code back into Lean" :-)

view this post on Zulip Chris Hughes (May 12 2020 at 09:27):

Even if you do need sage, can sage not just return a certificate that can be passed as an argument to the tactic?

view this post on Zulip Chris Hughes (May 12 2020 at 09:28):

So there's one version that interfaces with sage and one that just asks for the certificate.

view this post on Zulip Mario Carneiro (May 12 2020 at 09:28):

yes, but if the replacement tactic is so arcane that it can't be used directly, then you still need to use sage to construct the proof

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:29):

In @Daniel Fabian 's example from yesterday, he had

h1 : f (2 * (a + k)) + 2 * f (l - a) = f (f (k + l)),
h2 : f (2 * (b + k)) + 2 * f (l - b) = f (f (k + l))
 2 * (f (l - a) - f (l - b)) = f (2 * (b + k)) - f (2 * (a + k))

and ring++ [(1,h1),(1,<-h2)] would do it, as would ring++ [(1,h1),(-1,h2)] (note in particular that there is no need for <- I guess). The fact that these numbers are +-1 is why linarith solved it, but in general they won't be.

view this post on Zulip Mario Carneiro (May 12 2020 at 09:30):

the back arrow (and the subtractions in my gloss of what they mean) are to support semirings

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:30):

rofl

view this post on Zulip Mario Carneiro (May 12 2020 at 09:31):

@Chris Hughes for example, if you are a maintainer and are fixing a broken proof, and the certificate no longer works, you need to have sage to regenerate the proof

view this post on Zulip Chris Hughes (May 12 2020 at 09:39):

If you were fairly strict about how to use it, then it might be okay. As in you always used it as have _ : by groebner [certificate], then the proofs would be fairly stable

view this post on Zulip Rob Lewis (May 12 2020 at 09:39):

If this is implemented, it would be great if the Sage call could fall back to a Lean implementation. Try the fast one first, but if Sage isn't there, do it natively. A rudimentary meta groebner basis algorithm isn't crazy hard.

view this post on Zulip Mario Carneiro (May 12 2020 at 09:45):

how expensive is FFI to sage/mathematica? Is it possible that the lean version will win for not being "external"?

view this post on Zulip Rob Lewis (May 12 2020 at 09:47):

It depends how much effort you put into the architecture of both. Sage and Mathematica are both very expensive to start up. If you don't have a server running, the native version will probably win for small problems, especially if you do a decent job implementing it.

view this post on Zulip Kevin Buzzard (May 12 2020 at 09:57):

In case there are any people who don't really know what Groebner bases are, here is a summary of what is going on.

import tactic

example (a b : ) (h1 : a^2 = b^2) (h2 : a^3=b^4) : a^8=b^10 :=
begin
  -- proof which contains a human-generated mathematical idea
  rw (show a^8 = a^2 * a^3 * a^3, by ring),
  rw h1,
  rw h2,
  ring -- note `ring` called twice, once to implement the idea and once to finish the job
end

-- the Commelin-Barton trick
@[reducible] def eq.lhs {α : Type*} {x y : α} (e : x = y) : α := x
@[reducible] def eq.rhs {α : Type*} {x y : α} (e : x = y) : α := y

example (a b : ) (h1 : a^2 = b^2) (h2 : a^3 = b^4) : a^8 = b^10 :=
begin
  -- "the same" human-generated idea, in a different format
  suffices : a^8  + a^6*h1.rhs + b^6*h2.rhs + a^3*b^2*h2.rhs =
             b^10 + a^6*h1.lhs + b^6*h2.lhs + a^3*b^2*h2.lhs,
  { rw (show eq.lhs h1 = eq.rhs h1, from h1) at this,
    rw (show eq.lhs h2 = eq.rhs h2, from h2) at this,
    simp at this, exact this}, -- note: no `ring` needed
  unfold eq.lhs eq.rhs,
  ring,
end

example (a b : ) (h1 : a^2 = b^2) (h2 : a^3 = b^4) : a^8 = b^10 :=
begin
  -- the above script, all packed into a tactic
  ring++ [(a^6, h1), (b^6+a^3*b^2, h2)]
  -- doesn't work yet though
end

/-
The underlying question: Let R be the ring ℤ[A,B] and let I be the ideal (A^2-B^2,A^3-B^4).
Is A^8-B^10 in I? Yes it is, because it's A^6(A^2-B^2)+(A^3B^2+B^6)(A^3-B^4)

The point is a computer algebra package such as SAGE could find the representation of A^8-B^10
and then ring++ can just take the inputs and check that the computer algebra package gave
the right answer
-/

view this post on Zulip Kenny Lau (May 12 2020 at 10:00):

thanks for the explanation; that makes it very clear

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:00):

I never know if you are being sarcastic ;-)

view this post on Zulip Mario Carneiro (May 12 2020 at 10:00):

your proof is a bit unexpected. I would have expected something akin to h1 * h2 * h2

view this post on Zulip Mario Carneiro (May 12 2020 at 10:01):

I guess this is part of the grobner basis idea that this can be written as a linear function of the h's

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:01):

Yes, the problem is that to prove (h2.lhs)^2=(h2.rhs)^2 you have to write 0 as a difference of two squares and observe that one of the factors is zero

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:02):

b^6+a^3b^2=b^2(b^4+a^3) which is the LHS+RHS factor for h2.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:02):

but that's not true, right? I mean h2.lhs^2 = h2.rhs^2 follows trivially from h2.lhs = h2.rhs

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:03):

But your ring++ specification didn't have this

view this post on Zulip Mario Carneiro (May 12 2020 at 10:03):

that is true

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:03):

I could only subtract c*h1.lhs and c*h1.rhs, but I know how all this works in practice so I just worked around it

view this post on Zulip Mario Carneiro (May 12 2020 at 10:03):

I was thinking abot being able to write some equation like h1 * h2 * h2 where it means what you think it means

view this post on Zulip Mario Carneiro (May 12 2020 at 10:04):

If ring++ is to be a human usable tactic, I think it should probably allow such things even if they aren't strictly required for the ideal membership problem

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:05):

If you're happy with more work for you, that's great. I'm observing that ring++ in the form you proposed seems to me to be writable in a small amount of code and provides a tool which looks like it might already be really useful.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:06):

I believe that a grobner basis algorithm will always produce a certificate which is a linear function of the hypotheses

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:06):

It should be easy to write the Sage code which turns (h1 : a^2 = b^2) (h2 : a^3 = b^4) : a^8 = b^10 into ring++ [(a^6, ←h1), (b^6+a^3*b^2, ←h2)]

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:08):

You are proposing making something easier for humans to use, and of course the easier it is for humans to use the better, but what has dawned on me is that even this "stupid" version of ring++ where there is no syntax for being able to add h1.lhs*h3.rhs^2 to one side and h1.rhs*h3.lhs^2 to the other, is still something which has got far more power than I had realised.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:09):

because I can write sage code from there

view this post on Zulip Mario Carneiro (May 12 2020 at 10:10):

I think another way to think about the coefficients you got is to successively rewrite a^2 * a^3 * a^3 = b^2 * a^3 * a^3 = b^2 * b^4 * a^3 = b^2 * b^4 * b^4. Each equality is a coefficient times one of the hypotheses, and the chaining is adding the functions together, so you get a linear combination in the end

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:22):

I think that what's happening now is that you are interested in making some kind of better, or easier-to-use algorithm, but this is not the kind of thing I know anything about; I can already see the path to enlightenment and it uses external forces which I have (computer algebra packages), so as far as I am concerned the problem is solved.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:33):

rather, I'm reverse engineering where you got those constants since they weren't in the first version of the proof

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:34):

oh but they're just obvious ;-)

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:34):

The second rewrite is really two rewrites. I am doing them separately

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:34):

The first changes a6a2a^6a^2 into a6b2a^6b^2

view this post on Zulip Mario Carneiro (May 12 2020 at 10:34):

as for making ring ++, there is no real added difficulty in multiplying equations compared to adding them. Especially if you give the remainder term, this is pretty trivial and you can have the equations under arbitrary functions

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:35):

the second changes a6b2a^6b^2 into a3b6a^3b^6 and the third changes that to b10b^{10}. I guess I wrote them in a different order though.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:36):

actually, the version I proposed might still not be sufficient for semirings unless you include transitivity

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:36):

I am too unimaginative to imagine the syntax for "now add h1.L*h3.R^2 to one side and h1.R*h3.L^2 to the other"

view this post on Zulip Mario Carneiro (May 12 2020 at 10:37):

I am just thinking about literally writing ring h1 * h2 * h2

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:38):

Of course I personally don't care about semirings. If I ever have an equality between naturals which I want to prove, then I can embed it into the integers and prove it there, and if it uses subtraction then I already did something wrong (I didn't embed into the integers early enough).

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:38):

Nat subtraction does not exist in maths so you never see it in the wild

view this post on Zulip Mario Carneiro (May 12 2020 at 10:38):

We see it in the wild all the time

view this post on Zulip Mario Carneiro (May 12 2020 at 10:38):

the lean wild

view this post on Zulip Mario Carneiro (May 12 2020 at 10:39):

same with nat equalities

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:39):

Now we have norm_cast I just move between nat and int freely.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:39):

Yeah you see nat subtraction in CS Lean, but in CS lean you surely don't see complicated Groebner bases questions? omega will do for you, right?

view this post on Zulip Mario Carneiro (May 12 2020 at 10:39):

Sure you do

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:40):

Oh OK I stand corrected!

view this post on Zulip Mario Carneiro (May 12 2020 at 10:40):

That problem that you used in the example could just as easily have been on nat

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:40):

Sure, but it's not a problem a computer scientist needs to solve when they're verifying that their code has no bugs

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:40):

whereas it's the sort of thing which comes up all the time in number theory

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:41):

except that we can move to int

view this post on Zulip Mario Carneiro (May 12 2020 at 10:41):

I know for a fact that linear arithmetic comes up all the time, and this is essentially the equality version

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:42):

but you already have linarith, which Patrick observed solved Daniel Fabian's question.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:42):

Do we have a generic construction for putting negation in a semiring?

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:43):

You mean localising it? I think that @Amelia Livingston has worked her socks off with this.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:43):

although she is in the middle of UG maths exams now (like Chris)

view this post on Zulip Mario Carneiro (May 12 2020 at 10:43):

is it good enough to be used behind the scenes by ring ++?

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:44):

Now that I don't know.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:44):

In particular does it need additional hypotheses on the semiring

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:44):

The map from the semiring to its ringification won't be injective in general

view this post on Zulip Mario Carneiro (May 12 2020 at 10:46):

that's... bad, right?

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:49):

Mario Carneiro said:

I am just thinking about literally writing ring h1 * h2 * h2

My example is too superficial perhaps. In general life won't be as easy as this.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:50):

Mario Carneiro said:

that's... bad, right?

Well the question as to whether a computer scientist cares about a non-ring semiring whose map to its ringification is not injective is one for which I'd be surprised to hear that the answer was "yes", but you already surprised me once.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:50):

Isn't it though? At least for everything covered by grobner basis algorithm it is ring a * h1 + b * h2.symm and so on

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:50):

Yes, but we just got lucky that the goal literally was h1h2^2

view this post on Zulip Mario Carneiro (May 12 2020 at 10:51):

Well the question as to whether a computer scientist cares about a non-ring semiring whose map to its ringification is not injective is one for which I'd be surprised to hear that the answer was "yes", but you already surprised me once.

The CS problem is not that the map is not injective, but rather that we don't have available the knowledge that the map is injective

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:53):

example (a b c d e : ) (h1 : a+b = c+d) (h2 : a^2+b^2=c^2+d^2) : a^2-c^2+e*b-e*d=d^2-b^2+e*a-e*c :=

This is the sort of goal I'd really like to be able to dispatch quickly. Goals like this come up annoyingly often.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:54):

You have that the map from nat to int is injective. I've seen no coherent argument from you for why to make the tactic work for semirings. If it works for all commutative rings and nat, will the CS people be satisfied? I conjecture that the maths people will.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:55):

I wouldn't use it with nat anyway, because if I have a question about nat then I will coerce to int, work there, and coerce back. This will always work for me because I don't do pathological things with naturals like subtract them until I have coerced to int.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:55):

commutative rings and nat is probably enough? There are also ennreal, enat and a few other examples of semirings that are not commutative rings or nat in mathlib

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:56):

Oh! I could quite imagine ennreal being something that people might need. This is a nice example.

view this post on Zulip Mario Carneiro (May 12 2020 at 10:56):

it's also not even cancellative

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:56):

I never quite know how seriously to take arithmetic in types like ennreal.

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:56):

Sure it's a really important target type for certain norms

view this post on Zulip Kevin Buzzard (May 12 2020 at 10:57):

but what one actually does in practice with outputs of norm functions -- I am not so sure that people end up doing complicated polynomial arithmetic with them, or if they did then they might be able to say "if a=infinity then what we actually want to prove is trivial, and if a is finite let's just coerce back into the reals"

view this post on Zulip Mario Carneiro (May 12 2020 at 10:58):

Here's an interface that would work with semirings: ring_rw [a*h1] tries to find a b such that goal.lhs = a * h1.lhs + b and then rewrites it to a * h1.rhs + b

view this post on Zulip Mario Carneiro (May 12 2020 at 10:59):

and you can have a sequence of such, and it closes with ring

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:26):

My example

example (a b c d e : ) (h1 : a+b = c+d) (h2 : a^2+b^2=c^2+d^2) : a^2-c^2+e*b-e*d=d^2-b^2-e*a+e*c :=

is a great example of what is currently hard to do. If h1 : a = F(b,c,d,e) then you can just eliminate all a's with rw h1 and you now have 1 fewer generator. When you're down to 0 generators you've won. With the example you don't have just one variable on one side in either hypothesis so currently you have to start faffing around with various eq_add_iff_sub_eq-type lemmas.

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:28):

oh hang on, it's also not true (sign error fixed)

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:29):

example (a b c d e : ) (h1 : a+b = c+d) (h2 : a^2+b^2=c^2+d^2) : a^2-c^2+e*b-e*d=d^2-b^2-e*a+e*c :=
begin
  apply_fun (λ x, e*x) at h1,
  rw [mul_add, mul_add] at h1,
  linarith,
end

This is the sort of hackery I'd come up with for that

view this post on Zulip Mario Carneiro (May 12 2020 at 11:31):

with ring_rw, I'm imagining that it will make it match, even if it doesn't obviously match. So if you ring_rw [h2] on that goal, a^2-c^2+e*b-e*d turns into (a^2+b^2)-c^2+e*b-e*d-b^2 and then it gets rewritten to (c^2+d^2)-c^2+e*b-e*d-b^2, which it can also simplify if desired.

view this post on Zulip Mario Carneiro (May 12 2020 at 11:32):

After cancelling factors, the goal generated by ring_rw [h2] might be e*b-e*d=-e*a+e*c

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:32):

I multiplied one equation by e; if I'd also multiplied the non-linear equation by something it would have been harder to sort out. In general you have to know what factor to multiply by which is what your original ring++ was asking for.

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:33):

ring_rw [h2] is just like ring++ [(1,h2)]

view this post on Zulip Mario Carneiro (May 12 2020 at 11:33):

Right, ring_rw [h1] at this point would not solve the goal, it would make a mess, but ring_rw [-e * h1] would work

view this post on Zulip Mario Carneiro (May 12 2020 at 11:34):

Yes, this is an alternative interface in terms of multiple rewrites instead of linear functions

view this post on Zulip Kevin Buzzard (May 12 2020 at 11:34):

Yes, I now see that the way you're thinking about it is going to make it far easier for humans to use.


Last updated: May 10 2021 at 08:14 UTC