 Note used to lambda-calculs

#1

I’ve got this code :

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 ?

#2

Please format code like this:

```
code here
```

#3

Edited sorry for the miss

#4

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.

#5

Okay, I don’t really know the meaning of evaluated calculus but I’m going to search about that

#6

If this is a homework exercise then your course materials should contain something about beta-reduction.

#7

No it’s not it’s only for personal project

#8

The wikipedia article on lambda calculus has some useful external links: https://en.wikipedia.org/wiki/Lambda_calculus#External_links.

For example, the video by Computerphile with Graham Hutton: https://www.youtube.com/watch?v=eis11j_iGMs.

#9

Should I need to find something like (/x.a)(/x.b) ??

#10

Something like that, but not quite that.

#11

Can you explain to me a bit more please ? I really want to understand

#12

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?

#13

Here I understand the use of the substitution (right?), but i can’t figure out how to affect the x part with it Edit: should I do something like a let in a let ?

#14

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.

#15

I found : (\y.(\x.y))(\x.a)

#16

That is correct. Now translating it to your algebraic data type gives the following:

App (Abs "y" (Abs "x" (Var "y"))) (Abs "x" (Var "a"))

Giving that as input to the getFlag function should result in Congratulations! being printed.