Step by Step reducer (incomplete)

src/Reducer.hs

@@ -1,4 +1,4 @@
-module Reducer (reduce, alphaEq) where
+module Reducer (reduce, alphaEq, betaReduce) where
 
 import Lib (Id, Term (Abs, App, Var))
 

src/StepByStepReducer.hs

@@ -0,0 +1,43 @@
+module StepByStepReducer (reduce, Strategy (..), MaxSteps) where
+
+import Lib (Term (Abs, App, Var))
+import Reducer (betaReduce)
+
+data Strategy = LeftmostOutermost | LeftmostInnermost
+  deriving (Show)
+
+type MaxSteps = Int
+
+reduce :: Term -> Strategy -> MaxSteps -> Term
+reduce term _ 0 = term
+reduce term strategy steps = reduce (strategyF term) strategy (steps - 1)
+  where
+    strategyF = case strategy of
+      LeftmostOutermost -> reduceOutermost1
+      LeftmostInnermost -> reduceInnermost1
+
+-- TOOD: I am not sure all of this is correct and/or complete :)
+
+-- Some things to read and think about:
+-- "If we restrict the normal order and applicative order strategies so as not to perform reductions inside the body of λ-abstractions, we obtain strategies known as call-by-name (CBN) and call-by-value (CBV), respectively."
+-- Source: https://www.cs.cornell.edu/courses/cs6110/2018sp/lectures/lec04.pdf
+-- CBN: Leftmost outermost strategy
+-- CBV: Leftmost innermost strategy
+
+-- Does leftmost outermost, one time
+-- Description: A function's arguments are substituted into the body of a function before they are reduced. A function's arguments are reduced as often as they are needed.
+-- Remark: In case a normal form exists, the leftmost outermost reduction strategy will find it.
+reduceOutermost1 :: Term -> Term
+reduceOutermost1 app@(App Abs {} _) = betaReduce app
+reduceOutermost1 (App lhs@App {} rhs) = App (reduceOutermost1 lhs) rhs
+reduceOutermost1 (App lhs rhs) = App lhs (reduceOutermost1 rhs)
+reduceOutermost1 val = val
+
+-- Does leftmost innermost, one time
+-- Description: A function's arguments are substituted into the body of a functionj after they are reduced. A function's arguments are reduced exactly once.
+-- Remark: In case a normal form exists, the leftmost innermost reduction strategy might not find it. It may never terminate.
+reduceInnermost1 :: Term -> Term
+reduceInnermost1 var@Var {} = var
+reduceInnermost1 (App abs@Abs {} app@App {}) = App abs $ reduceInnermost1 app
+reduceInnermost1 app@(App Abs {} _) = betaReduce app
+reduceInnermost1 val = val

test/Spec.hs

@@ -2,6 +2,7 @@ import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import qualified LibTest (spec)
 import qualified ParserTest (spec)
 import qualified ReducerTest (spec)
+import qualified StepByStepReducerTest (spec)
 import Test.Hspec (Spec, describe, hspec)
 import qualified TokenizerTest (spec)
 
@@ -16,3 +17,4 @@ spec = do
   describe "Parser Tests" ParserTest.spec
   describe "Reducer Tests" ReducerTest.spec
   describe "Lib Tests" LibTest.spec
+  describe "Step by Step Reducer Tests" StepByStepReducerTest.spec

test/StepByStepReducerTest.hs

@@ -0,0 +1,68 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module StepByStepReducerTest where
+
+import LCQQ (λ)
+import Lib (Term (..))
+import qualified Reducer (alphaEq)
+import StepByStepReducer (MaxSteps, Strategy (..), reduce)
+import Test.Hspec (Spec, describe, it, shouldBe)
+
+-- No test should reach that complexity anyways
+maxReductionAttempts = 20
+
+spec :: Spec
+spec = do
+  spec' LeftmostOutermost maxReductionAttempts
+  spec' LeftmostInnermost maxReductionAttempts
+  describe "Leftmost Outermost Single Step Verification" $ do
+    it "Steps are equal to reference example" $ do
+      let strategy = LeftmostOutermost
+      let initial = [λ| (λa.a) ((λa.a) x)((λb.b) y) |]
+      let firstReduction = [λ| ((λa.a) x)((λb.b) y) |]
+      reduce initial strategy 1 `shouldBe` firstReduction
+      let secondReduction = [λ| (x)((λb.b) y) |]
+      reduce firstReduction strategy 1 `shouldBe` secondReduction
+      let thirdReduction = [λ| (x)(y) |]
+      reduce secondReduction strategy 1 `shouldBe` thirdReduction
+  describe "Leftmost Innermost Single Step Verification" $ do
+    it "Steps are equal to reference example" $ do
+      let strategy = LeftmostInnermost
+      let initial = [λ| (λa.a) ((λa.a) x)((λb.b) y) |]
+      let firstReduction = [λ| (λa.a) (x)((λb.b) y) |]
+      reduce initial strategy 1 `shouldBe` firstReduction
+      let secondReduction = [λ| (λa.a) (x)(y) |]
+      reduce firstReduction strategy 1 `shouldBe` secondReduction
+      let thirdReduction = [λ| (x)(y) |]
+      reduce secondReduction strategy 1 `shouldBe` thirdReduction
+
+spec' :: Strategy -> MaxSteps -> Spec
+spec' strategy maxSteps = do
+  describe ("Step by Step reduction with strategy " ++ show strategy) $ do
+    it "Reduction with 0 steps is identity operation" $ do
+      reduce
+        [λ| (λx.x) whatever |]
+        strategy
+        0
+        `shouldBe` [λ| (λx.x) whatever |]
+    it "Identity lambda is reduced to value when value is applied within one step" $ do
+      reduce [λ| (λx.x) whatever |] strategy 1 `shouldBe` [λ| whatever |]
+    it "Identity lambda reduction still works with higher max steps allowed" $ do
+      reduce' [λ| (λx.x) whatever |] `shouldBe` [λ| whatever |]
+    it "Endless recursion stops correctly at max steps" $ do
+      reduce' [λ| (λx.x x) (λx.x x) |] `shouldBe` [λ| (λx.x x) (λx.x x) |]
+    it "Other endless recursion example terminates correctly" $ do
+      reduce' [λ| (λx.λy.y) |] `shouldBe` [λ| (λx.λy.y) |]
+  describe "General reduction tests" $ do
+    it "Identity lambda is reduced to value when value is applied" $ do
+      reduce' [λ| (λx.x) whatever |] `shouldBe` [λ| whatever |]
+    it "`(λx.x x) (λx.x)` reduces to `λx.x`" $ do
+      reduce' [λ| (λx.x x) (λx.x) |] `shouldBe` [λ| λx.x |]
+    it "sanity check with manual ast" $ do
+      reduce' (App (Abs "x" (App (Var "x") (Var "x"))) (Abs "x" (Var "x"))) == Abs "x" (Var "x")
+    it "`(λx.λy.x y) y` reduces to `λy1.y y1`, and not `λy.y y` (hint: may be brittle, equivalent to next test" $ do
+      reduce' [λ| (λx.λy.x y) y |] `shouldBe` [λ| λy1.y y1 |]
+    it "`(λx.λy.x y) y` reduces to a term that is alpha equivalent to `λz.y z`" $ do
+      Reducer.alphaEq (reduce' (App (Abs "x" (Abs "y" (App (Var "x") (Var "y")))) (Var "y"))) (Abs "z" (App (Var "y") (Var "z")))
+  where
+    reduce' lc = reduce lc strategy maxSteps