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