Author Ondřej Pavlata Jablonec nad Nisou Czech Republic

Document date Initial release June 2, 2011 Last major release June 2, 2011 Last update September 2, 2018 (see Document history)

Warning

1. This document has been created without any prepublication review except those made by the author himself.
2. The author has no experience with the Linux operating system except for simple tests.

Linux version

Table of contents

Introduction

VFS versus RTFS

• (A) The Real Time File System ([]).
• (B) As used in [], within the term RTFS country.

User-observable semantics of the Virtual Filesystem should be described outside the RTFS country.

Preliminaries

General conventions

Mixture of partial functions

Ruby conventions

• List handling functions (see Lists).
• Ruby blocks are used for function definition: { |x| expression(x) } means the map x ↦ expression(x).

Lists

Monounary algebra

• X is a set,
• .p¯ is a function X → X.

Algebraic forest

1. (1) A partial order whose every principal up-set is a finite chain:
   A partial order (X, ≤) such that for every x ∈ X, the set x.ps = { y ∈ X | x ≤ y } is finite and totally ordered by ≤.
2. (2) A monounary algebra whose every non-empty subalgebra has a fixed point:
   An algebra (X, .p¯) with just one unary operator, .p¯ : X → X, such that for every x ∈ X, x.p¯(i) = x.p¯(i+1) for some natural i.
3. (3) A partial monounary algebra without total non-empty subalgebras:
   A partial algebra (X, .p) with just one partial unary operator, the parent partial function .p: X ↷ X, such that for every x ∈ X, x.p(i) is defined for only finitely many i.

1. x is .r-closed,
2. x is a fixed point w.r.t. .p¯,
3. x has undefined parent x.p.

Notes:

1. x.p¯(i) (resp. x.p(i)) means the i-th application of .p¯ (resp. .p) to x.
2. The form (3) shows that an algebraic forest can be viewed as a special case of a directed acyclic graph (DAG) which in turn is a special case of a digraph (a directed graph). In this context the term algebraic forest is equivalent to that of a rooted forest [].

Algebraic tree

1. (X, .p¯) is an algebraic forest,
2. r is the only fixed point of .p¯.

Pointed forest

1. (X, .p¯) is an algebraic forest,
2. r is an arbitrary element of X.

Component-wise finite linear order

• (a) Each component of (X, ≤) is a finite chain.
• (b) Both (X, ≤) and its opposite (X, ≥) are algebraic forests.

Ordered tree

1. (1) A locally finite algebraic tree together with sibling ordering: A structure (X, ≤_V, ≤_S) such that
   1. (X,≤_V) is a locally finite algebraic tree.
   2. (X,≤_S) is a component-wise linear order.
   3. .r_S.p_V = .p_V, i.e. components of ≤_S are sibling-sets of ≤_V.
2. (2) A locally finite algebraic tree together with a complementary horizontal ordering: A structure (X, ≤_V, ≤_H) such that
   1. (X,≤_V) is a locally finite algebraic tree.
   2. (X,≤_H) is a partial order.
   3. ≤_V and ≤_H are complementary, i.e. (<_V) ⊎ (>_V) ⊎ (<_H) ⊎ (>_H) = X × X ∖ Id.
   4. ≤_V and ≤_H are consistent: (<_H)  =  (≤_V) ○‣ (<_H) ○‣ (≥_V).
      (That is, for every nodes x, y such that x <_H y, all descendants of x precede all the descendants of y.)
3. (3) A locally finite algebraic tree together with a consistent linear extension: A structure (X, ≤_V, ≤_L) such that
   1. (X,≤_V) is a locally finite algebraic tree.
   2. (X,≤_L) is a linear order.
   3. (≤_V) ⊆ (≤_L), i.e. ≤_L is an extension of ≤_V.
   4. The same consistency condition as in (2) holds, with (≤_H) defined as (≤_L) ∖ (<_V).
4. (4) A parent-to-children-list map: A structure (X, .qs) such that
   1. X is a non-empty set.
   2. .qs is function X → X^∗.uniq, i.e. .qs maps X to non-repetitive lists over X.
   3. The set { (x,y) | x ∈ y.qs } is the parent partial function of a locally finite algebraic tree on X.

• (<_H)  =  (≤_V) ○‣ (<_S) ○‣ (≥_V)  =  (≤_L) ∖ (<_V)
• (<_L)  =  (<_H) ⊎ (<_V)
• x <_S y   iff   x.p_V = y.p_V and x <_L y.
• x <_S y   iff   x appears before y in some list from X.qs.
• x.p_V = y   iff   x ∈ y.qs.

• x.qs =	[ ]	if x ∉ X.pV,
  x.qs =	y.psS	otherwise, where y is the unique element of X such that y.pV = x and y ∉ X.pS.

Ordered forest

Tree navigation

Labelled transition system

• S is a set of states,
• Λ is a set of labels,

• ——›

  is a subset of S × Λ × S, elements of

  ——›

  are called transitions.

Multidigraph

• N is a set of nodes,
• A is a set of arrows, disjoint from N,
• .s and .t are functions A → N assigning to each arrow its source and target node, respectively.

Naming multidigraph

• (N, A, .s, .t) is a multidigraph,
• Σ is a naming domain – a set of names,
• .σ is a function A → Σ, called (arrow) naming, assigning to each arrow its name.

Lookup system

• X is a set (the lookup domain),
• Σ is a set of names,
• .ℓ() is a partial function X × Σ ↷ X, called the Σ-lookup.

Proposition: The following structures are equivalent:

1. A lookup system.
2. A deterministic labelled transition system.
3. A naming multidigraph, up to identification of arrows.  □

Pathnames

• .ℓ^∗([ ]) = Id ↾ X,
• .ℓ^∗([α₁, …, α_n]) = .ℓ(α₁) ⋯ .ℓ(α_n).

Proposition: For a partial function .f() : X × Σ^∗ ↷ X the following are equivalent:

1. (a) The map p ↦ .f(p) is a monoid homomorphism between (Σ^∗, +, [ ]) and (X^↷, ○‣, Id ↾ X), i.e.
   • .f(p).f(q) = .f(p + q), for every p, q ∈ Σ^∗, and
   • .f([ ]) = Id ↾ X.
2. (b) .f() is a Σ-pathname lookup, i.e. .f() = .ℓ^∗() for some .ℓ() : X × Σ ↷ X.
   (Necessarily, .ℓ() is given by .ℓ(α) = .f([α]).)  □

Pathname resolution system

• X, Σ are disjoint sets (with the same semantics as in a lookup system),
• .ϖ() is a partial function X × Σ^∗ ↷ X such that for every x ∈ X and every pathnames p, q,
  • x.ϖ([ ]) = x,
  • .ϖ(p + q) ⊆ .ϖ(p).ϖ(q).
    (If x.ϖ(p + q) is defined then   x.ϖ(p) and x.ϖ(p).ϖ(q) are defined and x.ϖ(p).ϖ(q) = x.ϖ(p + q).)

Proposition:

1. The domain of .ϖ() is pathname-prefix closed, i.e. for every (x,p) ∈ X × Σ^∗,
   • if x.ϖ(p) is defined then x.ϖ(p.pop) is defined.
2. Let .ℓ() : X × Σ ↷ X be a lookup defined by x.ℓ(α) = x.ϖ([α]). Then .ϖ() is a restriction of .ℓ^∗().

Corollary:

1. A pathname resolution system can be viewed as a lookup system (X, Σ, .ℓ()) equipped with a restriction .ϖ() of the induced pathname lookup .ℓ^∗() such that the domain of .ϖ()
   • is pathname-prefix closed, and
   • coincides with the domain of .ℓ^∗() on pathnames of length ≤ 1.
2. A lookup system can be viewed as a pathname resolution system such that .ℓ^∗() = .ϖ().

Reachability

(Double-)pointed lookup system

• (X, Σ, .ℓ()) is a lookup system,
• ‹/› is a distinguished element of Σ,
• r and d are distinguished elements of X   (called the current root and the current directory, respectively).

• {r, d} × {r}   ⊆   .ℓ(‹/›)   ⊆   X × {r}   (in particular, .ℓ(‹/›) maps constantly to r).

The (global) resolution target partial function .rt : Σ^∗ ↷ X maps pathnames to X as follows:

• p.rt = r.ℓ^∗(p)   if p[0] = r,
• p.rt = d.ℓ^∗(p)   otherwise.

Naming Forest

Forest Naming Domain

• Σ_down is the set of down names,
• Σ_spec is the set op special names with forest-related semantics. They are considered logical constants (cf. []), We distinguish these names by enclosing guillemets, like in ‹r› or ‹·›.
• Σ_‰ is the set op permil names containing just 3 special names ‹·›, ‹/› and ‹··›,
• Σ_Ό is the set of ordinary names.

Naming forest

• (A, ≤) is a forest,
• Σ is a forest naming domain,
• .σ is a function A ↷ Σ_down called down-naming.

• (1) Dom(.σ) = Dom(.p), i.e. x has a name iff x has a parent.
• (2) .p ⋈ .σ is injective, i.e. different siblings have different names.

Proposition: Given the forest naming domain Σ, the following structures are equivalent:

1. A naming forest (A, ≤, Σ, .σ).
2. A lookup system (A, Σ_down, .ℓ_down()) such that
   • .ℓ_down() is injective,
   • .ℓ_down (the single down-step reachability) is inverse to the parent partial function of a forest.

The default lookup operator .ℓ() : A × Σ ↷ A is defined as an extension of .ℓ_down() according to the following table:

Pathnames

Pathname reduction

Notes:

1. The ℅ symbol means care of trailing dot. The ℅-variants of reduction preserve pathname characteristics of ending with a down-name, see proposition (B). This is important for enforcing directory/non-directory (leaf/non-leaf) pathname resolution logic.
2. Pathname reduction .reduct_℅(‹·›).reduct_℅(‹··›) is used in URI resolution []. The following example shows the impact of the ℅ feature.

   URI	URI (after reduction)
   http://tools.ietf.org/pdf/rfc2606.pdf/some/..	http://tools.ietf.org/pdf/rfc2606.pdf/
   http://tools.ietf.org/pdf/some/../rfc2606.pdf	http://tools.ietf.org/pdf/rfc2606.pdf

Proposition:

• (A) For every .f, .g ∈ {.reduct(‹··›), , reduct_℅(‹··›), …,  .reduct},   p, q, r ∈ Σ^∗,
  1. .f.f = .f,
  2. .f.g = .g.f,
  3. (p + q + r).f = (p + q.f + r).f.
• (B) For every .f ∈ { reduct_℅(‹·›), reduct_℅(‹··›), reduct_℅},   p ∈ Σ^∗,
  1. p.last ∈ Σ_down   iff   p.f.last ∈ Σ_down.
• (C) Ά.reduct = Ϲ, i.e. .reduct maps absolute pathnames to canonical pathnames.

Canonical pathname tree

• .p = .pop ↾   Ϲ ∖ {[‹/›]},
• .σ = .last ↾   Ϲ ∖ {[‹/›]}.

Proposition: For every canonical pathname p and every ordinary pathname q,

• p.p¯ = (p + [‹··›]).reduct,
• p.ℓ_Ϲ^∗(q) = (p + q).reduct.

Induced pathname tree

• Ͼ = { q ∈ Ϲ | q.rt is defined },   (i.e. Ͼ is the set of all resolvable canonical pathnames)
• .ℓ_Ͼ() = .ℓ_Ϲ() ∩   Ͼ × Σ × Ͼ.

Proposition:

1. Ͼ.p ⊆ Ͼ,
2. (Ͼ, .p, Σ, .σ, [‹/›]) is a naming tree – we call it the induced pathname tree,
3. .ℓ_Ͼ() is the corresponding lookup.  □

Dot-dot handling modes

Proposition: Let (X, Σ, .ℓ(), r) be a pointed lookup system with a forest naming domain Σ such that

• .ℓ(‹··›) is defined for all x ∈ X, but does not necessarily have the semantics of a naming forest,
• .ℓ(‹·›) is identity on X.

1. If ‹··› ∉ p then the operators are equal.
2. If ‹··› ∈ p then the operators are pairwise different in general.

Note: For differences between [] and [], see step 8b.

Filesystem forest

Filesystem forest

• N is a set of nodes,
• A is a set of arrows, disjoint from N,
• ≤ is a partial order between arrows,
• .t is a function A → N assigning each arrow its target node.

1. (1) (A, ≤) is an algebraic forest.
2. (2) .t is injective on A.p, i.e. only leaf arrows a ≠ b can have equal target.

Filesystem forest as a multidigraph

S1: Filesystem forest

The following table shows basic correspondence of the S1 structure to its in-memory representation in the Linux kernel.

S2: Mounted filesystem forest

• M is a finite set of mounts, disjoint from both N and A,
• ≤ is a partial order between mounts,
• ≤_mpl is a component-wise linear order between mounts, encoding mountpoint lists,
• .s¯, .t are functions M → A assigning each mount its source and target, respectively (i.e. (M, A, .s¯, .t) is a multidigraph).

The following table shows basic correspondence of the mount structure to the Linux kernel source code.

(*) Notes:

1. Application of the list_entry macro is required: x.nei_mpl(−) corresponds to list_entry(y, struct vfsmount, mnt_hash) iff y equals x.mnt_hash.prev and is not the head of x.mnt_hash.
2. Mountpoint lists (i.e. components of (M, ≤_mpl) do not have direct one-to-one correspondence to .mnt_hash lists in general – a hash list can be merged from several mountpoint lists. The direct corresponence is established by a mountpoint equality check in __lookup_mnt.

Derived arrows

• Ѧ = { (m,a) ∈ M × A | m.t = a.r }

Proposition: Ѧ is finite.  □

We use the (m,a) signature for derived arrows, so that .m and .a are the natural projections, e.g. (m,a).a = a for (m,a) ∈ Ѧ.

Derived arrows Ѧ have the following form in the Linux source:

struct path {
        struct vfsmount *mnt;
        struct dentry *dentry;
};

Derived nodes

• N^′ = { (m,a.t) ∈ M × N | (m,a) ∈ Ѧ }

Mountpoints

• x ∈ (m,a).mpl   iff   (x.p,x.s) = (m,a),
• x appears before y in (m,a).mpl   iff   x ≤_mpl y.

Mount-front and mount-back

• (m,a).m_f is undefined   if (m,a) is not a mountpoint (i.e. the set X = { x ∈ M | (x.p,x.s) = (m,a) } is empty),
• (m,a).m_f = (y, y.t)   otherwise, where y = (m,a).mpl.last (the last mount in the mountpoint list of (m,a)).

Note: The ≤_mpl order just provides deterministic selection from the set X.

The mount-front function .f : Ѧ → Ѧ is defined recursively by

• x.f = x   if x.m_f is undefined,
• x.f = x.m_f.f   otherwise.

• (m,a).m_b is undefined   if a ∉ A.r or (m,a) ∈ M.r × A.r,
• (m,a).m_b = (m.p, m.s)   otherwise.

• x.b = x   if x.m_b is undefined,
• x.b = x.m_b.b   otherwise.

Proposition:

1. (i) .f and .b are root maps of forests (Ѧ, .m_f) and (Ѧ, .m_b), respectively. In addition, .m_f is injective.
2. (ii) .f.b = .b.
3. (iii) .b.p.a = .b.a.p.
4. (iv) A derived arrow x is a mountpoint iff x ∉ Ѧ.f.

The fine forest

• (m,a).p¯ = (m,a.p) if a ∉ A.r, else
• (m,a).p¯ = (m.p, m.s) if m ∉ M.r, else
• (m,a).p¯ = (m,a).

Proposition:

1. (i) (Ѧ, ≤) is an algebraic forest.
2. (ii) .f is idempotent and decreasing, .b is idempotent, increasing and monotone (a closure operator) in (Ѧ, ≤). For every x,y ∈ Ѧ,
   • x.f.f = x.f ≤ x ≤ x.b = x.b.b,
   • x ≤ y implies x.b ≤ y.b.
3. (iii) (N^′, Ѧ, ≤, .t) is a filesystem forest.
4. (iv) (Ѧ, .m_f⁻¹) ⊆ (Ѧ, .m_b) ⊆ (Ѧ, .p)   (forest inclusion).

Proof: (i) Follows from the fact that (Ѧ, .p) is a weak substructure of the lexicographic product of (M, .p) and (A, .p), respectively.  □

The up-front forest

Proposition:

1. (i) x.b < x.p_f.b whenever x.p_f is defined.
2. (ii) (Ѧ, ≤_f) is an algebraic forest.
3. (iii) .b is strictly monotone w.r.t. (Ѧ, ≤_f) and (Ѧ, ≤), i.e. x <_f y implies x.b < y.b.
4. (iv) (N^′, Ѧ, ≤_f, .t) is a filesystem forest.

Proof: (i) (x.p_f).b = (x.b.p.f).b = x.b.p.(f.b) = x.b.p.b > x.b.p > x.b.  □

The down-front forest

Proposition: Same statements apply as for the up-front forest, with f replaced by t.  □

S3: Naming

The fine lookup

Note: There is a shift in function naming between Linux versions 2.6.37 and 2.6.38.

• The function follow_down-version-2.6.37 corresponds to follow_down_one-version-2.6.38.
• The function follow_down-version-2.6.38 does not seem to have a counterpart in version 2.6.37.

Down-front naming

• .σ_t = .b.a.σ ↾ Ѧ.f,
• .ℓ_t(α) = .ℓ(α).f   for every down-name α.

Proposition: (Ѧ, ≤_t, Σ, .σ_t) is a naming forest with .ℓ_t() the correspondent down-lookup.  □

The .ℓ₃ lookup

S4: Current root

• r is a derived arrow called the current root.

The .ℓ₄ lookup

Proposition:

• (A) The following holds for differences between .ℓ₄() and .ℓ₃():
  1. The down lookup is coincident.
  2. Root lookups .ℓ₄(‹r›) and .ℓ₃(‹r›) coincide   iff   Ѧ.r ⊆ Ѧ.f.
  3. Root lookups .ℓ₄(‹/›) and .ℓ₃(‹r›) coincide   iff   {r} = Ѧ.r.
  4. Parent lookups .ℓ₄(‹··›) and .ℓ₃(‹p¯›) coincide   iff   r ∈ Ѧ.r ⊆ Ѧ.f.
• (B) Denote .p¯₄ = .ℓ₄(‹··›).
  1. (Ѧ, .p¯₄) is a forest.
  2. Ѧ.r₄ = Ѧ.r.f ∪ {r.f}.
   □

Ancestor pathname

Proposition: In general, .apn is NOT injective.  □

The canonical tree Ѧ_Ⅰ

We denote Ѧ_Ⅰ = r.ℓ₄^∗(Σ_down^∗), the canonical tree.

Proposition:

The reachable (double-)tree Ѧ_Ⅱ

Proposition:

1. Ѧ_Ⅱ = r.ℓ₄^∗(Ό) i.e. Ѧ_Ⅱ is the set of all derived arrows that are reachable from the current root r by an .ℓ₄^∗()-lookup over ordinary pathnames.
2. (Ѧ_Ⅱ, ≤_f) = (Ѧ_Ⅱ, ≤_t), i.e. restrictions of the up-front forest and the down-front forest to Ѧ_Ⅱ are equal.
3. The set of roots of the forest (Ѧ_Ⅱ, ≤_f) equals { r, r.f }. The forest (Ѧ_Ⅱ, ≤_f) is a tree   if r is not a mountpoint,   otherwise it has two components:
   • r.ℓ₄^∗(Σ_down^∗) = Ѧ_Ⅰ   – the canonical / standard tree,
   • r.f.ℓ₄^∗(Σ_down^∗) = Ѧ_Ⅱ ∖ Ѧ_Ⅰ   – the front tree.
4. The restriction of .ℓ₄() to Ѧ_Ⅱ × Σ_down is a down-lookup of (Ѧ_Ⅱ, ≤_f).
5. The structure (Ѧ_Ⅱ, .p¯₄, r.f) is an algebraic tree.
6. Ѧ_Ⅱ ∖ {r} ⊆ Ѧ.f, i.e. except possibly for the current root, an element of Ѧ_Ⅱ is never a mountpoint.

   Note: This is in contrast to the common terminology []: If an absolute path p is said to refer to a mountpoint via pathname resolution .ϖ() then it is meant that the mount-back r.ϖ(p).b is a mountpoint, not just r.ϖ(p).

Example: The following diagram shows a forest (Ѧ_Ⅱ, ≤_f) having both the canonical / standard tree (left, blue) and the front tree (right, green).

cd-navigation between Ѧ_Ⅰ and Ѧ_Ⅱ ∖ Ѧ_Ⅰ

Root reachability stratification

Notes:

1. It is possible to have x ∈ Ѧ_Ⅰ, y ∈ Ѧ_Ⅱ ∖ Ѧ_Ⅰ, and z ∈ Ѧ_Ⅲ ∖ Ѧ_Ⅱ such that x.apn = y.apn = z.apn.
2. The following Ruby code shows a derived arrow (originally pointed to by /home) outside Ѧ_Ⅲ.

   Dir.chdir "/home"
   Dir.chroot "/usr"
   puts Dir.pwd  #-> (unreachable)/home
   

S5: Basic file types

• .btype is an attribute of nodes N assigning each node its basic type, also called the unix file type .

The .ℓ₅ lookup

S6: Symbolic links

• .lpath is a function N.links → Σ^∗.

Path resolution stack

• a is a derived arrow,
• paths is a (possibly empty) list of non-empty pathnames.

• paths.pp is undefined if paths is empty, else
• paths.pp = paths.pop if paths.last.length = 1, else
• paths.pp = paths.pop + [paths.last.shift].

The partial operation .p_F : PRS ↷ PRS is then defined by

1. (A) (a,paths).p_F is undefined if paths is empty and a.a.t is not a symbolic link.
2. (B) Else if a.a.t is a symbolic link
   • (a,paths).p_F = (a.p, paths) if a.a.t.lpath is empty, else
   • (a,paths).p_F = (a.p, paths + [a.a.t.lpath]).
3. (C) Else if a.a.t is a directory, denote α = paths.last[0].
   • (a,paths).p_F is undefined if a.ℓ₄(α) is undefined, else
   • (a,paths).p_F = (a.ℓ₄(α), paths.pp).
4. (D) Otherwise (a.a.t is neither a directory nor a symbolic link)
   • (a,paths).p_F is undefined.

Note: Using ℓ₅ instead of ℓ₄ would result in a shorter prescription, with (C) and (D) merged.

For x ∈ PRS, the value x.p_F, if defined, is called the full resolution successor of x. The partial operation of a normal resolution successor .p_N : PRS ↷ PRS is defined as a restriction of .p_F to Ѧ × Σ⁺⁺.

Definition domains of .p_F and .p_N can be summarized as follows.

Proposition:

1. .p_F (resp. .p_N) has no fixed points.
2. The monounary algebra (PRS, p¯_F) (resp. (PRS, p¯_N)) is NOT an algebraic forest in general.

Link follower

Link target

Proposition: a.lt = b   iff   a.r_lnk = b and b.a.t ∉ N.links (i.e. b is the link target of a   iff   b is the last link follower of a and does not point to a symlink).  □

Linked lookup

Proposition: Let α ∈ Σ, d ∈ Ѧ such that d.a.t is directory. Then

Pathname resolution

Proposition:

1. .ϖ_F() = .ϖ_N().lt.
2. .ϖ_F() = .ℓ_F^∗()   (the pathname lookup induced by .ℓ_F()).
3. The previous statement with F replaced by N.

F / N modes in use

Induced pathname trees

Proposition:

1. Ͼ_N.p¯ ⊆ Ͼ_F ⊆ Ͼ_N.
2. Ͼ₄ ⊆ Ͼ_N.
3. .rt_N ↾ Ͼ₄   =   .rt₄ ↾ Ͼ₄.

Virtual identity layers

Further resolvability restrictions

• (A) Restrictions already applied to .ϖ_F().
• (C) Restrictions to be introduced in a further refinement of the S6 structure.
• (D) Rejecting extraordinary pathnames.

Proposition:

1. .ϖ_6F(p+q) ⊆ .ϖ_6F(p).ϖ_6F(q) for every pathnames p, q. Due to the symlink count limit, equality does not hold in general. (I.e. .ϖ_6F() is a pathname resolution operator, but – in contrast to .ϖ_F() – not a pathname lookup operator.)
2. The previous statement with F replaced by N.

Bibliographic references

Browser compatibility

• CSS level 3,
• HTML entities (Ϲ, Ͼ, ⤉, Ѧ, |, ‹, ›, ¯, ·, ř, ‖, ‣, ›, ℅, ℓ, ℕ, Ⅰ, Ⅱ, Ⅲ, Ⅳ, →, ↠, ↦, ↷, ↾, ⇡, ∅, ∋, ∖, ∗, ∞, ≠, ≰, ⊎, ⋈, ⋯, Ά, Ό, □, ○, ◐, ◑, ◖, ◗, ϖ, Λ, Σ, Τ, α, ∩, ∪, é, ≥, >, ↔, …, ∈, ←, ≤, <, —, −,  , –, ∉, ‰, ′, →, σ, ⊆, ×, ↑, ü, ‌),
• JavaScript.

Document history

License