6 Blog
Tue Dec 9 15:11:48 EST 2014
The final exam, PS5, has been posted. It consists of a single problem and is due by 12/20.
Tue Dec 2 11:36:52 EST 2014
The project presentation schedule has been set. On 12/9, Ugur Koc and Yi Qian will present and Josh Reese will present. On 12/11, Nicholas Kofinas will present, Nick Labich will present, and Xiong Fan, Zikai Wen, and Andrew Pachulski will present. (See Syllabus.)
Wed Nov 12 11:41:49 EST 2014
Remote office hours today: I will be holding my office hours remotely today. If you’d like to meet, my username on Skype and Google Hangouts is david.a.vanhorn.
Thu Nov 6 12:27:40 EST 2014
PS4 has been posted, due Nov 18.
Tue Nov 4 17:17:04 EST 2014
Code from today.
Tue Nov 4 15:01:36 EST 2014
Code from last Tuesday is here, which introduces imperative features to our abstract machine. Code from last Thursday is here, which pares down the language to the core of functions; the exercises on programming within this core are here.
Thu Oct 23 12:50:49 EDT 2014
Lecture is cancelled today; please use this time to make progress on your projects.
Tue Oct 14 17:04:52 EDT 2014
Code from today.
Sat Oct 11 10:53:24 EDT 2014
Here is the interpreter that was defunctionalized to obtain a closure datatype and here is the interpreter that makes context explicit via CPS.
Wed Oct 8 15:26:25 EDT 2014
I’ve added another Potential projects description on test equivalence. I may add another couple of project descriptions shortly.
Wed Oct 8 10:27:07 EDT 201
Remote office hours today: I need to work from home today so I will hold my office hours remotely on Skype and Google Hangouts; my username on both is david.a.vanhorn.
Tue Oct 7 19:53:55 EDT 2014
I’ve posted the descriptions of the rest of the research project deliverables: RP2, RP3, and RP4, which are also on the Syllabus.
Tue Oct 7 18:36:01 EDT 2014
Tue Oct 7 15:52:59 EDT 2014
The Potential projects descriptions have been revised to include the project proposals we heard today.
Thu Oct 2 17:00:33 EDT 2014
Today’s code.
Thu Sep 25 17:07:13 EDT 2014
Type checking code from today (includes an evaluator that handles all errors).
Tue Sep 23 18:18:56 EDT 2014
PS3 is out.
Tue Sep 23 17:14:04 EDT 2014
My stupid error today: I realized right after walking out of class what the problem was. I wanted to make a reduction relation that reduced a natural number to all numbers less than or equal to it.
We first wrote a relation <= with mode (<= I O), but that mode says we’re given a number and it produces all numbers for which it is less than or equal. That’s an infinite set.
We actually fixed that by changing the mode to (<= O I), which given a number produces all numbers less than or equal to it. That’s a finite set.
(--> N_1 N_2 (judgment-holds (<= N_1 N_2))) |
That’s saying a number reduces to anything greater than it, which is not what we were after.
(--> N_1 N_2 (judgment-holds (<= N_2 N_1))) |
which works just fine.
sigh.
Tue Sep 23 13:36:35 EDT 2014
Here are the partner assignments for problem set 3, which will be posted tonight.
pair10: labichn (Nicholas Labich)
pair18: leofanxiong (Xiong Fan), aidmony (Yi Qian)
pair19: jreeseue (Josh Reese), ugur-koc (Ugur Koc)
pair20: andrewpachulski (Andrew Pachulski), alexwzk (Zikai Wen)
pair21: eldr4d (Nikolas Kofinas), HosseinT (Hossein Torkashvand)
pair22: reflect9 (Tak Yeon Lee), ENOTTY (Joman Chu)
Thu Sep 18 18:59:50 EDT 2014
Today’s code.
Tue Sep 16 17:43:00 EDT 2014
Shortened office hours tomorrow: due to a department meeting at 2PM I will only be available from 1:30 to 2:00 tomorrow during office hours. However, you can always email me to schedule an appointment.
Tue Sep 16 17:36:06 EDT 2014
Here is the code from today.
Tue Sep 16 15:17:12 EDT 2014
I’ve pushed the deadline for PS2 back to Tuesday, 9/23. I’ve seen very few people (1 to be precise) push any work on their repository. You will not be able to complete this assignment the day before its due and I will have no sympathy for PhD students who fail to start early. There are still two people who have not accepted the github request to join the cmsc631 organization!
Mon Sep 15 10:21:54 EDT 2014
Here is the code from Thursday.
OCaml:
type bt = |
| Leaf |
| Node of int * bt * bt |
|
let rec sum (bt : bt) : int = |
match bt with |
| Leaf -> 0 |
| Node (i, l, r) -> i + sum l + sum r |
|
|
sum Leaf;; |
sum (Node (4, Node (2, Leaf, Leaf), Node (7, Leaf, Leaf)));; |
|
(* Now abstracting over the type of elements *) |
|
type 'a bt = |
| Leaf |
| Node of 'a * 'a bt * 'a bt |
|
let rec sum (bt : int bt) : int = |
match bt with |
| Leaf -> 0 |
| Node (i, l, r) -> i + sum l + sum r |
|
|
sum Leaf;; |
sum (Node (4, Node (2, Leaf, Leaf), Node (7, Leaf, Leaf)));; |
|
let rec inorder (bt : 'a bt) : 'a list = |
match bt with |
| Leaf -> [] |
| Node (x, l, r) -> inorder l @ [x] @ inorder r |
|
inorder Leaf;; |
inorder (Node (4, Node (2, Leaf, Leaf), Node (7, Leaf, Leaf)));; |
|
(* Evaluator for A lang *) |
|
type expr = |
| Int of int |
| Pred of expr |
| Succ of expr |
| Mult of expr * expr |
| Plus of expr * expr |
|
let rec eval (e : expr) : int = |
match e with |
Int i -> i |
| Pred e -> eval e - 1 |
| Succ e -> eval e + 1 |
| Plus (e1, e2) -> eval e1 + eval e2 |
| Mult (e1, e2) -> eval e1 * eval e2 |
|
(* Works fine because eval relation but also a function. Doesn't work as well |
when it is relation but not a function. *) |
|
type expr = |
| Int of int |
| Pred of expr |
| Succ of expr |
| Mult of expr * expr |
| Plus of expr * expr |
| Amb of expr * expr (* Ambiguous choice *) |
|
let rec eval (e : expr) : int = |
match e with |
| Int i -> i |
| Pred e -> eval e - 1 |
| Succ e -> eval e + 1 |
| Plus (e1, e2) -> eval e1 + eval e2 |
| Mult (e1, e2) -> eval e1 * eval e2 |
| Amb (e1, e2) -> eval e1 |
| Amb (e1, e2) -> eval e2 (* unreachable code *) |
|
(* We didn't see the rest in class, but here's how we could model |
an evaluation relation... *) |
|
(* Could model relation as a function returning a set. *) |
(* For simplicty, let's model a set as a list. *) |
|
(* We need a helper function to construct the |
Cartesian product of two lists *) |
|
let cartesian (l : 'a list) (l' : 'b list) : ('a * 'b) list = |
List.concat (List.map (fun e -> List.map (fun e' -> (e,e')) l') l) |
|
let rec eval (e : expr) : int list = |
match e with |
| Int i -> [i] |
| Pred e -> List.map (fun v -> v - 1) (eval e) |
| Succ e -> List.map (fun v -> v + 1) (eval e) |
| Plus (e1, e2) -> |
List.map (fun (v1, v2) -> v1 + v2) (cartesian (eval e1) (eval e2)) |
| Mult (e1, e2) -> |
List.map (fun (v1, v2) -> v1 * v2) (cartesian (eval e1) (eval e2)) |
| Amb (e1, e2) -> |
eval e1 @ eval e2 |
|
eval (Amb (Int 2, Int 3));; |
eval (Mult (Int 4, (Amb (Int 2, Int 3))));; |
Racket/Redex:
#lang racket |
;; bt = |
;; | (leaf) |
;; | (node int bt bt) |
|
(struct leaf ()) |
(struct node (i l r)) |
|
(define (sum bt) |
(match bt |
[(leaf) 0] |
[(node i l r) |
(sum i (sum l) (sum r))])) |
|
(define (inorder bt) |
(match bt |
[(leaf) empty] |
[(node i l r) |
(append (inorder l) |
(list i) |
(inorder r))])) |
|
|
(require redex) |
|
(define-language A |
(e ::= |
integer |
(Plus e e) |
(Mult e e) |
(Succ e) |
(Pred e) |
(Amb e e)) |
(i ::= integer) |
(E ::= hole |
(Plus E e) |
(Plus i E) |
(Mult E e) |
(Mult i E) |
(Succ E) |
(Pred E))) |
|
(define-judgment-form A |
#:mode (⇓ I O) |
#:contract (⇓ e i) |
[-------- |
(⇓ i i)] |
|
[(⇓ e i) |
-------------- |
(⇓ (Succ e) (unquote (+ (term i) 1)))] |
|
[(⇓ e i) |
-------------- |
(⇓ (Pred e) (unquote (- (term i) 1)))] |
|
[(⇓ e_1 i_1) (⇓ e_2 i_2) |
----------------------- |
(⇓ (Plus e_1 e_2) |
(unquote (+ (term i_1) (term i_2))))] |
|
[(⇓ e_1 i_1) (⇓ e_2 i_2) |
----------------------- |
(⇓ (Mult e_1 e_2) |
(unquote (* (term i_1) (term i_2))))] |
|
[(⇓ e_1 i_1) |
----------------------- |
(⇓ (Amb e_1 e_2) i_1)] |
|
[(⇓ e_2 i_2) |
----------------------- |
(⇓ (Amb e_1 e_2) i_2)]) |
|
(define a |
(reduction-relation |
A #:domain e |
(--> (Plus i_1 i_2) ,(+ (term i_1) (term i_2))) |
(--> (Mult i_1 i_2) ,(* (term i_1) (term i_2))) |
(--> (Pred i_1) ,(- (term i_1) 1)) |
(--> (Succ i_1) ,(+ (term i_1) 1)) |
(--> (Amb e_1 e_2) e_1) |
(--> (Amb e_1 e_2) e_2))) |
|
(define -->_a |
(compatible-closure a A e)) |
|
(define -std->_a |
(context-closure a A E)) |
|
|
;; Some examples: |
#| |
(judgment-holds |
(⇓ (Amb (Succ 5) (Pred 4)) 6)) |
|
(judgment-holds |
(⇓ (Amb (Succ 5) (Pred 4)) i)) |
|
(apply-reduction-relation -->_a |
(Mult (Succ 4) (Pred 4))) |
(apply-reduction-relation* -->_a |
(Mult (Succ 4) (Pred 4))) |
(traces -->_a |
(Mult (Succ 4) (Pred 4))) |
|
(traces -std->_a |
(Mult (Succ 4) (Pred 4))) |
|# |
Thu Sep 11 09:25:26 EDT 2014
I’ve updated the partner assignments (by editing the blog post below). I’ve added real names for convenience. Everyone’s team should have writeable private repos. Please veryify before PS2’s due date and let me know if there’s a problem.
Tue Sep 9 14:35:05 EDT 2014
PS2 will require you to do some programming in OCaml. CMSC 330 has a good slide deck on programming in OCaml.
There’s an Emacs mode I use called Tuareg.
Tue Sep 9 10:15:27 EDT 2014
I received almost all of the PS1 submissions. There was one student who didn’t submit anything and a couple students who failed to provide some of the requested deliverables. If you are one of these students, you should have received email.
I’ve created the initial partner assignments and repositories on github:
pair10: labichn (Nicholas Labich)
pair11: leofanxiong (Xiong Fan), ugur-koc (Ugur Koc)
pair12: jreeseue (Josh Reese), alexwzk (Zikai Wen)
pair13: bjkwon90 (Bum Jun Kwon), andrewpachulski (Andrew Pachulski)
pair14: aidmony (Yi Qian), ERJIALI (Erjia Li)
pair15: eldr4d (Nikolas Kofinas), ENOTTY (Joman Chu)
pair16: reflect9 (Tak Yeon Lee), HosseinT (Hossein Torkashvand)
For each pair, a private repository has been created for you. Use this repository for your work. If some other system is more useful for collaborating, feel free to use it, but you must commit your work to the repository by midnight of the due date for it to be graded.
The results of the language beauty contest are as follows:
C: 3
Python: 3
Ruby: 2
Agda: 1
C++: 1
Java: 1
JavaScript: 1
Perl: 1
Racket: 1
I will commit marked up copies of your essay to your pair’s repository by Thursday, September 11, giving you a week to make edits for PS2.
Wed Aug 27 19:30:43 EDT 2014
Welcome to CMSC 631, Program Analysis and Understanding.
I wanted to make you aware a few things before class starts:
The course web page is located at http://ter.ps/cmsc631f14. Please read it this week.
There is no lecture on 9/2 or 9/4—
I have to travel for a conference. However, there is an assignment due on 9/4.
Looking forward to seeing you soon!
Mon Aug 25 15:03:22 EDT 2014
Welcome to CMSC631! This “blog” is where course announcements will be made; be sure to check it regularly. – David