diff --git a/src/Reducer.hs b/src/Reducer.hs index ec4aeac..86505d3 100644 --- a/src/Reducer.hs +++ b/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)) diff --git a/src/StepByStepReducer.hs b/src/StepByStepReducer.hs new file mode 100644 index 0000000..b665f99 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/test/Spec.hs b/test/Spec.hs index c930d60..3bfbd7b 100644 --- a/test/Spec.hs +++ b/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 diff --git a/test/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs new file mode 100644 index 0000000..3447e22 --- /dev/null +++ b/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