------------------------------------------------------------------------
-- The two semantics are equivalent
------------------------------------------------------------------------

module Semantics.Equivalence where

open import Syntax
open import Semantics.BigStep
open import Semantics.SmallStep
open import Semantics.SmallStep.EvalCtxt
open ⟶-Reasoning
open import Infinite hiding (_⇓_; return)
open import Totality

open import Data.Star hiding (return)
open import Data.Product
open import Data.Nat
open import Relation.Nullary
open import Category.Monad
open RawMonad ¬¬-Monad hiding (_>>_)
open import Data.Function

------------------------------------------------------------------------
-- Statement of equivalence

record Big⇒Small : Set where
  field
    ⇓ : ∀ {t} {e : Expr t} {i v} → e ⇓[ i ] v → e ˢ ⟶⋆[ i ] done v
    ⇑ : ∀ {t} {e : Expr t} {i}   → e ⇑[ i ]   → e ˢ ⟶∞[ i ]

record Small⇒Big : Set where
  field
    ⟶⋆ : ∀ {t} {e : Exprˢ t} {i v} → e ⟶⋆[ i ] done v → e ˢ⁻¹ ⇓[ i ] v
    ⟶∞ : ∀ {t} (e : Exprˢ t) i     → e ⟶∞[ i ]    → ¬ ¬ e ˢ⁻¹ ⇑[ i ]

------------------------------------------------------------------------
-- Proof of Big⇒Small

big⇒small⇓ : ∀ {t} {e : Expr t} {i v} →
             e ⇓[ i ] v → e ˢ ⟶⋆[ i ] done v
big⇒small⇓ (Val {v = v}) = begin
  run ⌜ v ⌝ ⟶⟨ Red Val ⟩
  done  v   ∎
big⇒small⇓ (Loop {x = x} {v} ⇓) = begin
  run (loop (x ˢ))              ⟶⟨ Red Loop ⟩
  run (x ˢ >> run (loop (x ˢ))) ⟶⋆⟨ big⇒small⇓ ⇓ ⟩
  done v                        ∎
big⇒small⇓ (Add₁ {x = x} {y} {m} {n} x⇓ y⇓) = begin
  run (x ˢ          ⊕ y ˢ)          ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x⇓) ⟩
  run (done (nat m) ⊕ y ˢ)          ⟶⋆⟨ lift⟶⋆ (nat m ⊕• •) (big⇒small⇓ y⇓) ⟩
  run (done (nat m) ⊕ done (nat n)) ⟶⟨ Red Add₁ ⟩
  done (nat (m + n))                ∎
big⇒small⇓ (Add₂ {x = x} {y} x↯) = begin
  run (x ˢ        ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x↯) ⟩
  run (done throw ⊕ y ˢ) ⟶⟨ Red Add₂ ⟩
  done throw             ∎
big⇒small⇓ (Add₃ {x = x} {y} {m} x⇓ y↯) = begin
  run (x ˢ          ⊕ y ˢ)        ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x⇓) ⟩
  run (done (nat m) ⊕ y ˢ)        ⟶⋆⟨ lift⟶⋆ (nat m ⊕• •) (big⇒small⇓ y↯) ⟩
  run (done (nat m) ⊕ done throw) ⟶⟨ Red Add₃ ⟩
  done throw                      ∎
big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin
  run (x ˢ          >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •>> y ˢ) (big⇒small⇓ x⇓) ⟩
  run (done (nat m) >> y ˢ) ⟶⟨ Red Seqn₁ ⟩
  y ˢ                       ⟶⋆⟨ big⇒small⇓ y⇒ ⟩
  done v                    ∎
big⇒small⇓ (Seqn₂ {x = x} {y} x↯) = begin
  run (x ˢ        >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •>> y ˢ) (big⇒small⇓ x↯) ⟩
  run (done throw >> y ˢ) ⟶⟨ Red Seqn₂ ⟩
  done throw              ∎
big⇒small⇓ (Catch₁ {x = x} {y} {m} x⇓) = begin
  run (x ˢ          catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •catch y ˢ) (big⇒small⇓ x⇓) ⟩
  run (done (nat m) catch y ˢ) ⟶⟨ Red Catch₁ ⟩
  done (nat m)                 ∎
big⇒small⇓ (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin
  run (x ˢ        catch y ˢ)    ⟶⋆⟨ lift⟶⋆ (• •catch y ˢ) (big⇒small⇓ x↯) ⟩
  run (done throw catch y ˢ)    ⟶⋆⟨ lift⟶⋆ (handler• •) (big⇒small⇓ y⇒) ⟩
  run (done throw catch done v) ⟶⟨ Red Catch₂ ⟩
  done v                        ∎
big⇒small⇓ (Int {x = x}) = begin
  x ˢ        ⟶⟨ Red (Int (x ˢ-interruptible)) ⟩
  done throw ∎
big⇒small⇓ (Block {x = x} {v} x⇒) = begin
  run (block (x ˢ))    ⟶⋆⟨ lift⟶⋆ (block• •) (big⇒small⇓ x⇒) ⟩
  run (block (done v)) ⟶⟨ Red Block ⟩
  done v               ∎
big⇒small⇓ (Unblock {x = x} {v} x⇒) = begin
  run (unblock (x ˢ))    ⟶⋆⟨ lift⟶⋆ (unblock• •) (big⇒small⇓ x⇒) ⟩
  run (unblock (done v)) ⟶⟨ Red Unblock ⟩
  done v                 ∎

-- big⇒small⇑ʳ would not pass the productivity checker if it was
-- defined corecursively, so a workaround is used (see
-- Infinite.Infiniteʳ).

data Loops t i : Exprˢ t → Set where
  ⇑:_ : ∀ {e} (⇑ : e ⇑[ i ]) → Loops t i (e ˢ)

lift⟶∞ʳ : ∀ {t i j x g}
          (E : EvalCtxt t i j) →
          Infiniteʳ Step (Loops t) g i x →
          Infiniteʳ Step (Loops t) g j (E [ x ])
lift⟶∞ʳ E = map∞ʳ (λ x → E [ x ]) (lift⟶ E)

big⇒small⇑ʳ : ∀ {t g} → Stepper Step (Loops t) g
big⇒small⇑ʳ (⇑: Loop ⇑)       = Red Loop ◅∞ rec (⇑: ⇑)
big⇒small⇑ʳ (⇑: Add₁ x⇑)      = lift⟶∞ʳ (• •⊕ _) (big⇒small⇑ʳ (⇑: x⇑))
big⇒small⇑ʳ (⇑: Add₂ x↡ y⇑)   = lift⟶⋆ (• •⊕ _) (big⇒small⇓ (proj₂ x↡))
                                  ◅◅∞ʳ
                                lift⟶∞ʳ (nat proj₁ x↡ ⊕• •) (big⇒small⇑ʳ (⇑: y⇑))
big⇒small⇑ʳ (⇑: Seqn₁ x⇑)     = lift⟶∞ʳ (• •>> _) (big⇒small⇑ʳ (⇑: x⇑))
big⇒small⇑ʳ (⇑: Seqn₂ x↡ y⇑)  = lift⟶⋆ (• •>> _) (big⇒small⇓ (proj₂ x↡))
                                  ◅◅∞ʳ
                                Red Seqn₁
                                  ◅∞
                                big⇒small⇑ʳ (⇑: y⇑)
big⇒small⇑ʳ (⇑: Catch₁ x⇑)    = lift⟶∞ʳ (• •catch _) (big⇒small⇑ʳ (⇑: x⇑))
big⇒small⇑ʳ (⇑: Catch₂ x↯ y⇑) = lift⟶⋆ (• •catch _) (big⇒small⇓ x↯)
                                  ◅◅∞ʳ
                                lift⟶∞ʳ (handler• •) (big⇒small⇑ʳ (⇑: y⇑))
big⇒small⇑ʳ (⇑: Block x⇑)     = lift⟶∞ʳ (block• •) (big⇒small⇑ʳ (⇑: x⇑))
big⇒small⇑ʳ (⇑: Unblock x⇑)   = lift⟶∞ʳ (unblock• •) (big⇒small⇑ʳ (⇑: x⇑))

big⇒small⇑ : ∀ {t} {e : Expr t} {i} → e ⇑[ i ] → e ˢ ⟶∞[ i ]
big⇒small⇑ = unfold big⇒small⇑ʳ ∘ ⇑:_

-- An alternative solution to the productivity problem. Unfortunately
-- Agda does not normalise the right-hand sides (with the thing
-- defined kept neutral) before checking productivity, so the code is
-- not accepted. (And inlining lift⟶∞′ leads to less readable code,
-- especially since it appears that some hidden arguments need to be
-- given in order to keep the type checker happy.)

-- lift⟶∞′ : ∀ {t i j x}
--           (E : EvalCtxt t i j) →
--           Infinite″ (Step i) x →
--           Infinite″ (Step j) (E [ x ])
-- lift⟶∞′ E = map∞′ (λ x → E [ x ]) (lift⟶ E)

-- big⇒small⇑' : ∀ {t i} {e : Expr t} →
--               e ⇑[ i ] → Infinite″ (Step i) (e ˢ)
-- big⇒small⇑' (Loop ⇑)       ~ ↓ Red Loop ◅∞ big⇒small⇑' ⇑
-- big⇒small⇑' (Add₁ x⇑)      ~ lift⟶∞′ (• •⊕ _) (big⇒small⇑' x⇑)
-- big⇒small⇑' (Add₂ x↡ y⇑)   ~ lift⟶⋆ (• •⊕ _) (big⇒small⇓ (proj₂ x↡))
--                                ◅◅∞′
--                              lift⟶∞′ (nat proj₁ x↡ ⊕• •) (big⇒small⇑' y⇑)
-- big⇒small⇑' (Seqn₁ x⇑)     ~ lift⟶∞′ (• •>> _) (big⇒small⇑' x⇑)
-- big⇒small⇑' (Seqn₂ x↡ y⇑)  ~ lift⟶⋆ (• •>> _) (big⇒small⇓ (proj₂ x↡))
--                                ◅◅∞′
--                              (↓ Red Seqn₁ ◅∞ big⇒small⇑' y⇑)
-- big⇒small⇑' (Catch₁ x⇑)    ~ lift⟶∞′ (• •catch _) (big⇒small⇑' x⇑)
-- big⇒small⇑' (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •catch _) (big⇒small⇓ x↯)
--                                ◅◅∞′
--                              lift⟶∞′ (handler• •) (big⇒small⇑' y⇑)
-- big⇒small⇑' (Block x⇑)     ~ lift⟶∞′ (block• •) (big⇒small⇑' x⇑)
-- big⇒small⇑' (Unblock x⇑)   ~ lift⟶∞′ (unblock• •) (big⇒small⇑' x⇑)

-- big⇒small⇑₂ : ∀ {t i} {e : Expr t} → e ⇑[ i ] → e ˢ ⟶∞[ i ]
-- big⇒small⇑₂ ⇑ = ∞″→∞ (big⇒small⇑' ⇑)

big⇒small : Big⇒Small
big⇒small = record { ⇓ = big⇒small⇓; ⇑ = big⇒small⇑ }

------------------------------------------------------------------------
-- Proof of Small⇒Big

-- First note that we can map over combinations of evaluation contexts
-- and the big-step relations.

map⇓ : ∀ {t} {x₁ x₂ : Exprˢ t} {i j v} (E : EvalCtxt t i j) →
       (∀ {v} → x₁ ˢ⁻¹ ⇓[ i ] v → x₂ ˢ⁻¹ ⇓[ i ] v) →
       E [ x₁ ] ˢ⁻¹ ⇓[ j ] v → E [ x₂ ] ˢ⁻¹ ⇓[ j ] v
map⇓ •            f ⇓              = f ⇓
map⇓ (E •⊕ y)     f (Add₁ x↡ y↡)   = Add₁ (map⇓ E f x↡) y↡
map⇓ (E •⊕ y)     f (Add₂ x↯)      = Add₂ (map⇓ E f x↯)
map⇓ (E •⊕ y)     f (Add₃ x↡ y↯)   = Add₃ (map⇓ E f x↡) y↯
map⇓ (E •⊕ y)     f Int            = Int
map⇓ (E •>> y)    f (Seqn₁ x↡ y⇓)  = Seqn₁ (map⇓ E f x↡) y⇓
map⇓ (E •>> y)    f (Seqn₂ x↯)     = Seqn₂ (map⇓ E f x↯)
map⇓ (E •>> y)    f Int            = Int
map⇓ (E •catch y) f (Catch₁ x↡)    = Catch₁ (map⇓ E f x↡)
map⇓ (E •catch y) f (Catch₂ x↯ y⇓) = Catch₂ (map⇓ E f x↯) y⇓
map⇓ (E •catch y) f Int            = Int
map⇓ (nat m ⊕• E) f (Add₁ x↡ y↡)   = Add₁ x↡ (map⇓ E f y↡)
map⇓ (nat m ⊕• E) f (Add₂ x↯)      = Add₂ x↯
map⇓ (nat m ⊕• E) f (Add₃ x↡ y↯)   = Add₃ x↡ (map⇓ E f y↯)
map⇓ (nat m ⊕• E) f Int            = Int
map⇓ (handler• E) f (Catch₁ ())
map⇓ (handler• E) f (Catch₂ x↯ y⇓) = Catch₂ x↯ (map⇓ E f y⇓)
map⇓ (handler• E) f Int            = Int
map⇓ (block• E)   f (Block x⇓)     = Block (map⇓ E f x⇓)
map⇓ (block• E)   f Int            = Int
map⇓ (unblock• E) f (Unblock x⇓)   = Unblock (map⇓ E f x⇓)
map⇓ (unblock• E) f Int            = Int

map⇑ : ∀ {t} {x₁ x₂ : Exprˢ t} {i j} (E : EvalCtxt t i j) →
       (∀ {v} → x₁ ˢ⁻¹ ⇓[ i ] v → x₂ ˢ⁻¹ ⇓[ i ] v) →
       (x₁ ˢ⁻¹ ⇑[ i ] → x₂ ˢ⁻¹ ⇑[ i ]) →
       E [ x₁ ] ˢ⁻¹ ⇑[ j ] → E [ x₂ ] ˢ⁻¹ ⇑[ j ]
map⇑ •            f g ⇑                   = g ⇑
map⇑ (E •⊕ y)     f g (Add₁ x⇑)           = Add₁ (map⇑ E f g x⇑)
map⇑ (E •⊕ y)     f g (Add₂ (_ , x↡) y⇑)  = Add₂ (_ , map⇓ E f x↡) y⇑
map⇑ (E •>> y)    f g (Seqn₁ x⇑)          = Seqn₁ (map⇑ E f g x⇑)
map⇑ (E •>> y)    f g (Seqn₂ (_ , x↡) y⇑) = Seqn₂ (_ , map⇓ E f x↡) y⇑
map⇑ (E •catch y) f g (Catch₁ x⇑)         = Catch₁ (map⇑ E f g x⇑)
map⇑ (E •catch y) f g (Catch₂ x↯ y⇑)      = Catch₂ (map⇓ E f x↯) y⇑
map⇑ (nat m ⊕• E) f g (Add₁ ())
map⇑ (nat m ⊕• E) f g (Add₂ x↡ y⇑)        = Add₂ x↡ (map⇑ E f g y⇑)
map⇑ (handler• E) f g (Catch₁ ())
map⇑ (handler• E) f g (Catch₂ x↯ y⇑)      = Catch₂ x↯ (map⇑ E f g y⇑)
map⇑ (block• E)   f g (Block x⇑)          = Block (map⇑ E f g x⇑)
map⇑ (unblock• E) f g (Unblock x⇑)        = Unblock (map⇑ E f g x⇑)

-- Then note that the reduction relation is compatible with the
-- big-step relations in the following sense:

small⇒big⟶ʳ⇓ : ∀ {t i} {e₁ e₂ : Exprˢ t} {v} →
               e₁ ⟶ʳ[ i ] e₂ → e₂ ˢ⁻¹ ⇓[ i ] v → e₁ ˢ⁻¹ ⇓[ i ] v
small⇒big⟶ʳ⇓ Val       ⇓             = ⇓
small⇒big⟶ʳ⇓ Loop      (Seqn₁ x↡ y⇓) = y⇓
small⇒big⟶ʳ⇓ Loop      (Seqn₂ x↯)    = Loop (Seqn₂ x↯)
small⇒big⟶ʳ⇓ Loop      Int           = Int
small⇒big⟶ʳ⇓ Add₁      Val           = Add₁ Val Val
small⇒big⟶ʳ⇓ Add₁      Int           = Int
small⇒big⟶ʳ⇓ Add₂      Val           = Add₂ Val
small⇒big⟶ʳ⇓ Add₂      Int           = Int
small⇒big⟶ʳ⇓ Add₃      Val           = Add₃ Val Val
small⇒big⟶ʳ⇓ Add₃      Int           = Int
small⇒big⟶ʳ⇓ Seqn₁     ⇓             = Seqn₁ Val ⇓
small⇒big⟶ʳ⇓ Seqn₂     Val           = Seqn₂ Val
small⇒big⟶ʳ⇓ Seqn₂     Int           = Int
small⇒big⟶ʳ⇓ Catch₁    Val           = Catch₁ Val
small⇒big⟶ʳ⇓ Catch₁    Int           = Int
small⇒big⟶ʳ⇓ Catch₂    Val           = Catch₂ Val Val
small⇒big⟶ʳ⇓ Catch₂    Int           = Int
small⇒big⟶ʳ⇓ Block     Val           = Block Val
small⇒big⟶ʳ⇓ Block     Int           = Int
small⇒big⟶ʳ⇓ Unblock   Val           = Unblock Val
small⇒big⟶ʳ⇓ Unblock   Int           = Int
small⇒big⟶ʳ⇓ (Int int) Val           = Int
small⇒big⟶ʳ⇓ (Int int) Int           = Int

small⇒big⟶ʳ⇑ : ∀ {t} {e₁ e₂ : Exprˢ t} {i} →
               e₁ ⟶ʳ[ i ] e₂ → e₂ ˢ⁻¹ ⇑[ i ] → e₁ ˢ⁻¹ ⇑[ i ]
small⇒big⟶ʳ⇑ Val        ()
small⇒big⟶ʳ⇑ Loop       ⇑  = Loop ⇑
small⇒big⟶ʳ⇑ Add₁       ()
small⇒big⟶ʳ⇑ Add₂       ()
small⇒big⟶ʳ⇑ Add₃       ()
small⇒big⟶ʳ⇑ Seqn₁      ⇑  = Seqn₂ (_ , Val) ⇑
small⇒big⟶ʳ⇑ Seqn₂      ()
small⇒big⟶ʳ⇑ Catch₁     ()
small⇒big⟶ʳ⇑ Catch₂     ()
small⇒big⟶ʳ⇑ Block      ()
small⇒big⟶ʳ⇑ Unblock    ()
small⇒big⟶ʳ⇑ (Int int)  ()

-- It is then easy to prove the desired result in the terminating
-- case.

small⇒big⟶⋆ : ∀ {t} {e : Exprˢ t} {i v} →
              e ⟶⋆[ i ] done v → e ˢ⁻¹ ⇓[ i ] v
small⇒big⟶⋆ ε        = Val
small⇒big⟶⋆ (⟶ ◅ ⟶⋆) with ⟶⇒⟶E ⟶
small⇒big⟶⋆ (⟶ ◅ ⟶⋆) | Red E ⟶ʳ =
  map⇓ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶⋆ ⟶⋆)

-- The non-terminating case is not quite as easy, though. Note that
-- the following proof is not productive. The right-hand side inspects
-- the result of the recursive call before emitting the first
-- constructor, so if this proof were a Haskell function its semantics
-- would be ⊥.

-- small⇒big⟶∞ : ∀ {t} {e : Exprˢ t} {i} →
--               e ⟶∞[ i ] → e ˢ⁻¹ ⇑[ i ]
-- small⇒big⟶∞ (⟶ ◅∞ ⟶∞) with ⟶⇒⟶E ⟶
-- small⇒big⟶∞ (⟶ ◅∞ ⟶∞) | Red E ⟶ʳ =
--   map⇑ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶ʳ⇑ ⟶ʳ) (small⇒big⟶∞ ⟶∞)

-- In "Coinductive big-step operational semantics" Leroy and Grall use
-- excluded middle to prove this result. Here I follow them, but I use
-- double-negation instead of postulating anything (as suggested by
-- Thorsten Altenkirch).

open import Semantics.Equivalence.Lemmas

small⇒big⟶∞ : ∀ {t} (e : Exprˢ t) i →
              e ⟶∞[ i ] → ¬ ¬ e ˢ⁻¹ ⇑[ i ]
small⇒big⟶∞ (done v)     i ⟶∞                    = const (done↛∞ ⟶∞)
small⇒big⟶∞ (run ⌜ v ⌝)  i (Red Val       ◅∞ ⟶∞) = const (done↛∞ ⟶∞)
small⇒big⟶∞ (run ⌜ v ⌝) .U (Red (Int int) ◅∞ ⟶∞) = const (done↛∞ ⟶∞)

small⇒big⟶∞ (run (loop x)) i ⟶∞ = helper =<< excluded-middle
  where
  helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Loop.Pred i z) → _
  helper (yes (._ , x⟶⋆n , Loop.• n)) = return (loop-⇑ (n , small⇒big⟶⋆ x⟶⋆n))
  helper (no x↛⋆n)                    = Loop <$> (Seqn₁ <$> small⇒big⟶∞ x i x⟶∞)
    where x⟶∞ = ⋆∞⇒∞ (Loop.lemma ⟶∞) x↛⋆n

small⇒big⟶∞ (run (x ⊕ y)) i ⟶∞ = helper =<< excluded-middle
  where
  helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Add.Pred y i z) → _
  helper (yes (._ , x⟶⋆n , Add.• n y⟶∞)) = Add₂ (n , small⇒big⟶⋆ x⟶⋆n)
                                                <$> small⇒big⟶∞ y i y⟶∞
  helper (no x↛⋆n)                       = Add₁ <$> small⇒big⟶∞ x i x⟶∞
    where x⟶∞ = ⋆∞⇒∞ (Add.lemma ⟶∞) x↛⋆n

small⇒big⟶∞ (run (x >> y)) i ⟶∞ = helper =<< excluded-middle
  where
  helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Seqn.Pred y i z) → _
  helper (yes (._ , x⟶⋆n , Seqn.• n y⟶∞)) = Seqn₂ (n , small⇒big⟶⋆ x⟶⋆n)
                                                  <$> small⇒big⟶∞ y i y⟶∞
  helper (no x↛⋆n)                        = Seqn₁ <$> small⇒big⟶∞ x i x⟶∞
    where x⟶∞ = ⋆∞⇒∞ (Seqn.lemma ⟶∞) x↛⋆n

small⇒big⟶∞ (run (x catch y)) i ⟶∞ = helper =<< excluded-middle
  where
  helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Catch.Pred y i z) → _
  helper (yes (._ , x⟶⋆↯ , Catch.• y⟶∞)) = Catch₂ (small⇒big⟶⋆ x⟶⋆↯)
                                                  <$> small⇒big⟶∞ y B y⟶∞
  helper (no x↛⋆↯)                       = Catch₁ <$> small⇒big⟶∞ x i x⟶∞
    where x⟶∞ = ⋆∞⇒∞ (Catch.lemma ⟶∞) x↛⋆↯

small⇒big⟶∞ (run (block x))   i ⟶∞ = Block   <$> small⇒big⟶∞ x B (Block.lemma   ⟶∞)
small⇒big⟶∞ (run (unblock x)) i ⟶∞ = Unblock <$> small⇒big⟶∞ x U (Unblock.lemma ⟶∞)

small⇒big : Small⇒Big
small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ }