# Principles of Programming Languages: Understanding Judgements

I am taking a principles of programming languages class right now and am trying to understand the following judgement form.

n' = -toNumber(v)
------------------
-v --> n'


(Sorry, I can't post pictures yet. And Stack doesn't take LaTeX.) I think it means "n' = -v implies that -v maps to n' " or something along those lines. I guess I really just don't know what the --> means. In math it can either mean "maps to" or "implies" and "maps to" just made more sense.

• also, I didn't really know what else to tag the post with "judgements" and "judgement-form" don't exist. – steveclark Oct 19 '14 at 22:49

The --> is the relation that the judgement rules are defining. It's usually pronounced "steps to" or "reduces to". You can think of this relation as the analogue of "showing your work" in algebra:
(1 + 2) * 3 --> 3 * 3 --> 9
• Okay, so the relation -v --> n' is saying "-v steps to n prime"? With only one step what is a better way of saying it? Perhaps "-v = n prime"? – steveclark Oct 20 '14 at 18:47
• An equivalence relation = relation can be defined as the reflexive-symmetric-transitive closure of -->. But they're different things. There are also big-step relations, usually written with a double down arrow, that are also defined using judgement rules. Also a different thing, although if you have both a small-step and big-step semantics for a language, you might want to prove them equivalent. – Ryan Culpepper Oct 20 '14 at 20:15