Basics for a modular arithmetic type in Agda (11 March 2012)

Basics for a modular arithmetic type in Agda

11 March 2012 (programming agda haskell) (8 comments)

In my prevous post, I described a zipper-like representation for modular counters. That representation was well-suited for when your only operations are incrementing and decrementing. However, it'd be really cumbersome to do more complex arithmetics with it.

Then the next week, Peter Diviánszky told me about all the cool stuff that was presented at the latest Agda Implementors' Meeting, among them, the Quotient library. I still remember the time when, as a practice, I tried to implement integers in Agda without looking at the standard library. I came up with something much like the library representation, except mine had a separate constructor for zero (so I had +1+ n and -1- n). I really hated how I had to shift by one at least one of the cases to avoid ending up with two representations of zero. If only there was a way to tell Agda that those two representations actually mean the same thing...

Quotient types promise to do just that: you define a type where the constructors may be redundant so that there may be several values that should have the same semantics, and then you divide it with an equivalence relation so that the new type's values are the equivalence classes. See this example defining integers as pairs of natural numbers such that the pair (x, y) represents x-y.

I wanted to try doing the same for a proper modular integer type, by factoring integers with the equivalence relation x ∼ y ⇔ n ∣ ∣x-y∣. The point is, you take the integers, define this relation, then prove that it is indeed an equivalence (i.e. it is reflexive, symmetric and transitive), in other words, you create a setoid; then you use the Quotient type constructor to create your set-of-equivalence-classes type. After that's done, you can define functions over this quotient type by defining them over representations, and proving well-definedness, i.e. that the function maps equivalent representations to the same result.

This last step can be needlessly cumbersome when defining either non-unary functions or endomorphisms, so first of all I created a small library that makes it easier to define unary and binary operators over a quotient type. For example, to define a binary operator, all you need is a binary operator on the representation set, and a proof that the operator preserves the equivalence, thereby being agnostic to the choice of representant on both arguments:

    lift₂ : (f : Op₂ A₀) → f Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ → Op₂ (Quotient A)

So after writing loads and loads and loads of arithmetic proofs on divisibility of absolute values, like n ∣ ∣x∣ ∧ n ∣ ∣y∣ ⇒ n ∣ ∣x + y∣, I was finally ready to define modular addition:

Mod₀ : ℕ → Setoid _ _
Mod₀ n = {!!}

Mod : ℕ → Set
Mod n = Quotient (Mod₀ n)

plus : ∀ {n} → Mod n → Mod n → Mod n
plus {n} = lift₂ _+_ proof
  where
  proof : ∀ {x y t u} → n ∣ ∣x - y∣ → n ∣ ∣t - u∣ → n ∣ ∣(x + t) - (y + u)∣
  proof = {!!}

Of course, the meat of the work was in actually defining Mod₀ and proof above. But after that, we can get back our old increment/decrement functions as very simple and straightforward definitions:

_+1 : ∀ {n} → Mod n → Mod n
_+1 = plus [ + 1 ]

_-1 : ∀ {n} → Mod n → Mod n
_-1 = plus [ - (+ 1) ]

And proving that _+1 and _-1 are inverses of each other comes down to the very simple arithmetic proof (on vanilla integers!) that

pred-suc : ∀ x → ℤpred (ℤsuc x) ≡ x

Of course, much more properties need to be proven. The end goal of this project should be to prove that Mod n is a commutative ring; a much more ambitious project would be proving that Mod p is a field if p is prime. Unfortunately, on my machine Agda takes more than two minutes just to display the goal and context in the following hole:

plus-comm : ∀ {n} → (x y : Mod n) → plus x y ≡ plus y x
plus-comm {n} x y = {!!}

so this is a problem I'll have to find a workaround for before going on. But at least I have my counters, so I can at least get back to my original goal and work on the register machine semantics. Expect the next post to be about that.

You can browse the full source code here, and track it on GitHub.

« Static analysis with Applicatives

All entries

Mod-N counters in Agda »

pandawill 2013-04-23 04:53:20

z The Pandawill an online store, operates various brands,a variety of a variety of large-screen smart phones and tablet PCs,and the necessities of life.ONDA V711

the best china wholesale 2013-04-23 05:25:05

Y Tablets, smart phones, online sales, the cheapest electronic wholesale market, China - pandawill.comCUBE U18GT Elite

ルイ・ヴィトン (http://www.louisvuitonshopjp.com) 2013-04-28 11:03:57

dafadga 2013-04-29 07:16:49

K The gradual improvement of living standards, demand for mobile phones is not limited to communications, is the pursuit of the appearance of the phone and entertainment properties, then in the end what kind of phone is able to meet all these requirements? Pandawill special launch lifestylish digital shopping guide series, holding a purse you accurate shot, to buy their favorite products. cheap mobile phones

opcom 2009 (http://www.fireobd.de/ford-mazda-gm-opel-chrysler/633-opcom-op-com-2009-v-can-obd2-opel.html) 2013-05-03 04:39:54

Cruzeiro. PSV scoutte de jonge spits en in Eindhoven ontpopte hij zich tot goalgetter. Na twee seizoen vertrok hij naar FC Barcelona. Ook daar werd hij topscoorder. Na één seizoen vertrok hij naar Inter Milan. In Italië werd hij al snel 'Il Fenomeno' genoemd. AUTO

Adidas Jeremy Scott 2013-05-13 10:22:02

Prefabricated car port packages can be found in a number colors, styles and also expenditures. You possibly can purchase a fundamental 16 by thirty by 8-10 guide to get below 5K, and the greater 40' properties can be up to twenty : 50K+. In comparison with standard structure, these are generally very practical options. A number prefabricated car port packages don't are the car port entrances, walk-through entrances, masonry anchors, and also microsoft windows, although Femmes Maillot Cyclisme are available for order on their own. Most often, it truly is best if you're able to put together your current guide using a bare cement piece. This contains probably the most protected groundwork, although isn't really this exclusively alternative. You could build above natural area or perhaps little. A new bare cement groundwork includes obvious gains and it is is recommended. Upon having the foundation commited to memory you possibly can start structure and also assemblage. Seeing that usually, just make sure evaluate area creating rules to ensure most of can be properly before even thinking about. However these jerseys are in the beginning made for bike riders, a number of other sports lovers are utilising these jerseys seeing that effectively. Furthermore, these jerseys are possibly applied not merely for virtually any particular activities occurrences, although throughout just about any out of doors task way too. Cycling jerseys can be additionally termed as cycle jerseys. These are generally specially generated for people who carry out plenty of bicycling. In fact, cycling jerseys may not be including simply just about any common jerseys, since these jerseys are created specifically long within the returning. This Maillot Cycliste can be in fact very handy for bike riders since long-back style and design with cycling jerseys is good for this cyclist's reduce back to continue included seeing that he bends within the deal with club with this cycle. At the same time, specially made jerseys ordinarily have storage openings located with the back. Openings for cycling jerseys are smartly located with the back mainly because this maintains stuff by spilling, seeing that what exactly is probably for you to take place in the event openings are usually in top.

http://www.onfiredate.com/member/blog_post_view.php?postId=51169 http://bbs.ntc-world.com/Blog.asp?BlogUserName=bibi6612&menu=ShowBlog&BlogID=5919

louis vuitton (http://www.louisvuitonshopjp.com) 2013-05-14 11:54:56

ak810 mouse 2013-05-16 03:32:10

H I just wanted to comment on your blog and say I really enjoyed reading your blog here. It was very informative and I also digg the way you write! Keep it up and I'll be back soon to find out more mate.ak810 mouse

Contents

Blog tags