Wednesday, December 14th, 2011

The End.

Wednesday, December 14th, 2011

The graded project appendices are in the mail. The grade consists of five parts, worth 10 points each. Here are the very rough guidelines:

1. effort: does the code meet the expectations of your proposal memos/conversations?
2. correctness: are the functions (e.g., subst) and relations correct?
3. presentation: do you explain the project, the file, the functions? is it presented top-down?
4. testing: do you have test suites for functions and relations? do you use redex-chec as appropriate?
5. usability: can I get simple programs to run in a short amount of time? is the model accessible to a third person?

Keep in mind that these guidelines are rough and that I cannot possibly check every corner of the code.

The average percentage was 88 on this part of the project, which is a pretty impressive A- level grade.

Friday, December 2nd, 2011

Wednesday, November 23rd, 2011

I returned the graded versions of homework 9. Look for 'mf:' in your file and study my remarks on your code. Converting a CEK machine to a CESK machine is, in principle, a straightforward task and is covered extensively in the course text. Hence, the only interesting detail concerns the idea that the CESK machine "must use the store to safe-keep all values." In other words, all allocations go into the store. Since cons allocates storage (like new in Java), it must reserve a new location in the store and stick a pair into it. All other changes--in data representation and processing--follow from this insight.

In addition:

1. When an instructor blogs about common problems with homework files, please do pay attention. It is unhelpful to have to correct the same mistake over and over again. Your advisor won't like it either.
2. The other big problem concerned the management of environments, which is still wrong in about a third of the solutions.
3. Finally, I once again urge all of you to pay close attention to logical consistency. Logical consistency is critical to programming and modeling in computer science, no matter which sub-discipline you choose.

Sunday, November 13th, 2011

Handing in your project: Remember your project is due on Wednesday, November 16 (midnight). Please submit it as two files with the same naming conventions as your homework solutions: one file should be the required PDF document and the other one the Redex model.

Preparing your lecture: As with all presentations, you must start from a model of your target audience when you prepare your presentation. You need to figure out what they know, what "culture" you share with them, and what you want them to take away. The key is to develop a path from the former to the latter. This path typically starts with the problem and its motivation and the overall focus is on insights not technicalities. -- I cannot review your presentations before you deliver them, but if you have questions, see me.

Saturday, November 12th, 2011

I returned the graded versions of homework 8. Look for 'mf:' in your file and study my remarks on your code. They mark noteworthy points and subtractions. The average score is 79, with one perfect score.

Here are general points:

1. CEK machine with lists: Since values may contain free variables, your 'closure' representation for pairs must contain an environment for each part. Otherwise you lose variables.
2. The addition of exception handlers to the CEK mechanism exploits the K register. Raising an exception just means chopping off a part of K. If you instead "bubble" raise expressions through syntactic portions of the C register, you are not taking advantage of the essential elements of the machine. See the CC machine on page 136. From there, the standard machine transformations take you to a standard homework solution. The best solution would actually keep a stack of stacks.

In general, when you write down machines or transition systems, you should formulate operations on registers via metafunctions, e.g., extending an environment, looking up a variable in an environment. When you do create a real implementation then, you can keep the machine organization intact but replace the operations with efficient versions.

Tuesday, November 8th, 2011

Some of you noticed that some failures are due to "not in domain" exceptions. I have modified "8provided.rkt" to provide a new construct called not-in-domain. Please see the definition of eval*-s for a sample use.

Saturday, November 5th, 2011

I returned the graded versions of homework 7. Look for 'mf:' in your file and study my remarks on your code. They mark noteworthy points and subtractions. The average score is 81, with one perfect score. The grade distribution is truly bi-modal.

Here are general points:

1. Task 1: When you abstract over two functions, the test is to define new versions of the old functions in terms of the abstraction and to re-run the tests for the original versions. In addition you can test

     (test-equal (sum.v1 l) (sum.v2 l))

   for any list l, etc.
2. Task 2: As much as you may dislike "Algol" syntax by now, when it comes to type signatures for methods and functions, it works just fine:

     (rec t_ran x_fun(t_dom x_para) e)

   e.g.,

     (rec int f(int x) (if0 x 0 (+ 1 (f (- x 1)))))

3. Task 3: Since your task is to implement your specification, do not take a high grade on this task as a good sign. It merely reflects only your approach to programming this task not how appropriate or inappropriate your type checker is.
4. Task 4: When you admit programs of just numeric type, you know that a number can be the only result; the preservation lemma says so. When you admit programs of arbitrary type, you need an explain function.

Wednesday, November 2nd, 2011

Due to popular request, the project is now due November 16, midnight. In addition, I will switch problem sets 8 and 9.

Wednesday, November 2nd, 2011

Please pick up your projects (both partners) between 3:30 and 4:30 today. For some that's just a pick-up, for a few I would like to briefly discuss your goals.

Tuesday, November 1st, 2011

I have made a small change to assignment 7. You are allowed to use "5provided.rkt" as an import.

Some of you have eliminated the silly specification of if0 as an abbreviation and some of you haven't. Here is what I recommend:

  (if0 0 e_then e_else) = e_then 
  (if0 v e_then e_else) = e_else if v != 0

Tuesday, November 1st, 2011

I returned the graded versions of homework 6. Look for 'mf:' in your file and study my remarks on your code. They mark noteworthy points and subtractions. The average score is around 76, a B 82, a B+.

Here are general points:

1. Problem 1 seem to pose two substantial problems. First, several pairs "baked" sum and product into the language. The question asked for ISWIM functions, i.e., functions defined inside the language. Second, several pairs extended the calculus semantics (arbitrary reductions) and did not create a standard reduction semantics. At this point it is impossible to compare the two flavors; they are the same.
2. Problem 2 posed a lot of smaller problems. The key is to recognize that the addition of new features requires the addition of new syntax (new kinds of lambda), new values (both are values), new application syntax, and new contexts.
3. I saw a really nice way of explaining mu-lambda without redoing all of the substitution function:

       (==> ((mu-lambda x e) v_1 ...)
            ((lambda (x) e) (create-list v_1 ...)))
   

4. Function application in ISWIM consists of two expressions. In the book and in lecture, I whimsically picked left-to-right evaluation order. With the addition of multi-argument functions, this choice becomes an even more obvious source of potential problems. The addition of assignment statements or non-local jumps would definitely enable the programmer to write programs that determine the order of evaluation. The question is whether programmers can already do so in the flavor of ISWIM you have engineered. Here are two possible answers:
   1. externally If you changed ISWIM in response to problem 1 so that it maps stuck states to error answers, i.e.,

        (--> (in-hole E (n v)) error)  ;; for n in number

      an external observer can see what is going on assuming you have distinct errors.
   2. internally Even if you changed ISWIM in response to problem 1 so that it maps stuck states to error answers, a program cannot discover the order of evaluation and exploit it for computations. Doing so requires the ability to recover from errors within the program.
   My grading on the answers was somewhat loose. No pair came close to the above analysis.

Tuesday, November 1st, 2011

The project memos are mostly on point. The average grade on this part is 85/100, a low A. While this grade is high, it does not mean the memos are perfect; I do not have the time to give them same treatment I give to the writings of my own PhD students.

Your proposal should have either the format of a review (title details paper) or the format of a plain paper (body refers to paper, cited in bibliography section). -- A proposal consists of three sections. The first section summarizes the background, in this case the chosen paper. The second one explains the goal, i.e., the research question, you wish to tackle. The third and final section lays out a plan of attack; it explains methods, tools, and procedures that you wish to use.

When you write a public piece of technical prose, you need to use a formal language. Avoid contractions, colloquialisms, bad words such as "thing", etc. Also prefer active verbs over non-descriptive verbs (to be, to have, to do) and passive phrases. -- As for questions, formulate them indirectly not as direct questions. -- To discuss a paper, refer to its contents (results, methods, tools) not to its authors. Indeed, avoid mentioning authors other than as part of a citation.

Friday, October 28th, 2011

Here are the new partnerships for the remaining problem sets:

  (define ps7/8/9
    '(("Zahra"     "Aniko")
      ("Matthew"   "Triet")
      ("Justin"    "Jonathan")
      ("Hamidreza" "James")
      ("Yue"       "Scott")
      ("Do Hyong"  "Henry")
      ("Arash"     "Mitesh")
      ("Liang"     "Travis")
      ("Maryam"    "Phil")
      ("Tony"      "Tim")))

You are responsible for contacting your partner this weekend and exchanging vital contact information (primary email, phone, facebook, etc). You must start working with your new partner as of Tuesday.

Wednesday, October 26th, 2011

When you define or extend a programming language, you need to develop two parts: a syntax and a notion of value. The syntax is intended for programmers so that they can write down expressions with the new features. The values are for the programmer and the machine. The former needs it to reason about the meaning of programs, the latter implements it. -- The book and the course covered this idea from week 2 through 5.

Since several solutions for problem set 5 suggest that some of you didn't understand/appreciate this idea, let me sketch the list extension to ISWIM:

  (define-extended-language ISWIM* ISWIM
    (e .... ;; surface syntax 
       (cons e e)
       (cons? e)
       (first e)
       (rest e)
       empty
       (empty? e))
    (v .... ;; evaluation syntax 
       empty
       (cons v v))
    ...)

With this definition, for example, the beta-v law automatically applies to lists. There is no need to special-case lists or other values, which -- as the book briefly explains -- produced all kinds of misunderstandings about PLs in the past.

The above extension is only one possible way to add lists correctly to ISWIM. If you have a correct version and you are happy with it, you are welcome to stick to it.

Saturday, October 22nd, 2011

I have modified problem 1 on problem set 7. The modification asks you to explain the precise meaning of the random testing that redex-check performs and thus clarifies the nature of your task.

Saturday, October 22nd, 2011

I returned the graded versions of homework 5. Look for 'mf:' in your file and study my remarks on your code. They mark noteworthy points and subtractions. The average score rose to 82.

Here are general points:

1. Please check your line width. I took of a point when I found lines over the limit (102).
2. Don't test metafunctions via test-->>. This involves too many moving parts. Unit tests should be simple and easy to read.
3. Your proofs in problem 1 would have benefited from the equations (lemmas) in 5provided.rkt.
4. Problem 2 requires eval to map closed terms to answers. Not one term enforced closedness of the given program. I did not deduct points this time.
5. A number of people had serious problems with problem 3. When you extend a language with a data type, you need to extend the set of operations and the set of values. That is usually enough. In this case, (cons v v) and empty were new values. A typical notion of reduction looks like (first (cons v_1 v_2)) relates to v_1.

Thursday, October 20th, 2011

Question	Answer
Problem 2 requests implementing numeric ISWIM as suggested in the book, which implies the use of integers. But integers aren't closed under exponentation. What should we do?	You are free to use Racket numbers (reals, complexes) and/or get stuck. All I ask for is that your specification is consistent.
Problem 2 asks for a syntactic reduction. Does this mean you want us to use Racket's syntax rules?	No. I am asking for a reduction rule that "translates" if expressions into something sensible.
How should eval*-v in Problem 3 deal with lists that contain lambda expressions?	Turn them into 'closure.

Wednesday, October 19th, 2011

Some of you may be planning on traveling. You may count on 12/9 as the end of the semester.

In addition, I have finalized the schedule as much as possible at this point. Each project pair has a presentation slot now. Each slot is 40 minutes long, with 20 minutes per person. (I will post details on the presentation later.) If any pair wishes to swap slots with another pair, all four partners must agree before you inform me.

Sunday, October 16th, 2011

I sent out graded versions of homework 4. Look for 'mf:' in your file and study my remarks on your code. They mark noteworthy points and subtractions. The average score rose to 87.

Here are a few general points:

1. When you communicate a small model to someone/anyone, running a short (300-400line) file shouldn't take a minute. Four minutes are boderline polite. Twenty and more minutes is rude. I subtracted three points for these cases.
2. If one or two lines are overly widely and difficult to read, I ignored it this time. If you had a bunch of these, I subtracted points.
3. As the book explains, a normal form is a term that does not contain any redexes. A term such as (if0 x (1 + 1) (1 / 0)), however, does contain redexes, and I expect a compiler to reduce them as much as possible. Furthermore, (if0 error x x) propagates error, while (if0 x error 1) does not.
4. Several defined metafunctions instead of LC encodings for stacks. If you do not understand the difference, ask in class.
5. Almost all of you defined a single-path reduction to reduce the running time. I was really hoping for some more algorithmic thinking here. -- Then again, this course is not about algorithms, and the tricks you would learn, aren't essential. I therefore did not deduct points. -- In the real world, you would have to justify this point.

Tuesday, October 11th, 2011

Some clarifications on problem set 4:

Question	Answer
How should we represent numbers in problem 2? Should we leave them in an encoded form since we can't escape to racket?	You may escape to Racket for small things---such as numbers and perhaps adding numbers---but that's it. Nothing else is needed.
What does "another test must demonstrate that you can predict the outcome only up to α equivalence" mean?	If you experiment with subst-n, you will see that it renames bound variables as needed -- just as illustrated in class. Hence, when you formulate a reduction test you may not get the exact term but a term that is a different representative of the same α equivalence class. Fortunately Redex allows you to state "up to some equivalence" in reduction tests. Do so for at least one of them and include the same test without this option; the former will succeed, and the latter will fail.

Some clarification on the next step for your project: As you have seen over the course of the past few weeks, scientists ask questions and try to answer them. Many find such questions while reading papers. When they ask question, they usually do not start with questions that go beyond the content of a paper but questions about the content itself. It is these kinds of questions that I want you to focus on. You are not supposed to conduct research in programming languages; you are merely figuring out what the authors could have meant with statements and claims in their papers. The one constraint is that you pick questions that are amenable to the kind of analysis we study in class and you practice in homework assignments. (Naturally once researchers can answer all questions about an interesting paper, they move on to novel questions raised by the paper.)

Monday, October 10th, 2011

I sent out graded versions of homework 3. Look for 'mf:' in your file and study my remarks on your code. They mark noteworthy points and subtractions. The average score was again 83, with one pair getting a perfect score.

Here are three general points:

1. Include your email addresses on one separate line in the header.
2. Keep all the code/text for one problem contiguous.
3. Do not use comment boxes or other graphical syntax.

Since I have mentioned the first point here and in class, I subtracted one beauty point this time for failure to live up to it.

Problem 2a caused some confusion. It demands that nested expressions are reduced to numbers in a certain order, but it does not specify in which order the actual additions happen. As a consequence, the model could reduce expressions in left-to-right order and perform right-to-left addition after the expressions are reduced to numbers. Here is an example:

      (+ (* 2 2) (* 3 3) (* 4 4))
  --> (+ 4 (* 3 3) (* 4 4))
  --> (+ 4 9 (* 4 4))
  --> (+ 4 9 16)
  --> (+ 4 25)
  --> 29

As a matter of fact, for part c, it is possible to argue that there is no distinction. If your model reduces expressions left-to-right and right-to-left but sums up/multiplies all fully numeric operations in a fixed order, you can't see a difference.

More generally, just because a problem statement (paper) says, conjecture X should hold and readers should figure out how to prove it, does not mean that X is true.

Friday, October 7th, 2011

You should have received email introducing you electronically to your partner. In case something goes wrong, here are the partnerships:

  (define ps4/5/6
    '(("Zahra"     "Justin")
      ("Matthew"   "Aniko")
      ("Yue"       "Mitesh")
      ("Hamidreza" "Maryam")
      ("James"     "Jonathan")
      ("Do Hyong"  "Travis")
      ("Arash"     "Scott")
      ("Liang"     "Tim")
      ("Triet"     "Henry")
      ("Phil"      "Tony")))

You are responsible for contacting your partner this weekend and exchanging vital contact information (primary email, phone, facebook, etc).

Sunday, October 2nd, 2011

I sent out graded versions of homework 2. Look for 'mf' in your file and study my remarks on your code. They also mark my subtractions.

In general, pay attention to the following:

1. Include your email addresses on one-line in the header.
2. Do not include any templates.
3. Stick to a width of at most 102 chars.
4. Label problems and subproblems in a distinctive manner. Comments with 99 dashes or large letters work well.
5. Comment out traces and redex-check examples with #; comments.
6. Keep (some) tests with functions to illustrate functionality.
7. Present functions top-down.

This time I allocate 2 points to style and next time it will be 4.

Here is a sample solution to problem 4, which many of you got wrong.

  #lang racket
  (require redex)

  (define-extended-language vStacks Stacks
    (vS mtS
	(push vS n)))

  (define-metafunction vStacks 
    evalS : S -> vS 
    [(evalS mtS) mtS]
    [(evalS (push S e)) (push (evalS S) (e-eval e))]
    [(evalS (pop S))    (popF (evalS S))])

  (define-metafunction vStacks 
    e-eval : e -> n
    [(e-eval n) n]
    [(e-eval (add1 e)) ,(+ 1 (term (e-eval e)))]
    [(e-eval (top S))   (topF (evalS S))]
    [(e-eval (depth S)) (how-deep (evalS S))])

  (define-metafunction vStacks 
    how-deep : vS -> n
    [(how-deep mtS) 0]
    [(how-deep (push S n)) ,(+ 1 (term (how-deep S)))])

  (define-metafunction vStacks 
    topF : vS -> vS
    [(topF (push S n)) n])

  (define-metafunction vStacks 
    popF : vS -> vS
    [(popF (push S n)) S])

  (test-equal (term (evalS ,ex1)) (term (push mtS 1)))
  ... more tests ...

The key is that two mutually inductive data definitions are processed by two mutually recursive functions with recursions and cross-recursions as in the data definitions.

Thursday, September 29th, 2011

Please submit your homework electronically as a single file, using the same naming protocol as last time.

You do not need to submit the Book exercises, labeled "finger exercises" on homework set 2.

Monday, September 26th, 2011

Please visit the new project page and carefully read it over. Start checking out the papers to get a sense of what you might find an interesting project. The first milestone is due in two weeks from now.

Sunday, September 25th, 2011

I sent out graded versions of homework 1. Look for 'mf' in your file and study my remarks on your code. They also mark my subtractions. In general, please pay attention to the following:

1. A header must include your email addresses.
2. Use

     #lang racket 
     (require redex)
   

to start your file.
3. There is no need to spell out the steps of the design recipe. They exist to help you find solutions. If you're stuck, be sure to use them. If you ever teach programming, be sure to remember them. See sample solution below.

   You need to practice formulating concise (one line, 100 chars) purpose statements.

   You also need to practice the concise formulation of accumulator statements.

4. Label problems and subproblems in a distinctive manner.
5. Mimic the Redex style from the book to make it look pretty. Many of you had extremely ugly style. Here are some hints:
   • Don't insert extraneous spaces.
   • DrRacket has a natural autoindent functionality. When you hit return, it places your cursor at a certain spot for a reason. If you think it's wrong, you program is ugly and/or wrong. Use the Racket | Indent All menu to format your file.
   • Limit yourself to 102 character-wide lines.
   • Put all closing parentheses on one line. No extraneous white space.

Here is a sample solution to problem 5:

  #lang racket
  (require redex)

  (define-language Problem5
    (XY x
	(function x XY)
	(XY XY))
    (AB natural
	x
	(function x AB)
	(AB AB))
    (x variable)
    (n natural)
    ;; auxiliary result
    (LL (x ...)))

  (define ex1 (term (function x ((function y (function x (x y))) x))))
  (define re1 (term (function x ((function y (function x (0 1))) 0))))

  (define ex2 (term (x ((function x y) x))))
  (define re2 ex2)

  (define ex3 (term ((function x (x (function y (function z x)))) x)))
  (define re3 (term ((function x (0 (function y (function z 2)))) x)))

  ;; replace variables by static distance 
  (define-metafunction Problem5 
    sd : XY -> AB
    [(sd XY_0) (aux XY_0 ())])

  ;; accumulator: l is the variables encontered between XY_0 and XY  
  (define-metafunction Problem5 
    aux : XY LL -> AB
    [(aux x LL_0) 
     (distance x LL_0 0)]
    [(aux (function x XY) LL)
     (function x (aux XY ,(cons (term x) (term LL))))]
    [(aux (XY_f XY_a) LL)
     ((aux XY_f LL) (aux XY_a LL))])

  ;; determine the distance of the x to its first occurrence in LL plus n
  ;; accumulator: the number of variables between LL_0 and LL 
  (define-metafunction Problem5 
    ; distance : x LL n -> n or x
    [(distance x (x x_1 ...) n) 
     n]
    [(distance x (x_0 x_1 ...) n) 
     (distance x (x_1 ...) ,(+ (term n) 1))]
    [(distance x () n)
     x])

  (test-equal (term (sd ,ex1)) re1)
  (test-equal (term (sd ,ex2)) re2)
  (test-equal (term (sd ,ex3)) re3)
  (test-equal (term (sd ,ex4)) re4)

Here is an alternative formulation of distance that relies on the full power of Redex pattern matching:

  (define-metafunction Problem5
    ; distance : x LL -> n or x
    [(distance.v2 x (x_1 ... x x_2 ...))
     ,(length (term (x_1 ...)))
     (side-condition (not (member (term x) (term (x_1 ...)))))]
    [(distance.v2 x (x_1 ...)) x])

  (test-equal (term (distance.v2 x (y z x w x r s))) 2)
  (test-equal (term (distance.v2 x (y z b w a r s))) (term x))

I will introduce some of this power in lecture.

Friday, September 23rd, 2011

The creators of Simula 67 were Messrs. Dahl and Nygaard, two Norwegian computer scientists. The company that runs ECCOP has named two awards after the two, and they are considered the two European pioneers of OO programming.

Thursday, September 22nd, 2011

Note: I have slightly revised the syllabus.

Wednesday, September 21st, 2011

The third part of the lecture notes is released.

Homework 2 is in near-final shape.

Send me your solutions for homework 1 as a single Racket (.rkt) file attached to an email that CCs your partner. The name of your file should consist of your two first names separated by a dash:

       firstname1-firstname2.rkt

For those of you who work alone, use

       firstname.rkt

The file must have a proper header (homework, names, emails) and must be properly organized. Check out "large letters" in the Insert menu.

Sunday, September 18th, 2011

Notes for the second lecture on the design of Redex metafunctions are now available.

Wednesday, September 14th, 2011

Please note two corrections to Problem 1, marked in red. (HTML isn't perfect and neither am I.)

Tuesday, September 13th, 2011

Note the new Lectures tab on the left. These notes are not a substitute for your own notes but a supplement. Also, I will provide notes only for the Redex programming part of the course. Otherwise the text book is your best resource.

Wednesday, August 31st, 2011

Welcome to the PhD-level course on programming languages.

Our organizational meeting will take place on Friday 9/9. Enrollment permitting I will move the course to WVH to make it convenient for all of us. Stay tuned to announcements.