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

It's used as a way of specifying the semantics of a programming language through a binary relation on programs. These kinds of semantics are called small-step semantics. Within small-step semantics, there are approaches include reduction semantics and structural operational semantics. If the program is augmented first to a "configuration" that includes extra components like environments and stores, and the relation is on these configurations instead of just plain program terms, then it's called an abstract machine semantics.

Note: Sometimes you define multiple relations and build up more complicated relations out of them, so you have different arrows.

There are other kinds of operational semantics (eg big-step semantics) and there are other kinds of semantics besides operational semantics.

• 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