diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -34,7 +34,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.79
+cabal install --overwrite-policy=always phino-0.0.80
 phino --version
 ```
 
@@ -214,9 +214,9 @@
 $ phino explain --normalize
 \begin{tabular}{rl}
 \trrule{alpha}
-  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) }
+  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \eta -> e ) }
   { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }
-  { if $ \indexof{ \tau_2 } = \vert B_1 \vert $ }
+  { if $ \indexof{ \eta } = \vert \overline{ B_1 } \vert $ }
   { }
 \trrule{dc}
   { T ( \tau -> e ) }
@@ -237,13 +237,13 @@
 ```bash
 $ phino explain --morph
 \begin{tabular}{rl}
-\trrule{Mprim}
+\trrule{prim}
   { \mathbb{M}( e ) }
   { e }
   { if $ e \in \mathcal{P} $ }
   { }
 ...
-\trrule{Mphi}
+\trrule{root}
   { \mathbb{M}( Q . \tau * t ) }
   { \mathbb{M}( e * t ) }
   { }
@@ -288,7 +288,6 @@
   = and: [Condition]     # logical AND
   | or:  [Condition]     # logical OR
   | not: Condition       # logical NOT
-  | alpha: Attribute'    # check if given attribute is alpha
   | eq:                  # compare two comparable objects
       - Comparable
       - Comparable
@@ -319,7 +318,7 @@
 
 Number:                  # comparable number
   = Integer              # just regular integer
-  | index: Attribute'    # calculate index of alpha attribute
+  | index: Alpha'        # calculate index of alpha
   | length: BiMeta'      # calculate length of bindings by given meta binding
 
 Extension:               # substitutions extension used to introduce new meta variables
@@ -378,6 +377,7 @@
 This is the list of supported meta variables:
 
 * `!a` || `𝜏` - attribute
+* `!h` || `𝜂` - alpha, the positional index of an application argument
 * `!e` || `𝑒` - any expression
 * `!n` || `𝑛` - any expression that is already in normal form (behaves like
                 `!e`/`𝑒`, but only binds a sub-expression in NF, so no explicit
@@ -419,55 +419,55 @@
 === parse/phi ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      1299342.512 μs
-  avg:        129934.251 μs
-  min:        118253.218 μs
-  max:        162332.377 μs
-  std dev:    16619.006 μs
+  total:      1400685.745 μs
+  avg:        140068.575 μs
+  min:        128878.179 μs
+  max:        170778.015 μs
+  std dev:    15086.312 μs
 === parse/xmir ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      7609340.593 μs
-  avg:        760934.059 μs
-  min:        697264.466 μs
-  max:        801903.360 μs
-  std dev:    31387.398 μs
+  total:      7628269.229 μs
+  avg:        762826.923 μs
+  min:        700461.528 μs
+  max:        895566.916 μs
+  std dev:    53443.050 μs
 === rewrite/normalize ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      394738.996 μs
-  avg:        39473.900 μs
-  min:        38668.484 μs
-  max:        40389.889 μs
-  std dev:    473.832 μs
+  total:      389007.790 μs
+  avg:        38900.779 μs
+  min:        37763.081 μs
+  max:        40258.745 μs
+  std dev:    794.301 μs
 === print/sweet/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      4562591.028 μs
-  avg:        456259.103 μs
-  min:        451902.950 μs
-  max:        462770.604 μs
-  std dev:    3059.588 μs
+  total:      3943382.302 μs
+  avg:        394338.230 μs
+  min:        375291.020 μs
+  max:        416271.808 μs
+  std dev:    12394.321 μs
 === print/sweet/flat ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      4529234.270 μs
-  avg:        452923.427 μs
-  min:        418300.611 μs
-  max:        476533.304 μs
-  std dev:    23032.941 μs
+  total:      3855869.876 μs
+  avg:        385586.988 μs
+  min:        365284.728 μs
+  max:        405130.834 μs
+  std dev:    11941.433 μs
 === print/salty/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      13656171.599 μs
-  avg:        1365617.160 μs
-  min:        1311639.249 μs
-  max:        1429575.023 μs
-  std dev:    37618.391 μs
+  total:      13541528.033 μs
+  avg:        1354152.803 μs
+  min:        1307453.767 μs
+  max:        1399468.749 μs
+  std dev:    27649.598 μs
 ```
 
 The results were calculated in [this GHA job][benchmark-gha]
-on 2026-06-11 at 11:02,
+on 2026-06-18 at 23:15,
 on Linux with 4 CPUs.
 
 <!-- benchmark_end -->
@@ -489,6 +489,19 @@
 make coverage
 ```
 
+To build a `phino` executable into the root of the repository, run:
+
+```bash
+make phino
+```
+
+This produces an executable `phino` (or `phino.exe` on Windows) in the
+project root, which you can run directly for quick local testing:
+
+```bash
+./phino --version
+```
+
 You will need [GHC ≥ 9.6.7][GHC] and [Cabal ≥ 3.0 (recommended)][cabal]
 or [Stack ≥ 3.0][stack] installed.
 
@@ -503,4 +516,4 @@
 [jna]: https://github.com/java-native-access/jna
 [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java
 [jeo]: https://github.com/objectionary/jeo-maven-plugin
-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27342074018
+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27794897832
diff --git a/benchmark/Main.hs b/benchmark/Main.hs
--- a/benchmark/Main.hs
+++ b/benchmark/Main.hs
@@ -3,7 +3,7 @@
 
 module Main where
 
-import AST (Expression (ExGlobal))
+import AST (Expression (ExRoot))
 import Control.Exception (evaluate)
 import Control.Monad (replicateM, replicateM_)
 import Data.Time.Clock
@@ -33,7 +33,7 @@
 rewriteCtx :: RewriteContext
 rewriteCtx =
   RewriteContext
-    ExGlobal
+    ExRoot
     100
     100
     False
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.80
+version: 0.0.81
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/resources/dataization.yaml b/resources/dataization.yaml
--- a/resources/dataization.yaml
+++ b/resources/dataization.yaml
@@ -1,7 +1,8 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-# Dataization 𝔻 — applied top-to-bottom, first matching clause wins.
+# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. The input
+# is always a normal form: a non-NF expression matches no clause.
 
 - name: delta
   description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'
@@ -9,7 +10,7 @@
   then: δ
 
 - name: box
-  description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒞(e)) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'
+  description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒩(𝒞(e))) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'
   match: ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧
   where:
     - meta: 𝑒1
@@ -22,19 +23,20 @@
       - [Δ, λ]
       - [𝐵1, 𝐵2]
   then:
-    dataize: 𝑒1
+    dataize:
+      normalize: 𝑒1
 
 - name: norm
-  description: '𝔻(e) ⟿ 𝔻(𝕄(e)) if e ∉ 𝒫'
-  match: 𝑒
+  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) if n ∉ 𝒫'
+  match: 𝑛
   when:
     not:
-      primitive: 𝑒
+      primitive: 𝑛
   then:
     dataize:
-      morph: 𝑒
+      morph: 𝑛
 
 - name: none
-  description: '𝔻(e) ⟿ nothing otherwise'
-  match: 𝑒
+  description: '𝔻(n) ⟿ nothing otherwise'
+  match: 𝑛
   then: nothing
diff --git a/resources/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -1,27 +1,16 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-# Morphing 𝕄 — applied top-to-bottom, first matching clause wins.
-
-- name: Mprim
-  description: '𝕄(e) ⟿ e if e ∈ 𝒫'
-  match: 𝑒
-  when:
-    primitive: 𝑒
-  then: 𝑒
+# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input
+# is always a normal form: a non-NF expression matches no clause.
 
-- name: Mnmz
-  description: '𝕄(e) ⟿ 𝕄(𝒩(e)) if e ∉ NF'
-  match: 𝑒
-  when:
-    not:
-      nf: 𝑒
-  then:
-    morph:
-      normalize: 𝑒
+- name: prim
+  description: '𝕄(p) ⟿ p'
+  match: 𝑝
+  then: 𝑝
 
-- name: Mlambda
-  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(F(⟦𝐵1, 𝐵2⟧) * t)'
+- name: lambda
+  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(𝒩(F(⟦𝐵1, 𝐵2⟧) * t))'
   match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧ * !t'
   where:
     - meta: 𝑒
@@ -29,10 +18,11 @@
       args:
         - '⟦𝐵1, λ ⤍ !F, 𝐵2⟧'
   then:
-    morph: '𝑒 * !t'
+    morph:
+      normalize: '𝑒 * !t'
 
-- name: Mphi
-  description: '𝕄(Φ.τ * t) ⟿ 𝕄(e * t) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧'
+- name: root
+  description: '𝕄(Φ.τ * t) ⟿ 𝕄(𝒩(e * t)) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧'
   match: 'Φ.𝜏 * !t'
   where:
     - meta: 𝑒
@@ -40,9 +30,10 @@
       args:
         - 𝜏
   then:
-    morph: '𝑒 * !t'
+    morph:
+      normalize: '𝑒 * !t'
 
-- name: Mstuck
-  description: '𝕄(e) ⟿ ⊥ otherwise'
-  match: 𝑒
+- name: stuck
+  description: '𝕄(n) ⟿ ⊥ otherwise'
+  match: 𝑛
   then: ⊥
diff --git a/resources/normalize/alpha.yaml b/resources/normalize/alpha.yaml
--- a/resources/normalize/alpha.yaml
+++ b/resources/normalize/alpha.yaml
@@ -2,9 +2,9 @@
 # SPDX-License-Identifier: MIT
 ---
 name: alpha
-pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)
+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜂 ↦ 𝑒)
 result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)
 when:
   eq:
-    - index: 𝜏2
+    - index: 𝜂
     - domain: 𝐵1
diff --git a/resources/normalize/dca.yaml b/resources/normalize/dca.yaml
new file mode 100644
--- /dev/null
+++ b/resources/normalize/dca.yaml
@@ -0,0 +1,6 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+name: dca
+pattern: ⊥(𝜂 ↦ 𝑒)
+result: ⊥
diff --git a/resources/normalize/miss.yaml b/resources/normalize/miss.yaml
--- a/resources/normalize/miss.yaml
+++ b/resources/normalize/miss.yaml
@@ -5,10 +5,7 @@
 pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒)
 result: ⊥
 when:
-  and:
-    - not:
-        in:
-          - 𝜏
-          - 𝐵
-    - not:
-        alpha: 𝜏
+  not:
+    in:
+      - 𝜏
+      - 𝐵
diff --git a/src/AST.hs b/src/AST.hs
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -18,10 +18,10 @@
 
 data Expression
   = ExFormation [Binding]
-  | ExThis
-  | ExGlobal
+  | ExXi
+  | ExRoot
   | ExTermination
-  | ExApplication Expression Binding
+  | ExApplication Expression Argument
   | ExDispatch Expression Attribute
   | ExMeta Text
   | ExMetaTail Expression Text
@@ -29,13 +29,22 @@
   | ExPhiAgain (Maybe String) Int Expression
   deriving (Eq, Ord, Show, Generic)
 
+data Argument
+  = ArTau Attribute Expression
+  | ArAlpha Alpha Expression
+  deriving (Eq, Ord, Show, Generic)
+
+data Alpha
+  = Alpha Int
+  | AlMeta Text
+  deriving (Eq, Ord, Generic)
+
 data Binding
   = BiTau Attribute Expression
-  | BiDelta Bytes
   | BiVoid Attribute
-  | BiLambda Text
+  | BiDelta Bytes
+  | BiLambda Function
   | BiMeta Text
-  | BiMetaLambda Text
   deriving (Eq, Ord, Show, Generic)
 
 data Bytes
@@ -47,7 +56,6 @@
 
 data Attribute
   = AtLabel Text
-  | AtAlpha Int
   | AtPhi
   | AtRho
   | AtLambda
@@ -55,15 +63,23 @@
   | AtMeta Text
   deriving (Eq, Generic, Ord)
 
+data Function
+  = Function Text
+  | FnMeta Text
+  deriving (Eq, Generic, Show, Ord)
+
 instance Show Attribute where
   show (AtLabel label) = T.unpack label
-  show (AtAlpha idx) = 'α' : show idx
   show AtRho = "ρ"
   show AtPhi = "φ"
   show AtDelta = "Δ"
   show AtLambda = "λ"
   show (AtMeta meta) = '!' : T.unpack meta
 
+instance Show Alpha where
+  show (Alpha idx) = 'α' : show idx
+  show (AlMeta meta) = '!' : T.unpack meta
+
 -- A cheap, fixed-size digest of an expression, used for fast (dirty) equality
 -- checks during loop detection. Equal expressions always produce the same
 -- digest, but distinct expressions may collide, so a positive digest match
@@ -74,60 +90,72 @@
     fnvPrime, fnvOffset :: Int
     fnvPrime = 1099511628211
     fnvOffset = 14695981039
-
     -- FNV-1a style mixing step (Int multiplication wraps silently).
     step :: Int -> Int -> Int
     step h x = (h `xor` x) * fnvPrime
-
     hashText :: Int -> Text -> Int
     hashText = T.foldl' (\h c -> step h (fromEnum c))
-
     hashString :: Int -> String -> Int
     hashString = foldl' (\h c -> step h (fromEnum c))
-
     hashMaybeString :: Int -> Maybe String -> Int
     hashMaybeString h Nothing = step h 0
     hashMaybeString h (Just s) = hashString (step h 1) s
-
     goExpr :: Int -> Expression -> Int
     goExpr h = \case
       ExFormation bds -> foldl' goBinding (step h 1) bds
-      ExThis -> step h 2
-      ExGlobal -> step h 3
+      ExXi -> step h 2
+      ExRoot -> step h 3
       ExTermination -> step h 4
-      ExApplication ex bd -> goBinding (goExpr (step h 5) ex) bd
+      ExApplication ex arg -> goArgument (goExpr (step h 5) ex) arg
       ExDispatch ex at -> goAttribute (goExpr (step h 6) ex) at
       ExMeta t -> hashText (step h 7) t
       ExMetaTail ex t -> hashText (goExpr (step h 8) ex) t
       ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex
       ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex
-
     goBinding :: Int -> Binding -> Int
     goBinding h = \case
       BiTau at ex -> goExpr (goAttribute (step h 11) at) ex
       BiDelta bts -> goBytes (step h 12) bts
       BiVoid at -> goAttribute (step h 13) at
-      BiLambda t -> hashText (step h 14) t
+      BiLambda fn -> goFunction (step h 14) fn
       BiMeta t -> hashText (step h 15) t
-      BiMetaLambda t -> hashText (step h 16) t
-
     goBytes :: Int -> Bytes -> Int
     goBytes h = \case
       BtEmpty -> step h 17
       BtOne s -> hashString (step h 18) s
       BtMany ss -> foldl' hashString (step h 19) ss
       BtMeta t -> hashText (step h 20) t
-
     goAttribute :: Int -> Attribute -> Int
     goAttribute h = \case
       AtLabel t -> hashText (step h 21) t
-      AtAlpha i -> step (step h 22) i
       AtPhi -> step h 23
       AtRho -> step h 24
       AtLambda -> step h 25
       AtDelta -> step h 26
       AtMeta t -> hashText (step h 27) t
+    goArgument :: Int -> Argument -> Int
+    goArgument h = \case
+      ArTau at ex -> goExpr (goAttribute (step h 22) at) ex
+      ArAlpha al ex -> goExpr (goAlpha (step h 30) al) ex
+    goAlpha :: Int -> Alpha -> Int
+    goAlpha h = \case
+      Alpha idx -> step (step h 31) idx
+      AlMeta t -> hashText (step h 28) t
+    goFunction :: Int -> Function -> Int
+    goFunction h = \case
+      Function t -> hashText (step h 16) t
+      FnMeta t -> hashText (step h 29) t
 
+-- A primitive is the termination ⊥ or a formation without a λ binding.
+primitive :: Expression -> Bool
+primitive ExTermination = True
+primitive (ExFormation bds) = not (any lambda bds)
+  where
+    lambda :: Binding -> Bool
+    lambda (BiLambda _) = True
+    lambda _ = False
+primitive _ = False
+
 countNodes :: Expression -> Int
 countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds
   where
@@ -135,7 +163,8 @@
     nodesInBinding (BiTau _ expr) = countNodes expr + 2
     nodesInBinding (BiMeta _) = 1
     nodesInBinding _ = 3
-countNodes (ExApplication expr (BiTau _ expr')) = 4 + countNodes expr + countNodes expr'
+countNodes (ExApplication expr (ArTau _ expr')) = 4 + countNodes expr + countNodes expr'
+countNodes (ExApplication expr (ArAlpha _ expr')) = 4 + countNodes expr + countNodes expr'
 countNodes (ExDispatch expr' _) = 2 + countNodes expr'
 countNodes (ExMetaTail expr _) = 2 + countNodes expr
 countNodes (ExPhiMeet _ _ expr) = countNodes expr
diff --git a/src/Builder.hs b/src/Builder.hs
--- a/src/Builder.hs
+++ b/src/Builder.hs
@@ -24,7 +24,6 @@
 
 import AST
 import Control.Exception (Exception, throwIO)
-import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.Map.Strict as Map
 import Data.Text (Text)
 import qualified Data.Text as T
@@ -52,13 +51,16 @@
   show CouldNotBuildBytes{..} = printf "Couldn't build bytes '%s', %s" (printBytes _bts) _msg
 
 contextualize :: Expression -> Expression -> Expression
-contextualize ExGlobal _ = ExGlobal
-contextualize ExThis ex = ex
+contextualize ExRoot _ = ExRoot
+contextualize ExXi ex = ex
 contextualize ExTermination _ = ExTermination
 contextualize (ExFormation bds) _ = ExFormation bds
 contextualize (ExDispatch ex at) context = ExDispatch (contextualize ex context) at
-contextualize (ExApplication ex (BiTau at bexpr)) context =
-  ExApplication (contextualize ex context) (BiTau at (contextualize bexpr context))
+contextualize (ExApplication ex arg) context =
+  ExApplication (contextualize ex context) (contextualizeArg arg)
+  where
+    contextualizeArg (ArTau at bexpr) = ArTau at (contextualize bexpr context)
+    contextualizeArg (ArAlpha al bexpr) = ArAlpha al (contextualize bexpr context)
 contextualize ex _ = ex
 
 buildAttribute :: Attribute -> Subst -> Built Attribute
@@ -67,6 +69,12 @@
   _ -> Left (metaMsg meta)
 buildAttribute attr _ = Right attr
 
+buildAlpha :: Alpha -> Subst -> Built Alpha
+buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup meta mp of
+  Just (MvAlpha alpha) -> Right alpha
+  _ -> Left (metaMsg meta)
+buildAlpha a _ = Right a
+
 buildBytes :: Bytes -> Subst -> Built Bytes
 buildBytes (BtMeta meta) (Subst mp) = case Map.lookup meta mp of
   Just (MvBytes bytes) -> Right bytes
@@ -90,11 +98,21 @@
 buildBinding (BiDelta bytes) subst = do
   bts <- buildBytes bytes subst
   Right [BiDelta bts]
-buildBinding (BiMetaLambda meta) (Subst mp) = case Map.lookup meta mp of
-  Just (MvFunction func) -> Right [BiLambda func]
+buildBinding (BiLambda (FnMeta meta)) (Subst mp) = case Map.lookup meta mp of
+  Just (MvFunction func) -> Right [BiLambda (Function func)]
   _ -> Left (metaMsg meta)
 buildBinding binding _ = Right [binding]
 
+buildArgument :: Argument -> Subst -> Built Argument
+buildArgument (ArTau attr expr) subst = do
+  attribute <- buildAttribute attr subst
+  expression <- buildExpression expr subst
+  Right (ArTau attribute expression)
+buildArgument (ArAlpha alpha expr) subst = do
+  alpha' <- buildAlpha alpha subst
+  expression <- buildExpression expr subst
+  Right (ArAlpha alpha' expression)
+
 -- Build bindings that may contain meta binding (BiMeta)
 buildBindings :: [Binding] -> Subst -> Built [Binding]
 buildBindings [] _ = Right []
@@ -106,7 +124,7 @@
 buildExpressionWithTails :: Expression -> [Tail] -> Subst -> Expression
 buildExpressionWithTails expr [] _ = expr
 buildExpressionWithTails ex (tl : rest) subst = case tl of
-  TaApplication taus -> buildExpressionWithTails (ExApplication ex taus) rest subst
+  TaApplication arg -> buildExpressionWithTails (ExApplication ex arg) rest subst
   TaDispatch at -> buildExpressionWithTails (ExDispatch ex at) rest subst
 
 -- Build meta expression with given substitution
@@ -115,14 +133,10 @@
   dispatched <- buildExpression ex subst
   at' <- buildAttribute at subst
   Right (ExDispatch dispatched at')
-buildExpression (ExApplication expr (BiTau battr bexpr)) subst = do
+buildExpression (ExApplication expr arg) subst = do
   applied <- buildExpression expr subst
-  bd :| _ <- nonEmpty' =<< buildBinding (BiTau battr bexpr) subst
-  Right (ExApplication applied bd)
-  where
-    nonEmpty' :: [a] -> Built (NonEmpty a)
-    nonEmpty' [] = Left ""
-    nonEmpty' (x : xs) = Right (x :| xs)
+  arg' <- buildArgument arg subst
+  Right (ExApplication applied arg')
 buildExpression (ExFormation bds) subst = do
   bds' <- buildBindings bds subst >>= uniqueBindings
   Right (ExFormation bds')
diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs
--- a/src/CLI/Helpers.hs
+++ b/src/CLI/Helpers.hs
@@ -64,7 +64,7 @@
 printRewrittens :: PrintProgramContext -> Rewrittens' -> IO String
 printRewrittens ctx@PrintProgCtx{..} rewrittens@(chain, _)
   | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx)
-  | _focus == ExGlobal = mapM (printProgram ctx . fst) chain <&> intercalate "\n"
+  | _focus == ExRoot = mapM (printProgram ctx . fst) chain <&> intercalate "\n"
   | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) chain <&> intercalate "\n"
 
 printExpression :: PrintProgramContext -> Expression -> IO String
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -224,7 +224,7 @@
         False
         (justMeetPopularity Nothing)
         (justMeetLength Nothing)
-        ExGlobal
+        ExRoot
         Nothing
         Nothing
         Nothing
@@ -246,4 +246,4 @@
         else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))
   where
     rule :: Expression -> Maybe Y.Condition -> Y.Rule
-    rule ptn cnd = Y.Rule "custom" Nothing ptn ExGlobal cnd Nothing Nothing
+    rule ptn cnd = Y.Rule "custom" Nothing ptn ExRoot cnd Nothing Nothing
diff --git a/src/CLI/Validators.hs b/src/CLI/Validators.hs
--- a/src/CLI/Validators.hs
+++ b/src/CLI/Validators.hs
@@ -25,7 +25,7 @@
     asDispatch expr = asDispatch' expr
       where
         asDispatch' :: Expression -> IO Expression
-        asDispatch' ex@ExGlobal = pure ex
+        asDispatch' ex@ExRoot = pure ex
         asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp
         asDispatch' _ =
           invalidCLIArguments
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -11,7 +11,6 @@
 module CST where
 
 import AST
-import Data.Maybe (isJust)
 import qualified Data.Text as T
 import Misc
 import qualified Yaml as Y
@@ -84,9 +83,14 @@
   | N' -- n
   | K -- 𝑘
   | K' -- k
+  | P -- 𝑝
+  | P' -- p
   | A -- a
   | TAU -- 𝜏
   | TAU' -- \tau
+  | ETA -- 𝜂
+  | ETA' -- \eta
+  | H -- h
   | B -- 𝐵
   | B' -- B
   | D -- δ
@@ -164,8 +168,8 @@
   | EX_APPLICATION {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, tau :: APP_BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)
   | EX_APPLICATION_TAUS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, taus :: BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)(a2 -> e2)(...)
   | EX_APPLICATION_EXPRS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, args :: APP_ARG, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(e1, e2, ...)
-  | EX_STRING {str :: String, tab :: TAB, rhos :: [Binding]}
-  | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Binding]}
+  | EX_STRING {str :: String, tab :: TAB, rhos :: [Argument]}
+  | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Argument]}
   | EX_META {meta :: META}
   | EX_META_TAIL {expr :: EXPRESSION, meta :: META}
   | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}
@@ -263,6 +267,9 @@
 attributeToCST :: Attribute -> ATTRIBUTE
 attributeToCST = toCST'
 
+alphaToCST :: Alpha -> ATTRIBUTE
+alphaToCST = toCST'
+
 bindingsToCST :: [Binding] -> BINDING
 bindingsToCST = toCST'
 
@@ -286,12 +293,13 @@
 
 -- The first character of an expression meta name encodes its kind:
 -- 'n'-prefixed names are normal-form-constrained '𝑛' metas, 'k'-prefixed
--- names are absolute-constrained '𝑘' metas, everything else is an
--- ordinary '𝑒' meta.
+-- names are absolute-constrained '𝑘' metas, 'p'-prefixed names are
+-- primitive-constrained '𝑝' metas, everything else is an ordinary '𝑒' meta.
 exMetaHead :: T.Text -> META_HEAD
 exMetaHead mt
   | T.isPrefixOf "n" mt = N
   | T.isPrefixOf "k" mt = K
+  | T.isPrefixOf "p" mt = P
   | otherwise = E
 
 -- This class is used to convert AST to CST
@@ -304,8 +312,8 @@
   toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB NO_SPACE
 
 instance ToCST Expression EXPRESSION where
-  toCST ExGlobal _ = EX_GLOBAL Φ
-  toCST ExThis _ = EX_XI XI
+  toCST ExRoot _ = EX_GLOBAL Φ
+  toCST ExXi _ = EX_XI XI
   toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))
   toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (META EXCL TAIL (metaTail mt))
   toCST ExTermination _ = EX_TERMINATION DEAD
@@ -335,7 +343,7 @@
   -- their byte form `Φ.number(Φ.bytes(⟦ Δ ⤍ … ⟧))` by falling through to the
   -- generic application clause below.
   toCST (DataNumber bts) (tabs, _) | sweetNumber bts = EX_NUMBER (btsToNum bts) (TAB tabs) []
-  toCST (ExDispatch ExThis attr) ctx = EX_ATTR (toCST attr ctx)
+  toCST (ExDispatch ExXi attr) ctx = EX_ATTR (toCST attr ctx)
   toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) NO_SPACE (toCST attr ctx)
   -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings
   -- in primitives (more details here: https://github.com/objectionary/phino/issues/451)
@@ -353,7 +361,7 @@
         next = tabs + 1
         (ts', rs) = withoutRhosInPrimitives ex ts
         obj = ExApplication ex (head' ts')
-     in if length ts' == 1 && isJust (matchDataObject obj) && sweetCollapsible obj
+     in if length ts' == 1 && dataPrimitive obj && sweetCollapsible obj
           then applicationToPrimitive obj tabs rs
           else
             if null exs
@@ -380,9 +388,13 @@
     where
       primitives :: [T.Text]
       primitives = ["number", "string"]
-      withoutRhosInPrimitives :: Expression -> [Binding] -> ([Binding], [Binding])
+      dataPrimitive :: Expression -> Bool
+      dataPrimitive obj' = case matchDataObject obj' of
+        Just (label, _) -> label `elem` primitives
+        Nothing -> False
+      withoutRhosInPrimitives :: Expression -> [Argument] -> ([Argument], [Argument])
       withoutRhosInPrimitives _ [] = ([], [])
-      withoutRhosInPrimitives obj@(BaseObject label) bds@(rho@(BiTau AtRho _) : rest)
+      withoutRhosInPrimitives obj@(BaseObject label) bds@(rho@(ArTau AtRho _) : rest)
         | label `elem` primitives =
             let (bds', rhos) = withoutRhosInPrimitives obj rest
              in (bds', rho : rhos)
@@ -393,7 +405,7 @@
              in (bd : bds', rhos)
         | otherwise = (bds, [])
       withoutRhosInPrimitives _ bds = (bds, [])
-      applicationToPrimitive :: Expression -> Int -> [Binding] -> EXPRESSION
+      applicationToPrimitive :: Expression -> Int -> [Argument] -> EXPRESSION
       applicationToPrimitive (DataNumber bts) tabs = EX_NUMBER (btsToNum bts) (TAB tabs)
       applicationToPrimitive (DataString bts) tabs = EX_STRING (btsToStr bts) (TAB tabs)
       applicationToPrimitive _ _ = error "applicationToPrimitive expects DataNumber or DataString"
@@ -403,24 +415,24 @@
       -- 2. list of tau bindings which are applied to start expression
       -- 3. list of expressions which are applied to start expression with default
       --    alpha attributes (~0 -> e1, ~1 -> e2, ...)
-      complexApplication :: Expression -> (Expression, [Binding], [Expression])
+      complexApplication :: Expression -> (Expression, [Argument], [Expression])
       complexApplication expr =
         let (expr', taus', exprs') = complexApplication' expr
          in (expr', reverse taus', reverse exprs')
         where
-          complexApplication' :: Expression -> (Expression, [Binding], [Expression])
+          complexApplication' :: Expression -> (Expression, [Argument], [Expression])
           complexApplication' (ExApplication (ExApplication expr tau) tau') =
             let (before, taus, exprs) = complexApplication' (ExApplication expr tau)
                 taus' = tau' : taus
              in if null exprs
                   then (before, taus', [])
                   else case tau' of
-                    BiTau (AtAlpha idx) expr' ->
+                    ArAlpha (Alpha idx) expr' ->
                       if idx == length exprs
                         then (before, taus', expr' : exprs)
                         else (before, taus', [])
                     _ -> (before, taus', [])
-          complexApplication' (ExApplication expr (BiTau (AtAlpha 0) expr')) = (expr, [BiTau (AtAlpha 0) expr'], [expr'])
+          complexApplication' (ExApplication expr (ArAlpha (Alpha 0) expr')) = (expr, [ArAlpha (Alpha 0) expr'], [expr'])
           complexApplication' (ExApplication expr tau) = (expr, [tau], [])
           complexApplication' expr = (expr, [], [])
       -- This head' works the same as head from Prelude but doesn't throw an error
@@ -473,10 +485,22 @@
   toCST (BiTau attr exp) ctx = PA_TAU (toCST attr ctx) ARROW (toCST exp ctx)
   toCST (BiVoid attr) ctx = PA_VOID (toCST attr ctx) ARROW EMPTY
   toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)
-  toCST (BiLambda func) _ = PA_LAMBDA func
-  toCST (BiMetaLambda mt) _ = PA_META_LAMBDA (META EXCL F (metaTail mt))
+  toCST (BiLambda (Function name)) _ = PA_LAMBDA name
+  toCST (BiLambda (FnMeta mt)) _ = PA_META_LAMBDA (META EXCL F (metaTail mt))
   toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ T.unpack mt ++ " cannot be converted to PAIR"
 
+instance ToCST Argument PAIR where
+  toCST (ArTau attr exp) ctx = toCST (BiTau attr exp) ctx
+  toCST (ArAlpha alpha exp) ctx = PA_TAU (toCST alpha ctx) ARROW (toCST exp ctx)
+
+instance ToCST [Argument] BINDING where
+  toCST [] (tabs, _) = BI_EMPTY (TAB tabs)
+  toCST (arg : args) ctx@(tabs, _) = BI_PAIR (toCST arg ctx) (toCST args ctx) (TAB tabs)
+
+instance ToCST [Argument] BINDINGS where
+  toCST [] (tabs, _) = BDS_EMPTY (TAB tabs)
+  toCST (arg : args) ctx@(tabs, eol) = BDS_PAIR eol (TAB tabs) (toCST arg ctx) (toCST args ctx)
+
 instance ToCST Binding APP_BINDING where
   toCST bd@(BiTau _ _) ctx = APP_BINDING (toCST bd ctx :: PAIR)
   toCST bd _ = error $ "Only BiTau binding can be converted to APP_BINDING, got: " ++ show bd
@@ -489,17 +513,19 @@
 
 instance ToCST Attribute ATTRIBUTE where
   toCST (AtLabel label) _ = AT_LABEL label
-  toCST (AtAlpha idx) _ = AT_ALPHA ALPHA idx
   toCST AtPhi _ = AT_PHI PHI
   toCST AtRho _ = AT_RHO RHO
   toCST AtDelta _ = AT_DELTA DELTA
   toCST AtLambda _ = AT_LAMBDA LAMBDA
   toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt))
 
+instance ToCST Alpha ATTRIBUTE where
+  toCST (Alpha idx) _ = AT_ALPHA ALPHA idx
+  toCST (AlMeta mt) _ = AT_META (META NO_EXCL ETA (metaTail mt))
+
 instance ToCST Y.Condition CONDITION where
   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))
   toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right)
-  toCST (Y.Not (Y.Alpha attr)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])
   toCST (Y.Not (Y.Primitive expr)) _ = CO_PRIMITIVE (expressionToCST expr) NOT_IN
   toCST (Y.Primitive expr) _ = CO_PRIMITIVE (expressionToCST expr) IN
   toCST (Y.Not (Y.Absolute expr)) _ = CO_ABSOLUTE (expressionToCST expr) NOT_IN
@@ -512,7 +538,6 @@
   toCST (Y.Or conds) _ = case conds of
     [] -> CO_EMPTY
     _ -> CO_LOGIC (map toCST' conds) OR
-  toCST (Y.Alpha attr) _ = CO_BELONGS (attributeToCST attr) IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])
   toCST (Y.NF expr) _ = CO_NF (expressionToCST expr)
   toCST (Y.Not cond) _ = CO_NOT (conditionToCST cond)
   toCST (Y.Eq left right) _ = CO_COMPARE (comparableToCST left) EQUAL (comparableToCST right)
@@ -525,7 +550,7 @@
   toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num)
 
 instance ToCST Y.Number NUMBER where
-  toCST (Y.Index attr) _ = INDEX (attributeToCST attr)
+  toCST (Y.Index alpha) _ = INDEX (alphaToCST alpha)
   toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])
   toCST (Y.Domain binding) _ = DOMAIN (bindingsToCST [binding])
   toCST (Y.Literal num) _ = LITERAL num
diff --git a/src/Canonizer.hs b/src/Canonizer.hs
--- a/src/Canonizer.hs
+++ b/src/Canonizer.hs
@@ -12,9 +12,9 @@
 
 canonizeBindings :: [Binding] -> Int -> ([Binding], Int)
 canonizeBindings [] idx = ([], idx)
-canonizeBindings ((BiLambda _) : rest) idx =
+canonizeBindings ((BiLambda (Function _)) : rest) idx =
   let (bds', idx') = canonizeBindings rest (idx + 1)
-   in (BiLambda (T.pack ('F' : show idx)) : bds', idx')
+   in (BiLambda (Function (T.pack ('F' : show idx))) : bds', idx')
 canonizeBindings (BiTau attr expr : rest) idx =
   let (expr', idx') = canonizeExpression expr idx
       (bds', idx'') = canonizeBindings rest idx'
@@ -30,11 +30,19 @@
 canonizeExpression (ExDispatch expr attr) idx =
   let (expr', idx') = canonizeExpression expr idx
    in (ExDispatch expr' attr, idx')
-canonizeExpression (ExApplication expr (BiTau attr arg)) idx =
+canonizeExpression (ExApplication expr arg) idx =
   let (expr', idx') = canonizeExpression expr idx
-      (arg', idx'') = canonizeExpression arg idx'
-   in (ExApplication expr' (BiTau attr arg'), idx'')
+      (arg', idx'') = canonizeArgument arg idx'
+   in (ExApplication expr' arg', idx'')
 canonizeExpression expr idx = (expr, idx)
+
+canonizeArgument :: Argument -> Int -> (Argument, Int)
+canonizeArgument (ArTau attr expr) idx =
+  let (expr', idx') = canonizeExpression expr idx
+   in (ArTau attr expr', idx')
+canonizeArgument (ArAlpha alpha expr) idx =
+  let (expr', idx') = canonizeExpression expr idx
+   in (ArAlpha alpha expr', idx')
 
 canonize :: [Rewritten] -> [Rewritten]
 canonize [] = []
diff --git a/src/Condition.hs b/src/Condition.hs
--- a/src/Condition.hs
+++ b/src/Condition.hs
@@ -50,9 +50,9 @@
   choice
     [ do
         _ <- symbol "index" >> lparen
-        attr <- _attribute phiParser
+        alpha <- _alpha phiParser
         _ <- rparen
-        return (Y.Index attr)
+        return (Y.Index alpha)
     , do
         _ <- symbol "length" >> lparen
         bd <- _binding phiParser
@@ -108,11 +108,6 @@
         cond <- condition
         _ <- rparen
         return (Y.Not cond)
-    , do
-        _ <- symbol "alpha" >> lparen
-        attr <- _attribute phiParser
-        _ <- rparen
-        return (Y.Alpha attr)
     , do
         _ <- symbol "eq" >> lparen
         left <- comparable
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -52,7 +52,7 @@
 formation bds ctx = do
   let (lambda, bds') = maybeLambda bds
   case lambda of
-    Just (BiLambda func) -> Just <$> atom func (ExFormation bds') ctx
+    Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') ctx
     _ -> pure Nothing
   where
     maybeLambda :: [Binding] -> (Maybe Binding, [Binding])
@@ -65,7 +65,7 @@
             [bd] -> (Just bd, rest)
             _ -> (Nothing, bds)
 
--- Resolve dispatch from global object (Q.tau) for PHI Morphing rule.
+-- Resolve dispatch from global object (Q.tau) for ROOT Morphing rule.
 -- Here tau is the name of the attribute which is taken from Q
 -- and expr is expression which program refers to.
 -- If Q refers to formation which contains binding with attribute == tau -
@@ -81,11 +81,12 @@
       BiTau (AtLabel attr) expr' -> if attr == tau then Just expr' else boundExpr bds
       _ -> boundExpr bds
 
--- The Morphing function 𝕄 maps objects to primitives. It is driven by the
+-- The Morphing function 𝕄 maps normal forms to primitives. It is driven by the
 -- ordered rules from 'morphing.yaml': the first matching rule's 'then' outcome
 -- either stops with a primitive ('MoStop') or keeps morphing ('MoMorph'). When
--- the morphed argument is a normalization ('MaNormalize', the 'Mnmz' rule), the
--- rewriter runs and its individual steps are spliced into the chain.
+-- the morphed argument is a normalization ('MaNormalize', as in the 'lambda' and
+-- 'root' rules), the rewriter runs over the rule's product and its individual
+-- steps are spliced into the chain before morphing continues.
 morph :: Morphed -> DataizeContext -> IO Morphed
 morph (expr, seq) ctx@DataizeContext{..} = do
   matched <- firstMatch Y.morphingRules
@@ -104,7 +105,7 @@
     -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which
     -- 'matchExpressionWithRule'' runs before 'where').
     asRule :: Y.MorphRule -> Y.Rule
-    asRule rule = Y.Rule rule.name rule.description rule.match ExGlobal Nothing rule.where_ rule.when
+    asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when
     apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed
     apply (Y.MoStop result) name subst = do
       built <- buildExpressionThrows result subst
@@ -114,27 +115,14 @@
       built <- buildExpressionThrows result subst
       seq' <- leadsTo seq name built ctx
       morph (built, seq') ctx
-    -- 𝕄(𝒩(e)) delegates to the normalization rewriter and splices its
-    -- individual steps (alpha, copy, dot, …) into the chain before morphing on.
-    apply (Y.MoMorph (Y.MaNormalize arg)) _ subst = do
+    -- 𝕄(𝒩(e)) records the producing step, then delegates to the normalization
+    -- rewriter and splices its individual steps (alpha, copy, dot, …) into the
+    -- chain before morphing on the resulting normal form.
+    apply (Y.MoMorph (Y.MaNormalize arg)) name subst = do
       built <- buildExpressionThrows arg subst
-      prog' <- withLocatedExpression _locator built _program
-      (rewrittens, _) <- rewrite prog' normalizationRules (switchContext ctx)
-      let (rw :| rws) = NE.reverse rewrittens
-          seq' = rw :| rws <> NE.tail seq
-      expr' <- locatedExpression _locator (fst rw)
+      labelled <- leadsTo seq name built ctx
+      (expr', seq') <- normalized built labelled ctx
       morph (expr', seq') ctx
-    switchContext :: DataizeContext -> RewriteContext
-    switchContext DataizeContext{..} =
-      RewriteContext
-        _locator
-        _maxDepth
-        _maxCycles
-        _depthSensitive
-        _buildTerm
-        MtDisabled
-        Nothing
-        _saveStep
 
 dataize :: DataizeContext -> IO Dataized
 dataize ctx@DataizeContext{..} = do
@@ -162,7 +150,7 @@
         (subst : _) -> pure (Just (rule, subst))
         [] -> firstMatch rest
     asRule :: Y.DataizeRule -> Y.Rule
-    asRule rule = Y.Rule rule.name rule.description rule.match ExGlobal Nothing rule.where_ rule.when
+    asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when
     apply :: Y.DataizeRule -> Subst -> IO Dataized
     apply rule subst = case rule.then_ of
       Y.DoData bytes -> do
@@ -179,6 +167,14 @@
         built <- buildExpressionThrows arg subst
         (morphed, seq') <- morph (built, seq) ctx
         dataize' (morphed, seq') ctx
+      -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization), then
+      -- normalizes its result back to a normal form before dataizing on, so 𝔻
+      -- only ever sees normal forms.
+      Y.DoDataize (Y.DaNormalize arg) -> do
+        built <- buildExpressionThrows arg subst
+        labelled <- leadsTo seq (operation rule) built ctx
+        (normal, seq') <- normalized built labelled ctx
+        dataize' (normal, seq') ctx
     operation :: Y.DataizeRule -> String
     operation rule = case rule.where_ of
       Just (extra : _) -> Y.function extra
@@ -189,14 +185,35 @@
   prog' <- withLocatedExpression _locator expr prog
   pure ((prog', Nothing) :| (prog, Just rule) : rest)
 
+-- Reduce 'expr' to its normal form through the normalization rewriter,
+-- splicing the individual steps (alpha, copy, dot, …) into the chain and
+-- returning the normalized expression together with the extended sequence.
+normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten)
+normalized expr seq ctx@DataizeContext{..} = do
+  prog' <- withLocatedExpression _locator expr _program
+  (rewrittens, _) <- rewrite prog' normalizationRules (rewriteContext ctx)
+  let (rw :| rws) = NE.reverse rewrittens
+      seq' = rw :| rws <> NE.tail seq
+  expr' <- locatedExpression _locator (fst rw)
+  pure (expr', seq')
+
+-- Switch the dataization context to a rewriting context for normalization,
+-- disabling the must-checker and breakpoints.
+rewriteContext :: DataizeContext -> RewriteContext
+rewriteContext DataizeContext{..} =
+  RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep
+
 -- Synthetic dataize function for internal usage inside atoms
 -- Here we modify original program from context by adding new binding
--- which refers to expression we want to dataize.
+-- which refers to expression we want to dataize. As a caller of 𝔻, it first
+-- reduces the expression to a normal form, since 𝔻 only accepts normal forms.
 _dataize :: Expression -> DataizeContext -> IO (Maybe Bytes)
 _dataize expr ctx@DataizeContext{_buildTerm = buildTerm, _program = Program (ExFormation bds)} = do
   (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty
   let prog = Program (ExFormation (BiTau attr expr : bds))
-  (bts, _) <- dataize' (expr, (prog, Nothing) :| []) ctx{_program = prog}
+      ctx' = ctx{_program = prog}
+  (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx'
+  (bts, _) <- dataize' (normal, seq) ctx'
   pure bts
 _dataize _ _ = throwIO (userError "Can't call _dataize from atoms with non-formation program")
 
diff --git a/src/Encoding.hs b/src/Encoding.hs
--- a/src/Encoding.hs
+++ b/src/Encoding.hs
@@ -33,6 +33,7 @@
   toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) space eol tab (toASCII args) eol' tab' indent
   toASCII EX_META{meta = META{hd = N, ..}} = EX_META (META EXCL N' rest)
   toASCII EX_META{meta = META{hd = K, ..}} = EX_META (META EXCL K' rest)
+  toASCII EX_META{meta = META{hd = P, ..}} = EX_META (META EXCL P' rest)
   toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))
   toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta
   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)
@@ -73,6 +74,7 @@
   toASCII AT_ALPHA{..} = AT_ALPHA ALPHA' idx
   toASCII AT_PHI{} = AT_PHI AT
   toASCII AT_RHO{} = AT_RHO CARET
+  toASCII AT_META{meta = META{hd = ETA, ..}} = AT_META (META EXCL H rest)
   toASCII AT_META{..} = AT_META (META EXCL A (rest meta))
   toASCII attr = attr
 
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -211,10 +211,9 @@
     join' :: [Binding] -> Set.Set Attribute -> IO [Binding]
     join' [] _ = pure []
     join' (bd : bds) attrs =
-      case attributesFromBindings [bd] of
-        [attr] ->
-          if Set.member attr attrs
-            then
+      case attributeFromBinding bd of
+        Just attr
+          | Set.member attr attrs ->
               if attr == AtRho || attr == AtDelta || attr == AtLambda
                 then join' bds attrs
                 else do
@@ -223,8 +222,8 @@
                     BiVoid _ -> BiVoid <$> freshAttr
                     other -> pure other
                   (new :) <$> join' bds attrs
-            else (bd :) <$> join' bds (Set.insert attr attrs)
-        _ -> (bd :) <$> join' bds attrs
+          | otherwise -> (bd :) <$> join' bds (Set.insert attr attrs)
+        Nothing -> (bd :) <$> join' bds attrs
     freshAttr :: IO Attribute
     freshAttr = do
       term <- _randomTau [] subst
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -57,7 +57,7 @@
   }
 
 defaultLatexContext :: LatexContext
-defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExGlobal Nothing Nothing Nothing
+defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExRoot Nothing Nothing Nothing
 
 defaultMeetPopularity :: Int
 defaultMeetPopularity = 50
@@ -77,13 +77,16 @@
       let matched = if countNodes ex >= len then map (const ex) (matchProgram ex prog) else []
        in matched ++ case ex of
             ExDispatch ex' _ -> meetInExpression ex' prog
-            ExApplication ex' (BiTau _ arg) -> meetInExpression ex' prog ++ meetInExpression arg prog
+            ExApplication ex' arg -> meetInExpression ex' prog ++ meetInExpression (argExpr arg) prog
             ExFormation bds -> meetInBindings bds prog
             _ -> []
     meetInBindings :: [Binding] -> Program -> [Expression]
     meetInBindings [] _ = []
     meetInBindings (BiTau _ ex : bds) prog = meetInExpression ex prog ++ meetInBindings bds prog
     meetInBindings (_ : bds) prog = meetInBindings bds prog
+    argExpr :: Argument -> Expression
+    argExpr (ArTau _ ex) = ex
+    argExpr (ArAlpha _ ex) = ex
 
 {- | Here we're trying to compress sequence of programs with \phiMeet{} and \phiAgain LaTeX functions.
 We process the sequence of programs and trying to find all expressions in first program which are present
@@ -165,7 +168,7 @@
    in if _compress then zip (meetInPrograms progs ctx) rules else rewrittens
 
 rewrittensToLatex :: Rewrittens' -> LatexContext -> IO String
-rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExGlobal} =
+rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExRoot} =
   pure
     ( concat
         [ preamble ctx
@@ -267,8 +270,11 @@
   toLaTeX E = E'
   toLaTeX N = N'
   toLaTeX K = K'
+  toLaTeX P = P'
   toLaTeX A = TAU'
   toLaTeX TAU = TAU'
+  toLaTeX ETA = ETA'
+  toLaTeX H = ETA'
   toLaTeX B = B'
   toLaTeX D = D'
   toLaTeX mh = mh
@@ -372,6 +378,7 @@
     dataizeOutcome :: Y.DataizeOutcome -> String
     dataizeOutcome (Y.DoDataize (Y.DaExpr expr)) = dataize (renderToLatex (expressionToCST expr) defaultLatexContext)
     dataizeOutcome (Y.DoDataize (Y.DaMorph expr)) = dataize (morph (renderToLatex (expressionToCST expr) defaultLatexContext))
+    dataizeOutcome (Y.DoDataize (Y.DaNormalize expr)) = dataize (normalize (renderToLatex (expressionToCST expr) defaultLatexContext))
     dataizeOutcome (Y.DoData bytes) = T.unpack (render (toLaTeX (toCST' bytes :: BYTES)))
     dataizeOutcome Y.DoNothing = "\\varnothing"
 
diff --git a/src/Locator.hs b/src/Locator.hs
--- a/src/Locator.hs
+++ b/src/Locator.hs
@@ -26,7 +26,7 @@
   show CanNotFindObjectByLocator{..} = printf "Can't find object by locator: '%s'" (printExpression fqn)
 
 locatedExpression :: Expression -> Program -> IO Expression
-locatedExpression ExGlobal (Program expr) = pure expr
+locatedExpression ExRoot (Program expr) = pure expr
 locatedExpression locator (Program expr) = case fqnToAttrs locator of
   Just attrs -> locatedExpression' expr attrs
   _ -> invalidLocator locator
@@ -42,7 +42,7 @@
     locatedExpression' _ _ = cantFindBy locator
 
 withLocatedExpression :: Expression -> Expression -> Program -> IO Program
-withLocatedExpression ExGlobal tgt _ = pure (Program tgt)
+withLocatedExpression ExRoot tgt _ = pure (Program tgt)
 withLocatedExpression locator target (Program expr) = case fqnToAttrs locator of
   Just attrs -> Program <$> withLocatedExpression' expr attrs
   _ -> invalidLocator locator
diff --git a/src/Matcher.hs b/src/Matcher.hs
--- a/src/Matcher.hs
+++ b/src/Matcher.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
@@ -9,12 +11,13 @@
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Maybe (catMaybes)
-import Data.Text (Text)
+import Data.Text (Text, isPrefixOf)
 
 -- Meta value
 -- The right part of substitution
 data MetaValue
   = MvAttribute Attribute -- !a
+  | MvAlpha Alpha -- !h
   | MvBytes Bytes -- !b
   | MvBindings [Binding] -- !B
   | MvFunction Text -- !F
@@ -25,7 +28,7 @@
 -- Tail operation after expression
 -- Dispatch or application
 data Tail
-  = TaApplication Binding -- BiTau only
+  = TaApplication Argument -- application argument
   | TaDispatch Attribute
   deriving (Eq, Show)
 
@@ -68,19 +71,33 @@
   | ptn == tgt = [substEmpty]
   | otherwise = []
 
+matchAlpha :: Alpha -> Alpha -> [Subst]
+matchAlpha (AlMeta meta) tgt = [substSingle meta (MvAlpha tgt)]
+matchAlpha ptn tgt
+  | ptn == tgt = [substEmpty]
+  | otherwise = []
+
+matchFunction :: Function -> Function -> [Subst]
+matchFunction (FnMeta meta) (Function name) = [substSingle meta (MvFunction name)]
+matchFunction ptn tgt
+  | ptn == tgt = [substEmpty]
+  | otherwise = []
+
 matchBinding :: Binding -> Binding -> [Subst]
 matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr
 matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) = [substSingle meta (MvBytes tdata)]
 matchBinding (BiDelta pdata) (BiDelta tdata)
   | pdata == tdata = [substEmpty]
   | otherwise = []
-matchBinding (BiLambda pFunc) (BiLambda tFunc)
-  | pFunc == tFunc = [substEmpty]
-  | otherwise = []
-matchBinding (BiMetaLambda meta) (BiLambda tFunc) = [substSingle meta (MvFunction tFunc)]
+matchBinding (BiLambda pFunc) (BiLambda tFunc) = matchFunction pFunc tFunc
 matchBinding (BiTau pattr pexp) (BiTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)
 matchBinding _ _ = []
 
+matchArgument :: Argument -> Argument -> [Subst]
+matchArgument (ArTau pattr pexp) (ArTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)
+matchArgument (ArAlpha palpha pexp) (ArAlpha talpha texp) = combineMany (matchAlpha palpha talpha) (matchExpression' pexp texp)
+matchArgument _ _ = []
+
 -- Match bindings with ordering
 matchBindings :: [Binding] -> [Binding] -> [Subst]
 matchBindings [] [] = [substEmpty]
@@ -110,20 +127,22 @@
         ExDispatch expr attr -> do
           (substs, tails) <- tailExpressionsReversed ptn' expr
           Just (substs, TaDispatch attr : tails)
-        ExApplication expr tau -> do
+        ExApplication expr arg -> do
           (substs, tails) <- tailExpressionsReversed ptn' expr
-          Just (substs, TaApplication tau : tails)
+          Just (substs, TaApplication arg : tails)
         _ -> Just ([], [])
       substs -> Just (substs, [])
 
 matchExpression' :: MatchExpressionFunc
-matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]
-matchExpression' ExThis ExThis = [substEmpty]
-matchExpression' ExGlobal ExGlobal = [substEmpty]
+matchExpression' (ExMeta meta) tgt
+  | "p" `isPrefixOf` meta = [substSingle meta (MvExpression tgt) | primitive tgt]
+  | otherwise = [substSingle meta (MvExpression tgt)]
+matchExpression' ExXi ExXi = [substEmpty]
+matchExpression' ExRoot ExRoot = [substEmpty]
 matchExpression' ExTermination ExTermination = [substEmpty]
 matchExpression' (ExFormation pbs) (ExFormation tbs) = matchBindings pbs tbs
 matchExpression' (ExDispatch pexp pattr) (ExDispatch texp tattr) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)
-matchExpression' (ExApplication pexp pbd) (ExApplication texp tbd) = combineMany (matchExpression' pexp texp) (matchBinding pbd tbd)
+matchExpression' (ExApplication pexp parg) (ExApplication texp targ) = combineMany (matchExpression' pexp texp) (matchArgument parg targ)
 matchExpression' (ExMetaTail expr meta) tgt = case tailExpressions expr tgt of
   ([], _) -> []
   (substs, tails) -> combineMany substs [substSingle meta (MvTail tails)]
@@ -140,6 +159,10 @@
 matchBindingExpression (BiTau _ expr) ptn = matchExpressionDeep ptn expr
 matchBindingExpression _ _ = []
 
+matchArgumentExpression :: Argument -> Expression -> [Subst]
+matchArgumentExpression (ArTau _ expr) ptn = matchExpressionDeep ptn expr
+matchArgumentExpression (ArAlpha _ expr) ptn = matchExpressionDeep ptn expr
+
 -- Match expression with deep nested expression(s) matching
 matchExpressionDeep :: MatchExpressionFunc
 matchExpressionDeep ptn tgt =
@@ -147,7 +170,7 @@
       deep = case tgt of
         ExFormation bds -> concatMap (`matchBindingExpression` ptn) bds
         ExDispatch expr _ -> matchExpressionDeep ptn expr
-        ExApplication expr tau -> matchExpressionDeep ptn expr ++ matchBindingExpression tau ptn
+        ExApplication expr arg -> matchExpressionDeep ptn expr ++ matchArgumentExpression arg ptn
         _ -> []
    in matched ++ deep
 
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -78,17 +78,17 @@
   show DirectoryDoesNotExist{..} = printf "Directory '%s' does not exist" _dir
 
 matchBaseObject :: Expression -> Maybe T.Text
-matchBaseObject (ExDispatch ExGlobal (AtLabel label)) = Just label
+matchBaseObject (ExDispatch ExRoot (AtLabel label)) = Just label
 matchBaseObject _ = Nothing
 
 pattern BaseObject :: T.Text -> Expression
 pattern BaseObject label <- (matchBaseObject -> Just label)
   where
-    BaseObject label = ExDispatch ExGlobal (AtLabel label)
+    BaseObject label = ExDispatch ExRoot (AtLabel label)
 
 -- Minimal matcher function (required for view pattern)
 matchDataObject :: Expression -> Maybe (T.Text, Bytes)
-matchDataObject (ExApplication outer (BiTau (AtAlpha 0) inner)) = case (matchOuter outer, matchInner inner) of
+matchDataObject (ExApplication outer (ArAlpha (Alpha 0) inner)) = case (matchOuter outer, matchInner inner) of
   (Just label, Just bts) -> Just (label, bts)
   _ -> Nothing
   where
@@ -100,7 +100,7 @@
     matchInner (ExPhiAgain _ _ inner') = matchInner inner'
     matchInner inner' = matchInner' inner'
     matchInner' :: Expression -> Maybe Bytes
-    matchInner' (ExApplication bytes (BiTau (AtAlpha 0) formation)) = case (matchesBytes bytes, matchFormation formation) of
+    matchInner' (ExApplication bytes (ArAlpha (Alpha 0) formation)) = case (matchesBytes bytes, matchFormation formation) of
       (True, Just bts) -> Just bts
       _ -> Nothing
     matchInner' _ = Nothing
@@ -126,12 +126,12 @@
     DataObject label bts =
       ExApplication
         (BaseObject label)
-        ( BiTau
-            (AtAlpha 0)
+        ( ArAlpha
+            (Alpha 0)
             ( ExApplication
                 (BaseObject "bytes")
-                ( BiTau
-                    (AtAlpha 0)
+                ( ArAlpha
+                    (Alpha 0)
                     (ExFormation [BiDelta bts, BiVoid AtRho])
                 )
             )
@@ -140,11 +140,10 @@
 -- Extract attribute from binding
 attributeFromBinding :: Binding -> Maybe Attribute
 attributeFromBinding (BiTau attr _) = Just attr
+attributeFromBinding (BiVoid attr) = Just attr
 attributeFromBinding (BiDelta _) = Just AtDelta
 attributeFromBinding (BiLambda _) = Just AtLambda
-attributeFromBinding (BiVoid attr) = Just attr
 attributeFromBinding (BiMeta _) = Nothing
-attributeFromBinding (BiMetaLambda _) = Just AtLambda
 
 -- Extract attributes from bindings
 attributesFromBindings :: [Binding] -> [Attribute]
@@ -161,7 +160,7 @@
 
 -- Check if given binding list consists of unique attributes
 uniqueBindings :: [Binding] -> Either String [Binding]
-uniqueBindings bds = case maybeDuplicatedAttribute bds Set.empty of
+uniqueBindings bds = case duplicated bds Set.empty of
   Just attr ->
     Left
       ( printf
@@ -171,19 +170,13 @@
       )
   _ -> Right bds
   where
-    maybeDuplicatedAttribute :: [Binding] -> Set.Set Attribute -> Maybe Attribute
-    maybeDuplicatedAttribute [] = const Nothing
-    maybeDuplicatedAttribute ((BiTau attr _) : rest) = checkAttr attr rest
-    maybeDuplicatedAttribute (BiVoid attr : rest) = checkAttr attr rest
-    maybeDuplicatedAttribute (BiLambda _ : rest) = checkAttr AtLambda rest
-    maybeDuplicatedAttribute (BiMetaLambda _ : rest) = checkAttr AtLambda rest
-    maybeDuplicatedAttribute (BiDelta _ : rest) = checkAttr AtDelta rest
-    maybeDuplicatedAttribute (BiMeta _ : rest) = maybeDuplicatedAttribute rest
-
-    checkAttr :: Attribute -> [Binding] -> Set.Set Attribute -> Maybe Attribute
-    checkAttr attr rest acc
-      | attr `Set.member` acc = Just attr
-      | otherwise = maybeDuplicatedAttribute rest (Set.insert attr acc)
+    duplicated :: [Binding] -> Set.Set Attribute -> Maybe Attribute
+    duplicated [] _ = Nothing
+    duplicated (bd : rest) seen = case attributeFromBinding bd of
+      Just attr
+        | attr `Set.member` seen -> Just attr
+        | otherwise -> duplicated rest (Set.insert attr seen)
+      Nothing -> duplicated rest seen
 
 -- Add void rho binding to the end of the list of any rho binding is not present
 withVoidRho :: [Binding] -> [Binding]
@@ -206,25 +199,29 @@
 recoverFormations :: Expression -> Expression
 recoverFormations (ExFormation bindings) = ExFormation (withVoidRho (map recoverFormations' bindings))
 recoverFormations (ExDispatch expr attr) = ExDispatch (recoverFormations expr) attr
-recoverFormations (ExApplication expr binding) = ExApplication (recoverFormations expr) (recoverFormations' binding)
+recoverFormations (ExApplication expr arg) = ExApplication (recoverFormations expr) (recoverArgument arg)
 recoverFormations expr = expr
 
 recoverFormations' :: Binding -> Binding
 recoverFormations' (BiTau attr expr) = BiTau attr (recoverFormations expr)
 recoverFormations' binding = binding
 
+recoverArgument :: Argument -> Argument
+recoverArgument (ArTau attr expr) = ArTau attr (recoverFormations expr)
+recoverArgument (ArAlpha alpha expr) = ArAlpha alpha (recoverFormations expr)
+
 -- Transform dispatch to list of attributes
--- >>> fqnToAttrs (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))
+-- >>> fqnToAttrs (ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))
 -- Just [org,eolang,number]
 -- >>> fqnToAttrs (ExFormation [])
 -- Nothing
--- >>> fqnToAttrs ExGlobal
+-- >>> fqnToAttrs ExRoot
 -- Just []
 fqnToAttrs :: Expression -> Maybe [Attribute]
 fqnToAttrs expr = fqnToAttrs' expr <&> reverse
   where
     fqnToAttrs' :: Expression -> Maybe [Attribute]
-    fqnToAttrs' ExGlobal = Just []
+    fqnToAttrs' ExRoot = Just []
     fqnToAttrs' (ExDispatch ex at) = fqnToAttrs' ex <&> (:) at
     fqnToAttrs' _ = Nothing
 
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -12,6 +12,7 @@
   , parseExpressionThrows
   , parseAttribute
   , parseAttributeThrows
+  , parseAlpha
   , parseNumber
   , parseNumberThrows
   , parseBinding
@@ -47,13 +48,14 @@
 
 data PhiParser = PhiParser
   { _attribute :: Parser Attribute
+  , _alpha :: Parser Alpha
   , _binding :: Parser Binding
   , _expression :: Parser Expression
   , _string :: Parser String
   }
 
 phiParser :: PhiParser
-phiParser = PhiParser fullAttribute binding expression quotedStr
+phiParser = PhiParser attribute alpha binding expression quotedStr
 
 instance Show ParserException where
   show CouldNotParseProgram{..} = printf "Couldn't parse given phi program, cause: %s" message
@@ -239,13 +241,12 @@
         [(n, "")] -> return (chr n)
         _ -> fail ("Invalid hex escape: \\x" ++ digits)
 
-tauBinding :: Parser Attribute -> Parser Binding
-tauBinding attr = do
-  attr' <- attr
+tauValue :: Parser Expression
+tauValue =
   choice
     [ try $ do
         _ <- arrow
-        BiTau attr' <$> expression
+        expression
     , do
         _ <- symbol "("
         voids <-
@@ -258,12 +259,15 @@
         _ <- arrow
         bs <- formationBindings
         bds <- validatedBindings (voids ++ bs)
-        return (BiTau attr' (ExFormation (withVoidRho bds)))
+        return (ExFormation (withVoidRho bds))
     ]
   where
     rb :: Parser String
     rb = symbol ")"
 
+tauBinding :: Parser Attribute -> Parser Binding
+tauBinding attr = BiTau <$> attr <*> tauValue
+
 metaBinding :: Parser Binding
 metaBinding = BiMeta <$> meta' 'B' "𝐵"
 
@@ -290,10 +294,10 @@
     , try metaBinding
     , try $ do
         _ <- lambda
-        BiLambda . T.pack <$> function
+        BiLambda . Function . T.pack <$> function
     , do
         _ <- lambda
-        BiMetaLambda <$> meta 'F'
+        BiLambda . FnMeta <$> meta 'F'
     ]
     <?> "binding"
 
@@ -326,22 +330,30 @@
     ]
     <?> "attribute"
 
--- full attribute
--- 1. label
--- 2. meta
--- 3. rho
--- 4. phi
--- 5. alpha
-fullAttribute :: Parser Attribute
-fullAttribute =
+-- alpha
+-- 1. index: ~0, α0
+-- 2. meta: !h, 𝜂
+alpha :: Parser Alpha
+alpha =
   choice
-    [ attribute
-    , do
+    [ do
         _ <- choice [symbol "~", symbol "α"]
-        AtAlpha <$> lexeme L.decimal
+        Alpha <$> lexeme L.decimal
+    , AlMeta <$> meta' 'h' "𝜂"
     ]
-    <?> "full attribute"
+    <?> "alpha"
 
+-- application argument
+-- 1. tau: <attribute> ↦ <expression>
+-- 2. alpha: <alpha> ↦ <expression>
+argument :: Parser Argument
+argument =
+  choice
+    [ try (ArAlpha <$> alpha <*> tauValue)
+    , ArTau <$> attribute <*> tauValue
+    ]
+    <?> "argument"
+
 validatedBindings :: [Binding] -> Parser [Binding]
 validatedBindings bds = case uniqueBindings bds of
   Left msg -> fail msg
@@ -376,10 +388,10 @@
         return (ExFormation (withVoidRho bs))
     , do
         _ <- choice [symbol "$", symbol "ξ"]
-        return ExThis
+        return ExXi
     , do
         _ <- global
-        return ExGlobal
+        return ExRoot
     , do
         _ <- choice [symbol "T", symbol "⊥"]
         return ExTermination
@@ -388,11 +400,12 @@
     , try (ExMeta <$> meta' 'e' "𝑒")
     , try (ExMeta <$> meta' 'n' "𝑛")
     , try (ExMeta <$> meta' 'k' "𝑘")
-    , ExDispatch ExThis <$> attribute
+    , try (ExMeta <$> meta' 'p' "𝑝")
+    , ExDispatch ExXi <$> attribute
     ]
     <?> "expression head"
 
-application :: Expression -> [Binding] -> Expression
+application :: Expression -> [Argument] -> Expression
 application = foldl ExApplication
 
 -- tail optional part of application
@@ -411,17 +424,17 @@
             , do
                 guard
                   ( case expr of
-                      ExThis -> False
-                      ExGlobal -> False
+                      ExXi -> False
+                      ExRoot -> False
                       _ -> True
                   )
                 _ <- symbol "("
                 bds <-
                   choice
-                    [ try $ tauBinding fullAttribute `sepBy1` symbol ","
+                    [ try $ argument `sepBy1` symbol ","
                     , do
                         exprs <- expression `sepBy1` symbol ","
-                        return (zipWith (BiTau . AtAlpha) [0 ..] exprs) -- \idx expr -> BiTau (AtAlpha idx) expr
+                        return (zipWith (ArAlpha . Alpha) [0 ..] exprs)
                     ]
                 _ <- symbol ")"
                 return (application expr bds)
@@ -491,7 +504,10 @@
   Left err -> throwIO (CouldNotParseNumber err)
 
 parseAttribute :: String -> Either String Attribute
-parseAttribute = parse' "attribute" fullAttribute
+parseAttribute = parse' "attribute" attribute
+
+parseAlpha :: String -> Either String Alpha
+parseAlpha = parse' "alpha" alpha
 
 parseAttributeThrows :: String -> IO Attribute
 parseAttributeThrows attr = case parseAttribute attr of
diff --git a/src/Printer.hs b/src/Printer.hs
--- a/src/Printer.hs
+++ b/src/Printer.hs
@@ -10,6 +10,7 @@
   , printExpression
   , printExpression'
   , printAttribute
+  , printAlpha
   , printBinding
   , printBytes
   , printExtraArg
@@ -62,12 +63,23 @@
   let (_, encoding, _, _) = defaultPrintConfig
    in printAttribute' att encoding
 
+printAlpha' :: Alpha -> Encoding -> String
+printAlpha' index encoding = T.unpack $ render (withEncoding encoding (toCST index (0, NO_EOL) :: ATTRIBUTE))
+
+printAlpha :: Alpha -> String
+printAlpha index =
+  let (_, encoding, _, _) = defaultPrintConfig
+   in printAlpha' index encoding
+
 printBinding' :: Binding -> PrintConfig -> String
 printBinding' bd = printExpression' (ExFormation [bd])
 
 printBinding :: Binding -> String
 printBinding bd = printBinding' bd defaultPrintConfig
 
+printArgument' :: Argument -> PrintConfig -> String
+printArgument' arg (_, encoding, _, _) = T.unpack $ render (withEncoding encoding (toCST arg (0, NO_EOL) :: PAIR))
+
 printBytes :: Bytes -> String
 printBytes bts = T.unpack $ render (toCST bts (0, NO_EOL) :: BYTES)
 
@@ -81,11 +93,12 @@
 printExtraArg arg = printExtraArg' arg defaultPrintConfig
 
 printTail :: Tail -> PrintConfig -> String
-printTail (TaApplication bd) config = "(" <> printBinding' bd config <> ")"
+printTail (TaApplication arg) config = "(" <> printArgument' arg config <> ")"
 printTail (TaDispatch att) (_, encoding, _, _) = "." <> printAttribute' att encoding
 
 printMetaValue :: MetaValue -> PrintConfig -> String
 printMetaValue (MvAttribute att) (_, encoding, _, _) = printAttribute' att encoding
+printMetaValue (MvAlpha index) (_, encoding, _, _) = printAlpha' index encoding
 printMetaValue (MvExpression ex) config = printExpression' ex config
 printMetaValue (MvBytes bts) _ = printBytes bts
 printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -117,9 +117,14 @@
   render N' = "n"
   render K = "𝑘"
   render K' = "k"
+  render P = "𝑝"
+  render P' = "p"
   render A = "a"
   render TAU = "𝜏"
   render TAU' = "\\tau"
+  render ETA = "𝜂"
+  render ETA' = "\\eta"
+  render H = "h"
   render B = "𝐵"
   render B' = "B"
   render D = "δ"
diff --git a/src/Replacer.hs b/src/Replacer.hs
--- a/src/Replacer.hs
+++ b/src/Replacer.hs
@@ -42,6 +42,14 @@
   let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) ctx func
    in (bd : bds', ptns', repls')
 
+replaceArgument :: ReplaceState Argument -> ReplaceContext -> ReplaceExpressionFunc' -> ReplaceState Argument
+replaceArgument (ArTau attr expr, ptns, repls) ctx func =
+  let (expr', ptns', repls') = func (expr, ptns, repls) ctx
+   in (ArTau attr expr', ptns', repls')
+replaceArgument (ArAlpha alpha expr, ptns, repls) ctx func =
+  let (expr', ptns', repls') = func (expr, ptns, repls) ctx
+   in (ArAlpha alpha expr', ptns', repls')
+
 replaceExpression' :: ReplaceExpressionFunc'
 replaceExpression' state@(expr, ptns@(ptn : _ptns), repls@(repl : _repls)) ctx =
   if expr == ptn
@@ -50,11 +58,10 @@
       ExDispatch inner attr ->
         let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) ctx
          in (ExDispatch expr' attr, ptns', repls')
-      ExApplication inner tau ->
+      ExApplication inner arg ->
         let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) ctx
-         in case replaceBindings ([tau], ptns', repls') ctx replaceExpression' of
-              ([tau'], ptns'', repls'') -> (ExApplication expr' tau', ptns'', repls'')
-              (bds', _, _) -> error $ "Expected single binding, got " ++ show (length bds')
+            (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') ctx replaceExpression'
+         in (ExApplication expr' arg', ptns'', repls'')
       ExFormation bds ->
         let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) ctx replaceExpression'
          in (ExFormation bds', ptns', repls')
@@ -91,10 +98,10 @@
           ExDispatch inner attr ->
             let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls) ctx
              in (ExDispatch expr' attr, ptns', repls')
-          ExApplication inner (BiTau attr arg) ->
+          ExApplication inner arg ->
             let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls) ctx
-                (expr'', ptns'', repls'') = replaceExpressionFast' (arg, ptns', repls') ctx
-             in (ExApplication expr' (BiTau attr expr''), ptns'', repls'')
+                (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') ctx replaceExpressionFast'
+             in (ExApplication expr' arg', ptns'', repls'')
           _ -> state
 
 replaceExpression :: ReplaceExpressionFunc
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -50,11 +50,11 @@
 
 -- Returns True if given expression is in the normal form
 isNF :: Expression -> RuleContext -> Bool
-isNF ExThis _ = True
-isNF ExGlobal _ = True
+isNF ExXi _ = True
+isNF ExRoot _ = True
 isNF ExTermination _ = True
-isNF (ExDispatch ExThis _) _ = True
-isNF (ExDispatch ExGlobal _) _ = True
+isNF (ExDispatch ExXi _) _ = True
+isNF (ExDispatch ExRoot _) _ = True
 isNF (ExDispatch ExTermination _) _ = False -- dd rule
 isNF (ExApplication ExTermination _) _ = False -- dc rule
 isNF (ExFormation []) _ = True
@@ -96,10 +96,9 @@
 _in :: Attribute -> Binding -> Subst -> RuleContext -> IO [Subst]
 _in attr binding subst _ =
   case (buildAttribute attr subst, buildBinding binding subst) of
-    (Right attr, Right bds) -> pure [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []
+    (Right attr, Right bds) -> pure [subst | attrInBindings attr bds]
     (_, _) -> pure []
   where
-    -- Check if given attribute is present in given binding
     attrInBindings :: Attribute -> [Binding] -> Bool
     attrInBindings attr (bd : bds) = attrInBinding attr bd || attrInBindings attr bds
       where
@@ -111,13 +110,6 @@
         attrInBinding _ _ = False
     attrInBindings _ _ = False
 
-_alpha :: Attribute -> Subst -> RuleContext -> IO [Subst]
-_alpha (AtAlpha _) subst _ = pure [subst]
-_alpha (AtMeta name) (Subst mp) _ = case M.lookup name mp of
-  Just (MvAttribute (AtAlpha _)) -> pure [Subst mp]
-  _ -> pure []
-_alpha _ _ _ = pure []
-
 _eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]
 _eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of
   (Just left_, Just right_) -> pure [subst | left_ == right_]
@@ -125,10 +117,10 @@
   where
     -- Convert Number to Int
     numToInt :: Y.Number -> Subst -> Maybe Int
-    numToInt (Y.Index (AtMeta meta)) (Subst mp) = case M.lookup meta mp of
-      Just (MvAttribute (AtAlpha idx)) -> Just idx
+    numToInt (Y.Index (AlMeta meta)) (Subst mp) = case M.lookup meta mp of
+      Just (MvAlpha (Alpha idx)) -> Just idx
       _ -> Nothing
-    numToInt (Y.Index (AtAlpha idx)) _ = Just idx
+    numToInt (Y.Index (Alpha idx)) _ = Just idx
     numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of
       Just (MvBindings bds) -> Just (length bds)
       _ -> Nothing
@@ -139,7 +131,6 @@
     numToInt _ _ = Nothing
     notAsset (BiDelta _) = False
     notAsset (BiLambda _) = False
-    notAsset (BiMetaLambda _) = False
     notAsset _ = True
 _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst]
   where
@@ -189,8 +180,9 @@
   where
     xiFree :: Expression -> Bool
     xiFree (ExFormation _) = True
-    xiFree ExGlobal = True
-    xiFree (ExApplication e (BiTau _ te)) = xiFree e && xiFree te
+    xiFree ExRoot = True
+    xiFree (ExApplication e (ArTau _ te)) = xiFree e && xiFree te
+    xiFree (ExApplication e (ArAlpha _ te)) = xiFree e && xiFree te
     xiFree (ExDispatch e _) = xiFree e
     xiFree _ = False
 
@@ -222,15 +214,6 @@
   Just (MvExpression expr) -> _primitive expr (Subst mp) ctx
   _ -> pure []
 _primitive expr subst _ = pure [subst | primitive expr]
-  where
-    primitive :: Expression -> Bool
-    primitive ExTermination = True
-    primitive (ExFormation bds) = not (any lambda bds)
-    primitive _ = False
-    lambda :: Binding -> Bool
-    lambda (BiLambda _) = True
-    lambda (BiMetaLambda _) = True
-    lambda _ = False
 
 -- Hold if none of the given attributes is present in the union of the
 -- bindings captured by the given binding metas.
@@ -248,7 +231,6 @@
     presentInBinding attr (BiTau battr _) = attr == battr
     presentInBinding attr (BiVoid battr) = attr == battr
     presentInBinding AtLambda (BiLambda _) = True
-    presentInBinding AtLambda (BiMetaLambda _) = True
     presentInBinding AtDelta (BiDelta _) = True
     presentInBinding _ _ = False
 
@@ -257,7 +239,6 @@
 meetCondition' (Y.And conds) = _and conds
 meetCondition' (Y.Not cond) = _not cond
 meetCondition' (Y.In attr binding) = _in attr binding
-meetCondition' (Y.Alpha attr) = _alpha attr
 meetCondition' (Y.Eq left right) = _eq left right
 meetCondition' (Y.NF expr) = _nf expr
 meetCondition' (Y.Absolute expr) = _absolute expr
@@ -342,7 +323,7 @@
       | T.isPrefixOf prefix mt = [mt]
       | otherwise = []
     go (ExFormation bds) = concatMap goBinding bds
-    go (ExApplication e bd) = go e ++ goBinding bd
+    go (ExApplication e arg) = go e ++ goArgument arg
     go (ExDispatch e _) = go e
     go (ExMetaTail e _) = go e
     go (ExPhiMeet _ _ e) = go e
@@ -351,6 +332,9 @@
     goBinding :: Binding -> [T.Text]
     goBinding (BiTau _ e) = go e
     goBinding _ = []
+    goArgument :: Argument -> [T.Text]
+    goArgument (ArTau _ expr) = go expr
+    goArgument (ArAlpha _ expr) = go expr
 
 nfMetaNames :: Expression -> [T.Text]
 nfMetaNames = metaNamesWithPrefix "n"
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -113,7 +113,7 @@
   toSalty EX_META_TAIL{..} = EX_META_TAIL (toSalty expr) meta
   toSalty expr = expr
 
-saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Binding] -> EXPRESSION
+saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Argument] -> EXPRESSION
 saltifyPrimitive base bytes data' tb@TAB{..} rhos =
   let next = TAB (indent + 1)
    in toSalty
diff --git a/src/Tau.hs b/src/Tau.hs
--- a/src/Tau.hs
+++ b/src/Tau.hs
@@ -53,7 +53,7 @@
 
 exprLabels :: Expression -> Set Text
 exprLabels (ExFormation bds) = Set.unions (map bindingLabels bds)
-exprLabels (ExApplication expr bd) = exprLabels expr <> bindingLabels bd
+exprLabels (ExApplication expr arg) = exprLabels expr <> argumentLabels arg
 exprLabels (ExDispatch expr attr) = exprLabels expr <> attrLabel attr
 exprLabels (ExMetaTail expr _) = exprLabels expr
 exprLabels (ExPhiMeet _ _ expr) = exprLabels expr
@@ -64,6 +64,10 @@
 bindingLabels (BiTau attr expr) = attrLabel attr <> exprLabels expr
 bindingLabels (BiVoid attr) = attrLabel attr
 bindingLabels _ = Set.empty
+
+argumentLabels :: Argument -> Set Text
+argumentLabels (ArTau attr expr) = attrLabel attr <> exprLabels expr
+argumentLabels (ArAlpha _ expr) = exprLabels expr
 
 attrLabel :: Attribute -> Set Text
 attrLabel (AtLabel label) = Set.singleton label
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -85,8 +85,8 @@
 object attrs children = NodeElement (element "o" attrs children)
 
 expression :: Expression -> XmirContext -> IO (String, [Node])
-expression ExThis _ = pure (printExpression ExThis, [])
-expression ExGlobal _ = pure (printExpression ExGlobal, [])
+expression ExXi _ = pure (printExpression ExXi, [])
+expression ExRoot _ = pure (printExpression ExRoot, [])
 expression (ExFormation bds) ctx = do
   nested <- nestedBindings bds ctx
   pure ("", nested)
@@ -102,7 +102,7 @@
 expression (DataNumber bytes) XmirContext{..} =
   let bts =
         object
-          [("as", printAttribute (AtAlpha 0)), ("base", "Φ.bytes")]
+          [("as", printAlpha (Alpha 0)), ("base", "Φ.bytes")]
           [object [] [NodeContent (T.pack (printBytes bytes))]]
    in pure
         ( "Φ.number"
@@ -116,7 +116,7 @@
 expression (DataString bytes) XmirContext{..} =
   let bts =
         object
-          [("as", printAttribute (AtAlpha 0)), ("base", "Φ.bytes")]
+          [("as", printAlpha (Alpha 0)), ("base", "Φ.bytes")]
           [object [] [NodeContent (T.pack (printBytes bytes))]]
    in pure
         ( "Φ.string"
@@ -127,16 +127,18 @@
               , bts
               ]
         )
-expression (ExApplication expr (BiTau attr texpr)) ctx = do
+expression (ExApplication expr arg) ctx = do
   (base, children) <- expression expr ctx
   (base', children') <- expression texpr ctx
-  let as = printAttribute attr
-      attrs =
+  let attrs =
         if null base'
           then [("as", as)]
           else [("as", as), ("base", base')]
   pure (base, children ++ [object attrs children'])
-expression (ExApplication (ExFormation bds) tau) _ = throwIO (UnsupportedExpression (ExApplication (ExFormation bds) tau))
+  where
+    (as, texpr) = case arg of
+      ArTau attr value -> (printAttribute attr, value)
+      ArAlpha alpha value -> (printAlpha alpha, value)
 expression expr _ = throwIO (UnsupportedExpression expr)
 
 formationBinding :: Binding -> XmirContext -> IO (Maybe Node)
@@ -165,7 +167,7 @@
   ExFormation _ -> programToXMIR'
   ExApplication _ _ -> programToXMIR'
   ExDispatch _ _ -> programToXMIR'
-  ExGlobal -> programToXMIR'
+  ExRoot -> programToXMIR'
   _ -> throwIO (UnsupportedProgram prog)
   where
     programToXMIR' :: IO Document
@@ -205,13 +207,13 @@
     -- - X: list of package parts
     -- - Y: root object expression
     getPackage :: Expression -> IO ([String], Expression)
-    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiVoid AtRho]) = do
-      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])
+    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]), BiVoid AtRho]) = do
+      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho])
       pure (T.unpack label : pckg, expr')
-    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiLambda "Package", BiVoid AtRho]) = do
-      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])
+    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]), BiLambda (Function "Package"), BiVoid AtRho]) = do
+      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho])
       pure (T.unpack label : pckg, expr')
-    getPackage (ExFormation [BiTau at ex, BiLambda "Package", BiVoid AtRho]) = pure ([], ExFormation [BiTau at ex, BiVoid AtRho])
+    getPackage (ExFormation [BiTau at ex, BiLambda (Function "Package"), BiVoid AtRho]) = pure ([], ExFormation [BiTau at ex, BiVoid AtRho])
     getPackage (ExFormation [bd, BiVoid AtRho]) = pure ([], ExFormation [bd, BiVoid AtRho])
     getPackage ex = throwIO (userError (printf "Can't extract package from given expression:\n %s" (printExpression ex)))
     -- Convert root Expression to Node
@@ -378,7 +380,7 @@
               if null pckg
                 then pure (Program (ExFormation [obj, BiVoid AtRho]))
                 else
-                  let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda "Package", BiVoid AtRho])) obj pckg
+                  let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda (Function "Package"), BiVoid AtRho])) obj pckg
                    in pure (Program (ExFormation [bd, BiVoid AtRho]))
           | otherwise -> throwIO (InvalidXMIRFormat "Expected single <object> element" doc)
         _ -> throwIO (InvalidXMIRFormat "NodeElement is expected as root element" doc)
@@ -390,7 +392,7 @@
       name <- getAttr "name" cur
       bds <- mapM (`xmirToFormationBinding` (name : fqn)) (cur C.$/ C.element (toName "o")) >>= uniqueBindings'
       case name of
-        "λ" -> pure (BiLambda (T.pack (intercalate "_" ("L" : reverse fqn))))
+        "λ" -> pure (BiLambda (Function (T.pack (intercalate "_" ("L" : reverse fqn)))))
         ('α' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with α" cur)
         "φ" -> pure (BiTau AtPhi (ExFormation (withVoidRho bds)))
         _ -> pure (BiTau (AtLabel (T.pack name)) (ExFormation (withVoidRho bds)))
@@ -426,14 +428,14 @@
                       xmirToApplication disp args' fqn
         "ξ" ->
           if null (cur C.$/ C.element (toName "o"))
-            then pure ExThis
+            then pure ExXi
             else throwIO (InvalidXMIRFormat "Application of 'ξ' is illegal in XMIR" cur)
         "Φ" ->
           if null (cur C.$/ C.element (toName "o"))
-            then pure ExGlobal
+            then pure ExRoot
             else throwIO (InvalidXMIRFormat "Application of 'Φ' is illegal in XMIR" cur)
-        'Φ' : '.' : rest -> xmirToExpression' ExGlobal "Φ" rest cur fqn
-        'ξ' : '.' : rest -> xmirToExpression' ExThis "ξ" rest cur fqn
+        'Φ' : '.' : rest -> xmirToExpression' ExRoot "Φ" rest cur fqn
+        'ξ' : '.' : rest -> xmirToExpression' ExXi "ξ" rest cur fqn
         _ -> throwIO (InvalidXMIRFormat "The @base attribute must be either ['∅'|'Φ'] or start with ['Φ.'|'ξ.'|'.']" cur)
   | otherwise = do
       bds <- mapM (`xmirToFormationBinding` fqn) (cur C.$/ C.element (toName "o")) >>= uniqueBindings'
@@ -462,37 +464,38 @@
             | hasAttr "base" arg && hasText arg = throwIO (InvalidXMIRFormat "It's illegal in XMIR to have @base and text() at the same time" arg)
             | not (hasAttr "base" arg) && not (hasText arg) = do
                 bds <- mapM (`xmirToFormationBinding` fqn) (arg C.$/ C.element (toName "o"))
-                as <- asToAttr arg idx
-                pure (ExApplication expr (BiTau as (ExFormation (withVoidRho bds))))
+                key <- asToKey arg idx
+                pure (ExApplication expr (mkArg key (ExFormation (withVoidRho bds))))
             | not (hasAttr "base" arg) && hasText arg = do
-                as <- asToAttr arg idx
+                key <- asToKey arg idx
                 bytes <- getText arg
-                pure (ExApplication expr (BiTau as (ExFormation [BiDelta (bytesToBts bytes), BiVoid AtRho])))
+                pure (ExApplication expr (mkArg key (ExFormation [BiDelta (bytesToBts bytes), BiVoid AtRho])))
             | otherwise = do
-                as <- asToAttr arg idx
+                key <- asToKey arg idx
                 arg' <- xmirToExpression arg fqn
-                pure (ExApplication expr (BiTau as arg'))
+                pure (ExApplication expr (mkArg key arg'))
       app' <- app
       xmirToApplication' (idx + 1) app' args fqn
-
-    asToAttr :: C.Cursor -> Int -> IO Attribute
-    asToAttr cur idx
+    mkArg :: Either Alpha Attribute -> Expression -> Argument
+    mkArg (Left alpha) expr = ArAlpha alpha expr
+    mkArg (Right attr) expr = ArTau attr expr
+    asToKey :: C.Cursor -> Int -> IO (Either Alpha Attribute)
+    asToKey cur position
       | hasAttr "as" cur = do
           as <- getAttr "as" cur
-          attr <- toAttr as cur
-          case attr of
-            AtRho -> throwIO (InvalidXMIRFormat "The 'ρ' in @as attribute is illegal in XMIR" cur)
-            _ -> pure attr
-      | otherwise = pure (AtAlpha idx)
+          case as of
+            'α' : rest' -> case TR.readMaybe rest' :: Maybe Int of
+              Just idx -> pure (Left (Alpha idx))
+              Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur)
+            "ρ" -> throwIO (InvalidXMIRFormat "The 'ρ' in @as attribute is illegal in XMIR" cur)
+            _ -> Right <$> toAttr as cur
+      | otherwise = pure (Left (Alpha position))
 
 toAttr :: String -> C.Cursor -> IO Attribute
 toAttr attr cur = case attr of
-  'α' : rest' ->
-    case TR.readMaybe rest' :: Maybe Int of
-      Just idx -> pure (AtAlpha idx)
-      Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur)
   "φ" -> pure AtPhi
   "ρ" -> pure AtRho
+  'α' : _ -> throwIO (InvalidXMIRFormat "α-index is not a valid dispatch attribute in XMIR" cur)
   ch : _
     | ch `notElem` ['a' .. 'z'] -> throwIO (InvalidXMIRFormat (printf "The attribute '%s' must start with ['a'..'z']" attr) cur)
     | '.' `elem` attr -> throwIO (InvalidXMIRFormat "Attribute can't contain dots" cur)
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -43,6 +43,9 @@
             Right attr -> pure attr
       )
 
+instance FromJSON Alpha where
+  parseJSON = parseJSON' "Alpha" parseAlpha
+
 instance FromJSON Bytes where
   parseJSON = parseJSON' "Bytes" parseBytes
 
@@ -78,12 +81,11 @@
     withObject
       "Condition"
       ( \v -> do
-          validateYamlObject v ["and", "or", "not", "alpha", "nf", "absolute", "eq", "in", "matches", "part-of", "primitive", "disjoint"]
+          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "in", "matches", "part-of", "primitive", "disjoint"]
           asum
             [ And <$> v .: "and"
             , Or <$> v .: "or"
             , Not <$> v .: "not"
-            , Alpha <$> v .: "alpha"
             , NF <$> v .: "nf"
             , Absolute <$> v .: "absolute"
             , Primitive <$> v .: "primitive"
@@ -148,7 +150,7 @@
         }
 
 data Number
-  = Index Attribute
+  = Index Alpha
   | Length Binding
   | Domain Binding
   | Literal Int
@@ -165,7 +167,6 @@
   | Or [Condition]
   | In Attribute Binding
   | Not Condition
-  | Alpha Attribute
   | Eq Comparable Comparable
   | NF Expression
   | Absolute Expression
@@ -207,7 +208,7 @@
     decodeRule :: (FilePath, BS.ByteString) -> Rule
     decodeRule (path, bs) =
       case Yaml.decodeEither' bs of
-        Right r -> r
+        Right rule -> rule
         Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err
 
 yamlRule :: FilePath -> IO Rule
@@ -237,11 +238,13 @@
   | DoNothing
   deriving (Eq, Generic, Show)
 
--- The argument of a dataization continuation: either a plain expression
--- ('𝔻(e)') or the morphing of one ('𝔻(𝕄(e))', written '{ morph: e }').
+-- The argument of a dataization continuation: a plain expression ('𝔻(e)'),
+-- the morphing of one ('𝔻(𝕄(e))', written '{ morph: e }'), or the
+-- normalization of one ('𝔻(𝒩(e))', written '{ normalize: e }').
 data DataizeArg
   = DaExpr Expression
   | DaMorph Expression
+  | DaNormalize Expression
   deriving (Eq, Generic, Show)
 
 -- One ordered morphing rule: match the expression, build extra metas in
@@ -289,8 +292,11 @@
 
 instance FromJSON DataizeArg where
   parseJSON (Object o) = do
-    validateYamlObject o ["morph"]
-    DaMorph <$> o .: "morph"
+    validateYamlObject o ["morph", "normalize"]
+    morphed <- o .:? "morph"
+    case morphed of
+      Just expr -> pure (DaMorph expr)
+      Nothing -> DaNormalize <$> o .: "normalize"
   parseJSON v = DaExpr <$> parseJSON v
 
 instance FromJSON MorphRule where
diff --git a/test/ASTSpec.hs b/test/ASTSpec.hs
--- a/test/ASTSpec.hs
+++ b/test/ASTSpec.hs
@@ -29,14 +29,23 @@
 
   describe "Attribute Show instance renders AtAlpha" $
     forM_
-      [ ("zero index", AtAlpha 0, "α0")
-      , ("positive index", AtAlpha 42, "α42")
-      , ("large index", AtAlpha 999, "α999")
+      [ ("zero index", Alpha 0, "α0")
+      , ("positive index", Alpha 42, "α42")
+      , ("large index", Alpha 999, "α999")
       ]
       ( \(desc, attr, expected) ->
           it desc $ show attr `shouldBe` expected
       )
 
+  describe "Alpha Eq instance compares same constructors" $
+    forM_
+      [ ("alphas equal", Alpha 1, Alpha 1, True)
+      , ("alphas differ", Alpha 1, Alpha 2, False)
+      ]
+      ( \(desc, lhs, rhs, expected) ->
+          it desc $ (lhs == rhs) `shouldBe` expected
+      )
+
   describe "Attribute Show instance renders special attributes" $
     forM_
       [ ("rho", AtRho, "ρ")
@@ -62,8 +71,6 @@
     forM_
       [ ("labels equal", AtLabel "x", AtLabel "x", True)
       , ("labels differ", AtLabel "x", AtLabel "y", False)
-      , ("alphas equal", AtAlpha 1, AtAlpha 1, True)
-      , ("alphas differ", AtAlpha 1, AtAlpha 2, False)
       , ("metas equal", AtMeta "a", AtMeta "a", True)
       , ("metas differ", AtMeta "a", AtMeta "b", False)
       , ("rho equals rho", AtRho, AtRho, True)
@@ -77,8 +84,7 @@
 
   describe "Attribute Eq instance compares different constructors" $
     forM_
-      [ ("label vs alpha", AtLabel "x", AtAlpha 0, False)
-      , ("rho vs phi", AtRho, AtPhi, False)
+      [ ("rho vs phi", AtRho, AtPhi, False)
       , ("delta vs lambda", AtDelta, AtLambda, False)
       , ("meta vs label", AtMeta "x", AtLabel "x", False)
       ]
@@ -88,7 +94,7 @@
 
   describe "Attribute Ord instance orders correctly" $
     it "sorts attributes by constructor order" $
-      let attrs = [AtMeta "z", AtDelta, AtLambda, AtRho, AtPhi, AtAlpha 1, AtLabel "a"]
+      let attrs = [AtMeta "z", AtDelta, AtLambda, AtRho, AtPhi, AtLabel "a"]
           first : _ = sort attrs
           isLabel (AtLabel _) = True
           isLabel _ = False
@@ -126,19 +132,19 @@
 
   describe "Binding Eq instance compares same constructors" $
     forM_
-      [ ("tau equals tau", BiTau AtRho ExGlobal, BiTau AtRho ExGlobal, True)
-      , ("tau differs by attr", BiTau AtRho ExGlobal, BiTau AtPhi ExGlobal, False)
-      , ("tau differs by expr", BiTau AtRho ExGlobal, BiTau AtRho ExThis, False)
+      [ ("tau equals tau", BiTau AtRho ExRoot, BiTau AtRho ExRoot, True)
+      , ("tau differs by attr", BiTau AtRho ExRoot, BiTau AtPhi ExRoot, False)
+      , ("tau differs by expr", BiTau AtRho ExRoot, BiTau AtRho ExXi, False)
       , ("meta equals meta", BiMeta "B", BiMeta "B", True)
       , ("meta differs", BiMeta "B", BiMeta "C", False)
       , ("delta equals delta", BiDelta BtEmpty, BiDelta BtEmpty, True)
       , ("delta differs", BiDelta BtEmpty, BiDelta (BtOne "00"), False)
       , ("void equals void", BiVoid AtRho, BiVoid AtRho, True)
       , ("void differs", BiVoid AtRho, BiVoid AtPhi, False)
-      , ("lambda equals lambda", BiLambda "Func", BiLambda "Func", True)
-      , ("lambda differs", BiLambda "Func", BiLambda "Other", False)
-      , ("metalambda equals", BiMetaLambda "F", BiMetaLambda "F", True)
-      , ("metalambda differs", BiMetaLambda "F", BiMetaLambda "G", False)
+      , ("lambda equals lambda", BiLambda (Function "Func"), BiLambda (Function "Func"), True)
+      , ("lambda differs", BiLambda (Function "Func"), BiLambda (Function "Other"), False)
+      , ("metalambda equals", BiLambda (FnMeta "F"), BiLambda (FnMeta "F"), True)
+      , ("metalambda differs", BiLambda (FnMeta "F"), BiLambda (FnMeta "G"), False)
       ]
       ( \(desc, lhs, rhs, expected) ->
           it desc $ (lhs == rhs) `shouldBe` expected
@@ -146,9 +152,9 @@
 
   describe "Binding Eq instance compares different constructors" $
     forM_
-      [ ("tau vs meta", BiTau AtRho ExGlobal, BiMeta "B", False)
+      [ ("tau vs meta", BiTau AtRho ExRoot, BiMeta "B", False)
       , ("delta vs void", BiDelta BtEmpty, BiVoid AtDelta, False)
-      , ("lambda vs metalambda", BiLambda "F", BiMetaLambda "F", False)
+      , ("lambda vs metalambda", BiLambda (Function "F"), BiLambda (FnMeta "F"), False)
       ]
       ( \(desc, lhs, rhs, expected) ->
           it desc $ (lhs == rhs) `shouldBe` expected
@@ -156,7 +162,7 @@
 
   describe "Binding Ord instance orders correctly" $
     it "sorts bindings by constructor order" $
-      let bindings = [BiMetaLambda "Z", BiLambda "A", BiVoid AtRho, BiDelta BtEmpty, BiMeta "B", BiTau AtRho ExGlobal]
+      let bindings = [BiLambda (FnMeta "Z"), BiLambda (Function "A"), BiVoid AtRho, BiDelta BtEmpty, BiMeta "B", BiTau AtRho ExRoot]
           first : _ = sort bindings
           isTau (BiTau _ _) = True
           isTau _ = False
@@ -166,16 +172,16 @@
     forM_
       [ ("formation equals", ExFormation [], ExFormation [], True)
       , ("formation differs", ExFormation [], ExFormation [BiVoid AtRho], False)
-      , ("this equals this", ExThis, ExThis, True)
-      , ("global equals global", ExGlobal, ExGlobal, True)
+      , ("this equals this", ExXi, ExXi, True)
+      , ("global equals global", ExRoot, ExRoot, True)
       , ("termination equals", ExTermination, ExTermination, True)
       , ("meta equals meta", ExMeta "e", ExMeta "e", True)
       , ("meta differs", ExMeta "e", ExMeta "f", False)
-      , ("application equals", ExApplication ExGlobal (BiTau AtRho ExThis), ExApplication ExGlobal (BiTau AtRho ExThis), True)
-      , ("dispatch equals", ExDispatch ExGlobal AtRho, ExDispatch ExGlobal AtRho, True)
-      , ("dispatch differs", ExDispatch ExGlobal AtRho, ExDispatch ExGlobal AtPhi, False)
-      , ("metatail equals", ExMetaTail ExGlobal "t", ExMetaTail ExGlobal "t", True)
-      , ("metatail differs", ExMetaTail ExGlobal "t", ExMetaTail ExGlobal "s", False)
+      , ("application equals", ExApplication ExRoot (ArTau AtRho ExXi), ExApplication ExRoot (ArTau AtRho ExXi), True)
+      , ("dispatch equals", ExDispatch ExRoot AtRho, ExDispatch ExRoot AtRho, True)
+      , ("dispatch differs", ExDispatch ExRoot AtRho, ExDispatch ExRoot AtPhi, False)
+      , ("metatail equals", ExMetaTail ExRoot "t", ExMetaTail ExRoot "t", True)
+      , ("metatail differs", ExMetaTail ExRoot "t", ExMetaTail ExRoot "s", False)
       ]
       ( \(desc, lhs, rhs, expected) ->
           it desc $ (lhs == rhs) `shouldBe` expected
@@ -183,9 +189,9 @@
 
   describe "Expression Eq instance compares different constructors" $
     forM_
-      [ ("formation vs this", ExFormation [], ExThis, False)
-      , ("global vs termination", ExGlobal, ExTermination, False)
-      , ("meta vs dispatch", ExMeta "e", ExDispatch ExGlobal AtRho, False)
+      [ ("formation vs this", ExFormation [], ExXi, False)
+      , ("global vs termination", ExRoot, ExTermination, False)
+      , ("meta vs dispatch", ExMeta "e", ExDispatch ExRoot AtRho, False)
       ]
       ( \(desc, lhs, rhs, expected) ->
           it desc $ (lhs == rhs) `shouldBe` expected
@@ -193,14 +199,14 @@
 
   describe "Expression Ord instance orders correctly" $
     it "sorts expressions by constructor order" $
-      let exprs = [ExMetaTail ExGlobal "t", ExDispatch ExGlobal AtRho, ExApplication ExGlobal (BiVoid AtRho), ExMeta "e", ExTermination, ExGlobal, ExThis, ExFormation []]
+      let exprs = [ExMetaTail ExRoot "t", ExDispatch ExRoot AtRho, ExApplication ExRoot (ArTau AtRho ExRoot), ExMeta "e", ExTermination, ExRoot, ExXi, ExFormation []]
           first : _ = sort exprs
        in first `shouldBe` ExFormation []
 
   describe "Program Eq instance compares programs" $
     forM_
-      [ ("same programs equal", Program ExGlobal, Program ExGlobal, True)
-      , ("different programs differ", Program ExGlobal, Program ExThis, False)
+      [ ("same programs equal", Program ExRoot, Program ExRoot, True)
+      , ("different programs differ", Program ExRoot, Program ExXi, False)
       ]
       ( \(desc, lhs, rhs, expected) ->
           it desc $ (lhs == rhs) `shouldBe` expected
@@ -208,33 +214,33 @@
 
   describe "Program Ord instance orders correctly" $
     it "orders programs by expression" $
-      let progs = [Program ExThis, Program ExGlobal, Program (ExFormation [])]
+      let progs = [Program ExXi, Program ExRoot, Program (ExFormation [])]
           first : _ = sort progs
        in first `shouldBe` Program (ExFormation [])
 
   describe "Program Show instance renders programs" $
     it "shows program wrapper" $
       let hasProgram str = "Program" `elem` words str
-       in show (Program ExGlobal) `shouldSatisfy` hasProgram
+       in show (Program ExRoot) `shouldSatisfy` hasProgram
 
   describe "countNodes counts ExFormation with non-tau bindings" $
     forM_
-      [ ("Q", ExGlobal, 1)
+      [ ("Q", ExRoot, 1)
       , ("T", ExTermination, 1)
-      , ("$", ExThis, 1)
-      , ("dispatch on global", ExDispatch ExGlobal (AtLabel "x"), 3)
-      , ("application with globals", ExApplication ExGlobal (BiTau AtRho ExGlobal), 6)
-      , ("nested expressions", ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExGlobal], 9)
+      , ("$", ExXi, 1)
+      , ("dispatch on global", ExDispatch ExRoot (AtLabel "x"), 3)
+      , ("application with globals", ExApplication ExRoot (ArTau AtRho ExRoot), 6)
+      , ("nested expressions", ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExRoot], 9)
       , ("empty formation", ExFormation [], 1)
       , ("void binding", ExFormation [BiVoid AtRho], 5)
       , ("delta binding", ExFormation [BiDelta BtEmpty], 5)
-      , ("lambda binding", ExFormation [BiLambda "Func"], 5)
+      , ("lambda binding", ExFormation [BiLambda (Function "Func")], 5)
       , ("meta binding", ExFormation [BiMeta "B"], 3)
-      , ("metalambda binding", ExFormation [BiMetaLambda "F"], 5)
+      , ("metalambda binding", ExFormation [BiLambda (FnMeta "F")], 5)
       , ("meta expression", ExMeta "e", 1)
-      , ("metatail expression", ExMetaTail ExGlobal "t", 3)
-      , ("deeply nested dispatch", ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b"), 5)
-      , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x"))], 7)
+      , ("metatail expression", ExMetaTail ExRoot "t", 3)
+      , ("deeply nested dispatch", ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b"), 5)
+      , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExRoot (AtLabel "x"))], 7)
       ]
       ( \(desc, expr, expected) ->
           it desc $ countNodes expr `shouldBe` expected
diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs
--- a/test/BuilderSpec.hs
+++ b/test/BuilderSpec.hs
@@ -26,64 +26,64 @@
       buildExpression
       [
         ( "Q.!a => (!a >> x) => Q.x"
-        , ExDispatch ExGlobal (AtMeta "a")
+        , ExDispatch ExRoot (AtMeta "a")
         , [("a", MvAttribute (AtLabel "x"))]
-        , Right (ExDispatch ExGlobal (AtLabel "x"))
+        , Right (ExDispatch ExRoot (AtLabel "x"))
         )
       ,
         ( "Q.c(!a -> !e) => (!a >> x, !e >> $.y.z) => Q.c(x -> $.y.z)"
-        , ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtMeta "a") (ExMeta "e"))
-        , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z")))]
-        , Right (ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtLabel "x") (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))))
+        , ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtMeta "a") (ExMeta "e"))
+        , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")))]
+        , Right (ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtLabel "x") (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z"))))
         )
       ,
         ( "[[!a -> $.x, !B]] => (!a >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]"
-        , ExFormation [BiTau (AtMeta "a") (ExDispatch ExThis (AtLabel "x")), BiMeta "B"]
-        , [("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda "Func"])]
+        , ExFormation [BiTau (AtMeta "a") (ExDispatch ExXi (AtLabel "x")), BiMeta "B"]
+        , [("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda (Function "Func")])]
         , Right
             ( ExFormation
-                [ BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "x"))
+                [ BiTau (AtLabel "y") (ExDispatch ExXi (AtLabel "x"))
                 , BiVoid (AtLabel "b")
-                , BiLambda "Func"
+                , BiLambda (Function "Func")
                 ]
             )
         )
       ,
         ( "Q * !t => (!t >> [.a, .b, (~1 -> $.x)]) => Q.a.b(~1 -> $.x)"
-        , ExMetaTail ExGlobal "t"
-        , [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x")))])]
-        , Right (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))))
+        , ExMetaTail ExRoot "t"
+        , [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (ArAlpha (Alpha 1) (ExDispatch ExXi (AtLabel "x")))])]
+        , Right (ExApplication (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (ArAlpha (Alpha 1) (ExDispatch ExXi (AtLabel "x"))))
         )
       ,
         ( "Q.!a => () => X"
-        , ExDispatch ExGlobal (AtMeta "a")
+        , ExDispatch ExRoot (AtMeta "a")
         , []
         , Left "meta 'a' is either does not exist or refers to an inappropriate term"
         )
       ,
         ( "!e0(!a1 -> !e1, !a2 => !e2) => (!e0 >> [[]], !a1 >> x, !e1 >> Q, !a2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)"
-        , ExApplication (ExApplication (ExMeta "e0") (BiTau (AtMeta "a1") (ExMeta "e1"))) (BiTau (AtMeta "a2") (ExMeta "e2"))
+        , ExApplication (ExApplication (ExMeta "e0") (ArTau (AtMeta "a1") (ExMeta "e1"))) (ArTau (AtMeta "a2") (ExMeta "e2"))
         ,
           [ ("e0", MvExpression (ExFormation []))
           , ("a1", MvAttribute (AtLabel "x"))
-          , ("e1", MvExpression ExGlobal)
+          , ("e1", MvExpression ExRoot)
           , ("a2", MvAttribute (AtLabel "y"))
-          , ("e2", MvExpression ExThis)
+          , ("e2", MvExpression ExXi)
           ]
-        , Right (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis))
+        , Right (ExApplication (ExApplication (ExFormation []) (ArTau (AtLabel "x") ExRoot)) (ArTau (AtLabel "y") ExXi))
         )
       ,
         ( "⟦!a ↦ ∅, !B⟧.!a => (!a >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t"
         , ExDispatch (ExFormation [BiVoid (AtMeta "a"), BiMeta "B"]) (AtMeta "a")
         ,
           [ ("a", MvAttribute (AtLabel "t"))
-          , ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))])
+          , ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))])
           ]
         , Right
             ( ExDispatch
                 ( ExFormation
                     [ BiVoid (AtLabel "t")
-                    , BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                    , BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                     ]
                 )
                 (AtLabel "t")
@@ -96,14 +96,14 @@
       built <-
         buildExpressionsThrows
           (ExMeta "e")
-          [ substSingle "e" (MvExpression (ExDispatch ExGlobal (AtLabel "x")))
-          , substSingle "e" (MvExpression (ExDispatch ExThis (AtLabel "y")))
+          [ substSingle "e" (MvExpression (ExDispatch ExRoot (AtLabel "x")))
+          , substSingle "e" (MvExpression (ExDispatch ExXi (AtLabel "y")))
           ]
-      built `shouldBe` [ExDispatch ExGlobal (AtLabel "x"), ExDispatch ExThis (AtLabel "y")]
+      built `shouldBe` [ExDispatch ExRoot (AtLabel "x"), ExDispatch ExXi (AtLabel "y")]
     it "!e => [(!e1 >> Q.x)] => X" $
       buildExpressionsThrows
         (ExMeta "e")
-        [substSingle "e1" (MvExpression (ExDispatch ExGlobal (AtLabel "x")))]
+        [substSingle "e1" (MvExpression (ExDispatch ExRoot (AtLabel "x")))]
         `shouldThrow` anyException
 
   describe "build with duplicate attributes in bindings" $ do
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -868,7 +868,6 @@
               , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
               , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
               , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\} \\leadsto_{\\nameref{r:Mprim}}"
               , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               , "01-"
@@ -946,9 +945,9 @@
         [ unlines
             [ "\\begin{tabular}{rl}"
             , "\\trrule{alpha}"
-            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\eta -> e ) }"
             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"
-            , "  { if $ \\indexof{ \\tau_2 } = \\vert \\overline{ B_1 } \\vert $ }"
+            , "  { if $ \\indexof{ \\eta } = \\vert \\overline{ B_1 } \\vert $ }"
             , "  { }"
             , "\\trrule{copy}"
             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
@@ -960,6 +959,11 @@
             , "  { T }"
             , "  { }"
             , "  { }"
+            , "\\trrule{dca}"
+            , "  { T ( \\eta -> e ) }"
+            , "  { T }"
+            , "  { }"
+            , "  { }"
             , "\\trrule{dd}"
             , "  { T . \\tau }"
             , "  { T }"
@@ -973,7 +977,7 @@
             , "\\trrule{miss}"
             , "  { [[ B ]] ( \\tau -> e ) }"
             , "  { T }"
-            , "  { if $ \\tau \\notin B \\;\\text{and}\\; \\tau \\notin [ ~0, ~1, \\dots ] $ }"
+            , "  { if $ \\tau \\notin B $ }"
             , "  { }"
             , "\\trrule{null}"
             , "  { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"
@@ -1009,28 +1013,23 @@
         ["explain", "--morph"]
         [ unlines
             [ "\\begin{tabular}{rl}"
-            , "\\trrule{Mprim}"
-            , "  { \\mathbb{M}( e ) }"
-            , "  { e }"
-            , "  { if $ e \\in \\mathcal{P} $ }"
+            , "\\trrule{prim}"
+            , "  { \\mathbb{M}( p ) }"
+            , "  { p }"
             , "  { }"
-            , "\\trrule{Mnmz}"
-            , "  { \\mathbb{M}( e ) }"
-            , "  { \\mathbb{M}( \\mathcal{N}( e ) ) }"
-            , "  { if $ not( \\isnormal{ e } ) $ }"
             , "  { }"
-            , "\\trrule{Mlambda}"
+            , "\\trrule{lambda}"
             , "  { \\mathbb{M}( [[ B_1, L> F, B_2 ]] * t ) }"
-            , "  { \\mathbb{M}( e * t ) }"
+            , "  { \\mathbb{M}( \\mathcal{N}( e * t ) ) }"
             , "  { }"
             , "  { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"
-            , "\\trrule{Mphi}"
+            , "\\trrule{root}"
             , "  { \\mathbb{M}( Q . \\tau * t ) }"
-            , "  { \\mathbb{M}( e * t ) }"
+            , "  { \\mathbb{M}( \\mathcal{N}( e * t ) ) }"
             , "  { }"
             , "  { where $ e \\coloneqq global( \\tau ) $ }"
-            , "\\trrule{Mstuck}"
-            , "  { \\mathbb{M}( e ) }"
+            , "\\trrule{stuck}"
+            , "  { \\mathbb{M}( n ) }"
             , "  { T }"
             , "  { }"
             , "  { }"
@@ -1050,16 +1049,16 @@
             , "  { }"
             , "\\trrule{box}"
             , "  { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }"
-            , "  { \\mathbb{D}( e_1 ) }"
+            , "  { \\mathbb{D}( \\mathcal{N}( e_1 ) ) }"
             , "  { if $ [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset $ }"
             , "  { where $ e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } $ }"
             , "\\trrule{norm}"
-            , "  { \\mathbb{D}( e ) }"
-            , "  { \\mathbb{D}( \\mathbb{M}( e ) ) }"
-            , "  { if $ e \\notin \\mathcal{P} $ }"
+            , "  { \\mathbb{D}( n ) }"
+            , "  { \\mathbb{D}( \\mathbb{M}( n ) ) }"
+            , "  { if $ n \\notin \\mathcal{P} $ }"
             , "  { }"
             , "\\trrule{none}"
-            , "  { \\mathbb{D}( e ) }"
+            , "  { \\mathbb{D}( n ) }"
             , "  { \\varnothing }"
             , "  { }"
             , "  { }"
@@ -1157,7 +1156,7 @@
     it "builds substitutions with conditions" $
       withStdin "{[[ x -> Q.y ]].x}" $
         testCLISucceeded
-          ["match", "--pattern=[[ !a -> Q.y, !B ]].!a", "--when=and(not(alpha(!a)),eq(length(!B),1))"]
+          ["match", "--pattern=[[ !a -> Q.y, !B ]].!a", "--when=eq(length(!B),1)"]
           ["B >> ⟦ ρ ↦ ∅ ⟧\na >> x"]
 
     it "builds with condition from file" $
diff --git a/test/CSTSpec.hs b/test/CSTSpec.hs
--- a/test/CSTSpec.hs
+++ b/test/CSTSpec.hs
@@ -64,7 +64,7 @@
     let number = BaseObject "number"
         again = ExPhiAgain Nothing 1
         bts = BaseObject "bytes"
-        bt = BiTau (AtAlpha 0)
+        bt = ArAlpha (Alpha 0)
         app = ExApplication
         form = ExFormation [BiDelta (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"]), BiVoid AtRho]
         isCSTNumber (EX_NUMBER{}) = True
diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs
--- a/test/ConditionSpec.hs
+++ b/test/ConditionSpec.hs
@@ -5,7 +5,7 @@
 
 module ConditionSpec where
 
-import AST (Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExGlobal, ExMeta))
+import AST (Alpha (AlMeta, Alpha), Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExMeta, ExRoot))
 import Condition
 import Control.Monad (forM_)
 import Data.Either (isLeft, isRight)
@@ -18,15 +18,12 @@
     forM_
       [ "in (!a, !B)"
       , " not   (in (!a1,   !B))   "
-      , "alpha(x)"
       , "eq(1, 1)"
-      , "or(eq(index(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"
-      , "and(alpha(q),eq(-5,21))"
+      , "or(eq(index(~0),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"
       , "nf([[ x -> !e ]].x)"
       , "absolute(!e1)"
       , "matches(\"hello(\\\"\\u0000)\", !e)"
       , "part-of ( [[ x -> 1 ]] , !B ) "
-      , "and(not(alpha(!a)),eq(!a,x))"
       ]
       (\expr -> it expr (parseCondition expr `shouldSatisfy` isRight))
 
@@ -34,12 +31,11 @@
     forM_
       [ ("in(!a, !B)", Y.In (AtMeta "a") (BiMeta "B"))
       , ("not(in(!a,!B))", Y.Not (Y.In (AtMeta "a") (BiMeta "B")))
-      , ("alpha(y)", Y.Alpha (AtLabel "y"))
       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))
-      , ("eq(index(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))
-      , ("eq(index(z),domain(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Domain (BiMeta "B1"))))
+      , ("eq(index(α0),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (Alpha 0))) (Y.CmpNum (Y.Length (BiMeta "B1"))))
+      , ("eq(index(!h),domain(!B1))", Y.Eq (Y.CmpNum (Y.Index (AlMeta "h"))) (Y.CmpNum (Y.Domain (BiMeta "B1"))))
       , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))
-      , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])
+      , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])
       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])
       ]
       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))
@@ -48,7 +44,6 @@
     forM_
       [ "some()"
       , "in(!a, !a)"
-      , "alpha(!B)"
       , "or(or(), or())"
       ]
       (\expr -> it expr (parseCondition expr `shouldSatisfy` isLeft))
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -27,7 +27,7 @@
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
       let prog = Program expr
-      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExGlobal prog)
+      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog)
       res `shouldBe` output
 
 test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> DataizeContext -> IO (a, NonEmpty Rewritten)) -> [(String, Expression, Expression, a)] -> Spec
@@ -35,7 +35,7 @@
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
       let prog = Program expr
-      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExGlobal prog)
+      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog)
       res `shouldBe` output
 
 testDataize :: [(String, String, String, Bytes)] -> Spec
@@ -52,13 +52,13 @@
   describe "morph" $
     test'
       morph
-      [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExGlobal, ExFormation [BiDelta (BtOne "00")])
-      , ("T => T", ExTermination, ExGlobal, ExTermination)
-      , ("$ => X", ExThis, ExGlobal, ExTermination)
-      , ("Q => X", ExGlobal, ExGlobal, ExTermination)
+      [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])
+      , ("T => T", ExTermination, ExRoot, ExTermination)
+      , ("$ => X", ExXi, ExRoot, ExTermination)
+      , ("Q => X", ExRoot, ExRoot, ExTermination)
       ,
         ( "Q.x (Q -> [[ x -> [[]] ]]) => [[]]"
-        , ExDispatch ExGlobal (AtLabel "x")
+        , ExDispatch ExRoot (AtLabel "x")
         , ExFormation [BiTau (AtLabel "x") (ExFormation [])]
         , ExFormation []
         )
@@ -67,21 +67,15 @@
   describe "dataize" $
     test
       dataize'
-      [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExGlobal, Just (BtOne "00"))
-      , ("T => X", ExTermination, ExGlobal, Nothing)
+      [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, Just (BtOne "00"))
+      , ("T => X", ExTermination, ExRoot, Nothing)
       ,
         ( "[[ @ -> [[ D> 00-]] ]] => 00-"
         , ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]
-        , ExGlobal
+        , ExRoot
         , Just (BtOne "00")
         )
       ,
-        ( "[[ x -> [[ D> 01- ]] ]].x => 01-"
-        , ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiDelta (BtOne "01"), BiVoid AtRho]), BiVoid AtRho]) (AtLabel "x")
-        , ExGlobal
-        , Just (BtOne "01")
-        )
-      ,
         ( "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]] => 01-"
         , ExFormation
             [ BiTau
@@ -97,14 +91,14 @@
                                     , BiVoid AtRho
                                     ]
                                 )
-                                (BiTau (AtLabel "y") (ExFormation []))
+                                (ArTau (AtLabel "y") (ExFormation []))
                             )
                         ]
                     )
                     (AtLabel "x")
                 )
             ]
-        , ExGlobal
+        , ExRoot
         , Just (BtOne "01")
         )
       ]
@@ -113,7 +107,7 @@
     it "resolves global dispatch from the universe Q" $ do
       prog <- parseProgramThrows "Q -> [[ x -> [[ D> 42- ]] ]]"
       expected <- parseExpressionThrows "[[ D> 42- ]]"
-      term <- execBuildTerm (defaultDataizeContext ExGlobal prog) "global" [Yaml.ArgAttribute (AtLabel "x")] substEmpty
+      term <- execBuildTerm (defaultDataizeContext ExRoot prog) "global" [Yaml.ArgAttribute (AtLabel "x")] substEmpty
       case term of
         TeExpression actual -> actual `shouldBe` expected
         _ -> expectationFailure "global() did not return an expression"
@@ -144,6 +138,15 @@
         (null orphans)
         (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))
 
+  describe "names every rule uniquely across rule sets" $
+    it "shares no rule name between morphing, dataization and normalization" $ do
+      let names =
+            map (.name) Yaml.morphingRules
+              ++ map (.name) Yaml.dataizationRules
+              ++ map (.name) Yaml.normalizationRules
+          clashes = nub (filter (\n -> length (filter (== n) names) > 1) names)
+      clashes `shouldBe` []
+
   describe "preserves the reduction label sequence" $ do
     let labelsOf loc src = do
           prog <- parseProgramThrows src
@@ -157,33 +160,32 @@
           "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
       labels
         `shouldBe` [ "contextualize"
-                   , "Mphi"
+                   , "root"
                    , "alpha"
                    , "copy"
                    , "dot"
                    , "copy"
                    , "alpha"
                    , "copy"
-                   , "Mlambda"
-                   , "Mphi"
+                   , "lambda"
+                   , "root"
                    , "alpha"
                    , "copy"
-                   , "Mprim"
+                   , "prim"
                    , "contextualize"
                    , "dot"
-                   , "Mphi"
+                   , "root"
                    , "alpha"
                    , "copy"
                    , "copy"
-                   , "Mprim"
+                   , "prim"
                    , "contextualize"
                    , "dot"
                    , "copy"
-                   , "Mprim"
                    ]
     it "dataizes a located reference through the expected rules" $ do
       labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
-      labels `shouldBe` ["contextualize", "Mphi", "Mprim"]
+      labels `shouldBe` ["contextualize", "root", "prim"]
 
   testDataize
     [
diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs
--- a/test/FunctionsSpec.hs
+++ b/test/FunctionsSpec.hs
@@ -20,9 +20,9 @@
 spec :: Spec
 spec = describe "Functions" $
   it "contains only unique bindings after 'join'" $ do
-    let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExGlobal, BiVoid (AtAlpha 0)])
-        second = ("B2", MvBindings [BiTau AtRho ExThis, BiLambda "Func", BiDelta (BtOne "00"), BiVoid (AtAlpha 1)])
-        third = ("B3", MvBindings [BiLambda "Some", BiTau (AtLabel "y") ExThis, BiTau (AtLabel "x") ExThis, BiVoid (AtAlpha 0)])
+    let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "a0")])
+        second = ("B2", MvBindings [BiTau AtRho ExXi, BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid (AtLabel "a1")])
+        third = ("B3", MvBindings [BiLambda (Function "Some"), BiTau (AtLabel "y") ExXi, BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "a0")])
         subst = Subst (Map.fromList [first, second, third])
     TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2"), ArgBinding (BiMeta "B3")] subst
     bds' <- uniqueBindings' bds
diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs
--- a/test/MatcherSpec.hs
+++ b/test/MatcherSpec.hs
@@ -37,45 +37,45 @@
       matchExpressionDeep
       [
         ( "Q => [[ @ -> Q, ^ -> Q ]] => [(), ()]"
-        , ExGlobal
-        , ExFormation [BiTau AtPhi ExGlobal, BiTau AtRho ExGlobal]
+        , ExRoot
+        , ExFormation [BiTau AtPhi ExRoot, BiTau AtRho ExRoot]
         , substs [[], []]
         )
       ,
         ( "Q.!a => [[ @ -> Q.y, ^ -> [[ a -> Q.w ]], @ -> Q.y ]] => [(a >> y), (a >> w), (a >> y)]"
-        , ExDispatch ExGlobal (AtMeta "a")
+        , ExDispatch ExRoot (AtMeta "a")
         , ExFormation
-            [ BiTau AtPhi (ExDispatch ExGlobal (AtLabel "y"))
-            , BiTau AtRho (ExFormation [BiTau (AtLabel "a") (ExDispatch ExGlobal (AtLabel "w"))])
-            , BiTau AtPhi (ExDispatch ExGlobal (AtLabel "y"))
+            [ BiTau AtPhi (ExDispatch ExRoot (AtLabel "y"))
+            , BiTau AtRho (ExFormation [BiTau (AtLabel "a") (ExDispatch ExRoot (AtLabel "w"))])
+            , BiTau AtPhi (ExDispatch ExRoot (AtLabel "y"))
             ]
         , substs [[("a", MvAttribute (AtLabel "y"))], [("a", MvAttribute (AtLabel "w"))], [("a", MvAttribute (AtLabel "y"))]]
         )
       ,
         ( "[[!a -> Q.org.!a]] => [[f -> [[x -> Q.org.x]], t -> [[y -> Q.org.y]] => [(!a >> x), (!a >> y)]"
-        , ExFormation [BiTau (AtMeta "a") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtMeta "a"))]
+        , ExFormation [BiTau (AtMeta "a") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtMeta "a"))]
         , ExFormation
-            [ BiTau (AtLabel "f") (ExFormation [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x"))])
-            , BiTau (AtLabel "t") (ExFormation [BiTau (AtLabel "y") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "y"))])
+            [ BiTau (AtLabel "f") (ExFormation [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "x"))])
+            , BiTau (AtLabel "t") (ExFormation [BiTau (AtLabel "y") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "y"))])
             ]
         , substs [[("a", MvAttribute (AtLabel "x"))], [("a", MvAttribute (AtLabel "y"))]]
         )
       ,
         ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]] ), (!e >> Q)]"
         , ExMeta "e"
-        , ExFormation [BiTau (AtLabel "x") ExGlobal]
+        , ExFormation [BiTau (AtLabel "x") ExRoot]
         , substs
-            [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))]
-            , [("e", MvExpression ExGlobal)]
+            [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExRoot]))]
+            , [("e", MvExpression ExRoot)]
             ]
         )
       ,
         ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang), (!e >> Q, !a >> org)]"
         , ExDispatch (ExMeta "e") (AtMeta "a")
-        , ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")
+        , ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")
         , substs
-            [ [("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]
-            , [("e", MvExpression ExGlobal), ("a", MvAttribute (AtLabel "org"))]
+            [ [("e", MvExpression (ExDispatch ExRoot (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]
+            , [("e", MvExpression ExRoot), ("a", MvAttribute (AtLabel "org"))]
             ]
         )
       ,
@@ -84,23 +84,23 @@
         , ExApplication
             ( ExDispatch
                 ( ExFormation
-                    [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                    [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                     , BiVoid (AtLabel "t")
                     ]
                 )
                 (AtLabel "t")
             )
-            ( BiTau
+            ( ArTau
                 AtRho
                 ( ExFormation
-                    [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                    [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                     , BiVoid (AtLabel "t")
                     ]
                 )
             )
         , substs
             [
-              [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))])
+              [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))])
               , ("a", MvAttribute (AtLabel "t"))
               , ("B2", MvBindings [])
               ]
@@ -128,22 +128,22 @@
             [ BiTau
                 (AtLabel "i1")
                 ( ExFormation
-                    [ BiTau (AtLabel "a") ExGlobal
-                    , BiTau (AtLabel "b") ExThis
+                    [ BiTau (AtLabel "a") ExRoot
+                    , BiTau (AtLabel "b") ExXi
                     ]
                 )
             , BiTau
                 (AtLabel "i2")
                 ( ExFormation
-                    [ BiTau (AtLabel "a") ExGlobal
+                    [ BiTau (AtLabel "a") ExRoot
                     , BiTau (AtLabel "b") (ExFormation [BiVoid AtPhi])
                     ]
                 )
             ]
         , substs
             [
-              [ ("e0", MvExpression ExGlobal)
-              , ("e-first", MvExpression ExThis)
+              [ ("e0", MvExpression ExRoot)
+              , ("e-first", MvExpression ExXi)
               , ("e-second", MvExpression (ExFormation [BiVoid AtPhi]))
               ]
             ]
@@ -152,15 +152,22 @@
 
   describe "matchAttribute: attribute => attribute => substitution" $
     forM_
-      [ ("~1 => ~1 => [()]", AtAlpha 1, AtAlpha 1, substs [[]])
-      , ("!a => ^ => [(!a >> ^)]", AtMeta "a", AtRho, substs [[("a", MvAttribute AtRho)]])
+      [ ("!a => ^ => [(!a >> ^)]", AtMeta "a", AtRho, substs [[("a", MvAttribute AtRho)]])
       , ("!a => @ => [(!a >> @)]", AtMeta "a", AtPhi, substs [[("a", MvAttribute AtPhi)]])
-      , ("~0 => [] => [()]", AtAlpha 0, AtLabel "x", substs [])
       ]
       ( \(desc, ptn, tgt, expected) ->
           it desc $ matchAttribute ptn tgt `shouldBe` expected
       )
 
+  describe "matchAlpha: alpha => alpha => substitution" $
+    forM_
+      [ ("α1 => α1 => [()]", Alpha 1, Alpha 1, substs [[]])
+      , ("α0 => α1 => []", Alpha 0, Alpha 1, substs [])
+      ]
+      ( \(desc, ptn, tgt, expected) ->
+          it desc $ matchAlpha ptn tgt `shouldBe` expected
+      )
+
   describe "matchBindings: [binding] => [binding] => substitution" $
     test
       matchBindings
@@ -173,13 +180,13 @@
       ,
         ( "[[!B]] => T:[[x -> ?, D> 01-, L> Func]] => (!B >> T)"
         , [BiMeta "B"]
-        , [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda "Func"]
-        , substs [[("B", MvBindings [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda "Func"])]]
+        , [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda (Function "Func")]
+        , substs [[("B", MvBindings [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda (Function "Func")])]]
         )
       ,
         ( "[[D> 00-]] => [[D> 00-, L> Func]] => []"
         , [BiDelta (BtOne "00")]
-        , [BiDelta (BtOne "00"), BiLambda "Func"]
+        , [BiDelta (BtOne "00"), BiLambda (Function "Func")]
         , substs []
         )
       ,
@@ -203,8 +210,8 @@
       ,
         ( "[[!B1, !x -> ?, !B2]] => [[y -> ?, D> -> 00-, L> Func]] => (!x >> y, !B1 >> [[]], !B2 >> [[D> -> 00-, L> Func]])"
         , [BiMeta "B1", BiVoid (AtMeta "x"), BiMeta "B2"]
-        , [BiVoid (AtLabel "y"), BiDelta (BtOne "00"), BiLambda "Func"]
-        , substs [[("B1", MvBindings []), ("B2", MvBindings [BiDelta (BtOne "00"), BiLambda "Func"]), ("x", MvAttribute (AtLabel "y"))]]
+        , [BiVoid (AtLabel "y"), BiDelta (BtOne "00"), BiLambda (Function "Func")]
+        , substs [[("B1", MvBindings []), ("B2", MvBindings [BiDelta (BtOne "00"), BiLambda (Function "Func")]), ("x", MvAttribute (AtLabel "y"))]]
         )
       ,
         ( "[[!x -> ?, !y -> ?]] => [[a -> ?, b -> ?]] => (!x >> a, !y >> b)"
@@ -215,19 +222,19 @@
       ,
         ( "[[t -> ?, !B]] => [[t -> ?, x -> Q, y -> $]] => (!B >> [[x -> Q, y -> $]])"
         , [BiVoid (AtLabel "t"), BiMeta "B"]
-        , [BiVoid (AtLabel "t"), BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis]
-        , substs [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]
+        , [BiVoid (AtLabel "t"), BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi]
+        , substs [[("B", MvBindings [BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi])]]
         )
       ,
         ( "[[!B, z -> Q]] => [[x -> Q, y -> $, z -> Q]] => (!B >> [[x -> Q, y -> $]])"
-        , [BiMeta "B", BiTau (AtLabel "z") ExGlobal]
-        , [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis, BiTau (AtLabel "z") ExGlobal]
-        , substs [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]
+        , [BiMeta "B", BiTau (AtLabel "z") ExRoot]
+        , [BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi, BiTau (AtLabel "z") ExRoot]
+        , substs [[("B", MvBindings [BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi])]]
         )
       ,
         ( "[[L> Func, D> 00-]] => [[D> 00-, L> Func]] => []"
-        , [BiLambda "Func", BiDelta (BtOne "00")]
-        , [BiDelta (BtOne "00"), BiLambda "Func"]
+        , [BiLambda (Function "Func"), BiDelta (BtOne "00")]
+        , [BiDelta (BtOne "00"), BiLambda (Function "Func")]
         , substs []
         )
       ,
@@ -352,98 +359,122 @@
   describe "matchExpression: expression => pattern => substitution" $
     test
       matchExpression'
-      [ ("$ => $ => [()]", ExThis, ExThis, substs [[]])
-      , ("Q => Q => [()]", ExGlobal, ExGlobal, substs [[]])
+      [ ("$ => $ => [()]", ExXi, ExXi, substs [[]])
+      , ("Q => Q => [()]", ExRoot, ExRoot, substs [[]])
       ,
         ( "!e => Q => [(!e >> Q)]"
         , ExMeta "e"
-        , ExGlobal
-        , substs [[("e", MvExpression ExGlobal)]]
+        , ExRoot
+        , substs [[("e", MvExpression ExRoot)]]
         )
       ,
+        ( "!p => T => [(!p >> T)]"
+        , ExMeta "p"
+        , ExTermination
+        , substs [[("p", MvExpression ExTermination)]]
+        )
+      ,
+        ( "!p => [[ x -> Q ]] => [(!p >> [[ x -> Q ]])]"
+        , ExMeta "p"
+        , ExFormation [BiTau (AtLabel "x") ExRoot]
+        , substs [[("p", MvExpression (ExFormation [BiTau (AtLabel "x") ExRoot]))]]
+        )
+      ,
+        ( "!p => Q => []"
+        , ExMeta "p"
+        , ExRoot
+        , substs []
+        )
+      ,
+        ( "!p => [[ L> Func ]] => []"
+        , ExMeta "p"
+        , ExFormation [BiLambda (Function "Func")]
+        , substs []
+        )
+      ,
         ( "!e => Q.org(x -> $) => [(!e >> Q.org(x -> $))]"
         , ExMeta "e"
-        , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)
-        , substs [[("e", MvExpression (ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)))]]
+        , ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") ExXi)
+        , substs [[("e", MvExpression (ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") ExXi)))]]
         )
       ,
         ( "!e1.x => Q.org.x => [(!e1 >> Q.org)]"
         , ExDispatch (ExMeta "e1") (AtLabel "x")
-        , ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x")
-        , substs [[("e1", MvExpression (ExDispatch ExGlobal (AtLabel "org")))]]
+        , ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "x")
+        , substs [[("e1", MvExpression (ExDispatch ExRoot (AtLabel "org")))]]
         )
       ,
         ( "!e.org.!a => $.org.x => [(!e >> $, !a >> x)]"
         , ExDispatch (ExDispatch (ExMeta "e") (AtLabel "org")) (AtMeta "a")
-        , ExDispatch (ExDispatch ExThis (AtLabel "org")) (AtLabel "x")
-        , substs [[("e", MvExpression ExThis), ("a", MvAttribute (AtLabel "x"))]]
+        , ExDispatch (ExDispatch ExXi (AtLabel "org")) (AtLabel "x")
+        , substs [[("e", MvExpression ExXi), ("a", MvAttribute (AtLabel "x"))]]
         )
       ,
         ( "[[!a -> !e, !B]].!a => [[x -> Q, y -> $]].x => [(!a >> x, !e >> Q, !B >> [y -> $])]"
         , ExDispatch (ExFormation [BiTau (AtMeta "a") (ExMeta "e"), BiMeta "B"]) (AtMeta "a")
         , ExDispatch
             ( ExFormation
-                [ BiTau (AtLabel "x") ExGlobal
-                , BiTau (AtLabel "y") ExThis
+                [ BiTau (AtLabel "x") ExRoot
+                , BiTau (AtLabel "y") ExXi
                 ]
             )
             (AtLabel "x")
         , substs
             [
               [ ("a", MvAttribute (AtLabel "x"))
-              , ("e", MvExpression ExGlobal)
-              , ("B", MvBindings [BiTau (AtLabel "y") ExThis])
+              , ("e", MvExpression ExRoot)
+              , ("B", MvBindings [BiTau (AtLabel "y") ExXi])
               ]
             ]
         )
       ,
         ( "Q * !t => Q.org => [(!t >> [.org])]"
-        , ExMetaTail ExGlobal "t"
-        , ExDispatch ExGlobal (AtLabel "x")
+        , ExMetaTail ExRoot "t"
+        , ExDispatch ExRoot (AtLabel "x")
         , substs [[("t", MvTail [TaDispatch (AtLabel "x")])]]
         )
       ,
         ( "Q * !t => Q.org(x -> [[]]) => [(!t >> [.org, (x -> [[]])])]"
-        , ExMetaTail ExGlobal "t"
-        , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))
-        , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]
+        , ExMetaTail ExRoot "t"
+        , ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))
+        , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]
         )
       ,
         ( "Q.x * !t => Q.x(y -> [[]]) => [(!t >> [(y -> [[]])])]"
-        , ExMetaTail (ExDispatch ExGlobal (AtLabel "x")) "t"
-        , ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho]))
-        , substs [[("t", MvTail [TaApplication (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho]))])]]
+        , ExMetaTail (ExDispatch ExRoot (AtLabel "x")) "t"
+        , ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExFormation [BiVoid AtRho]))
+        , substs [[("t", MvTail [TaApplication (ArTau (AtLabel "y") (ExFormation [BiVoid AtRho]))])]]
         )
       ,
         ( "Q.!a * !t => Q.org.eolang(x -> [[]]) => [(!a >> org, !t >> [ .eolang, ( x -> [[ ]] ) ])]"
-        , ExMetaTail (ExDispatch ExGlobal (AtMeta "a")) "t"
-        , ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))
-        , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]
+        , ExMetaTail (ExDispatch ExRoot (AtMeta "a")) "t"
+        , ExApplication (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")) (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))
+        , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]
         )
       ,
         ( "Q.x(y -> $ * !t1) * !t2 => Q.x(y -> $.q).p => [(!t1 >> [.q], !t2 >> [.p])]"
-        , ExMetaTail (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExMetaTail ExThis "t1"))) "t2"
-        , ExDispatch (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "q")))) (AtLabel "p")
+        , ExMetaTail (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExMetaTail ExXi "t1"))) "t2"
+        , ExDispatch (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExDispatch ExXi (AtLabel "q")))) (AtLabel "p")
         , substs [[("t1", MvTail [TaDispatch (AtLabel "q")]), ("t2", MvTail [TaDispatch (AtLabel "p")])]]
         )
       ,
         ( "[[!B1, !a ↦ !e1, !B2]](!a ↦ !e2) => ⟦ t ↦ ξ.k, x ↦ ξ.t, k ↦ ∅ ⟧(x ↦ ξ) => [(!B1 >> [[ t -> $.k ]], !a >> x, !B2 >> [[ k -> ? ]], !e1 >> $.t, !e2 >> $)]"
-        , ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "a") (ExMeta "e1"), BiMeta "B2"]) (BiTau (AtMeta "a") (ExMeta "e2"))
+        , ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "a") (ExMeta "e1"), BiMeta "B2"]) (ArTau (AtMeta "a") (ExMeta "e2"))
         , ExApplication
             ( ExFormation
-                [ BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))
-                , BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                [ BiTau (AtLabel "t") (ExDispatch ExXi (AtLabel "k"))
+                , BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                 , BiVoid (AtLabel "k")
                 ]
             )
-            (BiTau (AtLabel "x") ExThis)
+            (ArTau (AtLabel "x") ExXi)
         , substs
             [
-              [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))])
+              [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExXi (AtLabel "k"))])
               , ("a", MvAttribute (AtLabel "x"))
               , ("B2", MvBindings [BiVoid (AtLabel "k")])
-              , ("e1", MvExpression (ExDispatch ExThis (AtLabel "t")))
-              , ("e2", MvExpression ExThis)
+              , ("e1", MvExpression (ExDispatch ExXi (AtLabel "t")))
+              , ("e2", MvExpression ExXi)
               ]
             ]
         )
diff --git a/test/MiscSpec.hs b/test/MiscSpec.hs
--- a/test/MiscSpec.hs
+++ b/test/MiscSpec.hs
@@ -32,8 +32,8 @@
         )
       ,
         ( "[[^ -> Q.x, x -> $.y]] => [[^ -> Q.x, x -> $.y]]"
-        , [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
-        , [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        , [BiTau AtRho (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        , [BiTau AtRho (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
         )
       , ("[[!B]] => [[!B]]", [BiMeta "B"], [BiMeta "B"])
       , ("[[x -> ?, !B]] => [[x -> ?, !B]]", [BiVoid (AtLabel "x"), BiMeta "B"], [BiVoid (AtLabel "x"), BiMeta "B"])
@@ -54,8 +54,8 @@
         )
       ,
         ( "[[!a -> Q.x, x -> $.y]] => [[!a -> Q.x, x -> $.y]]"
-        , [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
-        , [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        , [BiTau (AtMeta "a") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        , [BiTau (AtMeta "a") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
         )
       ]
 
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -32,44 +32,44 @@
     test
       parseProgram
       [ ("Q -> [[]]", Just (Program (ExFormation [BiVoid AtRho])))
-      , ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination (BiTau (AtLabel "x") ExGlobal))))
-      , ("Q -> Q.org.eolang", Just (Program (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))))
-      , ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExThis, BiVoid (AtLabel "y"), BiVoid AtRho])))
+      , ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination (ArTau (AtLabel "x") ExRoot))))
+      , ("Q -> Q.org.eolang", Just (Program (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"))))
+      , ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "y"), BiVoid AtRho])))
       ]
 
   describe "parse expression" $
     test
       parseExpression
-      [ ("Q.!a", Just (ExDispatch ExGlobal (AtMeta "a")))
-      , ("[[]](!a1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtMeta "a1") ExThis)))
+      [ ("Q.!a", Just (ExDispatch ExRoot (AtMeta "a")))
+      , ("[[]](!a1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "a1") ExXi)))
       ,
         ( "[[]](~0 -> $)(~11 -> Q)"
         , Just
             ( ExApplication
                 ( ExApplication
                     (ExFormation [BiVoid AtRho])
-                    (BiTau (AtAlpha 0) ExThis)
+                    (ArAlpha (Alpha 0) ExXi)
                 )
-                (BiTau (AtAlpha 11) ExGlobal)
+                (ArAlpha (Alpha 11) ExRoot)
             )
         )
-      , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtLabel "x") ExThis)) (BiTau (AtLabel "y") ExGlobal)))
+      , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) (ArTau (AtLabel "y") ExRoot)))
       , ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"]))
-      , ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExThis]))
+      , ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExXi]))
       , ("!e0", Just (ExMeta "e0"))
       , ("!k", Just (ExMeta "k"))
       , ("[[x -> !k1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "k1"), BiVoid AtRho]))
       , ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e"), BiVoid AtRho]))
       , ("[[!a -> !e1]]", Just (ExFormation [BiTau (AtMeta "a") (ExMeta "e1")]))
-      , ("Q * !t", Just (ExMetaTail ExGlobal "t"))
-      , ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtLabel "x") ExThis)) "t1"))
+      , ("Q * !t", Just (ExMetaTail ExRoot "t"))
+      , ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) "t1"))
       , ("[[D> --]]", Just (ExFormation [BiDelta BtEmpty, BiVoid AtRho]))
       , ("[[D> 1F-]]", Just (ExFormation [BiDelta (BtOne "1F"), BiVoid AtRho]))
-      , ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda "Func", BiDelta (BtOne "00"), BiVoid AtRho]))
+      , ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid AtRho]))
       , ("[[D> 1F-2A-00]]", Just (ExFormation [BiDelta (BtMany ["1F", "2A", "00"]), BiVoid AtRho]))
       , ("[[D> !d0]]", Just (ExFormation [BiDelta (BtMeta "d0"), BiVoid AtRho]))
-      , ("[[L> Function]]", Just (ExFormation [BiLambda "Function", BiVoid AtRho]))
-      , ("[[L> !F3]]", Just (ExFormation [BiMetaLambda "F3", BiVoid AtRho]))
+      , ("[[L> Function]]", Just (ExFormation [BiLambda (Function "Function"), BiVoid AtRho]))
+      , ("[[L> !F3]]", Just (ExFormation [BiLambda (FnMeta "F3"), BiVoid AtRho]))
       , ("[[x() -> [[]] ]]", Just (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho]))
       ,
         ( "[[y(^,@,z) -> [[q -> Q.a]] ]]"
@@ -81,7 +81,7 @@
                         [ BiVoid AtRho
                         , BiVoid AtPhi
                         , BiVoid (AtLabel "z")
-                        , BiTau (AtLabel "q") (ExDispatch ExGlobal (AtLabel "a"))
+                        , BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "a"))
                         ]
                     )
                 , BiVoid AtRho
@@ -93,7 +93,7 @@
         , Just
             ( ExApplication
                 (ExMeta "e")
-                ( BiTau
+                ( ArTau
                     (AtLabel "x")
                     ( ExFormation
                         [ BiVoid AtRho
@@ -110,16 +110,16 @@
             ( ExFormation
                 [ BiTau
                     (AtLabel "x")
-                    (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))
+                    (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z"))
                 , BiTau
                     (AtLabel "w")
-                    (ExDispatch ExThis AtRho)
+                    (ExDispatch ExXi AtRho)
                 , BiTau
                     (AtLabel "u")
-                    (ExDispatch ExThis AtPhi)
+                    (ExDispatch ExXi AtPhi)
                 , BiTau
                     (AtLabel "p")
-                    (ExDispatch ExThis (AtMeta "a"))
+                    (ExDispatch ExXi (AtMeta "a"))
                 , BiTau
                     (AtLabel "q")
                     (ExMeta "e")
@@ -133,19 +133,19 @@
             ( ExApplication
                 ( ExApplication
                     ( ExApplication
-                        (ExDispatch ExGlobal (AtLabel "x"))
-                        (BiTau (AtAlpha 0) (ExDispatch ExThis (AtLabel "y")))
+                        (ExDispatch ExRoot (AtLabel "x"))
+                        (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "y")))
                     )
-                    (BiTau (AtAlpha 1) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z")))
+                    (ArAlpha (Alpha 1) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z")))
                 )
-                ( BiTau
-                    (AtAlpha 2)
+                ( ArAlpha
+                    (Alpha 2)
                     ( ExApplication
                         ( ExApplication
-                            (ExDispatch ExGlobal (AtLabel "y"))
-                            (BiTau (AtAlpha 0) (ExDispatch ExThis AtRho))
+                            (ExDispatch ExRoot (AtLabel "y"))
+                            (ArAlpha (Alpha 0) (ExDispatch ExXi AtRho))
                         )
-                        (BiTau (AtAlpha 1) (ExDispatch ExThis AtPhi))
+                        (ArAlpha (Alpha 1) (ExDispatch ExXi AtPhi))
                     )
                 )
             )
@@ -158,15 +158,15 @@
                     (DataNumber (BtMany ["40", "14", "00", "00", "00", "00", "00", "00"]))
                     (AtLabel "plus")
                 )
-                ( BiTau
-                    (AtAlpha 0)
+                ( ArAlpha
+                    (Alpha 0)
                     ( ExApplication
                         ( ExDispatch
                             (DataNumber (BtMany ["40", "14", "00", "00", "00", "00", "00", "00"]))
                             (AtLabel "q")
                         )
-                        ( BiTau
-                            (AtAlpha 0)
+                        ( ArAlpha
+                            (Alpha 0)
                             ( ExDispatch
                                 (DataString (BtMany ["68", "65", "6C", "6C", "6F"]))
                                 (AtLabel "length")
@@ -181,7 +181,7 @@
         , Just
             ( ExFormation
                 [ BiMeta "B1"
-                , BiTau (AtMeta "a0") ExThis
+                , BiTau (AtMeta "a0") ExXi
                 , BiTau (AtLabel "x") (ExMeta "e")
                 ]
             )
@@ -287,28 +287,28 @@
   describe "parse binding" $
     test
       parseBinding
-      [ ("x -> $", Just (BiTau (AtLabel "x") ExThis))
-      , ("y -> Q", Just (BiTau (AtLabel "y") ExGlobal))
+      [ ("x -> $", Just (BiTau (AtLabel "x") ExXi))
+      , ("y -> Q", Just (BiTau (AtLabel "y") ExRoot))
       , ("z -> ?", Just (BiVoid (AtLabel "z")))
       , ("w -> ∅", Just (BiVoid (AtLabel "w")))
       , ("^ -> T", Just (BiTau AtRho ExTermination))
-      , ("@ -> $", Just (BiTau AtPhi ExThis))
-      , ("ρ -> Q", Just (BiTau AtRho ExGlobal))
+      , ("@ -> $", Just (BiTau AtPhi ExXi))
+      , ("ρ -> Q", Just (BiTau AtRho ExRoot))
       , ("φ -> T", Just (BiTau AtPhi ExTermination))
-      , ("!a -> $", Just (BiTau (AtMeta "a") ExThis))
-      , ("!a0 -> Q", Just (BiTau (AtMeta "a0") ExGlobal))
+      , ("!a -> $", Just (BiTau (AtMeta "a") ExXi))
+      , ("!a0 -> Q", Just (BiTau (AtMeta "a0") ExRoot))
       , ("D> --", Just (BiDelta BtEmpty))
       , ("D> 42-", Just (BiDelta (BtOne "42")))
       , ("D> 01-02-03", Just (BiDelta (BtMany ["01", "02", "03"])))
       , ("D> !d", Just (BiDelta (BtMeta "d")))
       , ("Δ ⤍ FF-", Just (BiDelta (BtOne "FF")))
       , ("Δ ⤍ --", Just (BiDelta BtEmpty))
-      , ("L> Func", Just (BiLambda "Func"))
-      , ("L> Function_name", Just (BiLambda "Function_name"))
-      , ("L> Aφ", Just (BiLambda "Aφ"))
-      , ("λ ⤍ Test", Just (BiLambda "Test"))
-      , ("L> !F", Just (BiMetaLambda "F"))
-      , ("L> !F0", Just (BiMetaLambda "F0"))
+      , ("L> Func", Just (BiLambda (Function "Func")))
+      , ("L> Function_name", Just (BiLambda (Function "Function_name")))
+      , ("L> Aφ", Just (BiLambda (Function "Aφ")))
+      , ("λ ⤍ Test", Just (BiLambda (Function "Test")))
+      , ("L> !F", Just (BiLambda (FnMeta "F")))
+      , ("L> !F0", Just (BiLambda (FnMeta "F0")))
       , ("!B", Just (BiMeta "B"))
       , ("!B0", Just (BiMeta "B0"))
       , ("!B_test", Just (BiMeta "B_test"))
@@ -317,8 +317,8 @@
       , ("x() -> [[]]", Just (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])))
       , ("y(^) -> [[]]", Just (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho])))
       , ("z(^, @) -> [[]]", Just (BiTau (AtLabel "z") (ExFormation [BiVoid AtRho, BiVoid AtPhi])))
-      , ("x -> [[y -> $]]", Just (BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExThis, BiVoid AtRho])))
-      , ("x ↦ ξ", Just (BiTau (AtLabel "x") ExThis))
+      , ("x -> [[y -> $]]", Just (BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExXi, BiVoid AtRho])))
+      , ("x ↦ ξ", Just (BiTau (AtLabel "x") ExXi))
       , ("x -> ", Nothing)
       , ("-> Q", Nothing)
       , ("L>", Nothing)
@@ -342,11 +342,11 @@
       , ("!a_test", Just (AtMeta "a_test"))
       , ("𝜏", Just (AtMeta "a"))
       , ("𝜏0", Just (AtMeta "a0"))
-      , ("~0", Just (AtAlpha 0))
-      , ("~1", Just (AtAlpha 1))
-      , ("~123", Just (AtAlpha 123))
-      , ("α0", Just (AtAlpha 0))
-      , ("α42", Just (AtAlpha 42))
+      , ("~0", Nothing)
+      , ("~1", Nothing)
+      , ("~123", Nothing)
+      , ("α0", Nothing)
+      , ("α42", Nothing)
       , ("X", Nothing)
       , ("123", Nothing)
       , ("", Nothing)
@@ -384,7 +384,7 @@
 
   describe "parseExpressionThrows" $ do
     it "returns expression on valid input" $
-      parseExpressionThrows "Q.x" `shouldReturn` ExDispatch ExGlobal (AtLabel "x")
+      parseExpressionThrows "Q.x" `shouldReturn` ExDispatch ExRoot (AtLabel "x")
     it "throws on invalid input" $
       parseExpressionThrows "[[invalid" `shouldThrow` anyException
 
@@ -426,24 +426,24 @@
   describe "parse unicode syntax" $
     test
       parseExpression
-      [ ("ξ", Just ExThis)
-      , ("Φ", Just ExGlobal)
+      [ ("ξ", Just ExXi)
+      , ("Φ", Just ExRoot)
       , ("⊥", Just ExTermination)
       , ("⟦⟧", Just (ExFormation [BiVoid AtRho]))
-      , ("⟦ x ↦ ξ ⟧", Just (ExFormation [BiTau (AtLabel "x") ExThis, BiVoid AtRho]))
-      , ("ξ.ρ", Just (ExDispatch ExThis AtRho))
-      , ("ξ.φ", Just (ExDispatch ExThis AtPhi))
+      , ("⟦ x ↦ ξ ⟧", Just (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid AtRho]))
+      , ("ξ.ρ", Just (ExDispatch ExXi AtRho))
+      , ("ξ.φ", Just (ExDispatch ExXi AtPhi))
       ]
 
   describe "parse labels with special characters" $
     test
       parseExpression
-      [ ("foo123", Just (ExDispatch ExThis (AtLabel "foo123")))
-      , ("with-dash", Just (ExDispatch ExThis (AtLabel "with-dash")))
-      , ("with_underscore", Just (ExDispatch ExThis (AtLabel "with_underscore")))
-      , ("aкирилиця", Just (ExDispatch ExThis (AtLabel "aкирилиця")))
-      , ("a日本語", Just (ExDispatch ExThis (AtLabel "a日本語")))
-      , ("name123_test", Just (ExDispatch ExThis (AtLabel "name123_test")))
+      [ ("foo123", Just (ExDispatch ExXi (AtLabel "foo123")))
+      , ("with-dash", Just (ExDispatch ExXi (AtLabel "with-dash")))
+      , ("with_underscore", Just (ExDispatch ExXi (AtLabel "with_underscore")))
+      , ("aкирилиця", Just (ExDispatch ExXi (AtLabel "aкирилиця")))
+      , ("a日本語", Just (ExDispatch ExXi (AtLabel "a日本語")))
+      , ("name123_test", Just (ExDispatch ExXi (AtLabel "name123_test")))
       ]
 
   describe "parse complex formations" $
@@ -452,16 +452,16 @@
       [ ("[[^ -> ?]]", Just (ExFormation [BiVoid AtRho]))
       , ("[[@ -> ?]]", Just (ExFormation [BiVoid AtPhi, BiVoid AtRho]))
       , ("[[^ -> ?, @ -> ?]]", Just (ExFormation [BiVoid AtRho, BiVoid AtPhi]))
-      , ("[[^ -> Q, @ -> $]]", Just (ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExThis]))
+      , ("[[^ -> Q, @ -> $]]", Just (ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExXi]))
       ]
 
   describe "parse applications with mixed bindings" $
     test
       parseExpression
-      [ ("[[]](Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtAlpha 0) ExGlobal)))
-      , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtAlpha 0) ExGlobal)) (BiTau (AtAlpha 1) ExTermination)))
-      , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") ExThis)))
-      , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (BiTau (AtAlpha 0) ExGlobal)))
+      [ ("[[]](Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)))
+      , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)) (ArAlpha (Alpha 1) ExTermination)))
+      , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi)))
+      , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (ArAlpha (Alpha 0) ExRoot)))
       ]
 
   describe "parse meta expressions" $
@@ -473,7 +473,7 @@
       , ("𝑒", Just (ExMeta "e"))
       , ("𝑒0", Just (ExMeta "e0"))
       , ("!e.x", Just (ExDispatch (ExMeta "e") (AtLabel "x")))
-      , ("!e(Q)", Just (ExApplication (ExMeta "e") (BiTau (AtAlpha 0) ExGlobal)))
+      , ("!e(Q)", Just (ExApplication (ExMeta "e") (ArAlpha (Alpha 0) ExRoot)))
       , ("!n", Just (ExMeta "n"))
       , ("!n1", Just (ExMeta "n1"))
       , ("𝑛", Just (ExMeta "n"))
@@ -484,8 +484,8 @@
   describe "parse meta tails" $
     test
       parseExpression
-      [ ("Q * !t", Just (ExMetaTail ExGlobal "t"))
-      , ("Q.x * !t", Just (ExMetaTail (ExDispatch ExGlobal (AtLabel "x")) "t"))
+      [ ("Q * !t", Just (ExMetaTail ExRoot "t"))
+      , ("Q.x * !t", Just (ExMetaTail (ExDispatch ExRoot (AtLabel "x")) "t"))
       , ("[[]].y * !t0", Just (ExMetaTail (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "y")) "t0"))
       , ("Q * !t * !t2", Nothing)
       ]
diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs
--- a/test/PrinterSpec.hs
+++ b/test/PrinterSpec.hs
@@ -26,40 +26,38 @@
 spec = do
   describe "printExpression with ASCII singleline renders primitives" $
     forM_
-      [ ("ξ renders as $", ExThis, "$")
-      , ("Φ renders as Q", ExGlobal, "Q")
+      [ ("ξ renders as $", ExXi, "$")
+      , ("Φ renders as Q", ExRoot, "Q")
       , ("⊥ renders as T", ExTermination, "T")
       , ("ρ void becomes empty", ExFormation [BiVoid AtRho], "[[]]")
       , ("φ void", ExFormation [BiVoid AtPhi], "[[ @ -> ? ]]")
       , ("label void", ExFormation [BiVoid (AtLabel "名前")], "[[ 名前 -> ? ]]")
-      , ("x to Φ", ExFormation [BiTau (AtLabel "x") ExGlobal], "[[ x -> Q ]]")
-      , ("α0 to ξ", ExFormation [BiTau (AtAlpha 0) ExThis], "[[ ~0 -> $ ]]")
+      , ("x to Φ", ExFormation [BiTau (AtLabel "x") ExRoot], "[[ x -> Q ]]")
       , ("ρ to ⊥", ExFormation [BiTau AtRho ExTermination], "[[ ^ -> T ]]")
       , ("empty delta", ExFormation [BiDelta BtEmpty], "[[ D> -- ]]")
       , ("single byte", ExFormation [BiDelta (BtOne "1F")], "[[ D> 1F- ]]")
       , ("multiple bytes", ExFormation [BiDelta (BtMany ["00", "01", "02"])], "[[ D> 00-01-02 ]]")
-      , ("función lambda", ExFormation [BiLambda "Función"], "[[ L> Función ]]")
-      , ("クラス lambda", ExFormation [BiLambda "クラス"], "[[ L> クラス ]]")
-      , ("Φ.org", ExDispatch ExGlobal (AtLabel "org"), "Q.org")
-      , ("ξ.ρ as sugar", ExDispatch ExThis AtRho, "^")
-      , ("ξ.φ as sugar", ExDispatch ExThis AtPhi, "@")
-      , ("chained dispatch", ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "éolang"), "Q.org.éolang")
-      , ("ξ.α0 as sugar", ExDispatch ExThis (AtAlpha 0), "~0")
+      , ("función lambda", ExFormation [BiLambda (Function "Función")], "[[ L> Función ]]")
+      , ("クラス lambda", ExFormation [BiLambda (Function "クラス")], "[[ L> クラス ]]")
+      , ("Φ.org", ExDispatch ExRoot (AtLabel "org"), "Q.org")
+      , ("ξ.ρ as sugar", ExDispatch ExXi AtRho, "^")
+      , ("ξ.φ as sugar", ExDispatch ExXi AtPhi, "@")
+      , ("chained dispatch", ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "éolang"), "Q.org.éolang")
       ,
         ( "dispatch with app"
-        , ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") ExThis)
+        , ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi)
         , "Q.x( y -> $ )"
         )
       ,
         ( "formation with app"
-        , ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtAlpha 0) ExGlobal)
+        , ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)
         , "[[]]( Q )"
         )
       , ("meta expr", ExMeta "e", "!e")
-      , ("meta tail", ExMetaTail ExGlobal "t", "Q * !t")
+      , ("meta tail", ExMetaTail ExRoot "t", "Q * !t")
       , ("meta binding", ExFormation [BiMeta "B"], "[[ !B ]]")
-      , ("meta lambda", ExFormation [BiMetaLambda "F"], "[[ L> !F ]]")
-      , ("meta attr tau", ExFormation [BiTau (AtMeta "a") ExThis], "[[ !a -> $ ]]")
+      , ("meta lambda", ExFormation [BiLambda (FnMeta "F")], "[[ L> !F ]]")
+      , ("meta attr tau", ExFormation [BiTau (AtMeta "a") ExXi], "[[ !a -> $ ]]")
       ]
       ( \(desc, expr, expected) ->
           it desc (printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) `shouldBe` expected)
@@ -84,7 +82,7 @@
   describe "printProgram with default config" $
     forM_
       [ ("empty formation", Program (ExFormation [BiVoid AtRho]), "{⟦⟧}")
-      , ("dispatch", Program (ExDispatch ExGlobal (AtLabel "org")), "{Φ.org}")
+      , ("dispatch", Program (ExDispatch ExRoot (AtLabel "org")), "{Φ.org}")
       ]
       ( \(desc, prog, expected) ->
           it desc (printProgram prog `shouldBe` expected)
@@ -104,7 +102,7 @@
         )
       ,
         ( "rho binding placed after another binding"
-        , Program (ExFormation [BiTau (AtLabel "café") ExGlobal, BiTau AtRho (ExFormation [BiVoid AtRho])])
+        , Program (ExFormation [BiTau (AtLabel "café") ExRoot, BiTau AtRho (ExFormation [BiVoid AtRho])])
         , "Φ ↦ ⟦ café ↦ Φ, ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧"
         )
       ]
@@ -117,7 +115,6 @@
       [ ("label", AtLabel "attr", "attr")
       , ("ρ", AtRho, "ρ")
       , ("φ", AtPhi, "φ")
-      , ("α42", AtAlpha 42, "α42")
       , ("λ", AtLambda, "λ")
       , ("Δ", AtDelta, "Δ")
       ]
@@ -125,12 +122,15 @@
           it desc (printAttribute attr `shouldBe` expected)
       )
 
+  describe "printAlpha with default encoding" $
+    it "α42" (printAlpha (Alpha 42) `shouldBe` "α42")
+
   describe "printBinding renders as formation" $
     forM_
-      [ ("tau binding", BiTau (AtLabel "x") ExGlobal, "x ↦ Φ")
+      [ ("tau binding", BiTau (AtLabel "x") ExRoot, "x ↦ Φ")
       , ("void binding", BiVoid (AtLabel "y"), "y ↦ ∅")
       , ("delta binding", BiDelta (BtOne "00"), "Δ ⤍ 00-")
-      , ("lambda binding", BiLambda "Func", "λ ⤍ Func")
+      , ("lambda binding", BiLambda (Function "Func"), "λ ⤍ Func")
       ]
       ( \(desc, bd, expected) ->
           it desc (printBinding bd `shouldContain` expected)
@@ -150,7 +150,7 @@
     forM_
       [ ("attribute arg", ArgAttribute (AtLabel "tëst"), "tëst")
       , ("binding arg", ArgBinding (BiVoid (AtLabel "βind")), "βind ↦ ∅")
-      , ("expression arg", ArgExpression ExGlobal, "Φ")
+      , ("expression arg", ArgExpression ExRoot, "Φ")
       , ("bytes arg", ArgBytes (BtOne "FF"), "FF-")
       ]
       ( \(desc, arg, expected) ->
diff --git a/test/ReplacerSpec.hs b/test/ReplacerSpec.hs
--- a/test/ReplacerSpec.hs
+++ b/test/ReplacerSpec.hs
@@ -22,42 +22,42 @@
       replaceProgram
       [
         ( "Q -> Q.y.x => ([Q.y], [$]) => Q -> $.x"
-        , Program (ExDispatch (ExDispatch ExGlobal (AtLabel "y")) (AtLabel "x"))
-        , [ExDispatch ExGlobal (AtLabel "y")]
-        , [ExThis]
-        , Program (ExDispatch ExThis (AtLabel "x"))
+        , Program (ExDispatch (ExDispatch ExRoot (AtLabel "y")) (AtLabel "x"))
+        , [ExDispatch ExRoot (AtLabel "y")]
+        , [ExXi]
+        , Program (ExDispatch ExXi (AtLabel "x"))
         )
       ,
         ( "Q -> [[x -> [[y -> $]], z -> [[w -> $]] ]] => ([[y -> $], [w -> $]], [Q.y, Q.w]) => Q -> [[x -> Q.y, z -> Q.w]]"
         , Program
             ( ExFormation
-                [ BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExThis])
-                , BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "w") ExThis])
+                [ BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExXi])
+                , BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "w") ExXi])
                 ]
             )
-        , [ExFormation [BiTau (AtLabel "y") ExThis], ExFormation [BiTau (AtLabel "w") ExThis]]
-        , [ExDispatch ExGlobal (AtLabel "y"), ExDispatch ExGlobal (AtLabel "w")]
+        , [ExFormation [BiTau (AtLabel "y") ExXi], ExFormation [BiTau (AtLabel "w") ExXi]]
+        , [ExDispatch ExRoot (AtLabel "y"), ExDispatch ExRoot (AtLabel "w")]
         , Program
             ( ExFormation
-                [ BiTau (AtLabel "x") (ExDispatch ExGlobal (AtLabel "y"))
-                , BiTau (AtLabel "z") (ExDispatch ExGlobal (AtLabel "w"))
+                [ BiTau (AtLabel "x") (ExDispatch ExRoot (AtLabel "y"))
+                , BiTau (AtLabel "z") (ExDispatch ExRoot (AtLabel "w"))
                 ]
             )
         )
-      , ("Q -> [[]] => ([], [$]) => X", Program (ExFormation []), [], [ExThis], Program (ExFormation []))
+      , ("Q -> [[]] => ([], [$]) => X", Program (ExFormation []), [], [ExXi], Program (ExFormation []))
       ,
         ( "Q -> [[L> Func, D> 00-]] => ([ [[L> Func, D> 00-]] ], [Q]) => Q -> Q"
-        , Program (ExFormation [BiLambda "Func", BiDelta (BtOne "00")])
-        , [ExFormation [BiLambda "Func", BiDelta (BtOne "00")]]
-        , [ExGlobal]
-        , Program ExGlobal
+        , Program (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")])
+        , [ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")]]
+        , [ExRoot]
+        , Program ExRoot
         )
       ,
         ( "Q -> Q.org.eolang => ([Q.org.eolang, Q.org], [$, $]) => $"
-        , Program (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))
-        , [ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"), ExDispatch ExGlobal (AtLabel "org")]
-        , [ExThis, ExThis]
-        , Program ExThis
+        , Program (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"))
+        , [ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"), ExDispatch ExRoot (AtLabel "org")]
+        , [ExXi, ExXi]
+        , Program ExXi
         )
       ,
         ( "Q -> [[ x -> $.t, t -> ? ]].t(^ -> [[ x -> $.t, t -> ? ]]) => ([ [[ x -> $.t, t -> ? ]].t ], [T]) => T(^ -> [[ x -> $.t, t -> ? ]])"
@@ -65,16 +65,16 @@
             ( ExApplication
                 ( ExDispatch
                     ( ExFormation
-                        [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                        [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                         , BiVoid (AtLabel "t")
                         ]
                     )
                     (AtLabel "t")
                 )
-                ( BiTau
+                ( ArTau
                     AtRho
                     ( ExFormation
-                        [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                        [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                         , BiVoid (AtLabel "t")
                         ]
                     )
@@ -83,7 +83,7 @@
         ,
           [ ExDispatch
               ( ExFormation
-                  [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                  [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                   , BiVoid (AtLabel "t")
                   ]
               )
@@ -93,10 +93,10 @@
         , Program
             ( ExApplication
                 ExTermination
-                ( BiTau
+                ( ArTau
                     AtRho
                     ( ExFormation
-                        [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))
+                        [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
                         , BiVoid (AtLabel "t")
                         ]
                     )
@@ -112,52 +112,45 @@
         )
       ,
         ( "Q -> $ => ([$], [Q]) => Q -> Q"
-        , Program ExThis
-        , [ExThis]
-        , [ExGlobal]
-        , Program ExGlobal
-        )
-      ,
-        ( "Q -> Q.α0 => ([Q.α0], [$.α1]) => Q -> $.α1"
-        , Program (ExDispatch ExGlobal (AtAlpha 0))
-        , [ExDispatch ExGlobal (AtAlpha 0)]
-        , [ExDispatch ExThis (AtAlpha 1)]
-        , Program (ExDispatch ExThis (AtAlpha 1))
+        , Program ExXi
+        , [ExXi]
+        , [ExRoot]
+        , Program ExRoot
         )
       ,
         ( "Q -> [[D> --]] => ([[D> --]], [[[L> Функція]]]) => Q -> [[L> Функція]]"
         , Program (ExFormation [BiDelta BtEmpty])
         , [ExFormation [BiDelta BtEmpty]]
-        , [ExFormation [BiLambda "Функція"]]
-        , Program (ExFormation [BiLambda "Функція"])
+        , [ExFormation [BiLambda (Function "Функція")]]
+        , Program (ExFormation [BiLambda (Function "Функція")])
         )
       ,
         ( "Q -> Q.プログラム => ([Q.プログラム], [$.コード]) => Q -> $.コード"
-        , Program (ExDispatch ExGlobal (AtLabel "プログラム"))
-        , [ExDispatch ExGlobal (AtLabel "プログラム")]
-        , [ExDispatch ExThis (AtLabel "コード")]
-        , Program (ExDispatch ExThis (AtLabel "コード"))
+        , Program (ExDispatch ExRoot (AtLabel "プログラム"))
+        , [ExDispatch ExRoot (AtLabel "プログラム")]
+        , [ExDispatch ExXi (AtLabel "コード")]
+        , Program (ExDispatch ExXi (AtLabel "コード"))
         )
       ,
         ( "Q -> [[^ -> T, @ -> T]] => ([T, T], [Q, $]) => Q -> [[^ -> Q, @ -> $]]"
         , Program (ExFormation [BiTau AtRho ExTermination, BiTau AtPhi ExTermination])
         , [ExTermination, ExTermination]
-        , [ExGlobal, ExThis]
-        , Program (ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExThis])
+        , [ExRoot, ExXi]
+        , Program (ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExXi])
         )
       ,
         ( "Q -> [[x -> [[y -> Q]]]].x => ([[y -> Q]], [[[z -> $]]]) => Q -> [[x -> [[z -> $]]]].x"
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExGlobal])]) (AtLabel "x"))
-        , [ExFormation [BiTau (AtLabel "y") ExGlobal]]
-        , [ExFormation [BiTau (AtLabel "z") ExThis]]
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "z") ExThis])]) (AtLabel "x"))
+        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x"))
+        , [ExFormation [BiTau (AtLabel "y") ExRoot]]
+        , [ExFormation [BiTau (AtLabel "z") ExXi]]
+        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "z") ExXi])]) (AtLabel "x"))
         )
       ,
         ( "Q -> Q.a(b -> Q.c) => ([Q.a, Q.c], [$, T]) => Q -> $(b -> T)"
-        , Program (ExApplication (ExDispatch ExGlobal (AtLabel "a")) (BiTau (AtLabel "b") (ExDispatch ExGlobal (AtLabel "c"))))
-        , [ExDispatch ExGlobal (AtLabel "a"), ExDispatch ExGlobal (AtLabel "c")]
-        , [ExThis, ExTermination]
-        , Program (ExApplication ExThis (BiTau (AtLabel "b") ExTermination))
+        , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExDispatch ExRoot (AtLabel "c"))))
+        , [ExDispatch ExRoot (AtLabel "a"), ExDispatch ExRoot (AtLabel "c")]
+        , [ExXi, ExTermination]
+        , Program (ExApplication ExXi (ArTau (AtLabel "b") ExTermination))
         )
       ,
         ( "Q -> [[D> 00-01-02-]] => ([[D> 00-01-02-]], [[[D> FF-]]]) => Q -> [[D> FF-]]"
@@ -168,21 +161,21 @@
         )
       ,
         ( "Q -> [[@ -> $.x, ^ -> $.y]] => ([$.x, $.y], [T, Q]) => Q -> [[@ -> T, ^ -> Q]]"
-        , Program (ExFormation [BiTau AtPhi (ExDispatch ExThis (AtLabel "x")), BiTau AtRho (ExDispatch ExThis (AtLabel "y"))])
-        , [ExDispatch ExThis (AtLabel "x"), ExDispatch ExThis (AtLabel "y")]
-        , [ExTermination, ExGlobal]
-        , Program (ExFormation [BiTau AtPhi ExTermination, BiTau AtRho ExGlobal])
+        , Program (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "x")), BiTau AtRho (ExDispatch ExXi (AtLabel "y"))])
+        , [ExDispatch ExXi (AtLabel "x"), ExDispatch ExXi (AtLabel "y")]
+        , [ExTermination, ExRoot]
+        , Program (ExFormation [BiTau AtPhi ExTermination, BiTau AtRho ExRoot])
         )
       ,
         ( "Q -> Q.a.b.c => ([Q.a.b.c, Q.a.b, Q.a], [$, T, Q]) => Q -> $"
-        , Program (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (AtLabel "c"))
+        , Program (ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c"))
         ,
-          [ ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
-          , ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")
-          , ExDispatch ExGlobal (AtLabel "a")
+          [ ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
+          , ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")
+          , ExDispatch ExRoot (AtLabel "a")
           ]
-        , [ExThis, ExTermination, ExGlobal]
-        , Program ExThis
+        , [ExXi, ExTermination, ExRoot]
+        , Program ExXi
         )
       ]
 
@@ -193,8 +186,8 @@
         ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]"
         , Program (ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta])
         , [ExFormation [BiVoid AtRho], ExFormation [BiVoid AtPhi], ExFormation [BiVoid AtDelta]]
-        , [ExFormation [BiTau AtRho ExThis], ExFormation [BiTau AtPhi ExThis], ExFormation [BiTau AtDelta ExThis]]
-        , Program (ExFormation [BiTau AtRho ExThis, BiTau AtPhi ExThis, BiTau AtDelta ExThis])
+        , [ExFormation [BiTau AtRho ExXi], ExFormation [BiTau AtPhi ExXi], ExFormation [BiTau AtDelta ExXi]]
+        , Program (ExFormation [BiTau AtRho ExXi, BiTau AtPhi ExXi, BiTau AtDelta ExXi])
         )
       ,
         ( "Q -> [[ ^ -> ? ]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> [[ !a -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]"
@@ -205,10 +198,10 @@
         )
       ,
         ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@"
-        , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (BiTau AtRho (ExFormation [BiTau AtRho ExThis]))) AtPhi)
-        , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExThis]]
-        , [ExFormation [BiTau AtRho ExGlobal], ExFormation [BiVoid AtPhi]]
-        , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExGlobal]) (BiTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi)
+        , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (ArTau AtRho (ExFormation [BiTau AtRho ExXi]))) AtPhi)
+        , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExXi]]
+        , [ExFormation [BiTau AtRho ExRoot], ExFormation [BiVoid AtPhi]]
+        , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExRoot]) (ArTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi)
         )
       ,
         ( "Q -> [[ ]] => ([], []) => Q -> [[ ]]"
@@ -219,59 +212,59 @@
         )
       ,
         ( "Q -> $ => ([$], [T]) => Q -> $"
-        , Program ExThis
-        , [ExThis]
+        , Program ExXi
+        , [ExXi]
         , [ExTermination]
-        , Program ExThis
+        , Program ExXi
         )
       ,
         ( "Q -> [[ a -> ?, b -> ?, c -> ? ]] => ([[a -> ?]], [[a -> Q]]) => Q -> [[a -> Q, b -> ?, c -> ?]]"
         , Program (ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "b"), BiVoid (AtLabel "c")])
         , [ExFormation [BiVoid (AtLabel "a")]]
-        , [ExFormation [BiTau (AtLabel "a") ExGlobal]]
-        , Program (ExFormation [BiTau (AtLabel "a") ExGlobal, BiVoid (AtLabel "b"), BiVoid (AtLabel "c")])
+        , [ExFormation [BiTau (AtLabel "a") ExRoot]]
+        , Program (ExFormation [BiTau (AtLabel "a") ExRoot, BiVoid (AtLabel "b"), BiVoid (AtLabel "c")])
         )
       ,
         ( "Q -> [[ λ -> ?, D> 00- ]] => ([[λ -> ?]], [[λ -> $]]) => Q -> [[λ -> $, D> 00-]]"
         , Program (ExFormation [BiVoid AtLambda, BiDelta (BtOne "00")])
         , [ExFormation [BiVoid AtLambda]]
-        , [ExFormation [BiTau AtLambda ExThis]]
-        , Program (ExFormation [BiTau AtLambda ExThis, BiDelta (BtOne "00")])
+        , [ExFormation [BiTau AtLambda ExXi]]
+        , Program (ExFormation [BiTau AtLambda ExXi, BiDelta (BtOne "00")])
         )
       ,
         ( "Q -> [[x -> [[y -> ?]]]].x => ([[y -> ?]], [[y -> Q]]) => Q -> [[x -> [[y -> Q]]]].x"
         , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid (AtLabel "y")])]) (AtLabel "x"))
         , [ExFormation [BiVoid (AtLabel "y")]]
-        , [ExFormation [BiTau (AtLabel "y") ExGlobal]]
-        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExGlobal])]) (AtLabel "x"))
+        , [ExFormation [BiTau (AtLabel "y") ExRoot]]
+        , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x"))
         )
       ,
         ( "Q -> [[アイテム -> ?]] => ([[アイテム -> ?]], [[アイテム -> $]]) => Q -> [[アイテム -> $]]"
         , Program (ExFormation [BiVoid (AtLabel "アイテム")])
         , [ExFormation [BiVoid (AtLabel "アイテム")]]
-        , [ExFormation [BiTau (AtLabel "アイテム") ExThis]]
-        , Program (ExFormation [BiTau (AtLabel "アイテム") ExThis])
+        , [ExFormation [BiTau (AtLabel "アイテム") ExXi]]
+        , Program (ExFormation [BiTau (AtLabel "アイテム") ExXi])
         )
       ,
         ( "Q -> [[a -> ?, a -> ?]] => ([[a -> ?]], [[a -> Q]]) => Q -> [[a -> Q, a -> Q]]"
         , Program (ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "a")])
         , [ExFormation [BiVoid (AtLabel "a")]]
-        , [ExFormation [BiTau (AtLabel "a") ExGlobal]]
-        , Program (ExFormation [BiTau (AtLabel "a") ExGlobal, BiTau (AtLabel "a") ExGlobal])
+        , [ExFormation [BiTau (AtLabel "a") ExRoot]]
+        , Program (ExFormation [BiTau (AtLabel "a") ExRoot, BiTau (AtLabel "a") ExRoot])
         )
       ,
         ( "Q -> Q.a(b -> [[c -> ?]]) => ([[c -> ?]], [[c -> T]]) => Q -> Q.a(b -> [[c -> T]])"
-        , Program (ExApplication (ExDispatch ExGlobal (AtLabel "a")) (BiTau (AtLabel "b") (ExFormation [BiVoid (AtLabel "c")])))
+        , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiVoid (AtLabel "c")])))
         , [ExFormation [BiVoid (AtLabel "c")]]
         , [ExFormation [BiTau (AtLabel "c") ExTermination]]
-        , Program (ExApplication (ExDispatch ExGlobal (AtLabel "a")) (BiTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") ExTermination])))
+        , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") ExTermination])))
         )
       ,
         ( "Q -> [[ L> Функція ]] => ([[ L> Функція ]], [[ L> Код ]]) => Q -> [[ L> Код ]]"
-        , Program (ExFormation [BiLambda "Функція"])
-        , [ExFormation [BiLambda "Функція"]]
-        , [ExFormation [BiLambda "Код"]]
-        , Program (ExFormation [BiLambda "Код"])
+        , Program (ExFormation [BiLambda (Function "Функція")])
+        , [ExFormation [BiLambda (Function "Функція")]]
+        , [ExFormation [BiLambda (Function "Код")]]
+        , Program (ExFormation [BiLambda (Function "Код")])
         )
       ]
 
@@ -282,7 +275,7 @@
         ( "Q -> [[a -> ?]] => ([[a -> ?]], [[a -> $]]) => Q -> [[a -> ?]]"
         , Program (ExFormation [BiVoid (AtLabel "a")])
         , [ExFormation [BiVoid (AtLabel "a")]]
-        , [ExFormation [BiTau (AtLabel "a") ExThis]]
+        , [ExFormation [BiTau (AtLabel "a") ExXi]]
         , Program (ExFormation [BiVoid (AtLabel "a")])
         )
       ]
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -8,7 +8,7 @@
 
 module RewriterSpec where
 
-import AST (Expression (ExGlobal))
+import AST (Expression (ExRoot))
 import Control.Monad (forM_, unless)
 import Data.Aeson
 import Data.Char (isSpace)
@@ -107,7 +107,7 @@
                   prog
                   rules'
                   ( RewriteContext
-                      ExGlobal
+                      ExRoot
                       repeat'
                       repeat'
                       False
diff --git a/test/RuleSpec.hs b/test/RuleSpec.hs
--- a/test/RuleSpec.hs
+++ b/test/RuleSpec.hs
@@ -7,7 +7,7 @@
 
 module RuleSpec where
 
-import AST (Attribute (..), Binding (..), Bytes (..), Expression (..), Program (Program))
+import AST (Argument (..), Attribute (..), Binding (..), Bytes (..), Expression (..), Function (..), Program (Program))
 import Control.Monad
 import Data.Aeson
 import Data.Yaml qualified as Y
@@ -61,17 +61,17 @@
   describe "isNF determines normal form" $ do
     let ctx = RuleContext buildTerm
     forM_
-      [ ("returns true for ExThis", ExThis, True)
-      , ("returns true for ExGlobal", ExGlobal, True)
+      [ ("returns true for ExXi", ExXi, True)
+      , ("returns true for ExRoot", ExRoot, True)
       , ("returns true for ExTermination", ExTermination, True)
-      , ("returns true for dispatch on ExThis", ExDispatch ExThis (AtLabel "foo"), True)
-      , ("returns true for dispatch on ExGlobal", ExDispatch ExGlobal (AtLabel "bar"), True)
+      , ("returns true for dispatch on ExXi", ExDispatch ExXi (AtLabel "foo"), True)
+      , ("returns true for dispatch on ExRoot", ExDispatch ExRoot (AtLabel "bar"), True)
       , ("returns false for dispatch on ExTermination", ExDispatch ExTermination (AtLabel "x"), False)
-      , ("returns false for application on ExTermination", ExApplication ExTermination (BiTau (AtLabel "y") ExGlobal), False)
+      , ("returns false for application on ExTermination", ExApplication ExTermination (ArTau (AtLabel "y") ExRoot), False)
       , ("returns true for empty formation", ExFormation [], True)
       , ("returns true for formation with only delta binding", ExFormation [BiDelta (BtMany ["00", "01"])], True)
       , ("returns true for formation with only void binding", ExFormation [BiVoid (AtLabel "x")], True)
-      , ("returns true for formation with only lambda binding", ExFormation [BiLambda "Func"], True)
-      , ("returns true for formation with delta void and lambda", ExFormation [BiDelta (BtOne "FF"), BiVoid (AtLabel "y"), BiLambda "G"], True)
+      , ("returns true for formation with only lambda binding", ExFormation [BiLambda (Function "Func")], True)
+      , ("returns true for formation with delta void and lambda", ExFormation [BiDelta (BtOne "FF"), BiVoid (AtLabel "y"), BiLambda (Function "G")], True)
       ]
       (\(desc, expr, expected) -> it desc $ isNF expr ctx `shouldBe` expected)
diff --git a/test/TauSpec.hs b/test/TauSpec.hs
--- a/test/TauSpec.hs
+++ b/test/TauSpec.hs
@@ -26,8 +26,8 @@
     seedTaus
       ( Program
           ( ExFormation
-              [ BiTau (AtLabel "a🌵0") ExGlobal
-              , BiTau (AtLabel "a🌵2") ExGlobal
+              [ BiTau (AtLabel "a🌵0") ExRoot
+              , BiTau (AtLabel "a🌵2") ExRoot
               ]
           )
       )