Reputation: 55
I'm working with the lambda calculus implemented in haskell. Expressions:
%x.e -- lambda abstraction, like \x->e in Haskell
e e' -- application
x,y,z -- variables
succ, pred, ifzero, 0, 1, 2....
Syntax:
type Id = String
-- The "builtin" functions.
data Op = Succ | Pred | IfZero
deriving (Show, Ord, Eq)
-- Expressions of L
data Exp = Var Id
| Nat Integer
| Op Op
| Lam Id Exp
| App Exp Exp
deriving (Ord, Eq, Show)
There's also a function that converts the usual representation into Exp
:
parse "%f. f 1 2" = Lam "f" App (App (Var "f") (Nat 1)) (Nat 2)`
And I have to write the function subst x e e'
that will substitute e
for all "free" occurrences of (Var x)
in e'
. "Free" means that the variable it is not declared by a surrounding %
. For example, in the expression
x (%x. x (%y.xz)) (%y.x)
there are 5 occurrences of x
. The first is "free". The second is the parameter for the %
expression and is never substituted for. The third and fourth occurrences refer to the parameter of the enclosing %
expression. The fifth is free. Therefore if we substitute 0
for x
we get 0 (%x. x (%y.xz)) (%y.0)
.
All I need to use is pattern-matching and recursion. All I was able to write is the function prototype as
subst :: Id -> Exp -> Exp -> Exp
subst x (App z z') (App e e') =
If somebody could give me a hint how to implement the function it would be great. Any help is highly appreciated
Upvotes: 3
Views: 4318
Reputation: 2024
I'd like to first point out that the pattern matching (subst x (App z z') (App e e')
) is non-exhaustive. (Most of) the other patterns are trivial, so it's easy to forget them. I'd suggest against pattern matching the third argument, because if all you're doing is subsituting it into the second argument, you don't care if it's an App
lication or Nat
ural.
The first step in most recursive functions is to consider cases. What's the base case? In this situation, it's where the second argument is equal to Var x
:
-- Replace x with y in a Var. If the Var is equal to x, replace
-- otherwise, leave alone.
subst x (Var a) y
| a == x = y
| otherwise = (Var a)
Then we need to consider the step cases, what if it's an application, and what if it's a lambda abstraction?
-- Replace x with y in an application. We just need to replace
-- x with y in z and in z', because an application doesn't
-- bind x (x stays free in z and z').
subst x (App z z') y = (App new_z new_z')
where new_z = -- Recursively call subst here.
new_z' = -- And recursively call subst here, too.
-- Replace x with y in a lambda abstraction. We *do* need to
-- check to make sure that the lambda doesn't bind x. If the
-- lambda does bind x, then there's no possibility of x being
-- free in e, and we can leave the whole lambda as-is.
subst x (Lam z e) y
| z == x = (Lam z e)
| otherwise = (Lam z new_e)
where new_e = -- Recursively call subst here.
Finally, all the trivial cases are the same (we leave alone both Nat and Op, since there's no chance we would be substituting them):
subst :: Id -> Exp -> Exp -> Exp
subst _ nat_or_op _ = nat_or_op
Upvotes: 2