Contents

Blog tags RSS

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


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

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>

Giuseppe Zanotti online 2013-09-02 08:58:57

<strong>replica christian louboutin heels </strong>book by Robert Irwin could be a noteworthy one together with a great source for the understanding of seual pleasure and even seual performance. <strong>christian louboutin heels</strong> When you're willing to eperience remarkable and immediate transformation when considering your se <strong>christian louboutin knockoffs</strong> life, read Seual Skills for your<strong>christian louboutin glitter pumps</strong> now and harness its potential! What makes this book completely different from secular se books and Christian se books?<strong>christian louboutin replica </strong>This book is much like the median Women usually really wants to get noticed by means of men. The more ladies is assured as well as self-assured, the greater that draws a person. These shoes offers you feeling of remaining by <strong>christian louboutin pumps</strong> far the most assured person space. Every woman really wants to generate the feet appearance lengthier, leaner which is the reason it truly is their<strong>Christian Louboutin Asteroid</strong> particular prolonged beloved dream to accumulate some Giuseppe Zanotti shoes reproductions. Giuseppe Zanotti fake pictures are usually remarkably beautiful <strong>Christian Louboutin Dafsling Glittery Leather Slingback Platform</strong> plus its incredibly possible to come across your individual two of terrific <strong>Christian Louboutin Isolde 20ans Specchio Laminato Black</strong> stilettos within the reasonably priced selling price.<strong>fake christian louboutin </strong>People identically appear to be an original exclusive layouts. Using these high ending shoes and boots can make you seem like hundreds of cash. <strong>replica louboutin shoes</strong> fakes usually are legitimate stilettos from the vogue of high heel dress shoes<strong>christian louboutin stores</strong> . These types of <strong>christian louboutin spiked heels</strong> is probably not <strong>Christian Louboutin Highness 160mm Aurora Colorful Pumps</strong> actual intercourse, but closest circumstances to the main ones. <strong>http://www.christian-louboutinsreplicas.com</strong> The renowned shoes and boots cost thousands, that many people are unable<strong>replica christian louboutin pumps</strong> to definitely have the funds for. But these replications are certainly affordable and they also price tag solely big money to the the same boot. A traditional set of <strong>christian louboutin daffodil pumps</strong> is involving high quality although the elevated amount isn&rsquo;t <strong>replica louboutin pumps</strong> going to ensure it is functional for many individuals to purchase them. Whenever you acquire the boots and shoes, <strong>christian louboutin narcissus pumps</strong> you make payment for for just a fine quality but you are also spending money on the marketing and advertising with his company, for the let with the shop you<strong>christian louboutin studded pumps</strong> pay for and also other lots of charges. Being style conscious tends to make outlet very difficult to acquire all of the affluent plus known ways. When you are taking a step <strong>christian louboutin studded pumps</strong> from your home where ever you are going, you want to make yourself stunning along with irresistible to males. To spend right after <strong>fake gianmarco lorenzi</strong> famed-fashions is <strong>replica christian louboutin</strong> difficult. reproductions can make it easier for you. To produce your self lovely in an affordable means, fakes will give you the most perfect items. Once you put them on, you will recognize that <strong>giuseppe zanotti shoes</strong> the way men give you <strong>Giuseppe Zanotti Sneakers online</strong> credit, how they talk to you may absolutely switch. This footwear possess the great charm so that you can have a person using newly found self-confidence. Your feelings, ones character, ones sexiness are going to be transformed whenever you fit one of them as part of your ft. <strong>giuseppe zanotti</strong> This sense of view would have been to lessen the anxiety that females experience into their daily lives. They created this by the ladies shape and the thinking was completely right. <strong>giuseppe zanotti outlet</strong> That feeling of perspective likewise offers a whole new hint inside the ladies take on life. uk provide you with plenty of confidence to rework all by yourself in how you would like to always be. In this<strong>Giuseppe Zanotti Sneakers</strong> fashionable as well as fast paced lifestyle<strong>gianmarco lorenzi pumps</strong> , we could however find a very good strategy to become the most appealing, sometimes by way of <strong>Giuseppe Zanotti Sneakers</strong> techniques. Do not for that mark-up, most of these reproductions are <strong>Giuseppe Zanotti Wedge Sneakers</strong> definitely the wisest route to take. backward and forward books. Incorporating what secular books teaches the technical, however not to begin se <strong>Giuseppe Zanotti Sneakers outlet</strong> concerning physical pleasure together with the true term se as what God planned instead of lacking the technical aspects. In simple words, what Robert Irwin write would be the book the bridges the space between the secular and Christian se books. Based on it,<strong>cheap gianmarco lorenzi</strong> can fully see the true concise explaination of se. Utilized, it is actually reliable advice that book is a really noteworthy one in discussing mens Giuseppe Zanotti replica the condition of se.<strong>Giuseppe Zanotti sale</strong> So, if you're wanting to alter your views regarding what se is, you'll want to read Robert Irwins Seual Skills to your Christian Husband book and do it. Eperience the particular concept se you won't amazed regarding <strong>Giuseppe Zanotti online</strong> how it'll change you! The Seual Skills for any<strong>gianmarco lorenzi gregory shoes</strong> is built to all Christian perhaps even<strong>gianmarco lorenzi</strong> will develop the <strong>gianmarco lorenzi knockoffs</strong> successful lead inside their seual relationship. Neoprene ambiance without worrying about the excess weight and even<strong>gianmarco lorenzi boots</strong> fast food.Gulf of mexico of Meico going provides obtained despite the presence of would-be economic<strong>gianmarco lorenzi shoes</strong> decline on the horizon. In the event that progress is certainly<strong>gianmarco lorenzi replica</strong> and shoes by just clothing <strong>gianmarco lorenzi heels</strong> superior to epected or <strong>gianmarco lorenzi crystal pumps</strong> if epectations with regards to potential is usually nicer, burrowing may perhaps pick-up a bit. At the moment tastes legal contracts originate from <strong>Giuseppe Zanotti Sneakers </strong> shoppers.<strong>gianmarco lorenzi sandals</strong> I imagined wearing the Pumps Sale gold platform pumps with gray-heathered tights regardless of the<strong>christian louboutin daffodile</strong> fashionista naysayers that balk at the mere idea of combining legwear with peep-toe pumps.all ages strutting surrounding the urban center through purple soled shoes or boots. For many people, experiencing green soled shoes or boots implies <strong>giuseppe zanotti</strong> absolutely nothing.

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

LiFePO4 battery

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.