reduce with combinators

pcp/lambda.hs

@@ -120,21 +120,25 @@ churchNum _ = Nothing
 
 isChurchNum t = churchNum t /= Nothing
 
-beta :: Term -> Term
-beta (App (Abs x t) u) = subst x u t
-beta x                 = x
-
 betastep :: Term -> Term
+betastep (Var x) = Var x
 betastep (Abs x t) = Abs x (betastep t)
-betastep (App (Abs x e1) e2) = beta (App (Abs x e1) e2)
+betastep (App (Abs x e1) e2) = subst x e2 e1
+betastep (App I e1) = e1
+betastep (App (App K e1) e2) = e1
+betastep (App (App (App S e1) e2) e3) = (App (App e1 e3) (App e2 e3))
 betastep (App e1 e2) =
         let left = betastep e1 in
         if left == e1 then App e1 (betastep e2)
         else App left e2
 betastep x         = x
 
-nf :: Term -> Term
-nf term = if (betastep term) == term then term else nf (betastep term)
+nf :: Term -> Int -> Term
+nf term i =
+  let new = betastep term in
+  if i > 0 then
+    if new == term then term else nf new (i-1)
+  else new
 
 
 -- data SKITerm = S | K | I | CA SKITerm SKITerm