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.78
+cabal install --overwrite-policy=always phino-0.0.79
 phino --version
 ```
 
@@ -419,55 +419,55 @@
 === parse/phi ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      1440313.041 μs
-  avg:        144031.304 μs
-  min:        129401.716 μs
-  max:        176360.645 μs
-  std dev:    17903.429 μs
+  total:      1299342.512 μs
+  avg:        129934.251 μs
+  min:        118253.218 μs
+  max:        162332.377 μs
+  std dev:    16619.006 μs
 === parse/xmir ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      7726130.473 μs
-  avg:        772613.047 μs
-  min:        698264.764 μs
-  max:        823731.966 μs
-  std dev:    37463.636 μs
+  total:      7609340.593 μs
+  avg:        760934.059 μs
+  min:        697264.466 μs
+  max:        801903.360 μs
+  std dev:    31387.398 μs
 === rewrite/normalize ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      354506.194 μs
-  avg:        35450.619 μs
-  min:        35028.708 μs
-  max:        36155.099 μs
-  std dev:    348.991 μs
+  total:      394738.996 μs
+  avg:        39473.900 μs
+  min:        38668.484 μs
+  max:        40389.889 μs
+  std dev:    473.832 μs
 === print/sweet/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      3996044.953 μs
-  avg:        399604.495 μs
-  min:        380451.516 μs
-  max:        426315.460 μs
-  std dev:    12846.211 μs
+  total:      4562591.028 μs
+  avg:        456259.103 μs
+  min:        451902.950 μs
+  max:        462770.604 μs
+  std dev:    3059.588 μs
 === print/sweet/flat ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      3922886.214 μs
-  avg:        392288.621 μs
-  min:        359335.839 μs
-  max:        413380.865 μs
-  std dev:    17623.494 μs
+  total:      4529234.270 μs
+  avg:        452923.427 μs
+  min:        418300.611 μs
+  max:        476533.304 μs
+  std dev:    23032.941 μs
 === print/salty/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      13752970.922 μs
-  avg:        1375297.092 μs
-  min:        1346097.350 μs
-  max:        1437457.343 μs
-  std dev:    32845.881 μs
+  total:      13656171.599 μs
+  avg:        1365617.160 μs
+  min:        1311639.249 μs
+  max:        1429575.023 μs
+  std dev:    37618.391 μs
 ```
 
 The results were calculated in [this GHA job][benchmark-gha]
-on 2026-06-11 at 08:27,
+on 2026-06-11 at 11:02,
 on Linux with 4 CPUs.
 
 <!-- benchmark_end -->
@@ -503,4 +503,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/27333912876
+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27342074018
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.79
+version: 0.0.80
 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/src/AST.hs b/src/AST.hs
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE LambdaCase #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
@@ -6,6 +7,8 @@
 -- This module represents AST tree for parsed phi-calculus program
 module AST where
 
+import Data.Bits (xor)
+import Data.List (foldl')
 import Data.Text (Text)
 import qualified Data.Text as T
 import GHC.Generics (Generic)
@@ -60,6 +63,70 @@
   show AtDelta = "Δ"
   show AtLambda = "λ"
   show (AtMeta 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
+-- must always be confirmed with a full structural (==) comparison.
+hashExpression :: Expression -> Int
+hashExpression = goExpr fnvOffset
+  where
+    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
+      ExTermination -> step h 4
+      ExApplication ex bd -> goBinding (goExpr (step h 5) ex) bd
+      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
+      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
 
 countNodes :: Expression -> Int
 countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -16,7 +16,7 @@
 import Control.Exception (Exception, throwIO)
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
-import qualified Data.Set as Set
+import qualified Data.Map.Strict as Map
 import Deps
 import Locator (locatedExpression, withLocatedExpression)
 import Logger (logDebug)
@@ -30,8 +30,24 @@
 import Text.Printf (printf)
 import qualified Yaml as Y
 
-type RewriteState = (NonEmpty Rewritten, Set.Set Expression, Bool)
+type RewriteState = (NonEmpty Rewritten, Seen, Bool)
 
+-- Loop-detection store. It maps a cheap fixed-size digest of a program (see
+-- 'hashExpression') to the full expressions that produced that digest. A
+-- digest collision is resolved by a slow, exact structural (==) comparison,
+-- so loops are still detected soundly while the common (no collision) case
+-- stays O(1) on the digest instead of O(programSize) per lookup/insert.
+type Seen = Map.Map Int [Expression]
+
+-- Has this exact program been seen before? The digest lookup is fast; the
+-- (==) check runs only on a digest match, guarding against hash collisions.
+seenMember :: Int -> Expression -> Seen -> Bool
+seenMember digest expr seen = maybe False (elem expr) (Map.lookup digest seen)
+
+-- Remember a program under its digest, keeping any earlier collisions.
+seenInsert :: Int -> Expression -> Seen -> Seen
+seenInsert digest expr = Map.insertWith (++) digest [expr]
+
 type Rewritten = (Program, Maybe String)
 
 type Rewrittens = (NonEmpty Rewritten, Bool)
@@ -174,20 +190,21 @@
                       logDebug (printf "Applied '%s', no changes made" ruleName)
                       pure (_rewrittens, _unique, False)
                     else
-                      if Set.member expr _unique
-                        then throwIO (LoopingRewriting (printExpression expr) ruleName _count)
-                        else do
-                          logDebug
-                            ( printf
-                                "Applied '%s' (%d nodes -> %d nodes)\n%s"
-                                ruleName
-                                (countNodes expression)
-                                (countNodes expr)
-                                (printExpression expr)
-                            )
-                          prog <- withLocatedExpression _locator expr program
-                          _saveStep prog (((iteration - 1) * _maxDepth) + _count)
-                          _rewrite (leadsTo prog, Set.insert expr _unique, False) (_count + 1)
+                      let digest = hashExpression expr
+                       in if seenMember digest expr _unique
+                            then throwIO (LoopingRewriting (printExpression expr) ruleName _count)
+                            else do
+                              logDebug
+                                ( printf
+                                    "Applied '%s' (%d nodes -> %d nodes)\n%s"
+                                    ruleName
+                                    (countNodes expression)
+                                    (countNodes expr)
+                                    (printExpression expr)
+                                )
+                              prog <- withLocatedExpression _locator expr program
+                              _saveStep prog (((iteration - 1) * _maxDepth) + _count)
+                              _rewrite (leadsTo prog, seenInsert digest expr _unique, False) (_count + 1)
       where
         leadsTo :: Program -> NonEmpty Rewritten
         leadsTo _prog =
@@ -197,7 +214,7 @@
 -- Rewrite program by provided locator from RewriteContext
 rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens
 rewrite prog rules ctx@RewriteContext{..} = do
-  (rewrittens, exceeded) <- _rewrite ((prog, Nothing) :| [], Set.empty, False) 0
+  (rewrittens, exceeded) <- _rewrite ((prog, Nothing) :| [], Map.empty, False) 0
   pure (NE.reverse rewrittens, exceeded)
   where
     _rewrite :: RewriteState -> Int -> IO Rewrittens