fv (Var x) = Set.singleton x
fv (App m n) = fv m `Set.union` fv n
fv (Abs x b) = fv b `Set.difference` Set.singleton x
alpha :: String -> String -> E -> E
alpha n v (Var x) | x == v = Var n
alpha n v t@(Var x) = t
alpha n v (App a b) = App (alpha n v a) (alpha n v b)
alpha n v t@(Abs x b) | v == x = t
alpha n v (Abs x b) = Abs x (alpha n v b)
subst :: E -> String -> E -> E
subst n v (Var x) | v == x = n
subst n v t@(Var x) = t
subst n v (App a b) = App (subst n v a) (subst n v b)
subst n v t@(Abs x b) | v == x = t
subst n v (Abs y b) | Set.notMember y (fv n) = Abs y (subst n v b)
subst n v (Abs y b) =
let
y' = newVar (nextVarName y) (fv b)
newVar yy frees | Set.member yy frees = newVar (nextVarName yy) frees
newVar yy _ = yy
in
subst n v (Abs y' (alpha y' y b))
-- if s ends with a number, increment that number by one; if not, add 0 at the end
nextVarName :: String -> String
nextVarName s =
let (prefix, num) = foldr (\a (b, c) ->
if (null b && isDigit a)
then (b, a:c)
else (a:b, c)) ("", "") s
in
prefix ++ show (if (null num) then 0 else (read num + 1))
hasRedex (App (Abs _ _) _) = True
hasRedex (App f a) = hasRedex f || hasRedex a
hasRedex (Abs x b) = hasRedex b
hasRedex _ = False
step :: E -> Maybe E
step (App (Abs x b) a) = return $ subst a x b -- beta
step (App f a) | hasRedex f =
step f >>= \f' -> return $ App f' a
step (App f a) | hasRedex a =
step a >>= \a' -> return $ App f a'
step (Abs x b) | hasRedex b =
step b >>= \b' -> return $ Abs x b'
step _ = Nothing
eval :: E -> E
eval e = eval' e 10
where
eval' e 0 = error "Number of allowed steps exceeded"
eval' e n = case step e of
Nothing -> e
Just e' -> eval' e' (n - 1)
dupAbsName :: E -> Bool
dupAbsName = dupAbsNameAux Set.empty
where
dupAbsNameAux ns (App f a) = (dupAbsNameAux ns f) || (dupAbsNameAux ns a)
dupAbsNameAux ns (Var _) = False
dupAbsNameAux ns (Abs x b)
| Set.member x ns = True
| otherwise = let newNs = ns `Set.union` (Set.singleton x) in
dupAbsNameAux newNs b
getFlag :: E -> IO ()
getFlag e | dupAbsName e = error "No duplicate abstraction name allowed!"
| dupAbsName e' = putStrLn $ "Congratulations! "
| otherwise = putStrLn "Nope!"
where
e' = eval e
I don't know how to access Congratulations, how do I have to think about the answer ?
So the task is to find a lambda calculus expression that does not abstract twice over the same variable (not (dupAbsName e)) that evaluates (within 10 steps) to an expression that does abstract twice over the same variable (dupAbsName e').
Maybe a good way to start is to think about what lambda calculus expression is completely evaluated and that does abstract twice over the same variable. Then you can work backwards from there.
So you want to end up with two nested abstractions over the same variable. The smallest that I can think of is: (\x. (\x. a)). But we cannot start with that, so we should find some other expression that evaluates to that. A common trick that is also used to define let bindings is the following.
Translate
let x = y in z
to
(\x. z) y
(Where z may be a lambda calculus expression that contains x.)
This trick can also be used in the example above. We can write
let y = (\x. a) in (\x. y)
That way there are no nested abstractions over the same variable anymore. Can you use that translation rule to find the expression that we are looking for?
A let binding is a higher level language element. It is not a part of the standard lambda calculus. I showed a way of translating expressions that have let bindings into the lambda calculus. Then I gave an expression that contains a let binding and asked you to use the translation rule to translate that expression to the lambda calculus. The result of that should be an expression that satisfies the requirements of the getFlag function.