Lambda expr reduction

Lambda.hs

module Lambda where

import Control.Monad.Trans.Maybe
import Control.Applicative
import Control.Monad.State
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.List as List

newtype LambdaVar = LV Char
  deriving (Eq, Ord)

data LambdaExpr
  = Abstr LambdaVar LambdaExpr
  | App LambdaExpr LambdaExpr
  | Var LambdaVar
  deriving Eq

instance Show LambdaVar where
  show (LV x) = x:""

instance Show LambdaExpr where
  show (Var v) = show v
  show (App a b) = "(" ++ show a ++ " " ++ show b ++ ")"
  show (Abstr v b) = "(\\" ++ show v ++ "." ++ show b ++ ")"

freeVariables :: LambdaExpr -> Set LambdaVar
freeVariables = frees Set.empty
  where frees env (Var x)
          | x `Set.member` env = Set.empty
          | otherwise = Set.singleton x
        frees env (Abstr var expr) =
          frees (var `Set.insert` env) expr
        frees env (App a b) = frees env a `Set.union` frees env b

boundVariables :: LambdaExpr -> Set LambdaVar
boundVariables (Abstr var expr) = var `Set.insert` boundVariables expr
boundVariables (Var _) = Set.empty
boundVariables (App a b) = boundVariables a `Set.union` boundVariables b

isClosed :: LambdaExpr -> Bool
isClosed expr = Set.null $ freeVariables expr

boundIn :: LambdaVar -> LambdaExpr -> Bool
boundIn var expr = var `Set.member` boundVariables expr

freeIn :: LambdaVar -> LambdaExpr -> Bool
freeIn var expr = var `Set.member` freeVariables expr

canBeEtad :: LambdaExpr -> Bool
canBeEtad (Abstr v1 (App a (Var v2)))
  | not (v1 `freeIn` a) && v1 == v2 = True
canBeEtad _ = False

etaConvert :: LambdaExpr -> LambdaExpr
etaConvert abstr@(Abstr _ (App a (Var _)))
  | canBeEtad abstr = etaConvert a
etaConvert expr = expr

alphaConvert :: LambdaExpr -> Maybe LambdaExpr
alphaConvert (Abstr v expr) = Abstr <$> var <*> subst expr
  where subst (Var x)
          | x == v = Var <$> var
          | otherwise = pure $ Var x
        subst (Abstr v2 e)
          | v2 == v = pure $ Abstr v2 e
          | otherwise = Abstr v2 <$> subst e
        subst (App a b) = App <$> subst a <*> subst b
        fvs = freeVariables expr
        var = List.find (\x -> not $ x `Set.member` fvs) variables
        variables = map LV $ "xyzuv" ++ ['a'..'t']
alphaConvert expr = pure expr

betaReduce :: LambdaExpr -> Maybe LambdaExpr
betaReduce (App (Abstr var a) b) = subst a
  where subst (Var v)
          | v == var = pure b
          | otherwise = pure $ Var v
        subst (App a1 b1) = App <$> subst a1 <*> subst b1
        subst ab@(Abstr v e)
          | var `freeIn` e && v `Set.member` fvs = alphaConvert ab >>= subst
          | otherwise = Abstr v <$> subst e
        fvs = freeVariables b
betaReduce expr = pure expr

reduce :: Int -> LambdaExpr -> Maybe LambdaExpr
reduce limit expr
  | isClosed expr = evalState (runMaybeT $ red expr) limit
  | otherwise = Nothing
    where red :: LambdaExpr -> MaybeT (State Int) LambdaExpr
          red (Var x) = lift $ pure $ Var x
          red (App (Var v) b) = do
            rb <- red b
            App <$> pure (Var v) <*> pure rb
          red app@(App (Abstr _ _) _) = do
            l <- get
            guard (l > 0)
            rd <- liftMaybe $ betaReduce app
            put (l - 1)
            red rd
          red (App a b) = do
            ra <- red a
            app <- App <$> pure ra <*> pure b
            red app
          red ab@(Abstr a b)
            | canBeEtad ab = red $ etaConvert ab
            | otherwise = do
                rb <- red b
                Abstr <$> pure a <*> pure rb

normalize :: Int -> LambdaExpr -> Maybe LambdaExpr
normalize limit expr
  | isClosed expr = reduce limit expr
  | otherwise = Nothing

liftMaybe :: (MonadPlus m) => Maybe a -> m a
liftMaybe = maybe mzero return

Main.hs

module Main where

import System.IO (isEOF)
import Control.Monad (unless)
import Data.Maybe (fromMaybe, listToMaybe)
import System.Environment (getArgs)
import Parser
import Lambda

main :: IO ()
main = do
  args <- getArgs
  let limit = fromMaybe 100 $ case args of
                  x:_ -> maybeRead x :: Maybe Int
                  _ -> Nothing

  loop limit
    where
      loop limit = do
        eof <- isEOF
        unless eof $ do
          line <- getLine
          let expr = maybeEither $ parse line
          case expr >>= reduce limit of
            Just r -> putStrLn $ "OK: " ++ show r
            Nothing -> putStrLn $ "ERROR: " ++ line

          loop limit


maybeRead :: Read a => String -> Maybe a
maybeRead = fmap fst . listToMaybe . filter (null . snd) . reads

maybeEither :: Either a b -> Maybe b
maybeEither (Right a) = Just a
maybeEither (Left _) = Nothing

Parser.hs

module Parser
  (
    parse
  ) where

import Control.Applicative
import Text.ParserCombinators.Parsec hiding ((<|>), parse)
import qualified Text.ParserCombinators.Parsec as P

import Lambda

pExpr :: CharParser () LambdaExpr
pExpr = spaces *> text <* eof
  where text = pApp <|> pAbstr <|> pVar
        pVar = Var <$> LV <$> letter
        pAbstr = do
          char '\\'
          vars <- many1 letter
          char '.'
          rest <- text
          return $ foldr (\c s -> Abstr (LV c) s) rest vars
        pApp = chainl1 subExpr $ spaces *> pure App
        subExpr = parens pApp <|> pAbstr <|> pVar
        parens = between (char '(') (char ')')

parse :: String -> Either ParseError LambdaExpr
parse = P.parse pExpr ""