Mod-N counters in Agda (19 February 2012)

Mod-N counters in Agda

19 February 2012 (programming agda correctness haskell) (16 comments)

First of all, before I start on the actual blog post, let me put this in context. I rembember a couple of years ago when I developed an interest in functional programming languages, and Haskell in particular. There was a phase when I was able to use Haskell to solve problems in the small. I understood most of the basics of pure functional programming; then there were things I regarded as magic; and of course there was a lot of things I didn't even know that I didn't know about. But none of it did I grok.

I feel like I'm starting to get to the same level with Agda now. So this is going to be one of those "look at this cool thing I made" posts where the actual result is probably going to be trivial for actual experts of the field; but it's an important milestone for my own understanding of the subject.

I wanted to play around with simple but Turing-complete languages, and I started implementing an interpreter for a counter machine. More on that in a later post; this present post describes just the representation of register values. In the model that I implemented, values of registers are byte counters, meaning they have 256 different values, and two operations +1 and -1 that the inverses of each other. Incrementing/decrementing should roll over: 255 +1 = 0 and 0 -1 = 255.

My first approach was to just use the Fin type from the standard library. However, the structure of Fin is nothing like the structure imposed by +1 and -1, so while one can define these functions, proving properties like -1 ∘ +1 = id is unwieldy and the resulting proofs are not easy to reuse in other proofs.

So I eventually settlend on a zipper-like representation. The intuition behind it is to think of the possible values of Counter (suc n) as points on the discrete number line from 0 to n. You have a vector of numbers behind you and a vector of numbers in front of you; with the invariant that the length of the two vectors is always n. For example, if n=3, you can be at positions ([], [1, 2, 3]), ([1], [2, 3]), ([1, 2], [3]) and ([1, 2, 3], []). To increase the value, just move the leftmost item of the second vector to the end of the first one; rollover is handled by the simple syntactic rule (xs, []) ↦ ([], xs).

Of course, there is no point in actually storing the numbers, so we can use vectors of units instead; but why store those if we only care about their length?

So the eventual representation I came up with was:

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc i + j)

I was hoping that I could write +1 and -1 like this:

_+1 : ∀ {n} → Counter n → Counter n
cut i zero    +1 = cut zero i
cut i (suc j) +1 = cut (suc i) j

_-1 : ∀ {n} → Counter n → Counter n
cut zero    j -1 = cut j zero
cut (suc i) j -1 = cut i (suc j)

But life with indexed types is not that simple: for example, in the first case, the left-hand side has, by definition, type Counter (suc i + 0) and the right hand Counter (suc 0 + i). So we also need to inject proofs that the types actually match (with the actual proofs p₁ and p₂ omitted here for brevity):

_+1 : ∀ {n} → Counter n → Counter n
cut i zero    +1 = subst Counter p₁ (cut zero i)
cut i (suc j) +1 = subst Counter p₂ (cut (suc i) j)

_-1 : ∀ {n} → Counter n → Counter n
cut zero    j -1 = subst Counter (sym p₁) (cut j zero)
cut (suc i) j -1 = subst Counter (sym p₂) (cut i (suc j))

However, this leads to more problems further down the line: you can't get rid of that subst later on, thus forcing you to use heterogenous equality for the rest of your proofs. While I was able to prove the property

+1-1 : ∀ {n} → {k : Counter n} → k +1 -1 ≡ k

using heterogenous equality, it broke down on me further down the road when actually trying to use these counters in the semantics of my register machines.

So instead of storing the size of the counter in a type index, I used a type parameter. This requires carrying around an explicit proof that the sizes match up, but we needed those proofs for the indexed case in the subst calls anyway, and then invoke proof irrelevance in the proof of +1-1:

data Counter (n : ℕ) : Set where
  cut : (i j : ℕ) → (i+j+1=n : suc (i + j) ≡ n) → Counter n

_+1 : ∀ {n} → Counter n → Counter n
(cut  i  zero     i+1=n)    +1  = cut  zero     i        p₁
(cut  i  (suc j)  i+j+2=n)  +1  = cut  (suc i)  j        p₂

_-1 : ∀ {n} → Counter n → Counter n
(cut  zero     j  j+1=n)    -1  = cut  j        zero     p₃
(cut  (suc i)  j  i+j+2=n)  -1  = cut  i        (suc j)  p₄

+1-1 : ∀ {n} → {k : Counter n} → k +1 -1 ≡ k
+1-1  {k = cut  i        zero     _}  = cong  (cut  i  zero)     (proof-irrelevance _ _)
+1-1  {k = cut  i        (suc j)  _}  = cong  (cut  i  (suc j))  (proof-irrelevance _ _)

-1+1 : ∀ {n} → {k : Counter n} → k -1 +1 ≡ k
-1+1  {k = cut  zero     j        _}  = cong  (cut  zero     j)  (proof-irrelevance _ _)
-1+1  {k = cut  (suc i)  j        _}  = cong  (cut  (suc i)  j)  (proof-irrelevance _ _)

With this approach, lifting these theorems to be about whole states, not just individual register values, is a breeze, e.g.:

+1-1Σ : ∀ {Σ x y} → (getVar y ∘ decVar x ∘ incVar x) Σ ≡ getVar y Σ
+1-1Σ {x = x} {y = y} with toℕ x ≟ toℕ y
... | yes x=y = +1-1
... | no x≠y = refl

But this is takes us to my actual application for these counters; and that will be the topic of a next post.

Here are the complete sources of the two counter implementations:

« Basics for a modular arithmetic type in Agda

All entries

How I learned about Java's lack of type erasure the hard way »

danr 2012-02-20 11:01:58

Ah, this is a very nice solution to get rid of subst everywhere in your proofs. I like it!

Dan Peebles 2012-02-21 04:42:49

You can use the irrelevance feature (on the equality proof in your Counter) to make the proofs even simpler, and just use refl for them :) I've done a counter like this using Fin, and you're right, it gets quite ugly. Using Conor McBride's embMax view on Fins makes it a bit more pleasant, though. Have you seen that?

Dan Peebles 2012-02-21 04:51:55

I like your representation though! I'm going to fool around with it a bit and see where I get :)

Dan Peebles 2012-02-21 17:35:24

It seems to work very nicely! Here's what I came up with: http://hpaste.org/64114

Also, have you seen the bitvector project that glguy and I worked on a while back? It gives you this sort of "machine word"-like numbers with wrapping, in a more efficient representation than unary. You can find it at https://github.com/copumpkin/bitvector but the proofs in it are a little icky (we hadn't figured out EqReasoning at the time, so used big chains of rewrites), so if you're aiming for simplicity it might not be what you want. On the upside, we have pretty much all the algebraic structures and (decidable) orderings you could imagine wanting :)

cactus 2012-02-22 14:35:22

Dan,

Sorry I haven't had time to look into your code in detail yet, but one question that popped into my mind after a superficial read-through is: what is the benefit of making Counter a record?

Dan Peebles 2012-02-22 22:10:56

Hi cactus,

I normally make anything that can be a record into a record, mostly because it simplifies some kinds of annoying proofs. Generally, if I have a one-constructor data type without index refinement, I'll make it into a record. This tells Agda that it doesn't need to wait for me to pattern match on the one constructor to continue reducing my terms.

Sometimes, that isn't what you want: for an example, see the difference between ⊤ (Data.Unit) and Unit (Data.Unit.Core) in the standard library. The distinction between the two unit types gives us some pretty fine-grained control over what reduces and what doesn't, which is exactly what the new inspect idiom (Relation.Binary.PropositionalEquality) needs to avoid the issues that made the old one so annoying to use.

But basically, I didn't have a good reason to make Counter in particular a record, other than wanting to pre-emptively avoid any annoyances in future proofs :)

pandawill 2013-04-23 05:00:31

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.Lenovo Phone

the best china wholesale 2013-04-23 05:29:56

Y Tablets, smart phones, online sales, the cheapest electronic wholesale market, China - pandawill.comUltraFire C1

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

adfaf 2013-04-29 07:21:06

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. Freelander PD10 Typhoon

Oakley Sunglasses Sale (http://www.oakleycanadasale.net) 2013-05-06 11:20:53

Oakley Romeo 2.0 Sunglasses ready banana.

superior prototype 2013-05-08 09:56:32

Some of the techniques are including CNC machining, vacuum casting, rapid tooling, and mass production injection tooling in house. Besides it there are some other methods of prototyping.Silicone mold and vacuum casting manufacturer

Adidas Jeremy Scott 2013-05-13 10:31:38

Prefabricated shed kits come in countless hues, measurements and costs. You may get a primary 14 x 20 x 8 kit for beneath 5K, as well as more substantial 40' structures is usually as much as 20 - 50K+. In comparison with traditional development, these are really cost effective solutions. Countless prefabricated shed kits do not add the shed doors, walk-through opportunities, masonry anchors, and your windows program, nevertheless Maillot Velo are offered regarding purchase independently. Individual bankruptcy, it's finest if you can assemble ones kit on a concrete piece. This particular allows for by far the most risk-free foundation, nevertheless just isn't the actual only solution. You could potentially assemble through live territory or small. Some sort of concrete basis features noticeable features and is important. After getting the inspiration ready to go you may start off layout as well as putting your unit together. While always, just be sure to check community constructing unique codes to make sure just about all is usually well before you begin. Though these kind of jerseys usually are actually designed for bike riders, all kinds of other sporting activities enthusiasts are using these kind of jerseys while well. Additionally, these kind of jerseys usually are actually employed not only for almost any certain sports incidents, nevertheless with any backyard pastime far too. Riding a bike jerseys will also be additionally referred to as street bike jerseys. These are in particular made for folks that can a lot of biking. In reality, riding a bike jerseys are not just like just almost any ordinary jerseys, given that these kind of jerseys usually are created specifically extended inside the back. This particular Maillot Cyclisme 2013 is usually without a doubt really sensible regarding bike riders since the long-back layout of riding a bike jerseys is for the actual cyclist's cheaper returning to stay insured while he or she bends over the handle standard of the street bike. Additionally, exclusively fashioned jerseys usually have storage space pockets to be found at the back again. Pockets regarding riding a bike jerseys usually are deliberately to be found at the back again simply because this particular keeps issues coming from spilling, while exactly what is most likely to help come about in the event that pockets are in front.

http://www.kalbimbos.com/member/blog_post_view.php?postId=50407 http://www.bd-classifieds.com/member/blog_post_view.php?postId=2652

coach store online (http://www.chanluustore.org/) 2013-05-14 06:07:11

For some of us, the only chan luu bracelet we have. If that http://www.chanluustore.org/ familiar, it will be no problem staring this Marc Jacobs Sale in the face as you down your booze.Steve Madden's popular "MARC JACOBS" ankle strap heels are $79.95 at stevemadden.com.Throughout the http://www.marcjacobssale.co.uk Marc Jacobs UK she wears tassel cheap coach purses and jewels with conch pearls, and at parties her flapper cheap coach purses is always completed with "The Marc By Marc Jacobs Clutch" - a headdress of diamonds and cultured marc jacobs handbdags, while daisy designed http://www.usitccoachpurses.net coach outlet store rings sit on her fingers.This is a http://www.marcjacobsbagsstore.com marc jacobs bags every woman raves about and I'm definitely an advocate of it. I use it to hydrate and protect my cheap coach purses as well as a hand marc by marc jacobs or to ease any bit of dry skin.chan luu may suffer accusations of nepotism from some quarters, but as we perch on a display case of the cheap coach purses store's stock, while random coach purses outlet pulsates in the background, I am afforded a close-up view of her http://www.voguecoachoutlet.com coach outlet online.With Mother's Day on Sunday, it's time to take a look back at our style-trailblazing cheap coach purses, past and present.

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

UltraFire WF-501A 2013-05-16 03:37:25

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.UltraFire WF-501A

Contents

Blog tags