src/Lambda.hs

   1 {-# LANGUAGE PatternSynonyms #-}
   2
   3 -- |
   4 -- Module      :  Lambda
   5 -- Copyright   :  Tomáš Musil 2014
   6 -- License     :  BSD-3
   7 --
   8 -- Maintainer  :  tomik.musil@gmail.com
   9 -- Stability   :  experimental
  10 --
  11 -- This is a toy λ-calculus implementation.
  12
  13 module Lambda
  14   ( -- * Types
  15     VarName
  16   , Term(..)
  17     -- * Reduction
  18   , alphaNorm
  19   , reduce
  20   , toNormalForm
  21   , Strategy(..)
  22   ) where
  23
  24 import Control.Monad.State
  25
  26 import Lambda.Term
  27
  28 -- $setup
  29 -- >>> import Control.Applicative
  30 -- >>> import Lambda.Parser.Fancy
  31 -- >>> import Test.Term
  32 -- >>> import Test.QuickCheck
  33
  34 varnames :: [VarName]
  35 varnames = map (:[]) ['a'..'z'] ++ [c : s | s <- varnames, c <- ['a'..'z']]
  36
  37 alphaNorm :: Term -> Term
  38 alphaNorm = alpha varnames
  39   where
  40     alpha (v:vs) (Lambda x r) = Lambda v . alpha vs $ substitute x (Var v) r
  41     alpha vs (App u v) = App (alpha vs u) (alpha vs v)
  42     alpha _ (Var x) = Var x
  43     alpha [] _ = undefined
  44
  45 isFreeIn :: VarName -> Term -> Bool
  46 isFreeIn x (Var v) = x == v
  47 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  48 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
  49
  50 rename :: Term -> Term
  51 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
  52   where n = rnm x
  53         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  54 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
  55
  56 substitute :: VarName -> Term -> Term -> Term
  57 substitute a b (Var x) = if x == a then b else Var x
  58 substitute a b (Lambda x t)
  59   | x == a = Lambda x t
  60   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
  61   | otherwise = Lambda x (substitute a b t)
  62 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  63
  64 -- | Reduce λ-term
  65 --
  66 -- >>> reduce $ tRead "(\\x.x x) (g f)"
  67 -- g f (g f)
  68
  69 reduce :: Term -> Term
  70 reduce (Var x) = Var x
  71 reduce (Lambda x t) = Lambda x (reduce t)
  72 reduce (App t u) = app (reduce t) u
  73   where app (Lambda x v) w = reduce $ substitute x w v
  74         app a b = App a (reduce b)
  75
  76 data Strategy = Eager | Lazy
  77
  78 reduceStep :: (Monad m) => Term -> m Term
  79 reduceStep (RedEx x s t) = return $ substitute x t s
  80 reduceStep t = return t
  81
  82 data Z = R Term Z | L Z Term | ZL VarName Z | E
  83 data D = Up | Down
  84 type TermZipper = (Term, Z, D)
  85
  86 move :: TermZipper -> TermZipper
  87 move (App l r, c, Down) = (l, L c r, Down)
  88 move (Lambda x t, c, Down) = (t, ZL x c, Down)
  89 move (Var x, c, Down) = (Var x, c, Up)
  90 move (t, L c r, Up) = (r, R t c, Down)
  91 move (t, R l c, Up) = (App l t, c, Up)
  92 move (t, ZL x c, Up) = (Lambda x t, c, Up)
  93 move (t, E, Up) = (t, E, Up)
  94
  95 unmove :: TermZipper -> TermZipper
  96 unmove (t, L c r, Down) = (App t r, c, Down)
  97 unmove x = x
  98
  99 travPost :: (Monad m) => (Term -> m Term) -> Term -> m Term
 100 travPost fnc term = tr fnc (term, E, Down)
 101   where
 102     tr f (t@RedEx{}, c, Up) = do
 103       nt <- f t
 104       tr f (nt, c, Down)
 105     tr _ (t, E, Up) = return t
 106     tr f (t, c, Up) = tr f $ move (t, c, Up)
 107     tr f (t, c, Down) = tr f $ move (t, c, Down)
 108
 109 travPre :: (Monad m) => (Term -> m Term) -> Term -> m Term
 110 travPre fnc term = tr fnc (term, E, Down)
 111   where
 112     tr f (t@RedEx{}, c, Down) = do
 113       nt <- f t
 114       tr f $ unmove (nt, c, Down)
 115     tr _ (t, E, Up) = return t
 116     tr f (t, c, Up) = tr f $ move (t, c, Up)
 117     tr f (t, c, Down) = tr f $ move (t, c, Down)
 118
 119 -- |
 120 --
 121 -- >>> toNormalForm Eager 100 cI
 122 -- Just (λx.x)
 123 --
 124 -- >>> toNormalForm Eager 100 $ App cI cI
 125 -- Just (λx.x)
 126 --
 127 -- >>> toNormalForm Eager 100 $ (App (App cK cI) cY)
 128 -- Nothing
 129 --
 130 -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
 131 -- Just (λx.x)
 132 --
 133 -- prop> (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 1000 x) (alphaNorm <$> toNormalForm Eager 1000 x)
 134
 135
 136 toNormalForm :: Strategy -> Int -> Term -> Maybe Term
 137 toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> reduceStep)
 138 toNormalForm Lazy  n = flip evalStateT 0 . travPre  (cnt >=> short n >=> reduceStep)
 139
 140 cnt :: (Monad m) => Term -> StateT Int m Term
 141 cnt t@RedEx{} = do
 142   modify (+ 1)
 143   return t
 144 cnt t = return t
 145
 146 short :: Int -> Term -> StateT Int Maybe Term
 147 short maxN t = do
 148   n <- get
 149   if n > maxN
 150     then lift Nothing
 151     else return t