“Elements of Programming” and the ↦ symbol
Posted by Ciaran McCreesh on May 19, 2008
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 λ!
Justin said
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.
anon said
“maps to”. See the TeX, LaTeX, or AMSTeX mnemonics; they often will lead you in the correct direction.
Mike Lundy said
It’s also a bit clumsy, but I read it as “implies”.
http://en.wikipedia.org/wiki/Logical_implication
Jayferd said
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}.
Paul McJones said
anon, Jayferd and Ciaran got it right; we’ll \mapsto to the notation appendix.