This is the teaching fellow's page. I will post some supplemental material here from time to time, allowing both students and the professor to keep track of what happened in discussion sessions.
You're welcome to make appointment by e-mail; please check my schedule first.
Working With CS Computing Resources
See the Getting Started guide for tips on working from home and transferring files over, and for a primer on using Linux.
In talking about the sample Final Exam, spent almost all the time on Question 7:
- Lambda calculus primer, t ::= x | t t | λx.t
- Use "canonical form" strategy to break down function type. If we want to construct a term t that type A → B, the term t has to have the form λx.t0 where x (the argument) has type A and t0 (the body) has type B (in ATS, it would be written as lam x => t0).
- If A is a function type, that means x is a function given to us.
- If B is a function type, then recursively break down B using the canonical form strategy.
- If B is not a function type, then look at all the arguments we are given so far (some of them are functions), and see if there is any combination of the function call that will give us B.
- Sometimes it may be useful to do function composition to obtain the required type, i.e. given f: A → B and g: B → C, if we want a function that has the type A → C, then we can write λx.g (f x).
- Use the typing rules of lam and app to verify your result is correct.
- Motivated why these typing rules are written the way they are.
- Operational semantics t ⇒ t' means that t is reduced in one step to t'. Imagine your program is a very long expression which runs by reducing to smaller programs until it becomes a value, which is irreducible, representing the result of computation. The only rule we're interested here concerns function call: (λx.t0) t ⇒ t0[x := t], by substitution all occurrences of variable x inside the function body with the term passed in as the argument. This is called β reduction.
- Call by value: evaluate argument t to a value first, then substitute for function call. Call by name: substitute t into the function body, and evaluate individual occurrences of t separately. If t is an expression that prints out a string, call by value only prints once prior to the function call, and call by name prints as many times as x occurs in the function.
- Type preservation theorem: if ∅ ⊢ t : A and t ⇒ t', then ∅ ⊢ t' : A, i.e. the intermediate steps of evaluation doesn't change the type of your program.
- Substitution lemma: if Γ, x : A ⊢ t0 : B and Γ ⊢ t : A, then Γ ⊢ t0[x := t] : B. This lemma describes what's the correct behavior for β reduction, which governs how lam and app rules can be written if we want the type system to be sound.
- Will go over some dependent type examples tomorrow at 2pm.
- Went over blackjack rules and the provided code.
- Went over the problems streamAverage and fib in the sample midterm 2; code attached below.
If you use the lrand48() function in "libc/SATS/random.sats", then you probably need a way to convert from lint (long int) to int. There is a primitive function called atspre_int_of_lint defined in "prelude/CATS/integer.cats" but there is no function type declaration in the corresponding "prelude/SATS/integer.sats". In order to use it in your code, add this to your .dats file:
extern fun int_of_lint (li: lint):<> int = "atspre_int_of_lint"
And you can call the function as int_of_lint. Example code is attached below.
You can also manipulate lint in ATS directly (arithmetics, comparison, etc.). You can write lint constants by suffixing a number with 'l', e.g. 0l for zero, and 1l for one.
See attachment; instructions for unpacking the file can be found in Getting Started
Went over ralist in Assignment 3 solution.
- ralist is analogous to binary representation of natural number (bignum) like singly linked list is analogous to unary representation.
- Unary representation: empty string is zero, successor adds one by prepending a digit to the string, predecessor removes a digit from the beginning of the string.
- Singly linked list represents a sequence of data by placing one element at each digit. Empty list is analogous to zero, cons analogous to successor, uncons (pattern matching) analogous to predessor.
- Binary representation: still a list of digits, least significant digit first so carrying is easier to implement. Each digit is either odd (1) or even (0).
- Random access list represents a sequence of data by grouping them into a forest of balanced binary trees. If the i-th digit is odd, then that digit carries a balanced binary tree of size 2i. The length of the data sequence is the binary number represented by odd and even.
- Racons is analogous to successor (needs to build the tree by carrying) and rauncons to the predecessor (needs destruct by borrowing).
- The easy way to implement ralookup and raupdate is to keep track of the indices skipped to the respective size of the trees, and to perform a binary tree lookup/update at the correct digit.
- Alternative way to define ralist:
datatype ralist (a:t@ype) = Emp(a) | Odd(a) of (a, ralist '(a, a)) | Evn(a) of ralist '(a, a)
The idea is that we recursively form pairs as we go down the digits. The pairing guarantee completely balanced binary tree. The key to lookup and update is to treat the rest of the list indexed in pairs. This is the approach taken by the solution.
Efficient update, however, requires a "map" function f: a → a. At the very top level, it updates only an element. As we recurse down the digits, we build the pair update function f': '(a, a) → '(a, a), which takes a pair, and according to the index, updates either the left or the right a using f. To go down one more digit, the update function becomes f'': '('(a, a), '(a, a)) → '('(a, a), '(a, a)) and so on.
Briefly talked about stream, partial sum, and Euler's method. Eratosthenes sieve construction using lazy evaluated streams (straightforward adaptation to the non-lazy version).
Went over sample midterm questions posted here. Some suggestions:
- Tail recursion is preferred when scanning a list left-to-right, and the result does not specify a particular order. If the result must be in the same order as input, then non-tail is easier to implement. If tail-recursion is desired and result must be in the same order as input, then the accumulator, which is constructed by prepending elements from left-to-right, needs to be reversed. Do not use list append, as it is O(n) for each element, which makes the whole function O(n2).
- When traversing the whole binary tree, tail recursion is still possible, but we need to use continuation passing style. For example, in post-order traversal, when traversing the left subtree, we pass it a continuation to tell it what to do when that's done (i.e. should traverse the right tree). When traversing the right tree, we pass it a continuation to tell what to do when that's done (i.e. do something with the parent). A continuation is a function closure that is called by the base case of recursion, taking the accumulator (which is the partial result) as the argument. The continuation would perform further computation on the accumulator.
- When tackling postbal problem, the function itself is too restricted to be called recursively: suppose length(xs) = 2h - 1, postbal(xs, h) = t returns balanced tree t such that postord(t) = xs. We want to divide xs into three parts, xs1, xs2, xn, where lenght(xs1) = length(xs2) = (length(xs) - 1) / 2 = 2h-1 - 1. A common strategy is to strengthen the recursion as follows: postbal_super(xs, h) = (t, xs') is like postbal(xs, h) except it only requires that length(xs) >= 2h - 1. It will return the excessive parts of xs in xs'.
- Print a "list0 int"
- Insertion sort on list0 int.
- Merge sort on list0 int.
- The code in merge sort has an infinite loop. Extra credit if you can spot where it is.
Homework 1 exercise 4 is typeset into PDF and attached below.