From ab16564ceef31f4818e35ea22450083b36da0e79 Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 12:25:51 +0200 Subject: [PATCH 1/7] Add step by step reducer with test basics --- test/Spec.hs | 2 ++ 1 file changed, 2 insertions(+) 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 From fbbba55a14ec9d1832d3d5fd60d3f1fab1d0ca1f Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 12:45:29 +0200 Subject: [PATCH 2/7] Implement basic leftmost outermost logic with max steps --- src/Reducer.hs | 2 +- src/StepByStepReducer.hs | 36 +++++++++++++++++++++++++++++++++++ test/StepByStepReducerTest.hs | 17 +++++++++++++++++ 3 files changed, 54 insertions(+), 1 deletion(-) create mode 100644 src/StepByStepReducer.hs create mode 100644 test/StepByStepReducerTest.hs 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..5bb2599 --- /dev/null +++ b/src/StepByStepReducer.hs @@ -0,0 +1,36 @@ +-- for comment evaluation during development +{-# HLINT ignore "Unused LANGUAGE pragma" #-} +{-# LANGUAGE QuasiQuotes #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} + +module StepByStepReducer (reduce, ReduceInstruction (..), Strategy (..), Steps) where + +import GHC.Base (undefined) +import LCQQ (lambda, λ) +import Lib (Id, Term (Abs, App, Var)) +import Reducer (betaReduce) + +data Strategy = LeftmostOutermost | LeftmostInnermost + deriving (Show) + +type Steps = Int + +data ReduceInstruction = ReduceInstruction Strategy Steps + deriving (Show) + +reduce :: Term -> ReduceInstruction -> Term +reduce term (ReduceInstruction _ 0) = term +reduce _ (ReduceInstruction LeftmostInnermost _) = undefined "not done" +reduce term (ReduceInstruction LeftmostOutermost steps) = reduce (reduce1 term) (ReduceInstruction LeftmostOutermost (steps - 1)) + +-- Does leftmost outermost +-- Remark: In case a normal form exists, the leftmost outermost reduction strategy will find it. +reduce1 :: Term -> Term +reduce1 var@Var {} = var +reduce1 (Abs id term) = Abs id (reduce1 term) +reduce1 app@(App (Abs {}) _) = betaReduce app +reduce1 (App lhs rhs) = App (reduce1 lhs) rhs + +-- >>> True +-- True diff --git a/test/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs new file mode 100644 index 0000000..2439d9b --- /dev/null +++ b/test/StepByStepReducerTest.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE QuasiQuotes #-} + +module StepByStepReducerTest where + +import LCQQ (λ) +import StepByStepReducer (ReduceInstruction (..), Strategy (..), reduce) +import Test.Hspec (Spec, describe, it, shouldBe) + +spec :: Spec +spec = do + describe "Step by Step reduction" $ do + it "Reduction with 0 steps is identity operation with LeftmostInnermost" $ do + reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostInnermost 0) `shouldBe` [λ| (λx.x) whatever |] + it "Reduction with 0 steps is identity operation with LeftmostOutermost" $ do + reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 0) `shouldBe` [λ| (λx.x) whatever |] + it "Identity lambda is reduced to value when value is applied within one step" $ do + reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 1) `shouldBe` [λ| whatever |] From 40a32ee1bb683601d690339791526bbc3fc2e8c9 Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 12:49:15 +0200 Subject: [PATCH 3/7] Add test proving value of max step setting --- test/StepByStepReducerTest.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs index 2439d9b..3f20d5a 100644 --- a/test/StepByStepReducerTest.hs +++ b/test/StepByStepReducerTest.hs @@ -15,3 +15,5 @@ spec = do reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 0) `shouldBe` [λ| (λx.x) whatever |] it "Identity lambda is reduced to value when value is applied within one step" $ do reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 1) `shouldBe` [λ| whatever |] + it "Endless recursion stops correctly at max steps" $ do + reduce [λ| (λx.x x) (λx.x x) |] (ReduceInstruction LeftmostOutermost 50) `shouldBe` [λ| (λx.x x) (λx.x x) |] From a83318873b818c1bae1f40d4d597723c09db646e Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 12:55:27 +0200 Subject: [PATCH 4/7] Test general reduction cases --- src/StepByStepReducer.hs | 13 +------------ test/StepByStepReducerTest.hs | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/StepByStepReducer.hs b/src/StepByStepReducer.hs index 5bb2599..9b59912 100644 --- a/src/StepByStepReducer.hs +++ b/src/StepByStepReducer.hs @@ -1,14 +1,6 @@ --- for comment evaluation during development -{-# HLINT ignore "Unused LANGUAGE pragma" #-} -{-# LANGUAGE QuasiQuotes #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} - module StepByStepReducer (reduce, ReduceInstruction (..), Strategy (..), Steps) where -import GHC.Base (undefined) -import LCQQ (lambda, λ) -import Lib (Id, Term (Abs, App, Var)) +import Lib (Term (Abs, App, Var)) import Reducer (betaReduce) data Strategy = LeftmostOutermost | LeftmostInnermost @@ -31,6 +23,3 @@ reduce1 var@Var {} = var reduce1 (Abs id term) = Abs id (reduce1 term) reduce1 app@(App (Abs {}) _) = betaReduce app reduce1 (App lhs rhs) = App (reduce1 lhs) rhs - --- >>> True --- True diff --git a/test/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs index 3f20d5a..40ba605 100644 --- a/test/StepByStepReducerTest.hs +++ b/test/StepByStepReducerTest.hs @@ -3,6 +3,8 @@ module StepByStepReducerTest where import LCQQ (λ) +import Lib (Term (..)) +import qualified Reducer (alphaEq) import StepByStepReducer (ReduceInstruction (..), Strategy (..), reduce) import Test.Hspec (Spec, describe, it, shouldBe) @@ -17,3 +19,21 @@ spec = do reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 1) `shouldBe` [λ| whatever |] it "Endless recursion stops correctly at max steps" $ do reduce [λ| (λx.x x) (λx.x x) |] (ReduceInstruction LeftmostOutermost 50) `shouldBe` [λ| (λx.x x) (λx.x x) |] + 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"))) + +-- No test should reach that complexity anyways +maxReductionAttempts = 20 + +-- makes general tests easier for now - once leftmost innermost is implemented, this has to be changed +reduce' :: Term -> Term +reduce' term = reduce term (ReduceInstruction LeftmostOutermost maxReductionAttempts) \ No newline at end of file From 8168bbe9653bd3d213e079c54a64633530dcaa43 Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 12:58:31 +0200 Subject: [PATCH 5/7] Simplify by removing instruction type --- src/StepByStepReducer.hs | 13 +++++-------- test/StepByStepReducerTest.hs | 12 ++++++------ 2 files changed, 11 insertions(+), 14 deletions(-) diff --git a/src/StepByStepReducer.hs b/src/StepByStepReducer.hs index 9b59912..febc3cf 100644 --- a/src/StepByStepReducer.hs +++ b/src/StepByStepReducer.hs @@ -1,4 +1,4 @@ -module StepByStepReducer (reduce, ReduceInstruction (..), Strategy (..), Steps) where +module StepByStepReducer (reduce, Strategy (..), Steps) where import Lib (Term (Abs, App, Var)) import Reducer (betaReduce) @@ -8,13 +8,10 @@ data Strategy = LeftmostOutermost | LeftmostInnermost type Steps = Int -data ReduceInstruction = ReduceInstruction Strategy Steps - deriving (Show) - -reduce :: Term -> ReduceInstruction -> Term -reduce term (ReduceInstruction _ 0) = term -reduce _ (ReduceInstruction LeftmostInnermost _) = undefined "not done" -reduce term (ReduceInstruction LeftmostOutermost steps) = reduce (reduce1 term) (ReduceInstruction LeftmostOutermost (steps - 1)) +reduce :: Term -> Strategy -> Steps -> Term +reduce term _ 0 = term +reduce _ LeftmostInnermost _ = undefined "not done" +reduce term LeftmostOutermost steps = reduce (reduce1 term) LeftmostOutermost (steps - 1) -- Does leftmost outermost -- Remark: In case a normal form exists, the leftmost outermost reduction strategy will find it. diff --git a/test/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs index 40ba605..6358f0c 100644 --- a/test/StepByStepReducerTest.hs +++ b/test/StepByStepReducerTest.hs @@ -5,20 +5,20 @@ module StepByStepReducerTest where import LCQQ (λ) import Lib (Term (..)) import qualified Reducer (alphaEq) -import StepByStepReducer (ReduceInstruction (..), Strategy (..), reduce) +import StepByStepReducer (Strategy (..), reduce) import Test.Hspec (Spec, describe, it, shouldBe) spec :: Spec spec = do describe "Step by Step reduction" $ do it "Reduction with 0 steps is identity operation with LeftmostInnermost" $ do - reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostInnermost 0) `shouldBe` [λ| (λx.x) whatever |] + reduce [λ| (λx.x) whatever |] LeftmostInnermost 0 `shouldBe` [λ| (λx.x) whatever |] it "Reduction with 0 steps is identity operation with LeftmostOutermost" $ do - reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 0) `shouldBe` [λ| (λx.x) whatever |] + reduce [λ| (λx.x) whatever |] LeftmostOutermost 0 `shouldBe` [λ| (λx.x) whatever |] it "Identity lambda is reduced to value when value is applied within one step" $ do - reduce [λ| (λx.x) whatever |] (ReduceInstruction LeftmostOutermost 1) `shouldBe` [λ| whatever |] + reduce [λ| (λx.x) whatever |] LeftmostOutermost 1 `shouldBe` [λ| whatever |] it "Endless recursion stops correctly at max steps" $ do - reduce [λ| (λx.x x) (λx.x x) |] (ReduceInstruction LeftmostOutermost 50) `shouldBe` [λ| (λx.x x) (λx.x x) |] + reduce [λ| (λx.x x) (λx.x x) |] LeftmostOutermost 50 `shouldBe` [λ| (λx.x x) (λx.x x) |] describe "General reduction tests" $ do it "Identity lambda is reduced to value when value is applied" $ do reduce' [λ| (λx.x) whatever |] `shouldBe` [λ| whatever |] @@ -36,4 +36,4 @@ maxReductionAttempts = 20 -- makes general tests easier for now - once leftmost innermost is implemented, this has to be changed reduce' :: Term -> Term -reduce' term = reduce term (ReduceInstruction LeftmostOutermost maxReductionAttempts) \ No newline at end of file +reduce' term = reduce term LeftmostOutermost maxReductionAttempts \ No newline at end of file From e2c7ed40cbc8c700359ca6c623845ddced11ca73 Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 13:43:21 +0200 Subject: [PATCH 6/7] Implement innermost reduction, test both strategys together and equally --- src/StepByStepReducer.hs | 43 ++++++++++++++++++++++++++--------- test/StepByStepReducerTest.hs | 35 ++++++++++++++++------------ 2 files changed, 52 insertions(+), 26 deletions(-) diff --git a/src/StepByStepReducer.hs b/src/StepByStepReducer.hs index febc3cf..b665f99 100644 --- a/src/StepByStepReducer.hs +++ b/src/StepByStepReducer.hs @@ -1,4 +1,4 @@ -module StepByStepReducer (reduce, Strategy (..), Steps) where +module StepByStepReducer (reduce, Strategy (..), MaxSteps) where import Lib (Term (Abs, App, Var)) import Reducer (betaReduce) @@ -6,17 +6,38 @@ import Reducer (betaReduce) data Strategy = LeftmostOutermost | LeftmostInnermost deriving (Show) -type Steps = Int +type MaxSteps = Int -reduce :: Term -> Strategy -> Steps -> Term +reduce :: Term -> Strategy -> MaxSteps -> Term reduce term _ 0 = term -reduce _ LeftmostInnermost _ = undefined "not done" -reduce term LeftmostOutermost steps = reduce (reduce1 term) LeftmostOutermost (steps - 1) +reduce term strategy steps = reduce (strategyF term) strategy (steps - 1) + where + strategyF = case strategy of + LeftmostOutermost -> reduceOutermost1 + LeftmostInnermost -> reduceInnermost1 --- Does leftmost outermost +-- 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. -reduce1 :: Term -> Term -reduce1 var@Var {} = var -reduce1 (Abs id term) = Abs id (reduce1 term) -reduce1 app@(App (Abs {}) _) = betaReduce app -reduce1 (App lhs rhs) = App (reduce1 lhs) rhs +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/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs index 6358f0c..74a913b 100644 --- a/test/StepByStepReducerTest.hs +++ b/test/StepByStepReducerTest.hs @@ -5,20 +5,30 @@ module StepByStepReducerTest where import LCQQ (λ) import Lib (Term (..)) import qualified Reducer (alphaEq) -import StepByStepReducer (Strategy (..), reduce) +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 - describe "Step by Step reduction" $ do - it "Reduction with 0 steps is identity operation with LeftmostInnermost" $ do - reduce [λ| (λx.x) whatever |] LeftmostInnermost 0 `shouldBe` [λ| (λx.x) whatever |] - it "Reduction with 0 steps is identity operation with LeftmostOutermost" $ do - reduce [λ| (λx.x) whatever |] LeftmostOutermost 0 `shouldBe` [λ| (λx.x) whatever |] + spec' LeftmostOutermost maxReductionAttempts + spec' LeftmostInnermost maxReductionAttempts + +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 |] LeftmostOutermost 1 `shouldBe` [λ| whatever |] + 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) |] LeftmostOutermost 50 `shouldBe` [λ| (λx.x x) (λx.x x) |] + 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 |] @@ -30,10 +40,5 @@ spec = 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"))) - --- No test should reach that complexity anyways -maxReductionAttempts = 20 - --- makes general tests easier for now - once leftmost innermost is implemented, this has to be changed -reduce' :: Term -> Term -reduce' term = reduce term LeftmostOutermost maxReductionAttempts \ No newline at end of file + where + reduce' lc = reduce lc strategy maxSteps From 3532b465463e13fb81479d2ecfecee171ba8af51 Mon Sep 17 00:00:00 2001 From: Mathias Fischler Date: Sat, 8 Apr 2023 14:00:59 +0200 Subject: [PATCH 7/7] Add failing test to prove incompleteness --- test/StepByStepReducerTest.hs | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/test/StepByStepReducerTest.hs b/test/StepByStepReducerTest.hs index 74a913b..3447e22 100644 --- a/test/StepByStepReducerTest.hs +++ b/test/StepByStepReducerTest.hs @@ -15,12 +15,36 @@ 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 |] + 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