Laypersons who are not trained in the relevant formal notation may sometimes feel lost when trying to read academic papers on computer science.
This gist is intended to be a short introductory "cheat sheet" for some of the symbols we may encounter in such papers, to help make the work more accessible to a broader audience, particularly those working in the software industry looking to gain a deeper understanding into formal computer science.
In addition to this introductory glossary of symbols, it may also be helpful to reference this glossary of terms so that the formal usage of certain words can be known to the reader.
One can also read a great bit more detail on this topic in The Formal Semantics of Programming Languages, a text introducing a lot of details in formal notation.
The sections below are delineated by the branch of mathematics / computer science where the symbols are commonly used, and the introduction to each section briefly describes the primary relevance to software and also gives resources for further reading if available.
These notes are from my personal reference - they are incomplete and subject to expansion and revision over time. Suggestions and feedback are welcome in the comments below.
TODO: Intro here
A or B - the logical disjunction (the overall predicate is true if and only if eiher A or B are true)
A and B - the logical conjunction (the overall predicate is true if and only if both A and B are true)
not A - the logical complement or negation (the predicate is true if and only if A is not true)
A entails/proves B, or we may say B follows from A (if predicate A is true, then predicate B must be true - A is "sufficient" for B, but it may not be "necessary")
A is true "if and only if" B is true (the condition B is both "necessary" and "sufficient" to prove A) - or put another way, A entails/proves B and B also entails/proves A
Set Theory is commonly used in computer science papers to describe semantics related to type systems - particularly algebraic types.
Below are some common symbols in set theory. See also this more comprehensive listing.
an element named a (denoted as a lowercase variable)
a set named A (denoted as an uppercase variable), implied to contain zero or more elements
a set containing the elements a, b, and c
a set containing every element x which satisfies the predicate function f (and containing no elements which do not satisfy it) - the | or : is sometimes called "set builder notation" and can be read as "such that" or "for which"
the union of sets A and B (the set of elements that are in either A or B)
the intersection of sets A and B (the set of elements that are in both A and B)
a is an element within the set/domain B
a is an element which is not within the set/domain B
set A is a subset of set B (all of the elements in A are also in B)
set A is a superset of set B (all of the elements in B are also in A)
set A is a strict/proper subset of set B (all of the elements in A are also in B, but there exist elements in B which are not in A)
set A is a strict/proper superset of set B (all of the elements in B are also in A, but there exist elements in A which are not in B)
Structural Operational Semantics is a system of notation for specifying formal semantics of a program or programming language.
It is used to specify a sort of "virtual machine" which knows certain rules for holding program state and reducing expressions based on that state.
This paper where Plotkin introduced the notation is a helpful resource.
A
---
B
If the condition A in the program state is met, then the program state will update as shown in B.
an initial state of a evaluates/transitions to a new state of b
typically a function accepting term a and emitting term b
typically a mapping of key a to value b within a state store
the predicate A is true within the given program state / runtime environment ∆/Γ (these two greek letters seem to be the most commonly used, but other names are possible)
TODO: Intro here
"for all" or "for any"
"there exists"
"such that"