Demystifying Symbols in The Calculus of Computation

2024-08-10

Categories: Computer Science Tags: Programming Languages

abstract

In computer science—particularly logic, formal methods, programming languages and set‐theory—many symbols appear that can confuse readers: turnstiles, arrows, maps, leads, etc. This article gathers a comparative table of such symbols, gives their common pronunciation (in English and Chinese), explains their meaning in various literature contexts, and provides illustrative examples. The goal is to demystify these symbols and help the reader read and write formal texts more confidently.

Comparative Table of Symbols

Formal notation in logic, set theory and programming language theory often uses special symbols that carry different subtle meanings. For example, the symbols (turnstile) and (double turnstile) signify different consequence relations; in set theory and PL/FM we see arrows like , , for functions, mappings or transitions. Understanding these at a glance improves clarity when reading research papers, proofs or formal definitions.

Symbol	Pronunciation (En / 中文)	Context / Usage	Illustrative Example
$\vdash$	“turnstile”, “yields” / “得出”, “推出”	Logic (proof theory, syntactic consequence — provability)	$\Gamma \vdash \varphi$ means “ is derivable from assumptions in a proof system.”
$\models$	“models”, “entails” / “语义蕴涵”, “满足”	Logic (model theory, semantic consequence — truth in all models)	$\Gamma \models \varphi$ means “in every model where all formulas in hold, also holds.”; $\mathcal{M} \models \varphi$ means “model satisfies .”
$\to$	“arrow”, “maps to” / “映射到”, “到”	Set theory / PL type theory (total function)	$f : A \to B$ means “ is a (total) function from to .”
$\mapsto$	“maps to”, “映射为”	Element-wise function mapping notation	$x \mapsto x^2$ describes how each in the domain is sent to .
$\leadsto$	“leads to”, “转化到”, “执行转移”	Operational semantics / transition systems	$s \leadsto s'$ means “state transitions to state in one (or a few) computation steps.”
$\Rightarrow$	“implies”, “蕴含”	Logic (meta-level implication), type systems (big-step semantics)	$\Gamma \Rightarrow \varphi$ means “ logically follows (meta-theoretically) from .”; in big-step semantics: $\langle c, s \rangle \Rightarrow s'$ .
$\circlearrowright$ / $\circlearrowleft$	“loop arrow”, “回路箭头”, “自环”	CFG, automata, state transition diagrams, control flow loops	A loop edge: $q \circlearrowright$ indicates state $q$ transitions back to itself (e.g., a loop in a CFG).
$\rightharpoonup$ (`\rightharpoonup`)	“partial mapping”, “偏函数”	Set theory / semantics (function not defined on every input)	$f : A \rightharpoonup B$ means “ is a partial function from to (not necessarily defined for all ).”
$\hookrightarrow$	“hook‐right arrow”, “钩向右箭头” / “右挂箭头”	Category theory / Algebra / Set theory (injective embedding or inclusion)	$f : A \hookrightarrow B$ means “ is an embedding (injective homomorphism) of into .”
$\hookleftarrow$	“hook‐left arrow”, “钩向左箭头” / “左挂箭头”	Algebra / Module theory (dual embedding or restriction)	$g : B \hookleftarrow A$ sometimes used to denote “ embeds into via (viewed as inclusion from the right).”

Detailed Notes and Remarks

Logic: vs

The single turnstile symbol (pronounced “turnstile” or “yields”) is traditionally used in proof theory to express syntactic derivability: i.e. from a set of premises or axioms one can derive a conclusion. In contrast, the double turnstile symbol (pronounced “models”, “semantic entailment”) is used in model theory to express semantic consequence: that in every model in which the premises are true, so is the conclusion. It is important to distinguish these two: one is about formal proofs (syntax), the other about truth in structures (semantics).

Set Theory and PL/FM: vs

In set theory and programming‐language theory, the arrow is used to denote a function type or a mapping between sets—i.e. means maps the whole set into set .
The arrow with tail is more specific: it describes what each element does—i.e. how an element of the domain is mapped to an element of the codomain. For example:

means “ is a function from reals to reals, and each real is mapped to ”.

Operational / Semantic Arrows:

In programming‐language semantics, a symbol like (pronounced “leads to” / “导向”) often denotes a transition relation—one configuration leads to another.
For instance, in an operational semantics of an imperative language we might write:

meaning “starting in state executing command leads to state and command ”.