decentralize

I’ve been using git for my source code control, and I’m happy I switched to it. I found out recently that my hosting service was burning; apparently something electrical exploded, knocking out a few of webfaction’s servers.

I noticed the problem only when I was trying to push my changes upstream from my machine back to the mothership.

Long pause, no motion.

No problem. I canceled the push, and just continued to work and commit changes to my local machine.

I remember back at my previous workplace how the knockout of our main svn server meant we got to take the day off because we couldn’t get any work done. Of course, I’m not telling the whole story. Not only was that server knocked out, but the whole building in general: we had a power outtage for a few hours. So that somewhat undercuts the story a little; decentralizing our source code server still wouldn’t have saved us on that day.

zelda

I held my sword in front, and approached the village cautiously. I would have to slaughter the terrible Yook monster disguised in one of the hapless villagers’s homes. I pushed the doors open, ready to hack and slash. To my shock, all of the villagers looked exactly the same!

And each had something to say about the other Anouki:

* FoFo said that Gumo was honest.
* Kumu said Mazo or Aroo was lying.
* Dobo said Mazo was honest.
* Gumo said Fofo or Aroo was lying.
* Aroo said Kumu was lying.
* Mazo said that he and Dobo were honest.

How dastardly! Only the Yook would lie to me. And I couldn’t just kill them all and let God sort them out. I had to think about this. So I did what anyone in this circumstance would do: I pulled out Alloy.

abstract sig Boolean {}
one sig True, False extends Boolean {}

abstract sig Anouki {
    truthful: Boolean
}

one sig Fofo, Kumu, Dobo, Gumo, Aroo, Mazo extends Anouki {}

pred whoTellsTruth {
   Fofo.truthful = True implies Gumo.truthful=True
   Kumu.truthful = True implies ((Mazo.truthful=False) or
                                 (Aroo.truthful=False))   

   Dobo.truthful = True implies Mazo.truthful=True
   Gumo.truthful = True implies ((Fofo.truthful=False) or                                                       
                                 (Aroo.truthful=False))
   Aroo.truthful = True implies (Kumu.truthful=False)
   Mazo.truthful = True implies (Mazo.truthful=True and
                                 Dobo.truthful=True)
}

pred onlyOneIsLying {
    one a: Anouki | a.truthful=False
}

run {
    whoTellsTruth
    onlyOneIsLying
}

Ah ha! But as I was about to raise my gleaming blade against the trembling liar, doubt came to my mind: what if there were two of them out there? Or three, or four? I thought: perhaps I should plan this out more carefully before executing my righteous justice. And maybe I should rewrite the model a little more to make it more general: who knows how many villages of liars I might run across?

/* Anouki can be friendly or antagonistic to other Anouki */
sig Anouki {
   supports: set Anouki,
   denies: set Anouki
} {
   /* and it's nonsensical to be both supportive and antagonistic of
      the same Anouki. *
   no (supports & denies)
}

/* A village consists of folks who tell the truth, and symmetrically,
   those who lie.  And we will categorically make every Anouki a
   truthteller or a liar. */
one sig Village {
   truthtellers: set Anouki,
   liars: set Anouki
} {
   no truthtellers & liars
   Anouki = truthtellers + liars
}

fact truthiness {
   all a : Village.truthtellers {
      all a' : a.supports | a' in Village.truthtellers
      all a': a.denies | a' not in Village.truthtellers
   }
}

/* Here's what everyone says about each other */
pred hearsay {
   some disj fofo, kumu, dobo, gumo, aroo, mazo : Anouki {
      fofo.supports = gumo
      fofo.denies = none
      kumu.supports = none
      kumu.denies = mazo or kumu.denies = aroo
      dobo.supports = mazo
      dobo.denies = none
      gumo.supports = none
      gumo.denies = fofo or gumo.denies = aroo
      aroo.supports = none
      aroo.denies = kumu
      mazo.supports = mazo + dobo
      mazo.denies = none
      fofo + kumu + dobo + gumo + aroo + mazo = Anouki
   }
}

pred oneLiar {
    hearsay and #Village.liars = 1
}

pred twoLiars {
   hearsay and #Village.liars = 2
}

run oneLiar for 6
run twoLiars for 6

Hours passed as I played out different scenarios. By this time, the Yook had already run away, but I had a model I was happy with.

consistency

There’s so much work that I have to do, and I’ve realized that one of my personal failings is not necessarily the understanding of hard stuff. Rather, it’s getting the easy stuff even started.

It’s a main point of Better: performance isn’t about the shiny tools: it is more about the “gruntwork”. It’s the mundane task of being consistent, of staying on target, with which I struggle and flounder about like a floppy fish. My failure to do better isn’t for lack of technical tools or skills: what I’m missing is consistency. Adults should have the firmness of mind to do something even if there are no immediate results. But my mind is still mushy and squishy. It has the consistency of oatmeal.

lists 1

One of my research topics may involve Alloy in its role as a language for developing software. The problem is, I don’t know Alloy quite well enough to use it in anger yet. That’s something I must fix.

I need a nice, simple TODO list-keeping application, and so I’ll try modeling it with Alloy. I’ll try to verbalize my thinking in real-time, just to show that software isn’t written in a vacuum, but is revised and re-revised.

These are the sort of things I’d want in a TODO list manager:

  • I should be able to make Items, and going the other way, deleting should be a snap.
  • I should be able to assign items to Tags.
  • I should be able to easily share my TODO lists with other people.

It’s the last requirement that seems interesting to me; I’m not quite sure what I mean by this yet, but it involves some kind of security thing that I’ll think about more in a moment. But let me first start modeling the relationships between the items in my imaginary system.

module lists
sig Person {
    tags: set Tag,
    items: set Item
}
sig Tag {}
sig Public, Private extends Tag {}
sig Item {
    tags: set Tag
}
run {}

I’m thinking of a design like delicious: a Person manages their TODO Items by tagging them. I’ll keep two special tags called Public and Private, which I’ll plan to use to restrict views by other people. Maybe it’s premature to think about this…

Oh, I do want to say that the tags that are associated with a person are the ones used in that person’s items: at the moment, my software model leaves that unconstrained. Let me fix that and revise the definition of a Person.

sig Person {
    tags: set Tag,
    items: set Item
} {
    tags = items.tags
}


At this point, I can ask Alloy: what would a possible situation of my model look like, by executing and showing a model. Here’s one sample visualization that the tool’s giving me.

Ok, but I haven’t yet done anything about privacy yet; I need to model the items that a person might be looking at the moment. Let me extend a Person to also include the items that they’re currently looking at, and also assign an “owner” to each Item.

module lists
sig Person {
    tags: set Tag,
    items: set Item,
    viewing: set Item
} {
    tags = items.tags
}
sig Tag {}
sig Public, Private extends Tag {}
sig Item {
    tags: set Tag,
    owner: one Person
}
run {}

Ok, so Items know who own them, so I should be able to write an expression capturing a notion of privacy. It might not be completely right, but let me see what things look like.

pred respectsPrivacy(p : Person) {
    all i : p.viewing | permit[p, i]
}
pred permit(p : Person, i : Item) {
    p = i.owner || Public in i.tags
}

Cool. Hmm, when I visualize this, though, the diagram’s a little cluttered. And on second thought, I don’t really need to have a Person keep track of their items’s tags explicitely: that’s easily computable as a function.

sig Person {
    items: set Item,
    viewing: set Item
}
// Returns the tags used by a Person
fun personalTags(p : Person) : set Tag {
    p.items.tags
}

Ok, let me visualize again, with a more interesting scenario.

pred show {
    all p : Person | respectsPrivacy[p]
    #Person > 1
    some p : Person | some i : Item {
        permit[p, i] && i.owner != p
    }
}
run show

Wait a minute, the diagram doesn’t look right at all. Why does Person0 see Item0: she doesn’t own it. Ooooh… I didn’t tell my design that a Person‘s items must be owned by them. Ooops. I want to prevent panhandling.

Actually, let me just simplify the model so that this issue doesn’t even happen. Just as I treated the personal tags as a function, I’ll just make a personalItems function to compute whenever I need it.

// Returns a set of the items owned by this person.
fun personalItems(p : Person) : set Item {
    { i : Item | i.owner = p }
}

Here’s my revised model so far.

module lists

sig Person {
    viewing: set Item
} 

// Returns a set of the items owned by this person.
fun personalItems(p : Person) : set Item {
    { i : Item | i.owner = p }
}

// Returns the tags used by a Person
fun personalTags(p : Person) : set Tag {
    p.personalItems.tags
}

sig Tag {}
sig Public, Private extends Tag {}

sig Item {
    tags: set Tag,
    owner: one Person
}

pred respectsPrivacy(p : Person) {
    all i : p.viewing | permit[p, i]
}

pred permit(p : Person, i : Item) {
    p = i.owner || Public in i.tags
}

pred show {
    all p : Person | respectsPrivacy[p]
    #Person > 1
    some p : Person | some i : Item {
        permit[p, i] && i.owner != p
    }
}

assert privateReallyMeansPrivate {
    all i : Item | all p : Person {
        (Private in i.tags && permit[p, i]) implies (i.owner = p)
    }
}

run show
check privateReallyMeansPrivate

I also added an assertion making sure that “private” really means private. There are plenty of counterexamples! It fails because my definition for permit() currently only cares about Public at the moment, and it’s very easy for an Item to get tagged both with the Public and Private tag at once.

This is pretty cool stuff! To be able to talk about this software’s design even without touching a single hashtable or SQL statement is really nice, and I’m already hitting core issues like handling privacy. But since the post is getting a bit long, I’ll stop for now and continue this when I get back to Massachusetts tomorrow.

powers of two


Knuth Check
Originally uploaded by dyoo

One of my friends complained that I didn’t put any interesting images on my blog. So I promised him I’d post something with an image on it. I thought this photo would bring a smile to his face.

Gotta love powers of two.

turing

The thing that struck me about the Turing Test, when I heard about it, was the crazy thought: how do I know that other people are anything like me? If we can’t even judge faithfully between ourselves, how can we judge between humans and computers? For I can do nothing but observe reactions, the effect of my actions on others. I can’t read people’s minds: they could, for all I know, run entirely different mental software. Everyone is, in some sense, a black box.

The act of empathy, then, is a little presumptuous and magical: I trust that we can share an understanding with each other, with the assumption that because I share a similar hardware architecture with you, that there’s a very strong chance that I share the same kinds of thoughts and values too. I think that’s why we put so much emphasis on physical bodies. If someone looks different, I may fear them: they don’t look like me, and so they might be thinking in an entirely different way. We all know the dilemma of the Turing Test deep in our bones, and we cheat a little (or a lot) by using irrelevant physical similarities in our judgements of one another.

I suppose I could be silly and wry and conclude that this is why women are mysterious and terrifying to me.

But I think that there’s something there that deserves more serious thinking.

aliasing renaming

People are often particular about naming. Names still hold special power: we may rationalize that names don’t matter, but there’s something hardcoded in human beings about choosing the right name for a thing. It’s a hard thing to fight.

Programmers are people too, and programmers also keep concerns (sometimes too much) about the right name for a thing. As a concrete example, the word lambda scares off a few people since it’s a foreign word. We might like to be brief and be able to say:


(def (make-adder x)
(fn (y) (+ x y)))

where def and fn are really meant to behave like define and lambda, respectively. One nice thing about Scheme is that it’s plastic enough to absorb a trivial change like this. Here’s a small library for aliasing identifiers:


(module alias mzscheme
;; Practice writing macros that themselves generate macros.

(provide alias)

;; (alias old-keyword new-keyword) SYNTAX
;; Creates a new syntax for new-keyword; any occurrence of new-keyword
;; is replaced with the old-keyword.
(define-syntax (alias stx-1)
(syntax-case stx-1 ()
[(_1 orig new)
(syntax/loc stx-1
(define-syntax (new stx-2)
(syntax-case stx-2 ()
[_2
(identifier? stx-2)
(syntax/loc stx-2
orig)]
[(_2 e (... ...))
(syntax/loc stx-2
(orig e (... ...)))])))])))

Once we have a tool like this, then we can test it out:


(module test-alias mzscheme
(require "alias.ss")
(alias lambda fn)
(alias define def)

(def (make-adder x)
(fn (y) (+ x y))))

That being said, the above example is a silly thing to do. Even in competent hands, this is easy to abuse; in the wrong hands, one can end up with something that belongs to an obfuscation contest.


> (alias alias a)
> (a define d)
> (a if i)
> (d (f x) (i (= x 0) 1 (* x (f (- x 1)))))
> (f 3)
6

Communication between people means that we “come to terms”, and the inherent abuse here is to turn the language into something that no one else can read. In PLT Scheme’s case, the above is especially bad because there’s already an established mechanism for controlled renaming of identifiers as part of PLT Scheme’s module system.


(module test-alias mzscheme
(require (rename mzscheme fn lambda)
(rename mzscheme def define))

(def (make-adder x) (fn (y) (+ x y))))

Still, I thought the macro definition was cute (even if it’s silly), and it’s one of the more direct applications of a “macro-generating macro” that I’ve seen. But maybe this is all just syntax, futzing with words, distracting us from the real work on nailing down the semantics of our thoughts.

logical

I didn’t get this so strongly before, but there’s a correspondence between the language and structures of first-order logic, and the signatures and units of PLT Scheme (as well as the signatures and structures of ML). I guess the analogy is something like: “language::signature as structure::unit.”

As a concrete example, a first-order language might just have equality (=), and a 2-arity P relation. Once we have a language, we can start writing statements in that language. Here are two statements using the language:

  • for all x, y, z: P(x, y) and P(x, z) implies y = z
  • for all x: there exists y: P(x, y)

These two sentences, taken together, are trying to say “P must be a relation that represents a total function”. These sentences don’t have a true or false value without being evaluated in the context of some structure. A structure tells us what domain of thingies (the universe) we’re iterating over when we say “for all” or “there exists”, and also provides a concrete definition for the relations of the language.

There are some structures that might satisfy this, and other structures that don’t. Structures that satisfy the sentences we care about are called “models”. One example of such a model for those two sentences might be the natural numbers (0, 1, 2, …), where the interpretation of P is:

P(x, y) if and only if y = square(x)

But an example of a similar structure that wouldn’t fit the above conditions would be natural numbers under a P that’s not a function relation, like:

P(x, y) if and only if x < y

and so we’d say that this structure isn’t a model of those sentences.

Programmers have an intuitive idea about this: it’s similar to the distinction between “interface” and “implementation”: the language provides the interface, and the structures provide implementations for that language. And when we have an interface, we usually have some implicit idea of how that interface should behave; if we have an interface called Stack, we have an expectation about what it should do. We can make those assumptions explicit by writing contracts or predicates with that interface: the things that satisfy our expectations are good implementations.

Again, to make this concrete, when we’re programming with signatures and units, we first have to specify the things we’re going to be fiddling with. For example, a signature like:


;; A function^ model consists of a universe of elements,
;; and a 2-place predicate P between elements.
(define-signature function^ (universe
P))

gives us a language for talking and using units that implement this signature. For example, to build a unit where P is the squaring relation, we can do this:


(define-unit squaring@
(import)
(export function^)
(define universe (list 0 1 2 3 4 '>4))
(define (P x y)
(cond
[(equal? x '>4)
(equal? y '>4)]
[(> (* x x) 4)
(equal? y '>4)]
[else
(equal? y (* x x))])))

(I’m defining the P function a bit peculiarly since I want the universe of elements to be finite.)

But again, not all implementations of the function^ signature will do the right thing. Here’s a structure that doesn’t satisfy the intent of the function^ signature.


(define-unit less-than@
(import)
(export function^)
(define universe '(1 2 3))
(define (P x y)
(< x y)))

How do we capture intent? We want to be able to catch implementations that don’t do what we expect, and one way is to write code to exercise the units. Here’s one example:


;; function-model?: function@ -> boolean
;; Checks to see if the given unit satisfies what we
;; expect out of functions, that their domain is total
;; and that each element of the domain maps to
;; just one element of the range.
;;
;; In first-order logic:
;; (for all x, y, z: P(x, y) and P(x, z) implies y = z)
;; and
;; (for all x: there exists y: P(x, y))
(define (function-model? model@)
(local ((define-unit-binding a-model@
model@ (import) (export function^))

(define-unit function-tester@
(import function^)
(export)
(and (for-all* (lambda (x y z)
(implies? (and (P x y) (P x z))
(equal? y z)))
universe universe universe)
(for-all* (lambda (x)
(exists? (lambda (y) (P x y))
universe))
universe))))
(invoke-unit
(compound-unit/infer
(import)
(export)
(link a-model@ function-tester@)))))

(There are a few definitions I’ve left out here; see logic-practice.ss for the other definitions.)

Once we have this, we can now check to see if squaring@ and less-than@ satisfy the function-model? predicate.


> (function-model? squaring@)
#t
> (function-model? less-than@)
#f