The following is some Haskell code in which it is shown by way of an example how substitution in the presence of variable binding operators can be defined using only structural recursion. I haven't got a description of what is going on categorically. However, the right-hand side of the definition of L' below is essentially a endofunctor on a certain category of set-valued functions, and L' is its initial algebra. The domain of these functions can be any family of sets closed under Maybe' - for example the von-Neumann natural numbers. The question of picking the right morphisms to make the members of this family into the objects of a category (and L into the initial object for a functor on the presheaves over that category) is a bit too abstruse for me at the moment. I leave it as an exercise for the categorically obsessed. The simple constructions here are strikingly close to the notions formalised in Pierre Lescanne's $\lambda\upsilon$ calculus of explicit substitutions. See: ||. > module Lambda_calculus (L(Var,App,Abs), > i_term,b_term,c_term,w_term,k_term,s_term,y_term,fix_term) where A data-type for lambda-expressions, de-Bruijn style. The parameter is a type of names for variables. > data L x = Var x > | App (L x) (L x) > | Abs (L (Maybe x)) > deriving (Show,Read) -- just for testing Like any other sum-of-products positive data-type, L is a functor in the sense of acting on arrows. To define this, we need polymorphic recursion, as supported in Haskell. Basically, the functor renames free variables. > instance Functor L where map = mL > mL :: (x -> y) -> L x -> L y -- need an explicit type assertion > mL f z = case z of > Var x -> Var (f x) > App e1 e2 -> App (mL f e1) (mL f e2) > Abs e -> Abs (mL f' e) > where -- note how bound variables are protected > f' = map f -- Maybe is itself a functor Like any other leafy data-type, L is a monad. The bind operator is simultaneous substitution. (Leafy data type': |f x = mu (\ y -> x + g y )|. See Bird and de Moor, Algebra of Programming, exercise 2.40.) > instance Monad L where > return a = Var a > e >>= f = case e of > Var x -> f x > App e1 e2 -> App (e1 >>= f) (e2 >>= f) > Abs e -> Abs (e >>= f') > where -- note how capture of frees is avoided > f' w = case w of Nothing -> Var Nothing > Just x -> map Just (f x) Conventional one-point substitution. As we have a monad, we can exploit Haskell's "do" notation. > subst1 :: L (Maybe x) -> L x -> L x > subst1 c e = do z <- c > case z of Nothing -> e > Just x -> Var x - An application We define a partial function which reduces lambda-calculus expressions to WHNF. (In 4 lines of code!) A helper. > app z = case z of Abs e -> evL . subst1 e > _ -> App z Compute WHNF > evL z = case z of App e1 e2 -> app (evL e1) e2 > _ -> z Unfortunately, de Bruijn machinery seems too costly for use in a practical reduction machine. - Some expressions for experimenting with > v0 = Var Nothing > v1 = Var (Just Nothing) > v2 = Var (Just (Just Nothing)) > b_term = Abs (Abs (Abs (App v2 (App v1 v0)))) > c_term = Abs (Abs (Abs (App (App v2 v0) v1))) > w_term = Abs (Abs (App (App v1 v0) v0)) > k_term = Abs (Abs v1) > i_term = Abs v0 > s_term = Abs (Abs (Abs (App (App v2 v0) (App v1 v0)))) > y_term = Abs (App x x) where x = Abs (App v1 (App v0 v0)) > sap = Abs (App v0 v0) > dont_evaluate_me = App sap sap > fix_term = Abs (let x = App v0 x in x) > fix_term, w_term, i_term, k_term, s_term, c_term :: L String