Homework Assignment 2 Due Wednesday, Feb 7th at 11:59PM (Pacific Time)
In this assignment, you will augment the simple arithmetic language in the last assignment with lambda calculus. The resulting language is called . This language is so powerful that it can simulate the execution of any Turing machine, and thus any computer program in any programming language: C++, Python, Java, or your favorite programming language.
This homework will consist of four parts.
The first part gives you some practice with higher-order functions in OCaml.
The second part is a review of the core concepts of lambda calculus with plenty of pen-and-paper exercises to reinforce your understanding.
The third part asks you to implement an interpreter for in OCaml.
The fourth part (bonus) walks you through a recipe that can be used to encode all kinds of fancy data structures into lambda calculus.
Instructions
1. Eitherclonethisdirectory,ordownloadthezippeddirectoryusingthislink.
2. Run opam install . –deps-only in the root directory of this homework to install the necessary
dependencies. You need to run this command again, since this assignment contains new
dependencies that were not used in HW1.
3. Completelib/part1/part1.ml,lib/lamp/eval.ml,and(forbonus)lib/part4/*.lpbyreplacing
the placeholders denoted by todo or bonus with your own code. You must not change the type signatures of the original functions. Otherwise, your program will not compile. If you accidentally change the type signatures, you can refer to the corresponding .mli file to see what the expected type signatures are.
4. Onceyou’redone,submitlib/part1/part1.ml,lib/lamp/eval.ml,and(forbonus) lib/part4/*.lp to Gradescope. If your program contains print statements, please remove them
before submitting. You do not need to submit any other file, including any .mli file or test code. The autograder will automatically compile your code together with our testing infrastructure and run the tests.
Important notes:
Problems marked with are pencil-and-paper problems, and are ungraded. You do not need to submit your solution. The goal is to review concepts that will help you solve subsequent problems, and/or to give you some practice with the kinds of questions that will appear on the midterm. Solutions to these problems will be released by the TAs and discussed in sections.
Problems marked with are programming tasks, and will be autograded on Gradescope. There are 8 of them in total. In solving those problems:
You are not allowed to use in built-in OCaml library functions in your solutions. If you do, you will not be awarded any points. Note that language features like pattern-matching do not count as
library functions. You may use library functions like Format.printf and Int.equal to test your code, but you must remove them before submitting.
You are not allowed to use any kind of imperative features, including mutable state (e.g. references and arrays), loops, etc. If you do, you will not be awarded any points.
Problems marked with bonus are optional. You will receive extra credit by solving them. You will not be tested on them in the midterm unless we explicitly say so.
The homework may appear to be long, but again, we decided to err on the more verbose side since we believe this might be more helpful. As usual, the TAs will go over a lot of the expository texts in the discussion sections.
The actual programming problems were designed so that you won’t write more than 100 lines of code in total, but they do require a deep understanding of the concepts covered in lectures.
Some parts of the next assignment will build on the concepts and the code you wrote in this assignment, so it’s important to get them right!
If you are struggling, please do not hesitate to ask questions in the #hw2 Slack channel or come to office hours.
We have provided one unit test for each programming problem. To run all unit tests, simply run
1 duneruntest
in the root directory of this homework. This will compile your programs and report tests that fail.
We highly encourage you to add your own tests, since the autograder won’t show you what the official test cases are (only the identifiers of passed/failed cases will be shown). You can locate the provided test cases in test/test_*.ml . For example, in test/test_part1.ml , you will find the following line:
test_singletons is a helper function that we defined for you. Its first argument is the input to your
singletons , and its second argument is the expected output. You can add your own test cases by adding more elements to the list.
Part 1. Higher-Order Functions in OCaml
Total: 5 points Important notes:
let singletons_tests =
test_singletons (* input *) [ 6; 7; 3 ]
(* expected output *) [ [ 6 ]; [ 7 ]; [ 3 ] ];
1. You may not use recursion (i.e., the rec keyword) to solve problems in this part. If you do, you
will not be awarded any points.
2. Youonlyneedtomodifylib/part1/part1.ml.
In OCaml, functions can take other functions as input, and return other functions as output. This is a very powerful feature that allows us to write very concise code. You have seen simple instances of higher-order function in HW1. For example, your compress has type (‘a -> ‘a -> bool) -> ‘a list -> ‘a list , so it’s a function whose first argument is another function of type ‘a -> ‘a -> bool !
Problem 1 ( ): In OCaml, a function can be defined using let , in which case the function has a name. However, sometimes we just want to make a one-off function on-the-fly, without giving it a name. These functions are called anonymous functions, or lambda functions, and can be defined using the syntax
1 fun
Using this syntax, write down a function of type int -> int -> int that takes two integers and returns
their sum.
Problem 2 ( ): Without looking at the lecture slides:
Informally describe what each of map , filter and fold does, and give an example of how to use each of them.
Write down the type signature of each of them. Check your solution against TODO. It’s ok to reorder some of the arguments.
Try writing down the implementation of each of them. Then compare what you wrote with the implementation in the lecture slides.
Problem 3 ( , 1 point): Using map and an anonymous function, complete the implementation of
which takes a list and returns a list of singleton lists, each containing one element from the original list. For example, singletons [6; 7; 3] will evaluate to [[6]; [7]; [3]] .
You may not use recursion or pattern matching in your solution. If you do, you will not be awarded any points.
Problem 4 ( , 1 point): Using map and anonymous functions, define the function map2d : (‘a -> ‘b) – > ‘a list list -> ‘b list list that applies a function to every element in a 2d list. Example:
1 map2d(funx->x+1)[[1;2];[3;4]]=[[2;3];[4;5]]
You may not use recursion or pattern matching in your solution. If you do, you will not be awarded any
Hint: Use map twice.
Problem 5 ( , 1 point): Using map and anonymous functions, define the function
that computes the cartesian product of two lists. For example,
1 letsingletons(xs:’alist):’alistlist= 2 map .. ns
‘b list -> (‘a * ‘b) list list
will evaluate to
product : ‘a list ->
[1; 2] [true; false]
[ (1, true); (1, false) ];
[ (2, true); (2, false) ]
If we think of the first list as the row labels and the second list as the column labels, then the cartesian product is the table of all possible pairs of row and column labels. For example, the above example can be visualized as
1 (1, true)
2 (2, true)
(1, false)
(2, false)
You may not use recursion or pattern matching in your solution. If you do, you will not be awarded any points.
Hint: Use map twice.
Consider the recursion recipe we talked about in the first section:
1. Identifytherecursivestructureoftheproblem 2. Decomposetheproblemstructureinto:
1. Basecase(s)
2. Inductive/recursivecase(s) 3. Solvethebasecase
4. Tosolvetheinductivecase:
1. Applythefunctiontoallrecursivesub-problems.
2. Assumingthatthesolutionstoallsub-problemsarecorrect,combinethemintoasolutiontothe
original problem.
If we specialize this recipe to the list data structure, we get the following “template”:
1 2 3 4 5 6
let rec solve (xs: ‘a list) : ‘result =
match xs with
| [] -> base_case
| x::xs’ ->
let r = solve xs’ in
combine x r
Note that the same template applies to a wide range of problems. The only difference is that each problem may differ by
1. Howwesolvethebasecase(base_case)
2. In the recursive case, how we combine the the current head value x and the solution to subproblem
y to get a solution to the original problem ( combine x y )
Since those are the only places that might be different for each problem, we can turn them into parameters of the solve function:
1 2 3 4 5 6 7 8 9
let rec solve
(base_case: ‘result)
(combine: ‘a -> ‘result -> ‘result)
(xs: ‘a list) : ‘result =
match xs with
| [] -> base_case
| x::xs’ ->
let r = solve base_case combine xs’ in
combine x r
Essentially, we are letting the specific problem dictates what to do with base_case and combine , which it can do by calling solve with an appropriate base case value and an appropriate combine function. Note that solve is a higher-order function since it takes another function ( combine ) as input.
As an example, recall the lookup function from HW1. We can re-implement it without recursion by using solve :
Here, the base_case is None , since the empty dictionary cannot contain our query key. The combine function takes the first thing in our dictionary, which is a key-value pair, and a (correct!) result of recursively looking up the key in the rest of the dictionary. If the first key already matches, we return the value associated with it. Otherwise, we return the recursive result.
Problem 6 ( ): Re-implement the following functions using solve , by calling it with the appropriate base_case and combine arguments:
1. compress from HW1 2. max from HW1
3. join from HW1
You must call solve . You may not use recursion in your solution.
Problem 7 ( , 1 point): Implement the function power : ‘a list -> ‘a list list that will take a list representing a set, and return a list representing the power set of the input set. The power set of set is the set of all subsets of . For example, power [1; 2; 3] will evaluate to
1 [[];[1];[2];[3];[1;2];[1;3];[2;3];[1;2;3]]
let lookup (equal: ‘k -> ‘k -> bool) (k1: ‘k) (d: (‘k * ‘v) list) : ‘v option =
(fun (k2,v) result -> if equal k1 k2 then Some v else result)
The order of the subsets do not matter for the purpose of grading.
1. Youmaynotuserecursion(includingdefiningrecursivehelperfunctions)inyoursolution.
2. You may use @ which concatenates two lists. For example, [1;2;3] @ [4;5] will evaluate to
[1;2;3;4;5] .
Hint: Use solve and map .
Background note: In functional programming literature, solve usually goes by the name fold_right .
Under the hood, “multi-argument” functions in OCaml are simply one-argument functions that return another function as its output. For example, under the hood, int -> int -> int is the same as int -> (int -> int) , which is a one-argument function that takes an integer, and returns another int -> int function as its output.
For example,
is secretly a function that takes an integer x , and returns another function that takes an integer y and returns x + y . I.e., it’s exactly the same as
A subtle but very useful corollary is that if we have a multi-argument function, we don’t need to supply all of the arguments at once. We can supply one argument at a time, and get a function back which awaits the remaining arguments. For example,
1 (funxy->x+y)12
supplies both arguments and evaluates to 3 , but
1 (funxy->x+y)1
supplies only the first argument, and gives us a function back:
1 fun(x:int)(y:int):int 2 -> x + y
fun (x : int) : (int -> int)
-> fun (y : int) : int
(fun x y -> x + y) 1
== (fun x -> fun y -> x + y) 1
== fun y -> 1 + y
I.e., we get a function that always increment its input by 1 !
Problem 8 ( , 1 point) Consider the function join2 :
let join2 (x: ‘a option) (y: ‘b option) : (‘a * ‘b) option =
match x, y with
| Some x, Some y -> Some (x, y)
| _ -> None
The join2 function takes two options, and if both are Some , it returns a Some that contains a pair of the two values. Otherwise, it returns None . This is similar to the join function you implemented in HW1, but for products instead of lists.
You task is to re-implement join2 as an explicitly one-argument function that returns another function as its output:
Part 2. Names, Bindings, and Substitution
This part only contains problems.
Total: N/A
Read through the notes for section 3, and do the exercises in the notes.
The TAs will thoroughly walk through this part of the assignment in the discussion sections. However, you are encouraged to read through this part and take a stab at the exercises before the section, and write down any questions you have or problems/concepts you would like the TAs to go over in detail. This will help you get the most out of the sections.
Part 3. Lambda Calculus in OCaml
Total: 35 points + 3 bonus points
Important note: You only need to modify lib/lamp/eval.ml .
In this part, we will augment the simple arithmetic expression language defined in the previous assignment
with lambda calculus. We’ll call resulting language is .
Since this is not a toy language anymore, the language will have a well-defined syntax and semantics. We wrote a parser that turns concrete syntax into abstract syntax for you, so you can focus on building the interpreter that consumes abstract syntax trees as input. But it helps to understand the concrete syntax since it may be easier for you to write test programs using the concrete syntax.
let join2 : ‘a option -> (‘b option -> (‘a * ‘b) option) =
match x with
| Some x -> (* todo *)
| None -> (* todo *)
3.1 Concrete Syntax and Informal Semantics
You can read about the informal semantics and the concrete syntax of in the Overview section of the language reference manual. Only sections up to and including Section 2.3 (Named Function Definitions) are relevant for this assignment. The remaining language constructs will be the focus of the next assignment.You’re encouraged to quickly scan through the reference manual first without worrying about the details. You can revisit it later when you’re working on the problems in this part.
The language itself is basically the arithmetic expression language you implemented in HW1 + lambda calculus, and it largely resembles OCaml (modulo some syntax differences). There are, however, a few things that are worth pointing out:
1. There’snounaryminusoperator,sincewecanjustwrite0-xinsteadof-x.Thisisjusttomakethe parser and your interpreter simpler.
2. Althoughtheconcretesyntaxsupportsmulti-argumentlambdas,theparserwillde-sugartheminto curried single-argument lambdas. For example, the following concrete syntax
1 lambdax,y,z.x+y+z
will be de-sugared into something like this
1 lambdax.(lambday.(lambdaz.x+y+z)) So in the AST, you will only see single-argument lambdas.
3. Similarly,afunctionapplicationwithmultipleargumentswillbeparsedintoachainofsingle-argument function applications. For example, the following concrete syntax
will be translated into something like this
1 ((fx)y)z
So in the AST, you will only see binary function applications.
4. Named function definitions like fun f with x = e1 in e2 is just a syntactic sugar for let f = lambda x. e1 in e2 . The parser will de-sugar them for you. So in the AST, you won’t see function definitions being explicitly represented as one of the constructors.
3.2 Abstract Syntax
A straightforward way to represent the abstract syntax tree of — which we won’t end up using — is to modify the expr data type we defined back in HW1 with new constructors for lambda calculus and let- expression. For example, we could — but won’t — augment expr like this:
1 2 3 4 5 6 7 8 9
type binop = Add | Sub | Mul
type expr =
(* arithmetic *)
| Num of int
| Binop of binop * expr * expr
(* lambda calculus *)
| Var of string
| Lambda of string * expr
| App of expr * expr
(* let expression *)
| Let of string * expr * expr
the Var of string case would represent a variable reference. We can use strings to represent variable names.
the Lambda of string * expr case would represent a lambda abstraction that declares a variable name to be in scope in the body expression.
the App of expr * expr case would represent a function application.
the Let of string * expr * expr case would represent a let-expression that first binds a variable name to an expression, and makes the variable in scope in the body expression.
For example, the concrete syntax (lambda f. f 0) (lambda x. let y = x + 1 in y) would be parsed into the following abstract syntax tree:
Although this representation is conceptually simple, working with it would unfortunately result in a lot of code duplication. The reason is that both the Lambda and Let cases contain the binding operation of declaring a variable name to be in scope in some other expression. Thus, if we want to define substitution for Lambda and Let , then we would end up repeating a lot of code in the two cases. Furthermore, since the next assignment will augment with more features that involve binding, any code duplication would only be multiplied, if we don’t prevent it now.
Thus, we will factor out the common pattern of binding into separate constructors:
Lambda (“f”, App (Var “f”, Num 0)),
Lambda (“x”,
Let (“y”, Add (Var “x”, Num 1),
Var “y”)))
Code Help
1 2 3 4 5 6 7 8 9
10 11 12 13
type binop = Add | Sub | Mul
type expr =
(* arithmetic *)
| Num of int
| Binop of binop * expr * expr
(* binding *)
| Var of string
| Scope of string * expr
(* lambda calculus *)
| Lambda of expr
| App of expr * expr
(* let expression *)
| Let of expr * expr
In this representation, the Scope of string * expr case represents the binding operation of declaring a variable name to be in scope in some body expression. The previous example (lambda f. f 0) (lambda x. let y = x + 1 in y) will be now parsed into the following expr:
Note that for Let , the expression whose value will be bound to the variable is the first argument to the constructor, and the second argument is the Scope constructor that declares the variable name to be in scope in let-body. For example, if the above example were instead parsed into
then we are saying that the variable y is in scope in the expression x+1 , and out-of-scope in the body expression y , which is not what we want!
Problem 1 ( ): Pretend you are the parser. For the following programs in concrete syntax, write down the abstract syntax tree as a value of type expr .
1. letx=2inlety=x*xinx+y
2. (lambdax,y.letz=x+yinz*z)23 3. funfwithx=letx=x+1inxinff
Lambda (Scope (“f”, App (Var “f”, Num 0))),
Lambda (Scope (“x”,
Let (Add (Var “x”, Num 1),
Scope(“y”, Var “y”)))))
Scope(“y”, Add (Var “x”, Num 1)),
Programming Help, Add QQ: 749389476
3.3 Well-Formedness of ASTs
A subtle point about the current expr type is that we can technically use the expr constructors to make non-sensible ASTs from a binding point of view. For example, we can write the following:
These expressions are not well-formed. However, because we wrote the parser ourselves that always generates well-formed ASTs, a malicious programmer cannot trick the parser into generating an ill-formed AST using some input program in concrete syntax.
However, it is possible that, when you write your own interpreter, you may accidentally generate an ill- formed AST (e.g., as the output of the subst function) if you aren’t careful. Thus, you should be very careful to maintain the well-formedness of ASTs as an invariant. An invariant like this is bit like a contract:
You are allowed to assume that all input expr are well-formed In return, you must ensure that any output expr is well-formed
Thus, it will be helpful to write a function that checks whether an expr is well-formed.
Problem 2 ( ): Finish the definition of the wf function, which takes a list of in-scope variables vs , and checks if the input expression e is well-formed in terms of the binding structure.
Scope (“x”, Scope “y”,
Binop ( Add,
Scope (“x”, Num 1),
1 2 3 4 5 6 7 8 9
let rec wf (vs: string list) (e: expr) : bool =
match e with
| Num _ -> true
| Binop (_, Scope _, Scope _) ->
(* binop doesn’t bind anything *)
| Binop (_, e1, e2) -> wf vs e1 && wf vs e2
| Var x -> (* todo *)
| Scope _ ->
(* a binder by itself is ill-formed; it must be part of
another language construct that uses it *)
| Lambda (Scope (x, body)) -> (* todo *)
| Lambda _ -> false
| Let (e1, Scope(x, e2)) ->
(* recursively check e1 is well-formed *)
wf vs e1 && ( (* todo *) )
You should also check for out-of-scope references. Hints:
1. Youmayfindithelpfultodefinehelperfunctionsthataresimilartoyoudidwithlist-baseddictionaries in HW1. It’s just that this time, we only need to keep track of the keys, not the values, so we use string list instead of (string * ‘v) list .
2. Eachtodocanbeimplementedwithjust1lineofcode,althoughthat1linemaybeacalltoahelper function. If you wrote more than 1 line, you are probably overthinking it.
Problem 3 ( ): Give two examples of e for which wf [“x”] e will return false , and one example of e for which wf [“x”] e will return true .
3.4 Semantics
Problem 4 ( , 5 points): Implement the free variable function free_vars: expr -> Vars.t that computes the set of free variable references in an expression. The Vars module provides a type ( Vars.t ) to represent a set of strings, and functions that operate on such sets, e.g.:
1 2 3 4 5 6 7 8 9
(* the empty set *)
val empty : Vars.t
(* add a string to a set *)
val add : string -> Vars.t -> Vars.t
(* take the difference of two sets *)
val diff : Vars.t -> Vars.t -> Vars.t
(* check if a set contains a string *)
val mem : string -> Vars.t -> bool
Please refer to vars.mli for the full list of functions in the Vars module. Hint: The only interesting cases are Var and Scope .
Problem 5 ( , 15 points): Finish the implementation of the substitution function
Here, subst x e c denotes the substitution c[x |-> e] , i.e., substituting all free occurrences of x in context c with expression e .
let rec subst (x: string) (e: expr) (c: expr) : expr =
match c with
| Let _ -> false
You don’t need to implement capture-avoiding substitution, or do any kind of alpha-renaming. You can also assume that e is well-formed, and you should maintain the invariant that c is part of a well-formed expression.
Hint: The only interesting cases are Var and Scope .
Problem 6 ( bonus , 3 points): Modify the Scope (x, e) case of your subst function to implement
capture-avoiding substitution using alpha-renaming.
Important note: If you choose not to do this problem, you should still understand how to do alpha- renaming and capture-avoiding substitution on a conceptual level, since you may be asked to do so in the midterm.
To be consistent with the autograder, whenever you need to alpha-rename some name y of a binder
scope y in e , you should rename y to yn where n is the smallest natural number such that using yn as
an argument will not capture any variables. Here are some examples of alpha renaming:
(lambda x, y. x y) (lambda x. y) will evaluate to (lambda y0. (lambda x. y) y0) .
(lambda x, y. x y y0) (lambda x. y) will evaluate to (lambda y1. ((lambda x. y) y1) y0) (lambda f, y. let y0 = 5 in y) (lambda x. y) will evaluate to lambda y0. let y00 = 5 in y0 (lambda z. lambda y. let x = 5 in z) (lambda y. x) will evaluate to lambda y. let x0 = 5
in lambda y. x
We suggest implementing a helper function for finding the next available name and testing it separately. By default helper functions are not visible outside the file they are defined in. To make them visible, simply add the type signature of your helper function to eval.mli .
Problem 7 ( , 15 points): Finish the implementation of the interpreter
The eval function will “run” your program by performing binary operations, evaluating function arguments, applying arguments to functions using subst , etc. You might want to refer to Section 4 (Operational Semantics) of the language reference manual for the precise meaning of each language construct. If no evaluation rule applies, then your interpreter should call im_stuck to signal that the interpreter is stuck.
You can assume that the input expression is well-formed.
Now you have a working interpreter for a Turing-complete programming language! Since we’ve also written a parser for you, you can run your interpreter interactively like you run utop , or use it to run program files. To run it interactively, simply run
1 duneexeclib/lamp/repl.exe
let rec eval (e: expr) : expr =
match e with
After which you should see a welcome message, and a prompt > after which you can type in expressions to evaluate. For example:
Use the / arrow keys to navigate the history of commands you typed in. You can also run your interpreter on a program file with
1 duneexeclib/lamp/repl.exe–
We also wrote a reference interpreter located on CSIL at ~junrui/lamp which you can use to compare the output of your interpreter. To run the reference interpreter, simply run ~junrui/lamp (interactive mode) or
~junrui/lamp
If you discovered any bug in the reference interpreter, please let us know!
Part 4. Church Encoding
This part is completely optional.
Total: 3 bonus points
In lectures, we learned that lambda calculus is super powerful, and can express all kinds of data structures and operations, e.g., booleans, natural numbers, etc. Of course, lambda calculus doesn’t support booleans or natural numbers natively, so we had to find a way to encode them into expressions that are valid in lambda calculus. Although those Church encodings don’t look like their counterparts, they have the same behavior as their counterparts.
Tip: For this part, you’ll be writing a lot of lambda calculus expressions. You can use our reference interpreter on CSIL to play the expressions you came up with. You may also find it helpful to use them as realistic cases to stress-test the interpreter you wrote in part 3.
4.1 Why Should I Care about Church Encoding?
Before diving into the Church encoding, let’s first motivate why we care about it in the first place. After all, half of this README is taken by this bonus part on Church encoding that you don’t even have to do, so it better be worth your time in case you choose to do it!
Your first reaction to Church encoding might be:
1. Sincealmosteverysensibleprogramminglanguagealreadyhasbooleansandnumbersbuiltin, why should we even bother to go through the mental gymnastic of encoding booleans and natural numbers into the language? Why doesn’t lambda calculus also just treat them as primitives, like every other language?
2. IsChurchencodingjustsomeacademicexercisethathasnopracticalvalue?Asafuturesoftware
Welcome to lambda+! Built on: Wed Jan 24 12:54:56 PST 2024 >1+1
浙大学霸代写 加微信 cstutorcs
engineer, or someone who’s probably not gonna use functional programming in my day job 1 , why should I care?
To answer the first question, note that when we encounter a new language, one of the most important questions we might want to ask is:
“How expressive is this language?”
For example, using this new language, can we do things like: integer arithmetic? branching? loops and recursion? procedural abstraction? mutable memory? message passing? generics?
The programming language we choose will fundamentally shape the way we think about and solve problems. So we really want expressive languages that make it easy to express a wide range of problem- solving paradigms.
However, the more features the language has, the more difficult for us to understand, master, and analyze it. This is because every language feature can potentially interact with any other feature, and may lead to complex behaviors that might not be apparent just by looking at the individual features in isolation. If the language has N features, then we may need to understand possible interactions between them!
This leads to a fundamental tension of language design: we want expressive languages, but we also want easily understandable languages. This can be a very hard question for language designers.
Fortunately, there’s a simple trick that allows us to have the best of both worlds: say a language has both feature X and Y , and we know that Y can be realized by translating it to X . Then, we just need to study the language with feature X , and we can ignore Y completely, since any program that uses Y can be turned into an equivalent program that jus