add (custom) de bruijn-y conversion and alpha equivalence check

lamb.cabal

@@ -13,7 +13,8 @@ executable lamb
     import:           warnings
     main-is:          Main.hs
     other-modules:    Parser,
-                      Evaluation
+                      Evaluation,
+                      Bruijn
     build-depends:    base, containers, parsec
     hs-source-dirs:   src
     default-language: Haskell2010
@@ -25,7 +26,8 @@ test-suite lamb-tests
     other-modules:      Parser,
                         ParserSpec,
                         Evaluation,
-                        EvaluationSpec
+                        EvaluationSpec,
+                        BruijnSpec
     build-depends:      base, containers, hspec, parsec
     build-tool-depends: hspec-discover:hspec-discover
     default-language:   Haskell2010

src/Bruijn.hs

@@ -0,0 +1,15 @@
+module Bruijn where
+
+import Data.Map (Map, empty, insert, lookup, size)
+import Parser (Expr (Abstraction, Application, Variable))
+
+-- | Convert to (unorthodox) De Bruijn form
+toDeBruijn :: Expr -> Expr
+toDeBruijn e = innerDB e empty
+
+innerDB :: Expr -> Map String Int -> Expr
+innerDB v@(Variable name) d = case Data.Map.lookup name d of
+  Just n -> Variable (show n)
+  Nothing -> v
+innerDB (Abstraction binder body) d = Abstraction (show $ size d) (innerDB body (insert binder (size d) d))
+innerDB (Application f arg) d = Application (innerDB f d) (innerDB arg d)

src/Evaluation.hs

@@ -1,5 +1,6 @@
 module Evaluation where
 
+import Bruijn (toDeBruijn)
 import Data.Set
 import Parser (Expr (Abstraction, Application, Variable), vName)
 
@@ -52,3 +53,6 @@ run :: Expr -> Expr
 run ex = case beta ex of
   Just ex' -> run ex'
   Nothing -> ex
+
+alphaEquiv :: Expr -> Expr -> Bool
+alphaEquiv e1 e2 = (toDeBruijn e1) == (toDeBruijn e2)

test/BruijnSpec.hs

@@ -0,0 +1,48 @@
+module BruijnSpec (spec) where
+
+import Bruijn (toDeBruijn)
+import Parser (Expr (Abstraction, Application, Variable))
+import Test.Hspec
+
+spec :: Spec
+spec = do
+  describe "toDeBruijn" $ do
+
+    -- Free variables
+    it "leaves a lone free variable unchanged" $
+      toDeBruijn (Variable "x") `shouldBe` Variable "x"
+    it "leaves free variables in abstraction body unchanged" $
+      toDeBruijn (Abstraction "x" (Variable "y"))
+        `shouldBe` Abstraction "0" (Variable "y")
+
+    -- Single abstraction
+    it "converts bound variable in identity" $
+      toDeBruijn (Abstraction "x" (Variable "x"))
+        `shouldBe` Abstraction "0" (Variable "0")
+    it "leaves free variable in abstraction body unchanged" $
+      toDeBruijn (Abstraction "x" (Variable "z"))
+        `shouldBe` Abstraction "0" (Variable "z")
+
+    -- Nested abstractions
+    it "inner binder resolves to depth 1" $
+      toDeBruijn (Abstraction "x" (Abstraction "y" (Variable "y")))
+        `shouldBe` Abstraction "0" (Abstraction "1" (Variable "1"))
+    it "outer binder resolves to depth 0 from within nested scope" $
+      toDeBruijn (Abstraction "x" (Abstraction "y" (Variable "x")))
+        `shouldBe` Abstraction "0" (Abstraction "1" (Variable "0"))
+    it "outermost of three binders resolves correctly" $
+      toDeBruijn (Abstraction "x" (Abstraction "y" (Abstraction "z" (Variable "x"))))
+        `shouldBe` Abstraction "0" (Abstraction "1" (Abstraction "2" (Variable "0")))
+
+    -- Application
+    it "converts self-application" $
+      toDeBruijn (Abstraction "x" (Application (Variable "x") (Variable "x")))
+        `shouldBe` Abstraction "0" (Application (Variable "0") (Variable "0"))
+    it "converts independent scopes in application" $
+      toDeBruijn (Application (Abstraction "x" (Variable "x")) (Abstraction "y" (Variable "y")))
+        `shouldBe` Application (Abstraction "0" (Variable "0")) (Abstraction "0" (Variable "0"))
+
+    -- Alpha equivalence
+    it "alpha-equivalent terms produce identical output" $
+      toDeBruijn (Abstraction "x" (Variable "x"))
+        `shouldBe` toDeBruijn (Abstraction "y" (Variable "y"))

test/EvaluationSpec.hs

@@ -1,7 +1,7 @@
 module EvaluationSpec (spec) where
 
 import Data.Set (Set, empty, fromList)
-import Evaluation (beta, bind, freeIn, freeVars, freshName, subst)
+import Evaluation (alphaEquiv, beta, bind, freeIn, freeVars, freshName, subst)
 import Parser (Expr (Abstraction, Application, Variable), parse)
 import Test.Hspec
 
@@ -106,6 +106,98 @@ spec = do
     it "bind with abstraction argument substitutes correctly" $
       -- (λx. x) applied to (λi. i)  →  (λi. i)
       bind absI absI `shouldBe` Just absI
+  describe "alphaEquiv" $ do
+
+    -- Reflexivity
+    it "a variable is alpha-equivalent to itself" $
+      alphaEquiv (Variable "x") (Variable "x") `shouldBe` True
+    it "an abstraction is alpha-equivalent to itself" $
+      alphaEquiv (Abstraction "x" (Variable "x")) (Abstraction "x" (Variable "x")) `shouldBe` True
+    it "a nested term is alpha-equivalent to itself" $
+      alphaEquiv (Abstraction "x" (Abstraction "y" (Application (Variable "x") (Variable "y"))))
+                 (Abstraction "x" (Abstraction "y" (Application (Variable "x") (Variable "y"))))
+        `shouldBe` True
+
+    -- Renaming bound variables (True)
+    it "identity with different binder names: λx. x ≡ λy. y" $
+      alphaEquiv (Abstraction "x" (Variable "x"))
+                 (Abstraction "y" (Variable "y"))
+        `shouldBe` True
+    it "constant body with different binder names: λx. z ≡ λy. z" $
+      alphaEquiv (Abstraction "x" (Variable "z"))
+                 (Abstraction "y" (Variable "z"))
+        `shouldBe` True
+    it "nested: λx. λy. x ≡ λa. λb. a (outer reference)" $
+      alphaEquiv (Abstraction "x" (Abstraction "y" (Variable "x")))
+                 (Abstraction "a" (Abstraction "b" (Variable "a")))
+        `shouldBe` True
+    it "nested: λx. λy. y ≡ λa. λb. b (inner reference)" $
+      alphaEquiv (Abstraction "x" (Abstraction "y" (Variable "y")))
+                 (Abstraction "a" (Abstraction "b" (Variable "b")))
+        `shouldBe` True
+    it "nested application body: λx. λy. x y ≡ λa. λb. a b" $
+      alphaEquiv (Abstraction "x" (Abstraction "y" (Application (Variable "x") (Variable "y"))))
+                 (Abstraction "a" (Abstraction "b" (Application (Variable "a") (Variable "b"))))
+        `shouldBe` True
+    it "self-application body: λx. x x ≡ λy. y y" $
+      alphaEquiv (Abstraction "x" (Application (Variable "x") (Variable "x")))
+                 (Abstraction "y" (Application (Variable "y") (Variable "y")))
+        `shouldBe` True
+
+    -- Symmetry
+    it "alpha equivalence is symmetric" $
+      alphaEquiv (Abstraction "x" (Variable "x"))
+                 (Abstraction "y" (Variable "y"))
+        `shouldBe`
+      alphaEquiv (Abstraction "y" (Variable "y"))
+                 (Abstraction "x" (Variable "x"))
+
+    -- Free variables are name-sensitive (False)
+    it "distinct free variables are not equivalent" $
+      alphaEquiv (Variable "x") (Variable "y") `shouldBe` False
+    it "different free variables in abstraction body: λx. y ≢ λx. z" $
+      alphaEquiv (Abstraction "x" (Variable "y"))
+                 (Abstraction "x" (Variable "z"))
+        `shouldBe` False
+    it "bound body vs free body: λx. x ≢ λx. y" $
+      alphaEquiv (Abstraction "x" (Variable "x"))
+                 (Abstraction "x" (Variable "y"))
+        `shouldBe` False
+
+    -- Structurally different terms (False)
+    it "abstraction vs bare variable are not equivalent" $
+      alphaEquiv (Variable "x")
+                 (Abstraction "x" (Variable "x"))
+        `shouldBe` False
+    it "different depths: λx. x ≢ λx. λy. y" $
+      alphaEquiv (Abstraction "x" (Variable "x"))
+                 (Abstraction "x" (Abstraction "y" (Variable "y")))
+        `shouldBe` False
+    it "argument order matters in application: x y ≢ y x" $
+      alphaEquiv (Application (Variable "x") (Variable "y"))
+                 (Application (Variable "y") (Variable "x"))
+        `shouldBe` False
+
+    -- Shadowing / name reuse
+    it "consistent inner shadowing: λx. λx. x ≡ λy. λy. y" $
+      alphaEquiv (Abstraction "x" (Abstraction "x" (Variable "x")))
+                 (Abstraction "y" (Abstraction "y" (Variable "y")))
+        `shouldBe` True
+    it "inner shadow differs from outer reference: λx. λx. x ≢ λx. λy. x" $
+      alphaEquiv (Abstraction "x" (Abstraction "x" (Variable "x")))
+                 (Abstraction "x" (Abstraction "y" (Variable "x")))
+        `shouldBe` False
+
+    -- Free variables unchanged across binder rename
+    it "free variable in body is preserved: λx. y ≡ λz. y" $
+      alphaEquiv (Abstraction "x" (Variable "y"))
+                 (Abstraction "z" (Variable "y"))
+        `shouldBe` True
+    it "free vs bound distinction preserved: λy. y ≢ λy. z" $
+      alphaEquiv (Abstraction "y" (Variable "y"))
+                 (Abstraction "y" (Variable "z"))
+        `shouldBe` False
+
   describe "beta reduction" $ do
     -- Normal forms (no redex)
     it "returns Nothing for a bare variable" $