| Important Messages from the Instructors
Sunday, November 28th, 2010
Your presentation must be a white board lecture.
Tuesday, November 23rd, 2010
Preparing Your Presentation
Your presentations should consist of two parts: a background section and a
work section. The former should bring across the essence of the chosen
paper; the latter is about your work, your model, and the insights you
derived from your work. The transition between the two sections is about
what questions the paper left you with and which parts of the paper you
decided not to include in your work/model and why.
Your talk should fit into the normal 30-minute conference slot. Do not
think of the two sections of your presentation as two halves, i.e., 15
minutes each. Indeed, it is unlikely that you will dedicate 15
minutes to each with a bridge segment of 0 seconds. Your challenge is to
figure out how to allocate the time on the two sections and the bridge.
The key to organizing a talk is to develop a mental model of the
audience. You know what your classmates know about PL. Base your talk on
that. For some papers, you need to bring in additional background, e.g.,
how the http protocol works. To assume less background in your audience is
a better mistake to make than to assume too much.
If you are presenting with a partner, you are welcome to split the
presentation in any way you want between the two of you. Each of you
should speak for half the time (some 15 minutes).
Finally, when you give conference talks, you must answer questions. In
PPL, the audience will be allowed to ask questions at any point, and you
will respond in turn. In other words, each of you must be ready to answer
all questions not just questions about your part.
Sunday, November 21st, 2010
Problem 9(1) was overly ambitious for a
plain homework problem. I have simplified it.
Sunday, November 14th, 2010
After grading the solutions to problem set 8, I thought I should explain
how you might have come up with a clean design (some did, some didn't).
For problem 5/2, you added recursive functions to Iswim like this:
(rec x (lambda (x) e) in e)
Since problem 8/1 describes
(loop x_loop (x_init e_init) e_body)
as a construct that sets up a recursive function and calls it
on e_init, it is possible to implement it
withrec like this:
(rec x_loop (lambda (x_init) e_body) (x_loop e_init))
Also in class I had described the solution for rec as a use
of Y_v, which would get you this much:
((Y_v (lambda (x_loop) (lambda (x_init) e_body))) e_init)
Turning this last insight into an instruction for the CEK machine is
straightforward:
< (loop x_loop (x_init e_init) e_body), rho, k >
-->
< ((Y_v (lambda (x_loop) (lambda (x_init) e_body))) e_init), rho, k >
Alternatively, you could use the fixpoint equation for Y_v
and step-for-step derive CC, CK, and CEK instructions. Either way you come
up with a simple and elegant design for loop instructions on
the CEK machine.
The questions concerning loop should have clarified that
x_loop is an explicitly named continue
statement.
As for the introduction of the break, the minimum to
recognize is that it demands some way to mark the entrance to the
loop on the control stack. Popping the stack to that point
gives you dynamic breaks; creating a fresh marker for the stack and
associating it with the name of marker. The problem is that the name is
now used for both the recursive function and the marker on the
stack. Solving this problem required some creativity and was worth five
out of 40 points (or some 12%) on this set.
Friday, November 12th, 2010
Problem set 10 is in final form.
The due date for problem set 9 is now 11/23 to give you some additional
time for the project.
Here is the promised sketch of a solution for the break feature:
[--> ((loop x_L (x e_0) e_L) rho k)
(e_0 rho (init x_L x e_L rho k))]
[--> (v rho_v (init x_L x e_L rho k))
(e_L
(extend (extend rho x_L (LL x_tag (lambda (x) e_L) rho)) x (v rho_v))
(loop x_tag k))
(fresh x_tag)]
[--> ((break x_L e_exn) rho k) (e_exn rho (cut k x_tag))
(where (LL x_tag v rho_v) (lookup rho x_L))]
You should be able to guess at the modification to continuations and
closure values.
Wednesday, November 10th, 2010
The solutions for problem set 7 are graded. You may pick up your
assignment between 4:00pm and 5:30pm in case you need to see the
feedback before Friday.
The interpreter for B seems to be a small problem for everyone, so I
wrote down two solutions:
;; the basic B language
(define-language B
(e true
false
(* e e))
(v true
false))
Here is an interpreter in plain Racket:
;; B/e -> E/v
;; evaluate programs from B according to rules
(define (eval-b-racket t)
(cond
[(eq? 'true t) t]
[(eq? 'false t) t]
[else
(define lft (eval-b-racket (second t)))
(cond
[(eq? 'true lft) 'true]
[(eq? 'false lft) (eval-b-racket (third t))])]))
And here is one in mostly Redex:
;; B/e -> E/v
;; evaluate programs from B according to rules
(define (eval-b-racket t)
(define-metafunction B
evalB : e -> v
[(evalB v) v]
[(evalB (* e_1 e_2)) true
(side-condition (eq? (term (evalB e_1)) (term true)))]
[(evalB (* e_1 e_2)) (evalB e_2)])
(term (evalB ,t)))
Tuesday, November 2nd, 2010
Here is my primary reaction to your project memos.
A project memo should consist of two distinct parts: a summary of the
background and a goal statement. Since the goal of the course project is
to digest the content of an existing research paper via the construction
of a Redex model, the background summary should recapitulate in your own
words what you currently think the paper reports. The goal statement
should specify with respect to this paper summary, what you wish to
understand in detail.
The (boring but) safest way is to explicitly label the parts of your memo
as "summary" and as "goal" statement and to present them in that order. If
you are confident about your writing skills, you may naturally deviate
from this rudimentary presentation and mix-and-match pieces.
Avoid "weasel words" and "weasel paragraphs" in both the summary and the
goal statement. They simply indicate that you are insecure or lack
understanding. Instead, express what you are insecure about and make it a
part of the goal.
Use complete sentences for the summary and the goal statement. It is
acceptable to have an enumeration of phrases, but when you use this
technique make sure to connect the phrases to the context so that you get
complete sentences.
For your project report, follow the same outline but replace the goal
statement with two parts: what you have learned and what you still fail to
grasp from the paper.
Saturday, October 30th, 2010
Most solutions for problem 6(1) suffer from basic organization
problems. Here is a Racket version in a syntax according to the first two
weeks of this course:
;; ISWIM/e -> ISWIM/answer
(define (evaluate program)
(unload-final-state
(evaluate-according-to-machine
(create-initial-state program)))
;; ISWIM/C??State -> ISWIM/C??State
(define (evaluate-according-to-machine s)
(if (final? s)
s
(evaluate-according-to-machine (transition-function s))))
(No an experienced Racketeer would not write quite this code.)
Here is a BraceLanguage-style piece of code:
ISWIM/answer evaluate(ISWIM/e program) {
State s = createInitialState(program);
while !isFinalState(s) {
s = transitionFunction(s);
}
return unloadFinalState(s);
}
From here on, you just develop and present the transition function.
Of course, after an hour of covering random checking in Redex, I did
expect some attempt to relate the evaluator program to the Redex model
from which you started.
Problem 6(2) called for a revision of a REDEX model. If you wrote an
evaluator in Racket instead, I reduced 10 points and graded out of these
10 points, if there was an attempt to deal with full-fledged
define and the rest of the evaluator looked 'decent'.
Problem 6(3) must have stumped people in ways that I couldn't
foresee. Since only one pair got this 100% correct and all others failed
completely, I have graded the problem set on a 40-point basis and have
assigned the successful pair 10 extra points.
(I am grateful that some people came to see me and asked me questions. BUT,
I think I heard the question I wanted to hear and the answers I gave were
answers that you thought related to the questions that were asked.)
The lemma requested in problem 6(3) came up as a "simple" step during the
proof of consistency and Church-Rosser. After explaining why it should be
true (not provable) and seeing some doubts in your faces, I said "this is
a good problem to add to the homework" and I did so. Given that the lemma
is needed to prove consistency and CR, you can't use the latter to prove
it. Keep the context in mind!
The Claim:
e e_1 e_3 e_5 e'
\ / \ / \ / ... .... ... \ /
\ / \ / \ / \ /
e_0 e_2 e_4 e_n
(where each pair of subsequent lines is
a pair of -->> and <<-- or
a pair of <<-- and -->> relations)
The Example: When you're stumped, make examples. The
design recipe tells you so.
\x.((\y.y)2+1) = \x.1+2
Here is a bunch of proof steps:
[1] (\x.(\y.y)2+1) = (\x.(\y.y)3) by -> base
[2] (\x.(\y.y)3) = (\x.3) by -> base
[3] (\x.(\y.y)2+1) = (\x.3) by [1]/[2] transitivity
[4] (\x.2+1) = (\x.3) by -> base
[5] (\x.3) = (\x.2+1) by [4] symmetry
[6] (\x.1+2) = (\x.3) by -> base
[7] (\x.3) = (\x.1+2) by [6] symmetry
[8] (\x.(\y.y)2+1) = (\x.2+1) by [3]/[5] transitivity
[9] (\x.(\y.y)2+1) = (\x.3) by [8]/[4] transitivity
[A] (\x.(\y.y)2+1) = (\x.1+2) by [9]/[6] transitivity
(now this is not the only possible way to use the def of =)
Here are the same proof steps arranged as the desired wave:
(\x.(\y.y)2+1) (\x.2+1) (\x.1+2)
\ -> / \ /
(\x.(\y.y)3) / <- \ -> / <-
\ -> / \ /
(\x.3) (\x.3)
The Proof:
Assume e = e'.
Prove that there is a sequence e_0 .. e_n of terms/expressions that are
chained via a pair of -->> and <<-- or a pair of <<-- and --
-- -->> relations.
The = relation is the symmetric-transitive-reflexive closure of the
reduction relation -->.
We proceed by induction on the size of the argument that establishes e = e'
and by cases on the last step
* reflexivity
e = e' because e is identical to e'
pick the empty chain
* transitivity
e = e' because e = e" and e" = e'
by inductive hypothesis, there exist chains
e, ..., e_i, e"
e", e_j, ..., e'
that satisfy the desired 'wave' criteria
if e_i -->> e" and e" -->> e_j, pick e_0, ..., e_i, e_j, ... e'
if e_i -->> e" and e" <<-- e_j, pick e_0, ..., e_i, e", e_j, ..., e'
ditto for e_i <<-- e" and e" -->> e_j
* symmetry
e = e' because e' = e"
by inductive hypothesis, there exists a chain; use it
* base
e = e' because e -> e'
pick the chain e, e' (yes, degenerate chains are fine, too)
Friday, October 29th, 2010
The partner switch is effective as of today.
Problem 7(2) calls for an evaluator for language B. Implement this
evaluator in RACKET.
Problem 7(2) also calls for an evaluator based on the CK machine for
language B. Implement this evaluator in REDEX.
Finally, problem 7(2) demands a thorough comparison between the two. Use
redex-check to implement this check. NOTE: random testing is
making an appearance in a wide spectrum of languages, and it is good for
you to explore it at least once in your grad student career.
Wednesday, October 27th, 2010
Jose points out that the pair of mutually recursive functions
odddP and evenP should be written like this:
(define evenP (lambda (x) (if0 x 1 (oddP (- x 1)))))
(define oddP (lambda (x) (if0 x 0 (evenP (- x 1)))))
It avoids the infinite loop for (oddP 0).
I will be happy if you get either version to work.
Tuesday, October 26th, 2010
Someone asks:
We don't know if we should model the first problem using Racket only
(i.e. without using Redex). Can we use a combination of Racket and Redex?
The answer is no, the evaluator must be in plain Racket.
Someone else asks:
Is the transition relation for the CC machine really a total function? It
doesn't seem to work on states such as < v , E > ?
I meant to say that the transition relation is a total function for proper
expressions, i.e., non-values. Since states such as the ones mentioned in
the question are final states, the relation should not
be defined on them.
Monday, October 25th, 2010
I have released a complete set of problems for the rest of the semester so
that you can calibrate how to allocate your efforts.
Just in case you have already read ahead, I had to change the statements
for problem set 7 to fit into the overall plan.
Email me if you discover inconsistencies/typos/etc.
Saturday, October 23rd, 2010
I have modified the project page, mostly to include a
grading guide.
I graded solutions for problem 5(4) liberally and the scores are all over
the map. The purpose of the problem was to figure out the essence of a
standardization theorem---that it is about an algorithm (a function) for
reducing programs to values. The goal here isn't to mimic and adapt proofs
as they are but to determine what is really needed. A proof follows.
;; -----------------------------------------------------------------------------
Problem 5.4:
Given:
def. language:
b = tt | ff | b * b
def. notion of reduction:
tt * b r tt
ff * b r b
def. general context:
C = [] | C * b | b * C
def. reduction relation:
C[tt * b] -> C[tt]
C[ff * b] -> C[b]
->> is the transitive reflexive closure of ->
def. evaluation
eval-b(b) = tt iff b ->> tt
eval-b(b) = ff iff b ->> ff
theorem 2.6 (in book): eval is a total function, i.e., for all b, (b,*) in eval
;; -----------------------------------------------------------------------------
The reduction relation is a proper relation, meaning for any given b, there are
usually many different reduction sequences from b to tt or ff. The purpose of a
standard reduction theorem is to identify one of these paths as the canonical
one and to provide an algorithm for detecting this path.
def. evaluation context
E = [] | E * b
def. standard reduction
E[tt * b] |--> E[tt]
E[ff * b] |--> E[b]
|-->> is the transitive reflexive closure of |-->
def. standard evaluation
eval-s(b) = tt iff b |-->> tt
eval-s(b) = ff iff b |-->> ff
THEOREM: eval-b = eval-s
Proof: Show that
(b,tt) in eval-b iff (b,tt) in eval-s [i]
and
(b,ff) in eval-b iff (b,ff) in eval-s [ii]
Wolg, pick [i] and show both directions.
;; -----------------------------------------------------------------------------
R2L: assume (b0,tt) in eval-s (in excessive detail)
.: b0 |-->> tt (by def of eval-s)
.: b0 |--> b1 |--> b2 |--> ... |--> tt (by def of trans-refl. closure)
.: E_0[b0_r] |--> E_1[b1_r] |--> E_2[b2_r] |--> ... |--> tt (by def of |-->)
for some E_i, bi_r
.: E_0[b0_r] --> E_1[b1_r] --> E_2[b2_r] --> ... --> tt (all Es are Cs)
.: b0 --> b1 --> b2 --> ... --> tt (by def of -->)
.: b0 -->> tt (by def of trans-refl closure)
.: (b0,tt) in eval-b (by def of eval-b)
;; -----------------------------------------------------------------------------
L2R: assume (b0,tt) in eval-b
.: b0 -->> tt (by def of eval-b)
.: b0 |-->> tt or b0 |-->> ff (by lemma below)
.: the second result is impossible, as we show by contradiction.
assume b0 |-->> ff
.: b0 -->> ff (by R2L direction of proof)
but this is a contradiction to the global assumption.
.: so this nested assumption can't work.
Hence, b0 |-->> tt, because it is the only possibility left
.: (b0,tt) in eval-s
QED
Lemma: for all b, b |-->> tt or b |-->> ff
proof:
(1) by induction on the structure of b, b is either tt, ff, or |-->
reducible. Assume b is b1 * b2. Either b1 is tt or ff, in which case
E = []. Or by induction hypothesis, there b1 |--> b1_s. By definition
of E, b1 * b2 |--> b1_s * b2. QED
(2) by definition of |-->, if b1 |--> b2, then b2 has fewer *s than b1.
Putting (1) and (2) together, every b starts a finite reduction sequence of
as many steps as there are *s in b and the end is either tt or ff. QED
Friday, October 22nd, 2010
I have marked a part of problem 6(2) as challenge so that
you can allocate your time properly.
Rather than provide you with a library for your work, I decided to
supply source code that you can use for evaluation S-expressions as
Racket programs:
;; ISWIM/e -> Any
;; evaluate an S-expression that represents an ISWIM program in RACKET
(define (eval-racket e)
(define raw-result
(with-handlers ((exn:fail? (lambda (x) 'STUCK)))
(eval e racket-ns)))
(if (procedure? raw-result) 'function raw-result))
;; a name space for evaluating Racket programs
(define racket-ns
(parameterize ([current-namespace (make-base-empty-namespace)])
(namespace-require 'racket)
(current-namespace)))
The one serious problem left with this code is that it goes into an
infinite loop for ISWIM programs that have infinite reduction
sequences. You have seen how to limit reduction sequences in Redex; to
limit evaluations in Racekt, see
call-with-limits
and with-limits in the Racket sandbox library.
Start looking for a partner with whom you will do problem sets 7 through 10.
I will write up grading guidelines for the project over the weekend.
These guidelines are not a checklist for getting a
perfect grade, but a tool for understanding what a research project is
like and how to allocate your time for the last six weeks of the
semester.
Tuesday, October 19th, 2010
Someone asked:
Is the ISWIM0 term (if0 ok (* 3 4) (^ 3 4)) considered stuck?
where ok is some variable name. The answer is that -- as
defined in the text book -- programs are closed terms, i.e.,
terms without free variables.
Upon request, I have slightly modified problems 2 and 3 for
assignment 5 so that you may
either extend Lambda0 or the preceding solutions.
Monday, October 18th, 2010
This week's lectures will use the ISWIM flavor of problem 4(3).
I have therefore posted a solution on-line so
that you can explore the ideas from lecture interactively without having
to worry about accidental mistakes in your language and reduction
systems.
Robby Findler just presented Redex to the FOOL Workshop co-located with
OOPSLA. His presentation is
on-line as a pdf and I encourage you to flip through the slides over
the next week or so. His FOOL Keynote complements my lectures with a
slightly different and extended example.
Saturday, October 9th, 2010
Please stay on top of your readings.
After grading the third problem set, I realized that we introduced
'contracts' for metafunctions after we published the book. So
here is a way to specify the depth function with a header
that ensures proper usage:
;; determine the depth of a context
(define-metafunction L
depth : C -> number
[(depth hole) 0]
[(depth (C * e)) ,(+ 1 (term (depth C)))]
[(depth (e * C)) ,(+ 1 (term (depth C)))])
Naturally, I did not subtract points for missing such a contract. An
informal contract suffices.
Wednesday, October 6th, 2010
Someone asks about problem 0, problem set 3:
this will not always return the first irreducible form of any arbitrary
t with respect to any arbitrary relation R. If R applied to t leads in
ANY step to an infinite chain of computations, apply-reduction-relation*
will never return.
Consider the problem in the context of problem set 3 only. Use the purpose
statement to explain why your answer solves the problem or why it only
approximates a solution.
Tuesday, October 5th, 2010
Someone requested a posting of the Redex model of addition from Friday (1
Oct 2010). It is now on-line.
Some of you still haven't specified a project partner.
Also don't forget the due date for choosing a paper.
Sunday, October 3rd, 2010
A draft of problem set 4 is now available.
The general information about the course has been revised to specify a
grade policy.
Saturday, October 2nd, 2010
Here is a solution for problem 2 from the second
problem set. Note that the problem statement contained the question
"how would you prove that your implementation is equivalent to the
specified semantics" and that truly called for a proof idea, not a full
proof (difficult!). The challenge of sketching a proof was also supposed
to make you experiment with alternative ways of designing this function.
The idea of proving the correctness of a programming language
implementation is no longer far fetched. Indeed, some projects tackle the
entire implementation stack: hardware, os, compiler. The purpose of such
projects is to create highly reliable -- and especially easily defendable
-- systems that are neither prone to random crashes nor easy attacks.
Friday, October 1st, 2010
Partners for course project:
Choose a partner for your course project. One of you must send me an email by
Tuesday, October 5 (before class)
and cc the other one to let me know of your choice.
Choice of paper for course project:
Read the abstracts and introductions of PL papers that might interest
you. One of the partners must send me email to inform me of the chosen
paper (with a cc to the partner). The papers on the project web page will
be assigned on a first-come/first-serve basis.
Partners for problem sets 3 and 4:
Choose a partner for your next two problem sets. One of you must send me an email by
Tuesday, October 5 (before class)
and cc the other one to let me know of your choice.
This task is distinct from the first one.
Handing in solutions:
Please hand in a paper copy of your complete solutions at the beginning of
class, and email me an attachment of Racket files for all problems that
call for programming.
Friday, October 1st, 2010
Most of you mangled problem 1.4 badly. Here is a
solution. Read it, study it, experiment. You should understand this
solution properly.
Just because someone shows you hashtables during a lecture does not mean
that you should use hashtables in your programs. My intention was to see
whether you thought through the problem or whether you are still in the
mode of copying existing programs and changing them until they (kind of)
do what you want; your use of hashtables informs the grader into which
class of program designer you fall.
Saturday, September 25th, 2010
The first draft of problem set 3 has been posted.
Please choose a new and distinct partner for problem set 3.
If you can't find a new partner, speak up at the beginning of class on
10/1. If you hand in solutions for problem set 3 with the same partner,
you will get no credit.
It is also time to choose a project partner and topic.
For the selection of a project topic, read the abstracts and introductions
of (some, all) papers (whose titles, looks, authors) you find intriguing.
Ask yourself whether you understand the problem that the paper addresses
and whether you find the problem interesting.
This is also how you select initial research topics and advisors;
eventually you end up with a dissertation topic that way.
The schedule now comes with reading assignments so that you can prepare
yourself for the lectures.
Tuesday, September 21st, 2010
The lecture notes contain the source files for accumulator and
intermediate-data structure programming. I will add notes tomorrow.
Homework #2 is final. If you're ready, tackle it.
In lecture I used the notation
R*
to denote the transitive closure. Someone reminded me after the lecture
that the conventional notation is
R+
(Even if the notation is just to say "this is a different relation",
I should stick to convention, because these conventions are used
widely -- even in the Redex book.)
Tuesday, September 14th, 2010
The first lecture is now available on-line. See tab on the left.
Sunday, September 12th, 2010
The web pages are now set up. Most importantly, the first assignment is
released, and I urge you to get started immediately. It is extremely labor
intensive, making up for significant gaps in your undergraduate
education. Other assignments will be released in a timely fashion,
matching the progress we make in lecture.
Also, the description and instructions for the project are out. You should
immediately start reading abstracts and introduction to determine which
paper(s) appeal to you. I will explain some points in class again, and you
will have a chance to ask questions.
Finally, check the schedule to get an idea of what we cover and how
quickly. Due to assignment 1, the reading load in this course will be
substantial.
Friday, September 10th, 2010
I will share the results of the first quiz with you on Tuesday. In the
meantime, I have posted a brief introduction to
proof by induction from Matthew Flatt (UUtah).
I have also written up two solutions of the programming problem,
- one in Java, because several people tried to
solve the quiz problem in this language and failed;
- another one in Typed Racket, which is my
primary programming language. (Racket is derived from Lisp and Scheme.)
Tuesday, September 7th, 2010
Welcome to the PhD-level course on programming languages.
Our organizational meeting will take place on Friday 9/10 in WVH 166.
Note that this is not the regular location. If you cannot attend this
meeting, please send me email as soon as possible.
In the meantime, here is an entertaining essay from the Wall Street
Journal weekend edition (30 Jul 2010) on (natural) language and thinking:
Does Language Influence Culture
For the bi-lingual among you, this essay may be of particular interest.
(A similar but longer piece appeared more recently in the NYT.)
|
|
