## Mod-N counters in Agda

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 p1 and p2 omitted here for brevity):

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

_-1 : ∀ {n} → Counter n → Counter n
cut zero    j -1 = subst Counter (sym p1) (cut j zero)
cut (suc i) j -1 = subst Counter (sym p2) (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        p1
(cut  i  (suc j)  i+j+2=n)  +1  = cut  (suc i)  j        p2

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

+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:

### 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 :)

### Kyle Leon (http://www.japmeqera.com/author/dionnedee/) 2013-08-20 11:31:44

Nice postings here to be get information share more posts like this to giving info to peoples.

### Best Customized Fat Loss Exercises (http://fatlosstips.mixxt.at/networks/blog/post.Admin:1) 2013-08-23 07:48:01

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.

### nike sko free run (http://www.dkfreesko3.com) 2013-08-25 04:23:21

This is very educational content and written well for a change. It's nice to see that some people still understand how to write a quality post.!

### http://www.jp-glassses.com (http://www.jp-glassses.com) 2013-08-28 03:45:22

<body>アディダスで2009年と2010年間の低迷成長の勢いは、確かに大量にドラッグ在庫。在庫一掃のためにタイムリーに、アクティブにキャッシュフロー、ディーラーらに製品を大きく割引をしただけでなく、移動アディダスのハイエンドブランドイメージ、そして、多くの損失をもたらし、店舗の状態、「双負け」局面、会社とディーラー関係緊張度。在庫になった解消危機全公司の共同任務が、主に変動者は、元々はアディダスヨーロッパ仕事、2007年にアディダス大中華圏の博済勇。この名法国籍マネージャーは在庫問題の最も深い2009年ごとの家を訪ねてみディーラー、図解開関係の真結び。いくつかの表層問題がすぐに見つかり、例えば、古い在庫出清ないからこそ、ディーラーたくない購入新品、こうして、販売末端ブースト力不足、オーバースットク、jp-glassses.com 悪循環を形成。安売り見た目は唯一の道が、 博済勇希望実施てすべてより整然としている。彼が設立されたEPR制度、厳しく定めにじっとしているだけ30日後、製品が8がけで売る。90日後、割引に変えることができる7折れ。もしどうしても出清できない、アディダスはこれらの製品を買ってきて、自分の工場の割引の店の販売。事実上、危機に見舞われて困っているナイキ期間も在庫は、開工場の割引の店の形式で消化在庫。そのため、アディダスも多くの工場の割引の店をオープンして、既存の総数48家。もっと重要なのは一挙に、博済勇ヨーロッパ市場導入からかつて彼は多くの利益を得る方法：会社内で売る商品、ディーラーと呼ばれる「Sell-in」で、ディーラーが小売店の担当で、真に売却されるお客様の品には、定義は「Sell-through」。スポーツ用品業界、ディーラーの注文や製品発売の時間差8前後から9ヶ月、この会をディーラーに間違って市場の見通しのリスク評価。過去には、すべてのブランド「商都Sell-in」の販売の任務の完成が宣告大吉、一体どれだけの「売れてSell-through」やシリーズ全ディーラーから滞货リスクを引き受ける。 </body>

### fdqw 2013-09-09 04:54:43

I just want to tell you that I am just very new to blogging and actually enjoyed this blog. Likely I'm going to bookmark your site . JIAYU G3S

### Battery Pack Manufacturer (http://www.ejbattery.com) 2013-09-10 05:35:00

NiMH,NICD,LITHIUM,LIPO,LiFePO4 Battery,Battery Pack Manufacturer-E&J Technology

### Kyle Leon Customized Fat Loss (http://productrevieu.wordpress.com/2013/09/06/kyle-leon-customized-fat-loss-2/) 2013-09-11 08:16:12

"Classic old toad" comment on my style.

Then offended, explain that the way your head above water, stroking water and the knees are too far from each other most of the floating population. "It is a somewhat antiquated method we learned as children. Nadar poor technique is obviously better than not anything at all, but for the health you do nothing.

### Siverek (http://www.sivereksonhaber.com) 2013-09-13 23:56:54

I’m very intrigued by your postings, thanks for sharing them when camping.