Zulip Chat Archive

Stream: maths

Topic: algorithms, Fraction in library


view this post on Zulip Sergei (Jun 08 2019 at 10:09):

Dear Lean people,
I have the three newbie questions.

1. Generally, can Lean be used as a provable programming language?
So that to implement an efficient algorithm and also prove its correctness, and then also to run the obtained code.

2. Concretely: consider implementing fraction arithmetic over an arbitrary GCD Domain R. Find sum of fractions by doing + and * in R, by computing gcd, and cancelling by it (in various places of the method). And provide a proof for that this +' and *' on Q = (Fraction R ) make Q a field.
a) Is this possible to program in Lean and to run as a more or less efficient program?
b) Is this already in some library for Lean ?
I see "localization.lean" somewhere in mathlib, this is a generalization for Fraction field. But I do not find there using GCD, any matter of algorithms. Also I do not see there any comments.

3) The mathlib materials are difficult to understand, they just show the code. But there are needed comments in a humanly language in the first place, a reference to a textbook, to a paper (a similar problem I find in Coq).

Please, advise,


Sergei

view this post on Zulip Kenny Lau (Jun 08 2019 at 10:17):

https://github.com/leanprover-community/mathlib/blob/master/src/data/rat.lean#L227

view this post on Zulip Kenny Lau (Jun 08 2019 at 10:18):

there are no "efficient" algorithms yet. they run kind of slowly.

view this post on Zulip Kevin Buzzard (Jun 08 2019 at 10:25):

I agree about comments in mathlib. Which files are you interested in in particular?

view this post on Zulip Reid Barton (Jun 08 2019 at 10:54):

I think we have a merge sort (of the kind that uses linear additional space)--that's about it

view this post on Zulip Sergei (Jun 08 2019 at 12:05):

https://github.com/leanprover-community/mathlib/blob/master/src/data/rat.lean#L227

But this is actually Rational = (Fraction Integer). And I talk about (Fraction R) for arbitrary integral domain R supplied with gcd.

view this post on Zulip Kevin Buzzard (Jun 08 2019 at 12:06):

Yes, this is rational numbers. We do have field of fractions of an arbitrary integral domain though: https://github.com/leanprover-community/mathlib/blob/b55e44de0cdd632c2a1c3c21ce05f814ab6f614a/src/ring_theory/localization.lean#L436

view this post on Zulip Sergei (Jun 08 2019 at 12:09):

I agree about comments in mathlib. Which files are you interested in in particular?

I do not see these files. They need to be about how so do + and * on Fractions with cancelling by gcd in a general case, not only for rational numbers.

view this post on Zulip Kevin Buzzard (Jun 08 2019 at 12:15):

The link I sent is just an abstract construction of the field of fractions of an integral domain. No gcd algorithm is needed to make this ring. There is no claim that any fraction can be put into a "canonical form" there.

view this post on Zulip Sergei (Jun 08 2019 at 12:33):

We do have field of fractions of an arbitrary integral domain though:
https://github.com/leanprover-community/mathlib> /blob/b55e44de0cdd632c2a1c3c21ce05f814ab6f614a/src/ring_theory/localization.lean#L436

I have seen this from the start. I understand that substituting {0} for a prime ideal in an integral ring R for localization we obtain actually the domain (Fraction R). But I do not know the Lean language. And I do not see any explanation concerning the algorithms. How are fractions summed? Is it
a/b + a'/b' = (ab' + a'b)/(b*b') ?
Is the result somehow reduced? If R has a sensible gcd, probably it can be applied, or may be one can reduce by some ideal ...
If it is not reduced, then how will this arithmetic work say for R = Z2[x] for
Z2 = Integer modulo 2 ? how will there grow the denominator degrees?
I mean different provable ways to sum fractions that aim at a bit of efficiency. Because in computer algebra not only proof matters, but also efficiency.
This file localization.lean is difficult to understand. The only thing I understood is that this is about a local ring, and that its equality is proved transitive. There needs to be somewhere a short explanation in a humanly language of what is such and such method, say, a reference to a textbook + several words about algorithms.
?
A similar strange problem is with the Coq math libraries. One needs just to read the bare code instead of observing literature references and humanly explanations.

view this post on Zulip Reid Barton (Jun 08 2019 at 12:43):

It's not reduced and it's not meant to be efficient. It's math, not computer algebra.
However, it would also be possible to implement what you suggest--it just hasn't been done in mathlib yet.

view this post on Zulip Sergei (Jun 08 2019 at 12:48):

I see now. Thank you.
Generally in these mathlib-s there is a problem of literature references and humanly explanations.

view this post on Zulip Kevin Buzzard (Jun 08 2019 at 12:57):

The reference is Atiyah and Macdonald's book "commutative algebra". Yes, this is maths not computer algebra. The code is written so we can reason about maths, not do computations with it.


Last updated: May 06 2021 at 17:38 UTC