“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:
Definition
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 λ!
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.
Comment by Justin — May 19, 2008 @ 10:56 pm
“maps to”. See the TeX, LaTeX, or AMSTeX mnemonics; they often will lead you in the correct direction.
Comment by anon — May 19, 2008 @ 11:27 pm
It’s also a bit clumsy, but I read it as “implies”.
http://en.wikipedia.org/wiki/Logical_implication
Comment by Mike Lundy — May 19, 2008 @ 11:31 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}.
Comment by Jayferd — May 19, 2008 @ 11:47 pm
anon, Jayferd and Ciaran got it right; we’ll \mapsto to the notation appendix.
Comment by Paul McJones — June 7, 2008 @ 3:53 am