files/practicum/Lambda.icl

   1 implementation module Lambda
   2
   3 import StdEnv
   4
   5 :: Term         = C Value                                                                                       // constante  v            (C v)
   6                         | X Index                                                                                       // variabele  x_i          (X i)
   7                         | (@.) infixl 7 Term  Term                                                      // applicatie (t1 t2)      (t1 @. t2)
   8                         |  \.           Index Term                                                      // abstractie (\x_i . t)   (\. i t)
   9 :: Value  :== Int                                                                                               // willekeurige integer waarde
  10 :: Index  :== Int                                                                                               // index (gebruikelijk i >= 0)
  11
  12 t0                      = (C 42)                                                                                        // 42
  13 t1                      = (X 0)                                                                                         // x_0
  14 t2                      = (\.0 (X 0))                                                                           // (\x_0 . x_0)
  15 t3                      = (\.0 (X 0)) @. (C 42)                                                         // (\x_0 . x_0) 42
  16 t4                      = (\.0 ((X 0) @. (X 0))) @. (\.1 ((X 1) @. (X 1)))      // (\x_0 . x_0 x_0) (\x_1 . x_1 x_1)
  17 t5                      = (\.0 (\.1 (X 0)))                                                                     // (\x_0 . (\x_1 . x_0))
  18 t6                      = (\.0 (\.1 (X 0))) @. (C 42) @. t4                                     // ((\x_0 . (\x_1 . x_0)) 42) ((\x_0 . x_0 x_0) (\x_1 . x_1 x_1))
  19
  20 terms                                                   = [t0, t1, t2, t3, t4, t5, t6]
  21
  22 instance toString Term where
  23         toString ...
  24
  25 Start = foldr (\s1 s2 -> s1 +++ "\n" +++ s2) "\n" (map toString terms)
  26
  27 nf :: Term -> Bool
  28 nf ...
  29
  30 //Start = map nf terms
  31
  32
  33 vars :: Term -> [Index]
  34 vars ...
  35
  36 //Start = map vars terms
  37
  38 fresh :: [Term] -> Index
  39 fresh ...
  40
  41 //Start = fresh terms
  42
  43
  44 (<:) infixl 6 :: Term (Index,Term) -> Term
  45 (<:) ...
  46
  47 //Start = (((X 2) @. t1) @. (\.0 t1)) <: (0,C 50)
  48
  49 beta_reduce :: Term Term -> Term
  50 beta_reduce ...
  51
  52 //Start = beta_reduce (\.0 ((X 0) @. (X 0))) (\.0 ((X 0) @. (X 0)))
  53
  54
  55 normal_order :: Term -> Term
  56 normal_order ...
  57
  58 applicative_order :: Term -> Term
  59 applicative_order ...
  60
  61 /*
  62 Start = (       toString t
  63                 , '\n', toString (normal_order      t)
  64                 , '\n', toString (applicative_order t)
  65                 )
  66 where
  67         t = (\.0 (\.1 (X 0))) @. ((\.0 (X 0)) @. (C 42)) @. (C 50)
  68 */
  69
  70 herschrijf :: (Term -> Term) Term -> Term
  71 herschrijf ...
  72
  73 //Start = herschrijf normal_order t3