Formalism tutorial

08 Oct 2013

This post was imported from blogspot.

Have you ever seen notation like this in a programming language paper? I have. And it's completely frustrating to encounter notation like this, because there is no obvious way to find out what it means. The paper itself will not give a name to the notation they are using, and there is no way to Google for the symbols that are used. Even if you can find one of these symbols in Character Map or whatever--and it probably won't be listed under standard fonts--Google responds with something like

Your search - ∏ - did not match any documents.

Luckily, I stumbled upon this page which briefly explains, and gives names for, these notations. For example: "|-" means "entails", "<:" is a subtype relation, ⊥ is "bottom", its inverse Τ is "top", Γ is "context", and the long horizontal line is sort of an if-then statement:

"if everything above the bar (the premises) is true, then the thing below the bar (the conclusion) is true"

Excellent, this will be very helpful when I encounter another one of these papers. I wish computer scientists understood that their notation is far from universally known and that, without a "legend" or informative URL, mere computer engineers like me not only cannot understand the notation, but cannot learn about it either.

Update: here's a more detailed introduction to Programming Language Theory.