Modular arithmetic

[WorldSEnder]

I wanted to come up with a better implementation for primality. Basic modular arithmetic should probably be tackled first but they might go hand in hand.

[MatthewDaggitt]

What are the current problems? And what would your suggestion be?

[WorldSEnder]

My biggest suggestion would be implementing finite field operations for Fin - multiplication, addition, subtraction and division alongside with the usual theorems - as binary operations on Fin. If those exist, I'm sorry for overlooking them.

After that, it might be beneficial to be less dependent on the representation of Nat. As numbers get bigger, modular arithmetic under some power of 2, say 2^1024 is - in my mind - better formulated in terms of Bin rather than Nat.

[MatthewDaggitt]

My biggest suggestion would be implementing finite field operations for Fin - multiplication, addition, subtraction and division alongside with the usual theorems - as binary operations on Fin. If those exist, I'm sorry for overlooking them.

Nope, you haven't missed them. If you'd be interested in coming up with an efficient implementation that'd be great!

After that, it might be beneficial to be less dependent on the representation of Nat. As numbers get bigger, modular arithmetic under some power of 2, say 2^1024 is - in my mind - better formulated in terms of Bin rather than Nat.

Yup, I think @mechvel has suggested something similar in #65. It's quite a big project though as Data.Bin isn't very developed and probably needs to be slightly rethought at some point.

[oisdk]

I tried to do this a little in the past. I found that Fin didn't really work well as a modular arithmetic type. I had better luck with the following:

infix 4 _≥_
data _≥_ (m : ℕ) : ℕ → Set where
  m≥m : m ≥ m
  m≥p : ∀ {n} → m ≥ suc n → m ≥ n

Mod : ℕ → Set
Mod = ∃ ∘ _≥_

(The Mod is kind of a misnomer: numbers in base-10, for instance, would be "mod-9")

Addition can be implemented with the same efficiency as on N:

infixl 6 _+_
_+_ : ∀ {n} → Mod n → Mod n → Mod n
(_ , x) + (ys , y) = go x ys y
  where
  go : ∀ {n m} → n ≥ m → ∀ ys → n ≥ ys → Mod n
  go m≥m ys y = ys , y
  go (m≥p x) zero y = _ , x
  go (m≥p x) (suc ys) y = go x ys (m≥p y)

I also have linear implementations of to/from N.

With Fin, the issue is that to check for "overflow" takes O(n) time, so + and so on implemented in the usual way are O(n^2).

[MatthewDaggitt]

Interesting read, thanks!

I found that Fin didn't really work well as a modular arithmetic type.

Yup, I've also run into this problem!

With Fin, the issue is that to check for "overflow" takes O(n) time, so + and so on implemented in the usual way are O(n^2).

I think you can implement it in O(n) time (with a big constant) by converting both to Nat, performing the addition, checking for overflow, subtracting if necessary, and then converting back again. But obviously it's incredibly ugly to work with and prove anything about...

It looks like your definitions might be a good fit for using to reimplement Data.Digit at some point...

[oisdk]

Yeah, I think I might have an O(n) conversion from Fin -> Mod and back lying around somewhere, which would allow for O(n) _+_. There's also this blog post for modular types

[oisdk]

this is a slightly fuller working through of the technique

[mechvel]

Fast modular arithmetic needs fast divMod, and fast divMod needs fast comparison <-cmp on natural nubmers. The Binary representation helps to exponentially reduce the cost order of these operations.
For Binary, there are libraries by A. Alekseev
https://github.com/Rotsor/BinDivMod,
by M. Escardo
http://www.cs.bham.ac.uk/~mhe/agda-new/BinaryNaturals.html,
and of mine
https://github.com/mechvel/Binary-3.2,
https://github.com/mechvel/Binary-4

There is a particular point about the performance of <-cmp on Bin in Binary-4.
If the user program analyses the proof construction in the result of <-cmp, this may cause exponential cost growth for evaluation.
Binary-3.2 is free of this danger, because _<_ on Bin is defined there as a lexicographic order on bit lists. But Binary-4 is more clearly written.

[Taneb]

I've been working on "unnormalised" modulo arithmetic here: https://github.com/Taneb/antlion/blob/master/src/NumberTheory/ModularArithmetic.agda

[mechvel]

Currently standard library applies built-in arithmetic for Nat. If we take this, then there does not remain any performance question about modulo arithmetic. Because divMod works fast, "almost in constant time".
If we insist on really proved arithmetic on natural numbers NN, with representing a number by a list of macro-digits, then the modulo arithmetic performance is the performance of really proved divMod for NN.

[MatthewDaggitt]

I've been working on "unnormalised" modulo arithmetic here: https://github.com/Taneb/antlion/blob/master/src/NumberTheory/ModularArithmetic.agda

Looks pretty good. We'd welcome a contribution to the library! My only comment is that it might be useful to expose a more obviously ternary version of the relation, i.e. _≈_%_

[Taneb]

I've been thinking about this some more, and I'm not sure exactly how I want to do it.

I think something like

module Data.R.ModularArithmetic where

module Mod (m : R) where
   _≋_ : Rel R 0ℓ

  isEquivalence : IsEquivalence _≋_
  +-*-isRing : IsRing _≋_ _+_ _*_

  -- some more properties where we stick to one modulus

_≋_%_ : ℕ → ℕ → ℕ → Set
x ≋ y % m = let open Mod m in x ≋ y

-- some properties where we use more than one modulus, like the Chinese remainder theorem

is the way to go, where R is either ℕ or ℤ. This avoids the time inefficiencies of using Fin and having to reduce every step, at the cost of potentially building up some very large numbers, although we can provide a function to reduce those.

If R is ℕ then the module has a much shallower dependency graph. The relation can be defined as

data _≋_ : Rel ℕ 0ℓ where
  k*m+a≡b  : ∀ k {a b} → k * m + a ≡ b → a ≋ b
  sk*m+b≡a : ∀ k {a b} → suc k * m + b ≡ a → a ≋ b

Because this has two cases, some of the proofs get a lot messier than if there were only one case.

If R is ℤ then we can define the relation in a single case:

data _≋_ : Rel ℤ 0ℓ where
  k*m+a≡b  : ∀ k {a b} → k * m + a ≡ b → a ≋ b

Or even using Data.Product as

_≋_ : Rel ℤ 0ℓ
x ≋ y = ∃[ k ] k * m + x ≡ y

This makes many proofs far simpler. For example, the proof of transitivity, when using naturals, needs 6 cases. When using integers, it only needs one.

However, this comes at the cost of a much deeper dependency graph, for very little semantic gain.

My personal preference is to use naturals, although I've got further with integers.
I changed my mind, using integers here would be so much easier to implement.

---

Either way, many of the congruence proofs end up as a long series of rearranging formulas, before in a couple of steps applying some equalities provided as arguments. It winds up far simpler using one of the Ring solvers to get through the sludge of +-assocs and *-distribʳ-+s, but I don't think we're actually using the ring solvers for proofs anywhere in stdlib currently.

[JacquesCarette]

The tactic solvers make the dependency graph completely crazy. Simplicity for the developer does not always mean the same for the library as whole. Some tedious proofs are absolutely worth having a sane dependency graph!

[MatthewDaggitt]

If R is ℕ then the module has a much shallower dependency graph. The relation can be defined as
Because this has two cases, some of the proofs get a lot messier than if there were only one case.

Hmm, we could very succinctly define it over the naturals using the difference operator and the divisibility relation:

agda-stdlib/src/Data/Nat/Base.agda

Line 158 in f6685da

∣_-_∣ : ℕ → ℕ → ℕ

agda-stdlib/src/Data/Nat/Divisibility/Core.agda

Line 34 in f6685da

record _∣_ (m n : ℕ) : Set where

data _≋_ : Rel ℕ 0ℓ where
  m∣|a-b|  : ∀ k {a b} → m ∣ | a - b |  → a ≋ b

and we already have a load of useful properties about both of them which should get us a long way to proving various results...
Admittedly, one of them will probably need renaming...

My personal preference is to use naturals, although I've got further with integers.
I changed my mind, using integers here would be so much easier to implement.

To be honest I think we should have modular arithmetic for both naturals and integers. I myself have a use case where I need to work over naturals/fin. The question is can we define modular arithmetic over integers in terms of naturals in order to save us duplicated effort?

The tactic solvers make the dependency graph completely crazy. Simplicity for the developer does not always mean the same for the library as whole. Some tedious proofs are absolutely worth having a sane dependency graph!

Strongly agree with this. The fact that I can't import modulus and division operators over naturals without type-checking half the library and therefore gobbling up 2.5Gb of memory is a source of great frustration!

I usually find that using some well chosen (and often independently useful) lemmas can reduce a lot of the boilerplate. The complete set of three element rearrangement lemmas in Algebra.Properties.CommutativeSemigroup are often very useful!

[Taneb]

If R is ℕ then the module has a much shallower dependency graph. The relation can be defined as
Because this has two cases, some of the proofs get a lot messier than if there were only one case.

Hmm, we could very succinctly define it over the naturals using the difference operator and the divisibility relation:

agda-stdlib/src/Data/Nat/Base.agda

Line 158 in f6685da

∣_-_∣ : ℕ → ℕ → ℕ

agda-stdlib/src/Data/Nat/Divisibility/Core.agda

Line 34 in f6685da

record _∣_ (m n : ℕ) : Set where

data _≋_ : Rel ℕ 0ℓ where
  m∣|a-b|  : ∀ k {a b} → m ∣ | a - b |  → a ≋ b

and we already have a load of useful properties about both of them which should get us a long way to proving various results...
Admittedly, one of them will probably need renaming...

A reason against using |_-_| here is that it's not backed by a primitive operation. After a lot of operations it's possible for the underlying naturals to blow up if we're not frequently normalizing them, or if we're dealing with large numbers from a start, then using this operation could be very slow.

[MatthewDaggitt]

A reason against using |-| here is that it's not backed by a primitive operation.

Eugh, I hate the fact that this consideration leaks into all our design decisions. I really do feel it's a strong code-smell... I still think defining it terms of difference and divisibility really is the way to go in order to avoid duplicating a load of work.

In order to fix the performance later on, then in version 2.0 we could then redefine min and max in terms of _<ᵇ_ and then redefine | m - n | = max(m ∸ n, n ∸ m)...

[Taneb]

Actually, that might not be an issue at all, thinking about it. It'll be pretty rare we actually want to use the value of | a - b |, far more often we'll want only the k outside of the proof term, which'll be erased at runtime without doing much work, with any luck. I guess I should implement it and find it 😅

[MatthewDaggitt]

Great, looking forward to the PR 😄

[Taneb]

I've partially implemented modular arithmetic in terms of Data.Nat.|_-_|.

As I was worried, it does indeed have performance issues. It takes significant time (more than a minute) to typecheck a term of type 1000000001 ≋ 1000000006 % 5, as it has to chip away at both of those numbers linearly to realise that this works out to be 5 ∣ 5.

This isn't an issue for small values, so I'll continue with my implementation.

I've got further with defining modular arithmetic with Data.Integer._-_, although I'm writing out the divisibility property explictly and not using _∣_.

[jamesmckinna]

How/where do we situate PR #2073 in relation to this issue?

[Taneb]

My opinion is that that PR doesn't solve this issue, at least not fully. Doing modular arithmetic with Fin n is very slow, but it's great for some purposes and useful for proving certain properties of other implementations. We still should aim to have a faster implementation.

[JacquesCarette]

I agree with @Taneb . I think the issue is exactly the same as with Peano Nats and blocks-of-binary-digits: one is great for proofs, one is great for efficient computation. You shouldn't choose between them, you should have both.

[jamesmckinna]

I happen also to agree as well. The question in my mind is whether Fin is a suitable basis cf. #2073 at all for implementing ℤ mod n compared to say, using Data.Nat.Bounded of #2257 ... specimen (inefficient!) prototype implementation based on normalisation to bounded Nats, at https://github.com/jamesmckinna/agda-stdlib/blob/modular-arithmetic/src/Data/Integer/Modulo/, taking care to back all the RawSemiring operations with primitives from Data.Nat.Base... UPDATED see #2292 with some rather different approaches to defining the mod n equivalence relation...