He's not dead, he's resting

“Elements of Programming” and the ↦ symbol

I’m working my way through the draft of Elements of Programming. And I have a gripe. A small gripe, admittedly, but a gripe non-the-less.

The book uses a lot of symbols. I don’t have a problem with that, and in general it’s more readable that way than spelling everything out. Most of the symbols are defined in an Appendix as well, which is also good. But there is one that is not: the ↦ symbol (or in ascii art, |-->). Here’s an example of its use, taken from page 123:

abstraction(Op : BinaryOperation)
associative : Op → bool
    op ↦ (∀a, b, c ∈ Domain(op)) op(a, op(b, c)) = op(op(a, b), c)

Whilst the meaning is obvious, I can’t work out how the symbol is supposed to be read. I can’t find that symbol used in reference literature either. The best I can come up with is “Is such that”, but that’s rather clumsy…

Update: Looks like it’s “maps to”. Essentially the associative : line defines the type signature for the associative property, and the last line defines it in terms of a lambda. Looks like mathematicians came up with yet another way of defining functions that I managed to miss. Give me back my λ!


5 responses to ““Elements of Programming” and the ↦ symbol

  1. Justin May 19, 2008 at 10:56 pm

    That symbol speaks of a type of function called an injective relation. Check out formal specification using Zed or the book the essence of zed. The functions mapping can only be on 1 to 1.

  2. anon May 19, 2008 at 11:27 pm

    “maps to”. See the TeX, LaTeX, or AMSTeX mnemonics; they often will lead you in the correct direction.

  3. Mike Lundy May 19, 2008 at 11:31 pm

    It’s also a bit clumsy, but I read it as “implies”.

  4. Jayferd May 19, 2008 at 11:47 pm

    That’s straight from theoretical math. You define a function using f:A\to B, and then you say x \mapsto ${EXPRESSION}, meaning \forall x \in A, f(x) = ${EXPRESSION}.

  5. Paul McJones June 7, 2008 at 3:53 am

    anon, Jayferd and Ciaran got it right; we’ll \mapsto to the notation appendix.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s