0440949 Andreas van Cranenburgh
Functionele Talen, assignment 1

1
a) ((λx.λy.y (λz.(z z) λz.(z z))) λu.(λv.λw.v λz.z))
         \/    \_/_/    \_/_/          \___/   \_/

b) ((((λu.λv.λw.((u v) w) λx.λy.λz.(x (y z))) a) b) c)
        \__|__|___/ /  /   \  \  \__|__|_/    [^^either constants or unbound]
           \__|____/  /     \  \____|__/
              \______/       \______/
c) λy.(λz.λy.((z u) y) λv.(λw.((w v) u) y))
     \  \   \__|_?_/     \  \__/ /   ? /
      \  \_____/          \_____/     /
       \_____________________________/
2
a) 
(((λ x (λ y y)) ((λ z (z z)) (λ z (z z)))) (λ u ((λ v (λ w v)) (λ z z))))

0. ((λx.λy.y (λz.(z z) λz.(z z))) λu.(λv.λw.v λz.z))
              --------    /
                  \______/   (reduces to itself, so this step is optional
				and can be repeated wherever this term appears)
1a. ((λx.λy.y (λz.(z z) λz.(z z))) λu.(λv.λw.v λz.z))
     -------      /
       \_________/      

2a. (λy.y λu.(λv.λw.v λz.z))
    ----          /
      \__________/

3a. λu.(λv.λw1.v λz.z)
       -------  /
          \____/

4a. λu.(λw1.λz.z)


0. ((λx.λy.y (λz.(z z) λz.(z z))) λu.(λv.λw.v λz.z))
                                      -------  /
                                         \____/
1b. ((λx.λy.y (λz.(z z) λz.(z z))) λu.(λw.λz.z))
      -------         /
         \___________/
2b. (λy.y λu.(λw.λz.z))
     ----       /
       \_______/
3b. λu.(λw.λz.z) == 4a




b) 
(((((λ u (λ v (λ w ((u v) w)))) (λ x (λ y (λ z ((x (y z))))))) a) b) c)

0.  ((((λu.λv.λw.((u v) w) λx.λy.λz.(x (y z))) a) b) c)
        ------------------          /
                \__________________/
1a. (((λv.λw.((λx.λy.λz.(x (y z)) v) w) a) b) c)
       _______________________________ /
                     \________________/
2a. ((λw.((λx.λy.λz.(x (y z)) a) w) b) c)
      ---------------------------- /
                    \_____________/
3a. (((λx.λy.λz.(x (y z)) a) b) c)
       ----------------- /
                \_______/ 
4a. ((λy.λz.(a (y z)) b) c)
       ----------------- /
                  \_____/
4a. (λz.(a (b z)) c)
     ----------- /
         \______/
5a. (a (b c))


1a. (((λv.λw.((λx.λy.λz.(x (y z)) v) w) a) b) c)
               ------------------ / 
                          \______/
2b (((λv.λw.(λy.λz.(v (y z)) w) a) b) c)
      ------------------------- /
                     \_________/       
3b ((λw.(λy.λz.(a (y z)) w) b) c)
     ---------------------  /
               \___________/
4b ((λy.λz.(a (y z)) b) c) == 4a


2b (((λv.λw.(λy.λz.(v (y z)) w) a) b) c)
             --------------- /
                     \______/
3c (((λv.λw.λz.(v (w z)) a) b) c)
      ------------------ /
             \__________/
4c (((λw.λz.(a (w z)) b) c) == alpha-equivalent to 4a


2a. ((λw.((λx.λy.λz.(x (y z)) a) w) b) c)
           ----------------- /
                  \_________/
3d. ((λw.(λy.λz.(a (y z)) w) b) c) == 3b


c) 
(λ y ((λ z (λ y ((z u) y))) (λ v (λ w ((w v) u) y))))

0. λy.(λz.λy.((z u) y) λv.(λw.((w v) u) y))
       ---------------        /
            \________________/

1a. λy.λy.((λv.(λw.((w v) u1) y1) u) y)
            -------------------- /
                       \________/
2a. λy.λy.((λw.((w u) u1) y1) y)
            ------------- /
                     \___/

3a. λy.λy.(((y1 u) u1) y)



0. λy.(λz.λy.((z u) y) λv.(λw.((w v) u) y))
                           ----------- /
                                 \____/
1b. λy.(λz.λy.((z u) y) λv.((y v) u))
        ---------------       /
               \_____________/
2b. λy.λy.((λv.((y1 v) u1) u) y)
            ------------- /
                   \_____/
3b. λy.λy.(((y1 u) u1) y)