Coursework 1 Functional Programming
Coursework 1 Due: End of week 4
Instructions Complete the given assignments in the file Coursework.hs . Make sure your file does not have syntax errors or type errors; where necessary, comment out partial solutions (and explain what you intended). Use the provided function names. You may use auxiliary functions, and you are encouraged to add your own examples and tests. Assessment and feedback Your work will be judged primarily on the correctness of your solutions. Secondarily, incorrect or partial solutions (also when commented out) may be given partial marks if they are well presented. Marking is part-automated, part-manual. You will receive individual marks, and we will publish an overall feedback document.
Lambda-calculus
Copyright By PowCoder代写 加微信 powcoder
In this coursework we will implement the lambda-calculus in Haskell. You are started off with the following, in the file Coursework.hs.
• Var: a type for variables, as a synonym of String.
• Term: a data type for lambda-terms. It has three constructors, Variable, Lambda,
and Apply, which match the three cases of the definition of lambda-terms: M ::= x|λx.M|MM
• example: an example lambda-term, λa.λx. (λy. a) x b .
• pretty: a function that renders a Term as a lambda-term (but with \ for λ ). Try it:
*Main> example
Lambda “a” (Lambda “x” (Apply (Apply (Lambda “y”
(Variable “a”)) (Variable “x”)) (Variable “b”)))
*Main> putStrLn (pretty example)
\a. \x. (\y. a) x b
We will first replace the standard show function for Terms with pretty. Comment out the line deriving Show and un-comment the two lines instance Show Term. . . .
*Main> example
\a. \x. (\y. a) x b
Assignment 1 (10%): Complete the function numeral which given a number i , returns the corresponding Church numeral Ni as a Term. Recall that the Church numerals are:
N0 = λf.λx.x N1 = λf.λx.f x N2 = λf.λx.f (f x) …
Coursework 1 Functional Programming
You may find the following recursive definition of the numeral Ni helpful. Ni = λf.λx.Ni′ N0′ =x
*Main> numeral 2
\f. \x. f (f x)
Next, we will build a function that generates a fresh variable. First, we create an infinite supply of variables; then we remove those already in use. We will store used variables as an alphabetically sorted list, with each variable mentioned at most once: we only care if variables occur, and not how often. To help with this you are given the merge function from the merge sort algorithm in the tutorials.
Assignment 2 (20%):
a) Complete the infinite list variables, which contains the variables “a” through “z”, then repeats these suffixed with 1, “a1″,…,”z1”, then 2, “a2″,…,”z2”, etc.
*Main> [variables !! i | i <- [0,1,25,26,27,100,3039]]
["a","b","z","a1","b1","w3","x116"]
b) Complete the function filterVariables which takes two lists of variables and re- turns the first with all variables from the second list removed from it.
*Main> filterVariables [“y”,”z”,”a1″,”a2″] [“y”,”a1″,”a3″]
[“z”,”a2″]
c) Complete the function fresh which given a list of variables, generates a fresh variable not occurring in the list. Use filterVariables to remove the given variables from variables, then take the first variable in the remaining list.
*Main> fresh [“a”,”b”,”x”]
d) Complete the function used that collects all the variable names used in a Term, both as a Variable and in a Lambda abstraction. Return them in an ordered list (use merge to combine two ordered lists into one).
*Main> used example
[“a”,”b”,”x”,”y”]
*Main> fresh it
Ni′ = f (Ni′−1) (if i ̸= 0)
Coursework 1 Functional Programming
Capture-avoiding substitution
In this part we will program capture-avoiding substitution. Recall the renaming operation M [y/x] ( M with x renamed to y ) from the lectures, slightly paraphrased:
(λz.M )[y/x] = (M N )[y/x] =
λz.(M [y/x])
if z = x otherwise
if z = x otherwise
(M [y/x]) (N [y/x])
The definition of capture-avoiding substitution, similarly paraphrased, is:
(M1M2)[N/x] = (M1[N/x])(M2[N/x])
Note that both definitions now give a direct template for the corresponding Haskell function.
Assignment 3 (30%):
a) Complete the function rename x y m that renames x to y in the term m, i.e. M [y/x] .
b) Complete the function substitute that implements capture-avoiding substitution, i.e. substitute x n m corresponds to M[N/x]. Use fresh to generate the fresh variable z as above; it must not be used in n and m, and not be x.
*Main> rename “b” “z” example
\a. \x. (\y. a) x z
*Main> substitute “b” (numeral 0) example
\c. \a. (\a. c) a (\f. \x. x)
(In the example, note the renaming of λy to λa , due to the substitution (λy. a)[N0/b] .)
(λy.M )[N/x] =
λz.(M [z/y][N/x])
if y = x otherwise
where z is fresh: not used in M or N, and z ̸= x
Coursework 1 Functional Programming
Beta-reduction
Now we have all we need to implement beta-reduction. A top-level beta-step is of the form
(λx.N)M →β N[M/x].
A beta-step can be applied anywhere in a term. This is defined by: if N1 →β N2 then
λx.N1 →β λx.N2 N1M →β N2M MN1 →β MN2 .
We will implement a beta-step with the function beta. Since a term may have many redexes,
or none at all (if it is in normal form), beta will return the list of all possible reductions. Assignment 4 (40%):
a) Complete the function beta, which returns the list of all beta-reducts of a term.
*Main> Apply example (numeral 1)
(\a. \x. (\y. a) x b) (\f. \x. f x)
*Main> beta it
[\c. (\b. \f. \x. f x) c b,(\a. \x. a b) (\f. \x. f x)]
*Main> it !! 1
(\a. \x. a b) (\f. \x. f x)
*Main> beta it
[\c. (\f. \x. f x) b]
*Main> beta (head it)
[\c. \a. b a]
*Main> beta (head it)
Hint: you will need four pattern-matching cases: one to see if the term is a redex, and if not, the three usual cases for Term to look further down in the term. In the first case, don’t forget to look for further redexes as well. Since beta returns a list, you will have to take care with your recursive calls.
b) Complete the functions normalize and normal which reduce a term to normal form (or continue indefinitely if there isn’t one). They should do the following:
• normalize should return a (possibly infinite) list with the input term at the head, such that each other term in the list is the result of applying a beta-step to the previous one; that is, if m follows n in the list, then m is a term taken from the list beta n;
• normal should return the normal form of a term, if it exists.
Coursework 1 Functional Programming
(Your functions need not have the same reduction strategy as the example below.)
*Main> normalize (Apply (numeral 2) (numeral 2))
[(\f. \x. f (f x)) (\f. \x. f (f x)),
\a. (\f. \x. f (f x)) ((\f. \x. f (f x)) a),
\a. \b. (\f. \x. f (f x)) a ((\f. \x. f (f x)) a b),
\a. \b. (\b. a (a b)) ((\f. \x. f (f x)) a b),
\a. \b. a (a ((\f. \x. f (f x)) a b)),
\a. \b. a (a ((\b. a (a b)) b)),
\a. \b. a (a (a (a b)))]
*Main> normal (Apply (numeral 2) (numeral 2))
\a. \b. a (a (a (a b)))
c) What reduction strategy does your normalize function implement? Demonstrate your understanding as follows.
i Make sure that beta, normalize, and normal implement normal-order reduc- tion (leftmost outermost); adjust them if necessary.
ii Copy all three functions to a_beta, a_normalize and a_normal and adjust these to implement applicative-order reduction (leftmost innermost). Don’t for- get to update all the recursive calls.
iii Give a lambda-term example1 :: Term which reduces to normal form in more steps with normal-order than with applicative-order reduction. Make sure both reductions do actually reach a normal form.
iv Give a lambda-term example2 :: Term which reduces to normal form in fewer steps with normal-order than with applicative-order reduction. Make sure both reductions do actually reach a normal form.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com