typelevel / algebra

Experimental project to lay out basic algebra type classes
https://typelevel.org/algebra/
Other
378 stars 69 forks source link

(Do not merge). Added finer definitions of modulo, and related laws. #172

Closed denisrosset closed 7 years ago

denisrosset commented 8 years ago

This is a basis for discussion, based on https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf

This adds a definition of the dividend/modulo operation in ordered rings, distinct from the quotmod operation on EuclideanRing.

I added instances on Rat and BigInt, as representatives of an ordered field and integers. The instances for Double and Long should match their behavior, but testing Double/Long is difficult due to limited precision and overflow.

(I do not know if we should add these types at all, but we should be clear about what we mean by the "modulo" operation. Same for the EuclideanFunction typeclass, which is there to help us write complete tests.)

codecov-io commented 8 years ago

Current coverage is 67.52% (diff: 66.66%)

Merging #172 into master will increase coverage by 0.06%

@@             master       #172   diff @@
==========================================
  Files            43         44     +1   
  Lines           885        936    +51   
  Methods         848        889    +41   
  Messages          0          0          
  Branches         37         47    +10   
==========================================
+ Hits            597        632    +35   
- Misses          288        304    +16   
  Partials          0          0          

Powered by Codecov. Last update b577b54...6cc6778

non commented 8 years ago

Thanks @denisrosset!

I propose that we do some renames to try to support both truncation and floor quotients in a reasonable way:

I don't think divmod will be confusing, since there isn't a precedent for combining true division with a remainder or modulus operation, and this operation is often defined in terms of quotient and remainder despite the name. Calling it quotrem might be a bit too far afield. (That said if others prefer quotrem we can totally use that instead.)

I think being consistent about using the f-prefix for the floor- operations will help to minimize confusion arising from this change.

If we don't want to add floor- operations I would still support the proposed renames, and being consistent in referring to rem as a remainder (and not using the words mod or modulus).

Relatedly, I would prefer to add something like OrderedRing into the laws project, since it's only used to write laws.

denisrosset commented 8 years ago

@non, beware. There are now three quotmod-like operations.

1) the one from EuclideanRing, for which the rem/mod is 0 on fields (see the law-abiding Rat test class). This one should have a default implemention in Field, setting quot(x,y) = x/y and mod(x,y) = 0. 2) the floor quotient 3) the truncation quotient

I don't think there is a way to have a common operation that abides the laws of 1+2 or 1+3 for fields.

denisrosset commented 8 years ago

For the fact that fields have mod(x,y)=0, see http://www.jstor.org/stable/2315810 or a precedent write-up here https://github.com/denisrosset/algebra/blob/master/EuclidianRing.md

non commented 8 years ago

@denisrosset My belief (maybe I'm wrong?) is that (1) satisfies the laws for (2) and/or (3), so that instances can choose to use this (or not) as they see fit without violating the laws.

One of the problems of euclidean rings is that the euclidean function is not unique, so I think there's no avoiding the fact that implementors have some leeway regarding which one they choose.

EDIT: I know that fields can choose to use quot(x, y) = x / y and rem(x, y) = 0 but is there any reason that they have to? I thought that other operations could still be law-abiding (despite maybe being less canonical in some contexts).

denisrosset commented 8 years ago

@non, hi! This is exactly what I want to explore.

(1) and (2)/(3) are the same on integers, because the Euclidean function is the absolute value.

On fields, the situation is different; I don't think there is a way to reconcile both (see the jstor reference).

Agree with the euclidean function freedom; however, we should not use this freedom to allow law-violating instances.

non commented 8 years ago

So I will dig up a way to read JSTOR articles, but in the meantime the question I have is this:

We can define some kind of quotient and remainder operation for real numbers (e.g. Double). These operations end up being extensions of quotient and remainder operations on integers (e.g. Int). Is it reasonable to generalize over these operations? If so, what should that mechanism be? Previously I had imagined that EuclideanRing provides quot and rem which can (often) be used to do this. In the case of real numbers we can be pretty sure they all support quotient and remainder. For more exotic structures, we may not be able to do so, but for fields we can use division and zero, and for other structures we can find something that is law-abiding.

If we can't use EuclideanRing to do this kind of generalization for types that represent integers/real numbers then I think we need to take a step back and figure out the right way to do that, and what else we expect to get from EuclideanRing instead.

non commented 8 years ago

Maybe we actually need two type classes here? One that supports quotient/remainder (and is pretty agnostic about sign, just requiring that y * q + r = x) and another that supports floor division, modulus, needs to care about sign, and is more constrained when dealing with fields.

denisrosset commented 8 years ago

Actually, the JSTOR reference is not needed. See simply: http://math.stackexchange.com/questions/69537/the-necessary-and-sufficient-condition-for-a-unit-element-in-euclidean-domain

In a field, all elements except zero are units, i.e. have an inverse. So the Euclidean function f is constant on them. We can then take f(x) = 1 or f(x) = 0 for all x != 0. The latter definition, f(x) = 0 has the advantage of being compatible with the degree of polynomials (a constant x is a polynomial of degree 0).

denisrosset commented 8 years ago

@non, let's summarize the instances. I'm writing equotmod for the definition coming from Euclidean rings, tquotmod and fquotmod for the operations defined on ordered rings for truncation division and floor division respectively. As noted in the Microsoft note, other definitions do not make mathematical sense.

Integers

scala> (BigInt(-3) % BigInt(2), BigInt(3) % BigInt(-2), BigInt(-3) % BigInt(-2)) 
res1: (scala.math.BigInt, scala.math.BigInt, scala.math.BigInt) = (-1,1,-1)
scala> ((-3) % 2, 3 % (-2), (-3) % (-2))
res2: (Int, Int, Int) = (-1,1,-1)
scala> java.lang.Math.floorMod(-3, 2)
res3: Int = 1

For BigInt.mod and java.math.BigInteger.mod, the result is always nonnegative but an exception is thrown if the rhs is negative.

Rationals

scala> Rational(3,2) % Rational(-1,3)
res3: spire.math.Rational = 1/6
scala> Rational(-3,2) % Rational(1,3)
res4: spire.math.Rational = -1/6
scala> Rational(-3,2) % Rational(-1,3)
res5: spire.math.Rational = -1/6

Doubles

scala> (2.125 % 1.5, (-2.125) % 1.5, 2.125 % (-1.5))
res10: (Double, Double, Double) = (0.625,-0.625,0.625)

Complex numbers

Univariate polynomials over a field

Univariate polynomials over an Euclidean ring (but not field); multivariate polynomials over an Euclidean ring or field

Note: Euclidean rings are GCD domains. While out of algebra scope, it's going to be difficult to insert a GCDDomain type later such that trait EuclideanRing[A] extends GCDDomain[A].

denisrosset commented 8 years ago

What I believe

EuclideanRing and its laws are correct. Its instances for Float, Double and BigDecimal have to be corrected such that emod(x,y) = constant.

What do we do with tquotmod or fquotmod? Should we include it into algebra? Should we include both, or only tquotmod, or a single type agnostic about the sign of the result?

Then we have to discuss the implications for Spire (but not here). In Scala stdlib, the % syntax is consistent with tquotmod. We should thus introduce new syntax for emod as to avoid any confusion.

non commented 8 years ago

@denisrosset OK, sorry for the long delay. In the last weeks I've been doing a ton of traveling, preparing for a conference, and just didn't have the time to sit down and write a clear response to your proposals (both here and in Spire). Let me try to lay out my thoughts:

Motivations

The original motivation to introduce Euclidean domains was that they seemed like a good way to abstract across the / and % operators that we have on types like Int, Double, etc. Since the Euclidean function is not unique, there are potentially many instances that would satisfy. Adding to the confusion here is that for types like Double, / and % do not form a valid quotient/remainder pair (which is something we'd overlooked in Spire).

Requirements

I think that in Spire at least we need the following things:

(1) Truncating quotient/remainder

We need to be able to abstract over "T-division" (which is intrinsic to the JVM for integer types). Despite the fact that E-division or F-division are mathematically more attractive, consistency with direct/primitive operations is really important. This would be a pair of operations, quotient and remainder, that have the truncation semantics (even in the case of fractional types).

(2) Best-effort division

Often people want to be able to write some code that abstracts over / on integers and /on floating point numbers. This probably doesn't belong in algebra, but would be supported by spire.math.Numeric or something. Confusion between this use-case and the previous use-case created an inconsistency around q*y+r = x in Spire.

(3) Generalized euclidean algorithm / GCD

We would like to be able to encode either or both of these concepts in a way that generalizes correctly (and doesn't necessarily require an Order[A]). They may need to be two separate things, or they could possibly be supported by one thing.

Way forward

The status quo right now is that EuclideanRing sort of combines (1) and (2), using the flexibility of the notion of a particular euclidean function to choose one that is "intuitive" to people working with generic numbers.

At a minimum, we need to fix the bug @denisrosset found. The least invasive fix would be to make EuclideanRing[Double] (and friends) support a correct truncated division (T-div) implementation and keep the existing remainder implementation. That would be lawful, and would maintain the existing semantics as much as possible. EuclideanRing would then be firmly written around (1), and able to support (3), depending on how we wanted to do it.

I'm open to doing something more intensive, but I think supporting F-div, T-div, and E-div is probably too much for most people to keep track of. Making E-div first class in EuclideanRing is possible, but we should be aware that it imposes a non-negotiable performance hit (including branch test) for all primitive types.

Apologies again for how long it's taken to respond to the comments and PRs on this. Thanks @denisrosset for helping us move forward.

denisrosset commented 8 years ago

@non: agree that Spire needs to support truncated division, with a % operator that obeys the Scala habitual semantics.

However, this truncated division cannot be put in EuclideanRing. Any formal definition of truncated division requires an Order (see definition in PR).

For example, complex rings such as Gaussian integers or complex numbers have a well-defined quotient/remainder for the EuclideanRing laws, but none for the truncated division laws (in the sense of tquotmod above).

I haven't looked yet at spire's GCD stuff, but it can be done (and has been done e.g. by Sage) such that the GCD operation is consistent with the EuclideanRing stuff.

To summarize, I don't see a way out except to split equotmod (which has to stay in Euclidean rings for the polynomial stuff), and tquotmod (which has to stay to provide the expected % behavior).

And I'm clearly against having a non-standard EuclideanRing; then the polynomial (univariate, multivariate) rings will become inconsistent.

non commented 8 years ago

@denisrosset OK. So in that case can we just stick with the changes you made in algebra in #174 and deal with the rest of this in Spire? Does that make sense? Spire will probably have a Gcd type class (or similar) so we can also support truncated quotient/remainder that way too.

denisrosset commented 8 years ago

@non, yep. I would even like to move EuclideanRing to spire, and have the complete hierarchy (including Gcd stuff) there.

I think that Gcd and truncated division are two different things. Gcd is well-defined on polynomials and complex numbers, while truncated division requires an Order.

But I need to have a complete look at the current implementation in Spire, including what has been done for univariate polynomials.

tixxit commented 8 years ago

I'm pretty sure we could define a default, truncated division for an OrderedRing[A] type in Spire (that extends Ring[A], not necessarily EuclideanRing[A]). Namely, I'm thinking of something like:

trait OrderedRing[A] extends Ring[A] with Order[A] with Signed[A] {
  def trem(x: A, y: A): A = x - (y * tdiv(x, y)) // Or whatever to make the signs correct.

  def tdiv(x: A, y: A): A = {
    def loop(acc: A, z: BigInt, k: BigInt): A = {
      val acc0 = acc + y * fromBigInt(k)
      if (acc0 == 0 || (acc0 > x && k == 1)) {
        fromBigInt(z)
      } else if (acc0 > x) {
        loop(acc0, z, BigInt(1))
      } else {
        loop(acc0, z + k, k * 2)
      }
    }

    loop(zero, BigInt(0), BigInt(1))
  }
}

There may be some nuances around negative numbers and such, but you get the idea. The laws for an ordered ring should mean the default tdiv is correct, albeit slow.

The only problem I could see is that Int and whatnot are actually not real integers, but integers modulo 2^32. This means the OrderedRing laws wouldn't quite hold for them, unless we constrain the values to be "small" so that we don't see overflow. One could argue it's morally an orderedring, similar to Double and field.

denisrosset commented 8 years ago

@tixxt, that's a an excellent idea. However, I think we should move this to Spire; Signed is not part of algebra.

Actually, Int are not integers nor integers modulo 2^32 (that would be UInt). IMHO, Int should be treated as an approximation of the integer ring ℤ that works as long as you don't go "too far" --- in the same spirit as we consider Double to be an approximation of real numbers.

It's actually an interesting question: how to test these approximate types? Let's have this conversation later. We should a minima document things like "Int approximates the BigInt euclidean ring for the range [...], the behavior outside this range is undefined", "Double approximate real numbers; the result of field operations (+ - * /) should be approximatively equal to the result of the corresponding Rational behavior".

denisrosset commented 7 years ago

The discussion will be moved to Spire.

Closing.