Last active
January 7, 2024 00:31
-
-
Save nerodono/eacc9543a35218cc82845a1c043b23f3 to your computer and use it in GitHub Desktop.
Lambda calculus reduction in Haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module LambdellCalculus where | |
import qualified Data.Bifunctor as Bi | |
data Term = ApplyT Term Term | |
| VarT Char | |
| FunT Char Term | |
deriving(Show, Eq) | |
isValidVar :: Char -> Bool | |
isValidVar = (flip elem) $ ['a'..'z'] ++ ['A'..'Z'] | |
foldApplication :: Term -> String -> (Term, String) | |
foldApplication init (v:t) | isValidVar v = | |
foldApplication (ApplyT init $ VarT v) t | |
foldApplication init ('\\':v:t) = parseLambda v t | |
foldApplication init ('(':t) = applyBracketFold (ApplyT init) t | |
foldApplication init rest = (init, rest) | |
applyBracketFold :: (Term -> Term) -> String -> (Term, String) | |
applyBracketFold f t = | |
foldApplication (f inside) outside | |
where (inside, ')':outside) = parseTerm t | |
parseLambda :: Char -> String -> (Term, String) | |
parseLambda v | isValidVar v = Bi.first (FunT v) . parseTerm | |
| otherwise = error $ v: " cannot be made into a bound variable" | |
parseTerm :: String -> (Term, String) | |
parseTerm ('\\':v:t) = parseLambda v t | |
parseTerm ('(':t) = applyBracketFold id t | |
parseTerm (h:t) | isValidVar h = foldApplication (VarT h) t | |
-- Reduction | |
reduce :: String -> Term | |
reduce s = reduceTerm term | |
where (term, "") = parseTerm s | |
reduceTerm :: Term -> Term | |
reduceTerm (VarT c) = VarT c | |
reduceTerm (FunT c t) = FunT c $ reduceTerm t | |
reduceTerm (ApplyT (FunT bv bterm) rhs) = | |
let reducedBody = reduceTerm bterm | |
reducedRhs = reduceTerm rhs | |
in | |
subst bv reducedRhs bterm | |
where subst :: Char -> Term -> Term -> Term | |
subst bv value (VarT v) | bv == v = value | |
subst bv value (VarT v) = VarT v | |
subst bv value (FunT bv' bterm') | |
| bv == bv' = FunT bv' bterm' -- shadowing, left term will be unused | |
| otherwise = FunT bv' $ reduceTerm $ subst bv value bterm' | |
subst bv value (ApplyT lhs rhs) = | |
let substLhs = reduceTerm $ subst bv value lhs | |
substRhs = reduceTerm $ subst bv value rhs | |
in case substLhs of | |
FunT bv' bterm' -> subst bv' substRhs bterm' | |
_ -> ApplyT substLhs substRhs | |
reduceTerm (ApplyT (VarT v) rhs) = ApplyT (VarT v) (reduceTerm rhs) | |
reduceTerm (ApplyT lhs rhs) = reduceTerm $ ApplyT (reduceTerm lhs) (reduceTerm rhs) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment