SCP-3247 (#4335)

equivalence between structural reduction and contextual reduction + progress and determinism of structural reduction.
IntersectMBO · Jan 18, 2022 · cc72a56 · cc72a56
1 parent 5836bf4
commit cc72a56
Show file tree

Hide file tree

Showing 4 changed files with 186 additions and 416 deletions.
diff --git a/plutus-metatheory/src/Algorithmic/Evaluation.lagda b/plutus-metatheory/src/Algorithmic/Evaluation.lagda
@@ -11,7 +11,7 @@ open import Utils
 open import Type
 open import Type.BetaNormal
 open import Algorithmic
-open import Algorithmic.Reduction
+open import Algorithmic.ReductionEC
 \end{code}
 
 ## Evaluation
@@ -42,7 +42,7 @@ data Finished {A : ∅ ⊢Nf⋆ *} :  (N : ∅ ⊢ A) →  Set where
 --   neutral : {L : ∅ ⊢ A} → Neutral L → Finished L
 \end{code}
 Given a term `L` of type `A`, the evaluator will, for some `N`, return
-a reduction sequence from `L` to `N` and an indication of whether
+Ma reduction sequence from `L` to `N` and an indication of whether
 reduction finished.
 \begin{code}
 data Steps : ∀ {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → Set where