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   , pattern RedEx
  18     -- * Reduction
  19   , alphaNorm
  20   , reduce
  21   , toNormalForm
  22   , Strategy(..)
  23   ) where
  24
  25 import Control.Monad.State
  26
  27 import Lambda.Term
  28
  29 import Debug.Trace
  30 import Lambda.Parser.Fancy ()
  31
  32 -- $setup
  33 -- >>> import Control.Applicative
  34 -- >>> import Lambda.Parser.Fancy
  35 -- >>> import Test.Term
  36 -- >>> import Test.QuickCheck
  37
  38 varnames :: [VarName]
  39 varnames = map (:[]) ['a'..'z'] ++ [c : s | s <- varnames, c <- ['a'..'z']]
  40
  41 alphaNorm :: Term -> Term
  42 alphaNorm = alpha varnames
  43   where
  44     alpha (v:vs) (Lambda x r) = Lambda v . alpha vs $ substitute x (Var v) r
  45     alpha vs (App u v) = App (alpha vs u) (alpha vs v)
  46     alpha _ (Var x) = Var x
  47     alpha [] _ = undefined
  48
  49 isFreeIn :: VarName -> Term -> Bool
  50 isFreeIn x (Var v) = x == v
  51 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  52 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
  53
  54 rename :: Term -> Term
  55 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
  56   where n = rnm x
  57         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  58 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
  59
  60 substitute :: VarName -> Term -> Term -> Term
  61 substitute a b (Var x) = if x == a then b else Var x
  62 substitute a b (Lambda x t)
  63   | x == a = Lambda x t
  64   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
  65   | otherwise = Lambda x (substitute a b t)
  66 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  67
  68 -- | Reduce λ-term
  69 --
  70 -- >>> reduce $ tRead "(\\x.x x) (g f)"
  71 -- g f (g f)
  72
  73 reduce :: Term -> Term
  74 reduce (Var x) = Var x
  75 reduce (Lambda x t) = Lambda x (reduce t)
  76 reduce (App t u) = app (reduce t) u
  77   where app (Lambda x v) w = reduce $ substitute x w v
  78         app a b = App a (reduce b)
  79
  80 data Strategy = Eager | Lazy
  81
  82 reduceStep :: Term -> Term
  83 reduceStep (RedEx x s t) = substitute x t s
  84 reduceStep t = t
  85
  86 data Z = R Term Z | L Z Term | ZL VarName Z | E
  87 data D = Up | Down
  88 type TermZipper = (Term, Z, D)
  89
  90 move :: TermZipper -> TermZipper
  91 move (App l r, c, Down) = (l, L c r, Down)
  92 move (Lambda x t, c, Down) = (t, ZL x c, Down)
  93 move (Var x, c, Down) = (Var x, c, Up)
  94 move (t, L c r, Up) = (r, R t c, Down)
  95 move (t, R l c, Up) = (App l t, c, Up)
  96 move (t, ZL x c, Up) = (Lambda x t, c, Up)
  97 move (t, E, Up) = (t, E, Up)
  98
  99 unmove :: TermZipper -> TermZipper
 100 unmove (t, L c r, Down) = (App t r, c, Down)
 101 unmove x = x
 102
 103 -- getTerm :: TermZipper -> Term
 104
 105 travPost :: (Monad m) => (Term -> m Term) -> Term -> m Term
 106 travPost fnc term = tr fnc (term, E, Down)
 107   where
 108     tr f (t@RedEx{}, c, Up) = do
 109       nt <- f t
 110       tr f (nt, c, Down)
 111     tr _ (t, E, Up) = return t
 112     tr f (t, c, Up) = tr f $ move (t, c, Up)
 113     tr f (t, c, Down) = tr f $ move (t, c, Down)
 114
 115 travPre :: (Monad m) => (Term -> m Term) -> Term -> m Term
 116 travPre fnc term = tr fnc (term, E, Down)
 117   where
 118     tr f (t@RedEx{}, c, Down) = do
 119       nt <- f t
 120       tr f $ unmove (nt, c, Down)
 121     tr _ (t, E, Up) = return t
 122     tr f (t, c, Up) = tr f $ move (t, c, Up)
 123     tr f (t, c, Down) = tr f $ move (t, c, Down)
 124
 125 -- |
 126 --
 127 -- >>> toNormalForm Eager 100 cI
 128 -- Just (λx.x)
 129 --
 130 -- >>> toNormalForm Eager 100 $ App cI cI
 131 -- Just (λx.x)
 132 --
 133 -- >>> toNormalForm Eager 100 $ (App (App cK cI) cY)
 134 -- Nothing
 135 --
 136 -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
 137 -- Just (λx.x)
 138 --
 139 -- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 100 x) (alphaNorm <$> toNormalForm Eager 100 x)
 140
 141 -- inf = tRead "(\\d.a ((\\d c.c d c) (\\x y z.x z (y z)) (\\f.(\\x.f (x x)) (\\x.f (x x))) e))"
 142
 143
 144 toNormalFormDebug :: Strategy -> Int -> Term -> Maybe Term
 145 toNormalFormDebug Eager n = flip evalStateT 0 . travPost (prnt >=> cnt >=> short n >=> return . reduceStep)
 146 toNormalFormDebug Lazy  n = flip evalStateT 0 . travPre  (prnt >=> cnt >=> short n >=> return . reduceStep)
 147
 148 toNormalForm :: Strategy -> Int -> Term -> Maybe Term
 149 toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep)
 150 toNormalForm Lazy  n = flip evalStateT 0 . travPre  (cnt >=> short n >=> return . reduceStep)
 151
 152 prnt :: (Monad m) => Term -> StateT Int m Term
 153 prnt t = traceShow t $ return t
 154
 155 cnt :: (Monad m) => Term -> StateT Int m Term
 156 cnt t@RedEx{} = do
 157   modify (+ 1)
 158   return t
 159 cnt t = return t
 160
 161 short :: Int -> Term -> StateT Int Maybe Term
 162 short maxN t = do
 163   n <- get
 164   if n > maxN
 165     then lift Nothing
 166     else return t