Prolog
====
1. Consider the following Prolog predicate definition
  
   remove_at(X,[X|Xs],1,Xs).
   remove_at(X,[Y|Xs],K,[Y|Ys]) :- K1 is K - 1, remove_at(X,Xs,K1,Ys).

It works for queries like 
   ?- remove_at(X,[a,b,c,d],2,R).
   X = b
   R = [a,c,d].

However, it throws an exception for queries like
   ?- remove_at(c,[a,b,c,d],V,R).
   ERROR: remove_at/4: Arguments are not sufficiently instantiated

How would you modify the predicate definition to make it work for the above 
query?

2. Write the prolog predicate flatten(L,R) that flattens a list of lists in 
L to a single list R. The equivalent OCaml function is given by
let rec flatten l = match l with
[] | [[]] -> []
|[]::t -> flatten t
|[h]::t -> h::flatten t
|((h1::t1)::t) -> h1::flatten(t1::t);;

Answers
====
1. remove_at(X,[X|Xs],1,Xs).
   remove_at(X,[Y|Xs],K,[Y|Ys]) :- remove_at(X,Xs,K1,Ys), K is K1 + 1. 

2. 
flatten([],[]):-!.
flatten([[]],[]):-!.
flatten([[]|T2],T):- flatten(T2,T),!.
flatten([[H]|T2],[H|T]):- flatten(T2,T),!.
flatten([[H1|T1]|T2],[H1|T]):- flatten([T1|T2],T).

Lambda Calculus
====
1. Find the lambda encoding obtained by evaluating the expression (alpha 3 1)
Given:
1 = \f.\y.f y
3 = \f.\y.f (f (f y)) 
alpha M N = \x.(M (N x))

For more examples, see 
http://www.cs.umd.edu/class/fall2011/cmsc330/tests/prac5-soln-fall09.pdf

Answers
====
1. alpha 3 1 
= \x.(3 (1 x))
= \x.(3 ((\f.\y.f y) x))                    //Substitute encoding for 1
= \x.(3 (\y.x y))                           //Beta reduction f->x
= \x.(\f.\y.f (f (f y)) (\y.x y))           //Substitute encoding for 3
= \x.(\y.(\y.x y) ((\y.x y) ((\y.x y) y)))  //Beta reduction f->(\y.x y)
= \x.(\y.(\y.x y) ((\y.x y) (x y)))         //Beta reduction y->y
= \x.(\y.(\y.x y) (x (x y)))                //Beta reduction y->(x y)
= \x.(\y.x (x (x y)))                       //Beta reduction y->(x (x y))
= \f.(\y.f (f (f y)))                       //Alpha conversion x->f
= 3

Here alpha is actually the encoding for the multiplication operator.