Make raw version of nameless term substitution

Author: nigosto

lambda-parser.cabal

@@ -30,11 +30,15 @@ executable lambda-parser
     other-modules:
         Examples.Terms
         Parser
-        Substitution
+        Transformer
+        Substitution.Named
+        Substitution.Nameless
         Generator
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions:
-    build-depends:    base ^>=4.17.2.0
+    build-depends:    
+        base ^>=4.17.2.0,
+        containers ^>= 0.7
     hs-source-dirs:   src
     default-language: Haskell2010

src/Generator.hs

@@ -1,11 +1,17 @@
 module Generator where
-import Parser (Token(Variable, Application, Abstraction))
+import Parser (Term (Variable, Application, Abstraction))
+import Transformer (NamelessTerm (NamelessVariable, NamelessApplication, NamelessAbstraction))
 
-generateTerm :: Token -> String
+generateTerm :: Term -> String
 generateTerm (Variable var) = [var]
-
 generateTerm (Application lhs rhs) = concatMap (\term -> case term of
   var@(Variable _) -> generateTerm var
   _ -> '(':generateTerm term ++ [')']) [lhs, rhs]
+generateTerm (Abstraction argument body) = 'λ':argument:'.':generateTerm body
 
-generateTerm (Abstraction argument body) = 'λ':argument:'.':generateTerm body
+generateNamelessTerm :: NamelessTerm -> String
+generateNamelessTerm (NamelessVariable var) = show var
+generateNamelessTerm (NamelessApplication lhs rhs) = concatMap (\term -> case term of
+  var@(NamelessVariable _) -> generateNamelessTerm var
+  _ -> '(':generateNamelessTerm term ++ [')']) [lhs, rhs]
+generateNamelessTerm (NamelessAbstraction depth body) = 'λ':generateNamelessTerm body

src/Main.hs

@@ -1,9 +1,13 @@
 module Main where
 
+import Prelude hiding (lookup)
 import System.IO (hSetBuffering, stdout, BufferMode (BlockBuffering))
-import Parser (parseTerm, Token (Variable))
-import Substitution (substitute)
-import Generator (generateTerm)
+import Parser (parseTerm, Term (Variable))
+import Substitution.Named (substitute)
+import Generator (generateTerm, generateNamelessTerm)
+import Transformer (toNameless)
+import Data.Map (empty, lookup)
+import Substitution.Nameless (substituteNameless)
 
 main :: IO ()
 main = do
@@ -13,6 +17,15 @@ main = do
   if length var /= 1 
   then error "please provide valid variable"
   else do
-    let substituteVariable = head var
-    substituteTerm <- putStr "Input substitution term: " >> getLine
-    putStrLn $ generateTerm $ substitute (parseTerm term) substituteVariable (parseTerm substituteTerm)
+    let (namelessTerm, context) = toNameless (parseTerm term) 0 [] empty
+        substituteVariable = head var `lookup` context 
+    case substituteVariable of
+      Nothing -> error "please provide valid variable"
+      Just index -> do 
+        substituteTerm <- putStr "Input substitution term: " >> getLine
+        let (substituteNamelessTerm, _) = toNameless (parseTerm substituteTerm) 0 [] context
+        putStrLn $ generateNamelessTerm $ substituteNameless namelessTerm index substituteNamelessTerm
+
+    -- let substituteVariable = head var
+    -- substituteTerm <- putStr "Input substitution term: " >> getLine
+    -- putStrLn $ generateTerm $ substitute (parseTerm term) substituteVariable (parseTerm substituteTerm)

src/Parser.hs

@@ -1,10 +1,10 @@
-module Parser (parseTerm, Token(Variable, Application, Abstraction)) where
+module Parser (parseTerm, Term(Variable, Application, Abstraction)) where
 import Data.Char (isAlpha)
 
-data Token =
+data Term =
   Variable Char |
-  Application Token Token |
-  Abstraction Char Token
+  Application Term Term |
+  Abstraction Char Term
   deriving (Show)
 
 takeWhileClosingBracket :: String -> Int-> String
@@ -22,7 +22,7 @@ dropWhileClosingBracket (x:xs) count = dropWhileClosingBracket xs count
 invalidTermError :: String
 invalidTermError = "invalid term"
 
-parseTerm :: String -> Token
+parseTerm :: String -> Term
 parseTerm [var]
   | isAlpha var = Variable var
   | otherwise = error invalidTermError

src/Substitution.hs renamed to src/Substitution/Named.hs

@@ -1,22 +1,22 @@
-module Substitution where
+module Substitution.Named where
 
-import Parser (Token (Application, Variable, Abstraction))
+import Parser (Term (Application, Variable, Abstraction))
 import Data.Char (chr, ord)
 
-freeVariables :: Token -> [Char]
+freeVariables :: Term -> [Char]
 freeVariables (Variable x) = [x]
 freeVariables (Application lhs rhs) = freeVariables lhs ++ freeVariables rhs
 freeVariables (Abstraction argument body) = filter (/= argument) $ freeVariables body
 
-chooseUniqueVariable :: Token -> Token -> Char
+chooseUniqueVariable :: Term -> Term -> Char
 chooseUniqueVariable first second = let vars = freeVariables first ++ freeVariables second
   in chooseVariable vars 'a'
     where chooseVariable :: [Char] -> Char -> Char
           chooseVariable vars current
             | current `notElem` vars = current
             | otherwise = chooseVariable vars $ chr $ ord current + 1
 
-substitute :: Token -> Char -> Token -> Token
+substitute :: Term -> Char -> Term -> Term
 substitute initial@(Variable var) x token
   | var == x = token
   | otherwise = initial

src/Substitution/Nameless.hs

@@ -0,0 +1,21 @@
+module Substitution.Nameless where
+import Transformer (NamelessTerm (NamelessVariable, NamelessApplication, NamelessAbstraction), NamingContext)
+
+shift :: Int -> Int -> NamelessTerm -> NamelessTerm
+shift c d var@(NamelessVariable k)
+    | 0 <= k && k < c = var
+    | otherwise = NamelessVariable (k + d)
+shift c d (NamelessApplication lhs rhs) = NamelessApplication (shift c d lhs) (shift c d rhs)
+shift c d (NamelessAbstraction depth body) = NamelessAbstraction depth (shift (c + 1) d body)
+
+singleShift :: NamelessTerm -> NamelessTerm
+singleShift = shift 0 1
+
+substituteNameless :: NamelessTerm -> Int -> NamelessTerm -> NamelessTerm
+substituteNameless (NamelessVariable var) x term
+    | x == var = term
+    | otherwise = NamelessVariable var
+substituteNameless (NamelessApplication lhs rhs) x term =
+    NamelessApplication (substituteNameless lhs x term) (substituteNameless rhs x term)
+substituteNameless (NamelessAbstraction depth body) x term =
+    NamelessAbstraction depth (substituteNameless body (x + 1) (singleShift term))

src/Transformer.hs

@@ -0,0 +1,42 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use first" #-}
+module Transformer where
+
+import Prelude hiding (lookup)
+import Parser (Term (Variable, Application, Abstraction))
+import Data.Map (Map, member, lookup, insert, size)
+import Data.List (elemIndex, union)
+
+data NamelessTerm
+  = NamelessVariable Int
+  | NamelessApplication NamelessTerm NamelessTerm
+  | NamelessAbstraction Int NamelessTerm
+  deriving (Show)
+
+type NamingContext = Map Char Int
+type BoundVariable = [Char]
+
+toNameless :: Term -> Int -> BoundVariable -> NamingContext -> (NamelessTerm, NamingContext)
+toNameless (Variable var) depth bv context = case var `elemIndex` bv of
+    Nothing -> case lookup var context of
+        Nothing -> let index = size context
+                   in (NamelessVariable (index + depth), insert var index context)
+        Just index -> (NamelessVariable (index + depth), context)
+    Just index -> (NamelessVariable index, context)
+
+toNameless (Application lhs rhs) depth bv context =
+    let namelessLhs = toNameless lhs depth bv context
+        namelessRhs = toNameless rhs depth bv (snd namelessLhs)
+    in (NamelessApplication (fst namelessLhs) (fst namelessRhs), snd namelessRhs)
+
+toNameless (Abstraction argument body) depth bv context = 
+    let namelessBody = toNameless body (depth + 1) (insertBoundVariable argument bv) context
+    in (NamelessAbstraction depth (fst namelessBody), snd namelessBody)
+    where insertBoundVariable var bv = if var `elem` bv then bv else var:bv
+
+-- a = Abstraction 'y' (Application (Variable 'x') (Application (Variable 'y') (Abstraction 'x' (Variable 'x'))))
+-- /x -> xy => Abstraction x (Application (Variable x) (Variable y))
+-- /01 => NamelessAbstraction 1 (NamelessApplication (Variable 0) (Variable 1))
+
+-- /y -> xy/x -> x => /10/0
+-- (NamelessAbstraction (NamelessApplication (NamelessVariable 1) (NamelessApplication (NamelessVariable 0) (NamelessAbstraction (NamelessVariable 1))))