# Blag

He's not dead, he's resting

## “Elements of Programming” and the ↦ symbol

May 19, 2008

Posted by on 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:

Definitionabstraction(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 λ!

Advertisements

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.

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

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

http://en.wikipedia.org/wiki/Logical_implication

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}.

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