BABYL OPTIONS: Version: 5 Labels: Note: This is the header of an rmail file. Note: If you are seeing it in rmail, Note: it means the file has no messages in it.  1,, Summary-line: 17-Sep to: 6044-forum #QUIZ dates Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA28671; Tue, 17 Sep 96 20:34:06 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA10689; Tue, 17 Sep 96 20:34:15 EDT Date: Tue, 17 Sep 96 20:34:15 EDT Message-Id: <199609180034.AA10689@stork.lcs.mit.edu> To: 6044-forum Subject: QUIZ dates *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Tue, 17 Sep 96 20:34:15 EDT To: 6044-forum Subject: QUIZ dates I propose we have our two in-class quizzes on (1) Wednesday Oct 2, 1996 (2) Wednesday Nov 6, 1996 Let me know if you have any problems with these dates. Regards, A.  1,, Summary-line: 17-Sep to: 6044-forum #PS2 is on the web Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA00632; Tue, 17 Sep 96 23:21:26 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA10809; Tue, 17 Sep 96 23:21:35 EDT Date: Tue, 17 Sep 96 23:21:35 EDT Message-Id: <199609180321.AA10809@stork.lcs.mit.edu> To: 6044-forum Subject: PS2 is on the web *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Tue, 17 Sep 96 23:21:35 EDT To: 6044-forum Subject: PS2 is on the web PS2 will be due Sept 25. I will bring hardcopies to class tomorrow. Regards, A.  1,, Summary-line: 21-Sep to: 6044-forum #PS2 extension Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA13835; Sat, 21 Sep 96 13:27:34 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA12151; Sat, 21 Sep 96 13:27:47 EDT Date: Sat, 21 Sep 96 13:27:47 EDT Message-Id: <199609211727.AA12151@stork.lcs.mit.edu> To: 6044-forum Subject: PS2 extension Reply-To: 6044-lecturer@theory.lcs.mit.edu *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Sat, 21 Sep 96 13:27:47 EDT To: 6044-forum Subject: PS2 extension Reply-To: 6044-lecturer@theory.lcs.mit.edu PS2 will be due FRIDAY 11/27 (instead of Wed 11/25). Regards, A.  1,, Summary-line: 23-Sep to: 6044-forum #[meyer@theory.lcs.mit.edu: PS2 extension] Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA09524; Mon, 23 Sep 96 12:56:33 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA12909; Mon, 23 Sep 96 12:56:47 EDT Date: Mon, 23 Sep 96 12:56:47 EDT Message-Id: <199609231656.AA12909@stork.lcs.mit.edu> To: 6044-forum Subject: [meyer@theory.lcs.mit.edu: PS2 extension] *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Mon, 23 Sep 96 12:56:47 EDT To: 6044-forum Subject: [meyer@theory.lcs.mit.edu: PS2 extension] Correction: make that SEPTEMBER 27th (9/27). From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Sat, 21 Sep 96 13:27:47 EDT To: 6044-forum Subject: PS2 extension Reply-To: 6044-lecturer@theory.lcs.mit.edu PS2 will be due FRIDAY 11/27 (instead of Wed 11/25). Regards, A.  1,, Summary-line: 23-Sep to: 6044-forum #Quiz dates Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA09630; Mon, 23 Sep 96 13:03:31 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA12912; Mon, 23 Sep 96 13:03:45 EDT Date: Mon, 23 Sep 96 13:03:45 EDT Message-Id: <199609231703.AA12912@stork.lcs.mit.edu> To: 6044-forum Subject: Quiz dates *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Mon, 23 Sep 96 13:03:45 EDT To: 6044-forum Subject: Quiz dates The confirmed Quiz dates are: (1) Friday Oct 4, 1996 (2) Wednesday Nov 6, 1996 These are FIFTY MINUTE, IN CLASS, CLOSED BOOK, quizzes. Re "closed book": you will be expected to be able to state key definitions and results from lectures and problem sets. But this does NOT mean you have to memorize such things as long tables of axioms or inference rules. Any such items needed on a Quiz will be supplied in Quiz appendices. Regards, A.  1,, Summary-line: 26-Sep djib@hematite.mit.edu #syntactic sugar Return-Path: Received: from HEMATITE.MIT.EDU by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA18736; Thu, 26 Sep 96 10:33:28 EDT Received: (from djib@localhost) by hematite.mit.edu (8.7.4/8.7.3) id KAA23371; Thu, 26 Sep 1996 10:33:29 -0400 Date: Thu, 26 Sep 1996 10:33:29 -0400 (EDT) From: Debajit Ghosh To: 6044-forum@theory.lcs.mit.edu Subject: syntactic sugar Message-Id: X-Url: http://www.mit.edu:8001/people/djib/home.html Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII *** EOOH *** Date: Thu, 26 Sep 1996 10:33:29 -0400 (EDT) From: Debajit Ghosh To: 6044-forum@theory.lcs.mit.edu Subject: syntactic sugar X-Url: http://www.mit.edu:8001/people/djib/home.html Professor Meyer told me to pass this along... For problem two, there is an initial mysterious step in which (define (foo n) .. ) gets unsugared into the appropriate lambda expression. This is just smeval being clever and is not part of the substitution model -- no substitution rules capture this step, so we can safely ignore it and start reducing/labelling during the following step.  1,, Summary-line: 26-Sep to: chenxh@MIT.EDU #Running Scheme Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA22130; Thu, 26 Sep 96 12:48:26 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA14676; Thu, 26 Sep 96 12:48:44 EDT Date: Thu, 26 Sep 96 12:48:44 EDT Message-Id: <199609261648.AA14676@stork.lcs.mit.edu> To: chenxh@MIT.EDU In-Reply-To: chenxh@MIT.EDU's message of Thu, 26 Sep 1996 12:36:52 EDT <9609261636.AA26676@m24-sun4.MIT.EDU> Subject: Running Scheme Cc: 6044-forum *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Thu, 26 Sep 96 12:48:44 EDT To: chenxh@MIT.EDU In-Reply-To: chenxh@MIT.EDU's message of Thu, 26 Sep 1996 12:36:52 EDT <9609261636.AA26676@m24-sun4.MIT.EDU> Subject: Running Scheme Cc: 6044-forum To run the submodel, you have to load the submodel code into Scheme. (See the README file in the submodel directory.) Namely, you must copy submodel the files into your own directory, start Scheme, and then evaluate (load "load-submodel.scm") After that smeval will be defined and work as claimed. Regards, A.  1,, Summary-line: 26-Sep to: 6044-forum #PS3, handouts Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA02859; Thu, 26 Sep 96 21:46:04 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA15226; Thu, 26 Sep 96 21:46:23 EDT Date: Thu, 26 Sep 96 21:46:23 EDT Message-Id: <199609270146.AA15226@stork.lcs.mit.edu> To: 6044-forum Subject: PS3, handouts *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Thu, 26 Sep 96 21:46:23 EDT To: 6044-forum Subject: PS3, handouts Problem Set 3 (Handout 7) is available on the course WWW page, as is a somewhat revised version of Handout 2, the Term Rewriting Model for Scheme. Handout 6 is handwritten solutions for Prob Set 1. Hard copies of all these will be available in class tomorrow. Regards, A.  1,, Summary-line: 27-Sep sparrow@MIT.EDU #equality of bodies Return-Path: Received: from MIT.EDU (PACIFIC-CARRIER-ANNEX.MIT.EDU) by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA05137; Fri, 27 Sep 96 01:06:33 EDT Received: from PRIMAVERA.MIT.EDU by MIT.EDU with SMTP id AA16363; Fri, 27 Sep 96 01:06:33 EDT From: sparrow@MIT.EDU Received: by primavera.MIT.EDU (5.57/4.7) id AA01962; Fri, 27 Sep 96 01:06:31 -0400 Message-Id: <9609270506.AA01962@primavera.MIT.EDU> To: 6044-forum@MIT.EDU Subject: equality of bodies Date: Fri, 27 Sep 1996 01:06:28 EDT *** EOOH *** From: sparrow@MIT.EDU To: 6044-forum@MIT.EDU Subject: equality of bodies Date: Fri, 27 Sep 1996 01:06:28 EDT Dear Professor Meyer, or anyone else in class, In Problem 4a) one of the conditions says that "M2 = M3". What does equality between bodies mean? Are two bodies equal if they have the same defines and expression but one has extra unnecessay defines left over (garbage) and the other does not? If M starts with garbage and A produces more garbage, then M1 has a pile of garbage in it. M3 will either have no garbage (if G is applied) or that same pile (if G is not applied). However, M2 has no garbage in it at all, by definition, thus applying A to M2 will produce a smaller amount of garbage than the M3 which is M1 without collection. So the second have of the either can't be true. M2 is M1 without the original garbage, but has not had A applied to it. Thus it cannot be equal to M3 which came from M1, except in the case where A=garbage collection, which is hardly general. So the first part of the either can't be true either. SO there is no M3 which meets the condidtions. This can't be correct thinking. My best guess is that there is something in the definition of = that I am missing. I hope that someone out there might understand what I am getting at and can tell me where I am going wrong. THanks, Gillian Bidgood sparrow@mit  1,, Summary-line: 30-Sep to: 6044-forum #Quiz 1 on MONDAY, OCT. 7 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA01044; Mon, 30 Sep 96 11:52:34 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA16546; Mon, 30 Sep 96 11:52:57 EDT Date: Mon, 30 Sep 96 11:52:57 EDT Message-Id: <199609301552.AA16546@stork.lcs.mit.edu> To: 6044-forum Subject: Quiz 1 on MONDAY, OCT. 7 *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Mon, 30 Sep 96 11:52:57 EDT To: 6044-forum Subject: Quiz 1 on MONDAY, OCT. 7 Quiz 1 has been rescheduled to MONDAY, OCTOBER 7 It is (still) a fifty minute, in class, closed book quiz. Regards, A.  1,, Summary-line: 30-Sep to: 6044-forum #[meyer: 6.044 Questions] Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA01152; Mon, 30 Sep 96 11:56:43 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA16549; Mon, 30 Sep 96 11:57:06 EDT Date: Mon, 30 Sep 96 11:57:06 EDT Message-Id: <199609301557.AA16549@stork.lcs.mit.edu> To: 6044-forum Subject: [meyer: 6.044 Questions] Reply-To: 6044-lecturer@theory.lcs.mit.edu *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Mon, 30 Sep 96 11:57:06 EDT To: 6044-forum Subject: [meyer: 6.044 Questions] Reply-To: 6044-lecturer@theory.lcs.mit.edu Date: Mon, 23 Sep 96 15:27:37 EST From: meyer To: In-reply-to: message of Mon, 23 Sep 1996 14:32:52 EDT Subject: 6.044 Questions 1) What's the URL of the 6.044 homepage? >From H01-course-info: ftp://theory.lcs.mit.edu/pub/classes/6.044/homepage.html 2) However, if I can show that [x := f] is a valuation... Sounds like you may not be clear about the following: (1) [x := f] is a kind of SUBSTITUTION, viz, a mapping from variables to EXPRESSIONS. We can APPLY a substitution to an expression to obtain a new expression. (2) A VALUATION is a mapping from variables to VALUES--in this case INTEGERS. We can EVALUATE an expression at a valuation to obtain an integer. (3) We also use similar notation [ . \leftarrow . ] to modify functions. We can PATCH a function f at element a with element b to obtain a new function indicated as f[a <-- b]. 3) Garbage Collecting: Am I correct in that applying G mutiple times without any other operation in between is useless, because applying G will collect all the garbage the first time through? OK to assume this, though as defined in the notes, GC does not have to be exhaustive, that is, it could involve erasing just a part of the garbage. Regards, A.  1,, Summary-line: 30-Sep to: 6044-forum #[meyer: equality of bodies] Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA01196; Mon, 30 Sep 96 11:59:17 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA16555; Mon, 30 Sep 96 11:59:40 EDT Date: Mon, 30 Sep 96 11:59:40 EDT Message-Id: <199609301559.AA16555@stork.lcs.mit.edu> To: 6044-forum Subject: [meyer: equality of bodies] Reply-To: 6044-lecturer@theory.lcs.mit.edu *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Mon, 30 Sep 96 11:59:40 EDT To: 6044-forum Subject: [meyer: equality of bodies] Reply-To: 6044-lecturer@theory.lcs.mit.edu Here's a reply I should have cc'd to the forum. Regards, A. ------------- Date: Fri, 27 Sep 96 01:40:53 EST From: meyer To: sparrow@MIT.EDU In-reply-to: sparrow@MIT.EDU's message of Fri, 27 Sep 1996 01:06:28 EDT <9609270506.AA01962@primavera.MIT.EDU> Subject: equality of bodies In Problem 4a) one of the conditions says that "M2 = M3". What does equality between bodies mean? Here "=" means syntactic identity: M2 and M3 have exactly the same characters in exactly the same order. Are two bodies equal if they have the same defines and expression but one has extra unnecessay defines left over (garbage) and the other does not? NO If M starts with garbage and A produces more garbage, then M1 has a pile of garbage in it. M3 will either have no garbage (if G is applied) or that same pile (if G is not applied). However, M2 has no garbage in it at all, by definition, thus applying A to M2 will produce a smaller amount of garbage than the M3 which is M1 without collection. So the second have of the either can't be true. I think you're overlooking the fact that there may be garbage in many parts of a body, so even if garbage collection is applied to one part, there may be garbage left elsewhere, eg, the body (define a (lambda (y) (define z 0) 3)) (define b 7) (a 9) Here, b is garbage in the whole body above, but the (define z 0) is also garbage in the body of the lambda expression. So the body above can be rewritten by G into 2 different bodies: (define a (lambda (y) (define z 0) 3)) (a 9) or (define a (lambda (y) 3)) (define b 7) (a 9) Hope that helps. Regards, A. From rmg@MIT.EDU Mon Sep 30 23:46:21 1996 Return-Path: Received: from MIT.EDU (PACIFIC-CARRIER-ANNEX.MIT.EDU) by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA14091; Mon, 30 Sep 96 23:46:21 EDT Received: from MIT.MIT.EDU by MIT.EDU with SMTP id AA00605; Mon, 30 Sep 96 23:46:22 EDT Received: from SMALL-HALF.MIT.EDU by MIT.MIT.EDU (5.61/4.7) id AA14571; Mon, 30 Sep 96 23:46:21 EDT Message-Id: <9610010346.AA14571@MIT.MIT.EDU> To: 6044-forum@theory.lcs.mit.edu Subject: hmm... Date: Mon, 30 Sep 96 23:46:09 From: rmg@MIT.EDU (Robby Griffin ) I have one of those annoying what-ifs about Monday's lecture. In demonstrating the strong diamond property on a C-redex whose alternative clause contains an L-redex, i.e., (if #t 3 ((lambda (x) x) 5)) What if you rewrite the L-redex first and have to put the define outside of the if? (define x_1 5) (if #t 3 x_1) Then when you rewrite the C-redex, you get a body that contains garbage: (define x_1 5) 3 And you wouldn't have had any garbage if you'd rewritten the C-redex first... Do we assume complete garbage collection between steps from now on, because we know it doesn't matter when you do it? --Robby Griffin From meyer@theory.lcs.mit.edu Tue Oct 1 06:49:35 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA23113; Tue, 01 Oct 96 10:49:11 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA17030; Tue, 01 Oct 96 10:49:35 EDT Date: Tue, 01 Oct 96 10:49:35 EDT Message-Id: <199610011449.AA17030@stork.lcs.mit.edu> To: rmg@MIT.EDU Cc: 6044-forum@theory.lcs.mit.edu In-Reply-To: Robby Griffin 's message of Mon, 30 Sep 96 23:46:09 <9610010346.AA14571@MIT.MIT.EDU> Subject: hmm... I have one of those annoying what-ifs about Monday's lecture. In demonstrating the strong diamond property on a C-redex whose alternative clause contains an L-redex, i.e., (if #t 3 ((lambda (x) x) 5)) What if you rewrite the L-redex first and have to put the define outside of the if? (define x_1 5) (if #t 3 x_1) Then when you rewrite the C-redex, you get a body that contains garbage: (define x_1 5) 3 And you wouldn't have had any garbage if you'd rewritten the C-redex first... Do we assume complete garbage collection between steps from now on, because we know it doesn't matter when you do it? --Robby Griffin Oops. Your ingenious counterexample is something I overlooked. I'm pleased that you spotted this proof bug so promptly. I agree that your suggestion that including complete GC as part of every rewriting step should correct the strong-diamond claim, though your counterexample emphasizes that we better work out a careful proof of this new strong-diamond claim. It bothers me, though, to force GC at every step. In practice, GC is an autonomous background process, and I believe our rewriting model should, and actually does, reflect this in the sense that the model works fine with GC unconstrained. I believe another way to fix the problem which will leave GC unconstrained is to define ONE step-"with-optional-GC" to be one of our current non-G steps, viz., a P,C,L, or R step (not I), along with ANY NONNEGATIVE number of G's before or after the non-G step. (We're analyzing the special case without I. Confluence fails with I.) I think step-with-optional-G satisfies strong-diamond, and therefore would be confluent. A proof of this should follow fairly directly from the special case of strong-diamond given in Prob Set 2, prob 4a, and another similar lemma: LEMMA: If B1 --G--> B2 --A--> B3 (where --A--> indicates one rewriting using rule A in {P,C, I, L, G}, then there is a B4 such that B1--A-->B4 and B4--G*-->B3. In other words, you can always do G* at the end of a step instead of the beginning. Confluence of step-with-G plus these lemmas now directly implies confluence of the system of non-I rewriting steps as given in the Handout 2. All this needs to be carefully checked of course. I'd be grateful for your or other classmate volunteers' help in verifying and developing class notes on this stuff. Thanks, A. From meyer@theory.lcs.mit.edu Wed Oct 2 06:04:24 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA13899; Wed, 02 Oct 96 10:03:59 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA17915; Wed, 02 Oct 96 10:04:24 EDT Date: Wed, 02 Oct 96 10:04:24 EDT Message-Id: <199610021404.AA17915@stork.lcs.mit.edu> To: 6044-forum In-Reply-To: <6044 student> message of Wed, 2 Oct 1996 01:54:28 -0400 (EDT) Subject: ps 3 questions o in 1b, is garbage collecting something of the form (define foo (lambda () 1)) considered a violation of the lambda body restriction -- ie is that considered a rewrite of the body (since it goes away?) It's OK to garbage collect the def of foo if the variable foo is not needed. The lambda body restriction does NOT prevent ERASING entire lam exps, it only prevent changes INSIDE lambda exps. This point comes clearer for conditionals: we certainly don't want the lambda-body restriction to prevent evaluation of conditionals. But notice that in rewriting (if #t (lambda () 1) (lambda () 2)) ---> (lambda () 1), the (lambda () 2) disappears. But now that you point it out, I agree there is a little ambiguity concerning erasure in the informal statement of the restriction in Handout 2. A more precise formulation is: LAMBDA BODY RESTRICTION No rewrite rule may be applied to a redex (lefthand-side of the rule) which is a subbody of a lambda expression. Since lambda expressions themselves are not redexes of any rule, the ambiguity about whether a lambda expression is a subbody of itself ("inside" itself) never arises. an immediate value includes lambda expressions, so (lambda (x) B) is considered an immediate (and therefore garbage-collectible) value no matter how complex an expression B may be? YES. It would help me to know what prompts this question. Did you find the definition of immediate value unclear? did you find it so surprising you thought the def might contain a misprint? o is () considered ... a kernel scheme expression? Depends on where () occurs, ie., how it parses according to the kernel grammar. In particular, right after LAMBDA in (lambda () B), it parses an an empty sequence of formals--which is PART of an expression, but not an . In ((lambda (x) x) ()), it parses as an which is a expression. if so, what is its meaning? We haven't assigned meaning to Scheme expressions. As a matter of fact, we will discuss TODAY in lecture why it takes some subtle mathematics to assign "meaning" to Scheme in the way we did for arithmetic expressions. But the rewrite rules relating to the "()" are intended to model the behavior of the empty list, NIL, in Scheme. o can we violate the lambda body rule for question five? YES, violate it. In fact, I think you have to violate it for uniqueness to fail--but this is another one of those hard theorems. o what is a "free occurrence" of a variable defined as (for question 3)? See Handout 2, Appendix B. Regards, A. From meyer@theory.lcs.mit.edu Sun Oct 6 15:13:57 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA08683; Sun, 06 Oct 96 19:13:28 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA19985; Sun, 06 Oct 96 19:13:57 EDT Date: Sun, 06 Oct 96 19:13:57 EDT Message-Id: <199610062313.AA19985@stork.lcs.mit.edu> To: 6044-forum Subject: ps3-solns for all but problem 4 are on the course web page. Regards, A. From meyer@theory.lcs.mit.edu Mon Oct 7 17:25:37 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA02470; Mon, 07 Oct 96 21:25:10 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA20982; Mon, 07 Oct 96 21:25:37 EDT Date: Mon, 07 Oct 96 21:25:37 EDT Message-Id: <199610080125.AA20982@stork.lcs.mit.edu> To: 6044-forum Subject: Quiz 1 Solution is on the course web page. Regards, A. From rmg@MIT.EDU Thu Oct 10 14:23:35 1996 Return-Path: Received: from MIT.EDU (PACIFIC-CARRIER-ANNEX.MIT.EDU) by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA02194; Thu, 10 Oct 96 14:23:35 EDT Received: from MIT.MIT.EDU by MIT.EDU with SMTP id AA16216; Thu, 10 Oct 96 14:23:29 EDT Received: from SMALL-HALF.MIT.EDU by MIT.MIT.EDU (5.61/4.7) id AA13671; Thu, 10 Oct 96 14:23:13 EDT Message-Id: <9610101823.AA13671@MIT.MIT.EDU> To: 6044-forum@theory.lcs.mit.edu Subject: context with set! Date: Thu, 10 Oct 96 14:20:34 From: rmg@MIT.EDU (Robby Griffin ) Okay, I have a pair of expressions which are observationally congruent in any functional context but break when we use set!. Unfortunately this isn't really a simple example. The expressions are: M = (lambda (thunk) (thunk)) N = (lambda (thunk) ((lambda (thunked) (thunk)) (thunk))) M takes a thunk (procedure of no arguments) and calls it once. N takes a thunk and calls it twice. This won't matter in functional Scheme because the thunk will return the same thing (and not affect anything else) no matter how many times it's called, and these two procedures by themselves are observationally congruent. A context with set! is: C[] = (define a 1) (define a++ (lambda () (set! a (+ a 1)))) ((lambda (foo) a) ([] a++)) Note that a++ is a thunk which increments a, so (M a++) increments it once and (N a++) increments it twice. The lambda at the bottom is a hack to evaluate a sequence of expressions, in this case ([] a++) and then a. C[M] should return 2 and C[N] should return 3. That's assuming we evaluate the set! before we instantiate the a. I think Uniqueness is going to fail if we introduce set! without some restrictions on the order of rewriting. --Robby From meyer@theory.lcs.mit.edu Thu Oct 10 13:56:44 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA06743; Thu, 10 Oct 96 17:56:11 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA23273; Thu, 10 Oct 96 17:56:44 EDT Date: Thu, 10 Oct 96 17:56:44 EDT Message-Id: <199610102156.AA23273@stork.lcs.mit.edu> To: rmg@MIT.EDU In-Reply-To: Robby Griffin 's message of Thu, 10 Oct 96 14:20:34 <9610101823.AA13671@MIT.MIT.EDU> Subject: context with set! Reply-To: 6044-lecturer@theory.lcs.mit.edu Cc: 6044-forum Great example! It might be helpful in explaining it to notice that it is the desugaring of expressions with the LET construct: M = (lambda (thunk) (let ((dummy1 (thunk))) #t)) N = (lambda (thunk) (let ((dummy1 (thunk)) (dummy2 (thunk))) #t)) A context with set! is: C[] = (define a 1) (define increment-a (lambda () (set! a (+ a 1)))) (let ((dummy ([ ] increment-a))) a) Then C[M] returns 2 and C[N] returns 3. ... assuming we evaluate the set! before we instantiate the a. I think Uniqueness is going to fail if we introduce set! without some restrictions on the order of rewriting. And your comment above is also right on: once there are side-effects, order of evaluation becomes critical, and not much freedom of rewriting order can be tolerated. Regards, A. From meyer@theory.lcs.mit.edu Tue Oct 22 05:59:28 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA14921; Tue, 22 Oct 96 09:58:42 EDT From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA09816; Tue, 22 Oct 96 09:59:28 EDT Date: Tue, 22 Oct 96 09:59:28 EDT Message-Id: <199610221359.AA09816@stork.lcs.mit.edu> To: 6044-forum Subject: Is term-rewriting for "real" programmers? This came was in my email this morning. Thought it might provide some added motivation to our term-rewriting studies: From: Sophia Drossopoulou Subject: paper on the soundness of the Java type system Date: Mon, 21 Oct 96 18:06 BST To: types@dcs.gla.ac.uk [------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------] A paper arguing the soundness of the Java type system is now available by anonymous ftp from directory: /vol/ftp/pub/papers/S.Drossopoulou file: JavaSound.ps It is still "work in progress", and we expect to be updating it regularly, improving the English and removing typos, but we believe that the formalisms and proofs are correct and stable. Regards, Sophia Drossopoulou and Susan Eisenbach, Imperial College Abstract ======== We argue that the Java type system is sound, by proving a subject reduction theorem. 6044: "SUBJECT REDUCTION" MEANS THAT IF M REWRITES TO N, AND A "TYPE" CAN BE DERIVED FOR M, THEN THAT SAME TYPE CAN BE DERIVED FOR N. THE TYPE DERIVATION RULES ENSURE THAT NO EXPRESSION WHICH CAN BE TYPED CAUSES AN "IMMEDIATE TYPE-ERROR," NMAELY, AN ERROR IN ONE REWRITING STEP. SO SUBJECT REDUCTION IMPLIES THAT IF M IS TYPEABLE, THEN EVALUATION OF M WILL NOT CAUSE A TYPE ERROR. We define a subset of Java, a language which is safe and which reflects the most essential features of Java, [6044: TAKE NOTE. (CAPS ADDED BY ME.)] A TERM REWRITING SYSTEM FOR THE OPERATIONAL SEMANTICS and a type inference system to describe compile time type checking. We prove that program execution preserves the types, up to the subclass/subinterface relationship.) In this paper we consider the following parts of the Java language: primitive types, classes and inheritance, instance variables and instance methods, interfaces, shadowing of instance variables, and dynamic method binding. We plan to extend our study, starting with arrays and the associated dynamic checks, until we either have covered all of Java -- or we have uncovered loopholes in the type system. As an interesting subsidiary result, we formulated and prove two important properties which any compile-time correct Java program must satisfy: * the requirement for any class which according to the type rules widens another interface or class to provide an implementation for any method declared in that superinterface or superclass * the substitution property for compiled Java expressions 1,, Date: Thu, 31 Oct 96 11:28:29 EST From: meyer To: 6044-forum Subject: Quiz 2 posponed reply-to: 6044-lecturer@theory.lcs.mit.edu *** EOOH *** Date: Thu, 31 Oct 96 11:28:29 EST From: meyer To: 6044-forum Subject: Quiz 2 posponed reply-to: 6044-lecturer@theory.lcs.mit.edu Quiz 2 will be postponed FROM next Wed, 11/6 to another date--most likely MONDAY, Nov. 18 Let me know if that date causes problems. We'll confirm the date in class tomorrow. Regards, A.  1, filed,, Date: Thu, 31 Oct 96 11:28:29 EST From: meyer To: 6044-forum Subject: Quiz 2 posponed reply-to: 6044-lecturer@theory.lcs.mit.edu *** EOOH *** Date: Thu, 31 Oct 96 11:28:29 EST From: meyer To: 6044-forum Subject: Quiz 2 posponed reply-to: 6044-lecturer@theory.lcs.mit.edu Quiz 2 will be postponed FROM next Wed, 11/6 to another date--most likely MONDAY, Nov. 18 Let me know if that date causes problems. We'll confirm the date in class tomorrow. Regards, A.  0, unseen,, *** EOOH *** Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA19737; Fri, 01 Nov 96 23:05:11 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA21621; Fri, 01 Nov 96 23:06:09 EST Date: Fri, 01 Nov 96 23:06:09 EST Message-Id: <199611020406.AA21621@stork.lcs.mit.edu> To: 6044-forum Subject: H15, H16 Handout 15, "Scheme Computability" and Handout 16, "Problem Set 5" are now available on the course web-page. Note that Handout 15 has been revised and slightly enlarged over the draft distributed in lecture today. Be sure to use the web version. For your convenience, I'll bring copies to class Monday. Regards, A.  0, unseen,, *** EOOH *** Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA28200; Sat, 02 Nov 96 14:12:51 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA21887; Sat, 02 Nov 96 14:13:49 EST Date: Sat, 02 Nov 96 14:13:49 EST Message-Id: <199611021913.AA21887@stork.lcs.mit.edu> To: robby@chaotic.MIT.EDU Cc: 6044-lecturer@theory.lcs.mit.edu In-Reply-To: Robby Griffin's message of Sat, 02 Nov 1996 10:31:18 EST <199611021531.KAA16253@chaotic.MIT.EDU> Subject: Detectors Cc: 6044-forum From: Robby Griffin Date: Sat, 02 Nov 1996 10:31:18 EST On page 2 of handout 15, Problem 1 says: ... such that ev-val((D V0)) == #t, and ev-val((D V)) == #f for any Scheme value V which is not syntactically identical to V0 ... Okay, that means ev-val((D V)) has to be either #t or #f for all Scheme values V. But what about this V: (define x 5) 2 It's an followed by an , isn't it? But if you give that to the detector D, you'll just get stuck instead of either #t or #f. That means there can't be a detector for any value, because you could always break a detector with the sample value above. So what's the deal? Should we restrict the domain of D to s? Thereby avoiding the question of whether V is an expression or a body by requiring it to be an expression? --Robby Good question. The problem should have been worded: ... such that ev-val((D V0)) == #t, and ev-val((D E)) == #f for any for any Scheme EXPRESSION E FOR WHICH EV-VAL(E) IS DEFINED AND not syntactically identical to V0 ... Note that ev-val(E) must, by edfintion, be garbage-free, so your value (define x 5) 2 won't be ev-val of anything. On the other hand, (define x 5) (lambda (z) (cons x z)) is a garbage-free value. To see what D does on it, evaluate (D ( (lambda() (define x 5) (lambda (z) (cons x z))) )) Regards, A.  0, unseen,, *** EOOH *** Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA28759; Sat, 02 Nov 96 14:58:01 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA21930; Sat, 02 Nov 96 14:58:59 EST Date: Sat, 02 Nov 96 14:58:59 EST Message-Id: <199611021958.AA21930@stork.lcs.mit.edu> To: 6044-forum In-Reply-To: Albert R. Meyer's message of Sat, 02 Nov 96 14:13:49 EST <199611021913.AA21887@stork.lcs.mit.edu> Subject: Handout 15, prob 1(a): on Detectors Hmm. Same fix is needed if V_0 is not printable. Here's the fully reworded version of problem 1(a). I've already entered this correction into the web-page copy. Let V_0 be some Scheme value. A V_0-DETECTOR is a Scheme expression, D, such that ev-val( (D E) ) = #t, for any Scheme expression, E, such that ev-val(E) = V_0, and ev-val( (D E) ) = #f for any E such that ev-val(E) is defined and is not syntactically IDENTICAL to V_0. 1(a) Show that every printable value has a detector. Regards, A.  0, unseen,, *** EOOH *** Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA28783; Sat, 02 Nov 96 15:00:08 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA21935; Sat, 02 Nov 96 15:01:06 EST Date: Sat, 02 Nov 96 15:01:06 EST Message-Id: <199611022001.AA21935@stork.lcs.mit.edu> To: 6044-forum Subject: Quiz 2 Having heard no objections, Quiz 2 is now officially rescheduled to MONDAY, 18 NOVEMBER, in class. Regards, A.  1,, Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA02598; Fri, 08 Nov 96 17:22:42 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA26826; Fri, 08 Nov 96 17:23:47 EST Date: Fri, 08 Nov 96 17:23:47 EST Message-Id: <199611082223.AA26826@stork.lcs.mit.edu> To: 6044-forum Subject: Handout 18: PS6, and Handout 17: Computability, II *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Fri, 08 Nov 96 17:23:47 EST To: 6044-forum Subject: Handout 18: PS6, and Handout 17: Computability, II Are now on the course web page. PS6 is due next Friday. Have an enjoyable long weekend. Regards, A.  1,, Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA02525; Sun, 10 Nov 96 18:29:37 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27214; Sun, 10 Nov 96 18:30:44 EST Date: Sun, 10 Nov 96 18:30:44 EST Message-Id: <199611102330.AA27214@stork.lcs.mit.edu> To: 6044-forum Subject: PS6, 6(c) *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Sun, 10 Nov 96 18:30:44 EST To: 6044-forum Subject: PS6, 6(c) We haven't developed Scheme theory enough for a proof of PS6, prob 6(c), so don't try to prove it. However, you should try to give a plausible, informal "programmer's explanation," for the claim made in 6(c). Regards, A.  1, edited,, Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA05416; Sun, 10 Nov 96 23:11:54 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27252; Sun, 10 Nov 96 23:12:59 EST Date: Sun, 10 Nov 96 23:12:59 EST Message-Id: <199611110412.AA27252@stork.lcs.mit.edu> To: 6044-forum Subject: Handout 17 *** EOOH *** From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Date: Sun, 10 Nov 96 23:12:59 EST To: 6044-forum Subject: Handout 17 Section 6 on Kleene's Recursion Theorem is not required reading; it's a lovely bit of theory, but not necessary for our purposes, and we won't cover it this term. The course web page is temporarily frozen because its server is out of disk space. Below is postscript for an updated version of Handout 17, with some typos corrected and a few more proofs filled in. I'll post it on the web-page when the server thaws and will bring hard copy to class Wednesday. Regards, A. %!PS-Adobe-2.0 %%Creator: dvips 5.58 Copyright 1986, 1994 Radical Eye Software From meyer@theory.lcs.mit.edu Mon Nov 11 08:18:10 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA17388; Mon, 11 Nov 96 13:17:02 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27364; Mon, 11 Nov 96 13:18:10 EST Date: Mon, 11 Nov 96 13:18:10 EST Message-Id: <199611111818.AA27364@stork.lcs.mit.edu> To: 6044-forum Subject: web-page unfrozen The course web-page server is no longer frozen, and I have placed the latest version of Handout 17, Scheme Computability, II, there. Regards, A. From meyer@theory.lcs.mit.edu Thu Nov 14 04:04:52 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA09887; Thu, 14 Nov 96 09:03:42 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA29136; Thu, 14 Nov 96 09:04:52 EST Date: Thu, 14 Nov 96 09:04:52 EST Message-Id: <199611141404.AA29136@stork.lcs.mit.edu> Subject: ps6, Handout 17, prob 4 To: 6044-forum Date: Wed, 13 Nov 1996 15:04:12 EST Professor Meyer, Just a quick question about Problem 4. You describe: {(0 A)|A in the set A} U {(1 B)|A in the set B} I am wondering if the latter part should be the set of (1 B) for each B in the set of B instead: {(0 A)|A in the set A} U {(1 B)|B in the set B} (**) YES, it should read as (**), as you indicated. Thanks for catching and properly correcting my typo. Regards, A. From djib@hematite.mit.edu Thu Nov 14 16:12:15 1996 Return-Path: Received: from HEMATITE.MIT.EDU by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA27016; Thu, 14 Nov 96 21:12:17 EST Received: (from djib@localhost) by hematite.mit.edu (8.7.6/8.7.3) id VAA10600; Thu, 14 Nov 1996 21:12:16 -0500 Date: Thu, 14 Nov 1996 21:12:15 -0500 (EST) From: Debajit Ghosh To: 6044-forum@theory.lcs.mit.edu Subject: Problem 1 (fwd) Message-Id: X-Url: http://www.mit.edu:8001/people/djib/home.html Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Date: Thu, 14 Nov 1996 12:27:22 -0500 (EST) From: Debajit Ghosh To: meyer@theory.lcs.mit.edu Subject: Problem 1 X-Url: http://www.mit.edu:8001/people/djib/home.html For number 1, I was wondering if you were looking for a theoretically difficult to prove argument, or something along the lines of "this can't be done, period" argument. Is the following reasoning valid? : congruence is theoretically impossible to prove so it is not possible to prove that any meta-circular interpretor (ev-val(smeval 'M)) will always be "=" to ev-val(M); we can only prove observation congruence (ie when printable values are invovled..)? -Jit ------------------- Date: Thu, 14 Nov 96 14:45:43 EST From: meyer To: djib@hematite.mit.edu In-reply-to: Debajit Ghosh's message of Thu, 14 Nov 1996 12:27:22 -0500 (EST) Subject: Problem 1 ...congruence is theoretically impossible to prove so it is not possible to prove that any meta-circular interpretor (ev-val(smeval 'M)) will always be "=" to ev-val(M); we can only prove observation congruence (ie when printable values are involved..)? I can't make much sense of your argument above. It doesn't seem likely to be salvageable either, because it's easy to modify any of the meta-circular evaluators so they DO return the same value as the official interpreter in many non-printable value cases. (I'm not sure what theoretical obstacles there may be to doing it ALL cases.) Think of it this way: the meta-circular interpreters run in Scheme, but are free to use their own representations of Scheme values. When the interpreter runs on an input expression which halts, it will finally get to its representation of the value of the expression. By our def of meta-circular, if the represented value is printable, the interpreter must then convert from its representation to the underlying Scheme's representation of that value. For example, the rewriting intepreter on the course web-page represents ALL values as printable values of the underlying Scheme. When it halts, it converts its internal representation into something which will print out appropriately by the underlying Scheme. This conversion is done by the procedure "printable-version" in the file smeval.scm. For example, internally, it would represent the value of the expression (list 'a) as the Scheme value of '(cons 'a ()). So the smevaluator represents a list of one symbol as a list of 3 elements: 2 symbols and the empty list. The procedure "printable-version" applied to the 3-element list, figures out that it has to get underlying Scheme to evaluate the expression "(cons 'a ())", and then it returns the value it gets for this expression from underlying Scheme. As currently written, the smevaluator would represent the procedure value (lambda (x) x)) by the Scheme value '(lambda (x) x)), and (printable-version '(lambda (x) x))) would return something which printed out an indication that it was returning a procedure value. But we could modify printable-version as follows: (define (new-printable-version val-rep) (if (equal? val-rep '(lambda (x) x)) (lambda (x) x) (printable-version val-rep))) Now, at least for this one procedure value, (smeval '(lambda (x) x)) would return the SAME value as the underlying Scheme in which it was implemented. Hope this helps... Regards, A. Date: Thu, 14 Nov 96 20:59:39 EST From: Albert R. Meyer To: djib@hematite.mit.edu Subject: Problem 1 Date: Thu, 14 Nov 1996 15:34:36 -0500 (EST) From: Debajit Ghosh X-Url: http://www.mit.edu:8001/people/djib/home.html > I can't make much sense of your argument above. It doesn't seem likely to > be salvageable either, because it's easy to modify any of the > meta-circular evaluators so they DO return the same value as the official > interpreter in many non-printable value cases. (I'm not sure what > theoretical obstacles there may be to doing it ALL cases.) Okay, I buy that. But then I'm really lost on how to approach number 1.. there doesn't seem to be any real reason why the meta-circular interpreters do not eval to the same thing scheme does in all cases (when both halt), because as you said, you can always get the meta-circular interpreter to return the same value as real scheme in probably every case.. am I missing something major here? Thanks, Jit Question was not meant to ask whether SOME meta-circular interpreter could meet the stronger condition. Just explain what values each of the three meta-c interpreters we've identified returns when applied, say, to '(lambda (x) x), and why none of these three values are equal to the procedure value that underlying Scheme returns when (lambda (x) x) is evaluated. I'd like to forward our correspondence to 6044-forum. OK? In fact, if it is, I'd be grateful if you'd forward it yourself. (Copy below in case you didn;t keep one). Thanks, A. From meyer@theory.lcs.mit.edu Thu Nov 14 18:07:02 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA28756; Thu, 14 Nov 96 23:05:51 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA01220; Thu, 14 Nov 96 23:07:02 EST Date: Thu, 14 Nov 96 23:07:02 EST Message-Id: <199611150407.AA01220@stork.lcs.mit.edu> To: 6044-forum Subject: re PS6, prob 11 I am confused about question 11. In 11(a) what does "the same functions from N to N are computable" mean? The prelude to the problem shows how to choose rewrite rules for int->sym so that it is a symbol enumerator, as required, but ALSO so that ANY given function f:N --> N, for example some NON-SCHEME-COMPUTABLE function f, IS computable in extended Scheme. Problem 11(a) asks for some rules for int->sym which do NOT raise this problem: any function from N to N computable in extended Scheme with these "good" rules was already computable in unextended Scheme. I don't understand 11(b) much at all. It seems like 11(a) asks us to define the rewrite rules to make int->sym rewrite properly, and that the correct answer would obviously include any necessary conditions on its implementation. A correct answer to 11(a) is a description of some "good' set of rewrite rules for int->sym. But there are many, many such "good" sets. 11(b) asks for some sufficient condition which guarantees "goodness." Of course, one could just say the "goodness" condition was that the rules be "good"--that is, they don't add any new functions to the set of Scheme computable N to N functions. But that answer is obviously uninformative. Instead, I'm looking for A MORE EASILY VERIFIABLE property of the rewriting rules which will imply that they are "good". I grant you that 11(b) is somewhat imprecise about the kind of "sufficient condition" which is asked for, but it has a sensible answer, which I hope you and your classmates will realize. Regards, A. From meyer@theory.lcs.mit.edu Sat Nov 16 16:22:13 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA12252; Sat, 16 Nov 96 21:21:00 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA02969; Sat, 16 Nov 96 21:22:13 EST Date: Sat, 16 Nov 96 21:22:13 EST Message-Id: <199611170222.AA02969@stork.lcs.mit.edu> To: 6044-forum Subject: old homework in file Your submitted problem sets 3--5, still ungraded, are available in the course file cabinet on the third floor of 545 Tech Sq (NE43) on the wall near office 307. You may take YOUR OWN problem sets to review your answers; return them in class Monday. Regards, A. From meyer@theory.lcs.mit.edu Tue Nov 19 08:48:58 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA15300; Tue, 19 Nov 96 13:47:42 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA05400; Tue, 19 Nov 96 13:48:58 EST Date: Tue, 19 Nov 96 13:48:58 EST Message-Id: <199611191848.AA05400@stork.lcs.mit.edu> To: 6044-forum Subject: q2 solutions Solutions to Quiz 2 are now available on the course web page. Regards, A. From meyer@theory.lcs.mit.edu Thu Nov 21 09:49:11 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA10463; Thu, 21 Nov 96 14:47:55 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA06884; Thu, 21 Nov 96 14:49:11 EST Date: Thu, 21 Nov 96 14:49:11 EST Message-Id: <199611211949.AA06884@stork.lcs.mit.edu> To: 6044-forum Subject: q2, prob 3(a) correction I made an error in the solution to Q2, prob 3(a): the symbol 'list was omitted. (This was pointed out by Robbie, whom I thank.) The proper solution is below and has already been incorporated into a revised quiz2-soln.ps on the course web page. This mistake may have led me to misgrade your quiz answer. If you think it did and want more credit, feel free to ask me to regrade your answer. Regards, A. ----------------------------------- ----------------------------------- Sol'n 3(a) [15pts] For the expression \textcircled{1}, suppose ev-val(qs) = ev-val('S). We want an expression for the application of N to '(0 S), which is the same as applying N to (list 0 ev-val(qs)). Then we want to apply the metacircular interpreter to the quote of this expression, namely, '(N (list 0 ev-val(qs))). But we can't simply plug in the variable qs for its value within the quoted expression above because it would be treated as a symbol 'qs instead of being evaluated. So we have to desugar the quote by hand and apply the interpreter to (list 'N (list 'list 0 qs)). So expression \textcircled{1} is (list 'list 0 qs). Similarly, expression \textcircled{2} is (list 'N (list 'list 1 qs)). From meyer@theory.lcs.mit.edu Mon Nov 25 12:32:16 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA01748; Mon, 25 Nov 96 17:30:53 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA12737; Mon, 25 Nov 96 17:32:16 EST Date: Mon, 25 Nov 96 17:32:16 EST Message-Id: <199611252232.AA12737@stork.lcs.mit.edu> To: 6044-forum Subject: [hershey@MIT.EDU: HUMOR: Scheme Explained] To: meyer@theory.lcs.mit.edu Date: Mon, 25 Nov 1996 17:26:23 EST From: "Mark A. Herschberg" I got this offer a humor mailing list I'm on. I thought you and possibly the class might appreciate it. --Mark ------- Forwarded Message Date: Sun, 17 Nov 1996 21:33:45 -0500 To: humor@MIT.EDU From: abennett@MIT.EDU (Andrew Bennett) Subject: HUMOR: Scheme Explained From: katyking@MIT.EDU Date: Sun, 17 Nov 1996 15:52:05 EST From: "Danyel A. Fisher" [from: alt.humor.best-of-usenet] Subject: Re: Q: What are the possibilities of Scheme? From: vfr750@netcom.com (Will Hartung) Newsgroups: comp.lang.scheme David.Pues@student.ac.be (David Pues) writes: >My question is : what is Scheme used for? (so: benefits, uses, ...) Here's the answer that you're looking for: Scheme is used for just a whole bunch of stuff. It's a general purpose programming language that can do general purpose things. It is not as advanced commercially as Lisp, but pretty popular in acadamic circles. There are fast implementations, there are slow implementations, there are big and small implementations. Which is really a blessing and a curse -- there are a LOT of implementations. I think that it can (almost) be safely said that there is SOME implementation somewhere that supports your platform for whatever application you want to write. Schemes weak point is in lacking a standard way to extend the system to adapt to the packages that keep popping up for all of the OS's, specifically graphics extensions (like the Windows API, etc). Now, here's the answer that's you're not looking for: Scheme is programmer poetry. It is used to help cleanse the soul of programmers who must use lesser languages to earn their daily bread. Programming in Scheme is like driving on an open freeway versus commuting in gridlocked traffic. You can concentrate on the destination versus trying to not get killed getting there. Scheme stays out of your way, wrapping you in a clean, almost noise-free environment. But, on the dark side, Scheme is a beautiful singing siren, resting on the white sand of a remote harbor that is deceptively shallow and bottomed with jagged rocks. She sits waiting for programmers who may have lost their way and find themselves out and about, searching for Something Else. They see the beauty of Scheme, hear its song, and turn their ships toward the white, sandy beaches that frame Her, only to have their hopes crushed against the hidden limitations by the pounding surf of "Commercial Deliverability, Corporate Confidence, and Business Realities". So, alas, the Professional Developers have body's in the gray cubicles of Corporate America, shackled to their mortagages by C++ and other horrors, while, inside, their souls scream for the peace and purity of Scheme, the tranquility. But you! For you it's not too late! Not everyone hears the sirens call. It touches some more than others, but take it from someone who has felt the touch! DON'T RISK IT! RUN! FLEE! While you are still in the dark! Before it claims another victim! DROP THE CLASS WHILE YOU STILL CAN! Grab a "C++ in 21 Days" book, lock yourself in a round room, and follow the chapters as it points you to the corners for answers. When you exit, you'll have the support of zillions of others, on their bait barges past the breakwater, content. Yeah, the environment is ugly, it smells bad, and some of the company could be better...but they seem to catch fish...not pretty or big fish, but enough fish to get by on. For the touched that are fighting the waves in the harbor, we diligently struggle to dredge the bottom, to make the harbor deeper and hopefully finally free Scheme out into the Real World. Of course, when she arrives, she'll grab the limelight, toss us aside, and court the muckraking pundits who've "Always known her". But we'll know. We loved her first. Does that help? ======================================================================= Andrew Bennett MIT Department Ocean Engineering MIT Room 5-424 77 Massachusetts Ave. Cambridge, MA 02139 Phone: (617) 253-7950 ===== Area 51 ============== Bureau 13 =============== Network 18 ===== ------- End of Forwarded Message From meyer@theory.lcs.mit.edu Wed Dec 11 18:24:46 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA14388; Wed, 11 Dec 96 23:23:05 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27187; Wed, 11 Dec 96 23:24:46 EST Date: Wed, 11 Dec 96 23:24:46 EST Message-Id: <199612120424.AA27187@stork.lcs.mit.edu> To: 6044-forum Subject: Handout 22, Lecture Outline ...is now on the course Web Page. More handouts to come tomorrow. Regards, A. From meyer@theory.lcs.mit.edu Fri Dec 13 19:13:06 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA05016; Sat, 14 Dec 96 00:11:23 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27603; Sat, 14 Dec 96 00:13:06 EST Date: Sat, 14 Dec 96 00:13:06 EST Message-Id: <199612140513.AA27603@stork.lcs.mit.edu> To: 6044-forum Subject: Handout 24 on The Semigroup Word Problem is now on the course web page. Regards, A. From meyer@theory.lcs.mit.edu Sat Dec 14 14:10:30 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA19673; Sat, 14 Dec 96 19:08:46 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27687; Sat, 14 Dec 96 19:10:30 EST Date: Sat, 14 Dec 96 19:10:30 EST Message-Id: <199612150010.AA27687@stork.lcs.mit.edu> To: 6044-forum Subject: Handout 25: Scheme->2Counter Machines is now available on the course webpage. I hope to have notes on relativization and jump on the page by early tomorrow. There will not be notes on Scheme->Pure-Procedural-Scheme; this won't be on the final either. Regards, A. From meyer@theory.lcs.mit.edu Sat Dec 14 14:36:33 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA19908; Sat, 14 Dec 96 19:34:53 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27706; Sat, 14 Dec 96 19:36:33 EST Date: Sat, 14 Dec 96 19:36:33 EST Message-Id: <199612150036.AA27706@stork.lcs.mit.edu> To: djib@hematite.mit.edu Cc: 6044-forum In-Reply-To: Debajit Ghosh's message of Sat, 14 Dec 1996 14:36:17 -0500 (EST) Subject: question on Semigroup notes Either I found a typo or I'm really confused :-).. for Corollary 1 of the Two-way Simulation lemma, should the corollary be: S--(E_M)*->T iff W--(R_M)*->T as written, or S--(E_M)*->T iff S--(R_M)*->T TYPO. Thanks for spotting it; i"ve already corrected the web version. Also, I have a bit of confusion on going from SWP to 2CM. Is what we're trying to do here going from any SWP to a 2CM, or going from 2CM to a SWP, namely the configuration word [rep(k,l,m)] that represents a state of the 2CM? We go from 2-CM, M, to SWP instance Q_M which consists of the equation sequence E_M folowed by the equation ( rep(0,0,0) = (rep(length(M),0,0) ). Then M halts (cleanly) iff Q_M is in SWP. So clean halting could be decided if membership in SWP could be decided: to decide if M cleanly halts, construct Q_M and decide if it is in SWP. But clean halting can't be decided, so SWP must not decidable either. Does that help? I've slightly revised the closing sentences of the handout in response to your query. Any other suggestions for clarifying this point? Regards, A. From meyer@theory.lcs.mit.edu Wed Dec 14 20:59:49 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA22665; Sun, 15 Dec 96 01:58:05 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27757; Sun, 15 Dec 96 01:59:49 EST Date: Sun, 15 Dec 96 01:59:49 EST Message-Id: <199612150659.AA27757@stork.lcs.mit.edu> To: 6044-forum Subject: Handout 26: Notes on Turing Reducibility is now on the 6044 web page. It is develops the material more thoroughly than was done in lectures, which may be helpful. But the final will only cover those results which were also discussed in lecture. There won't be any further notes. In particular, since there are no notes on the undecidability of the equivalence problem for BNF grammars, this result will not be on the final either. Regards, A. From meyer@theory.lcs.mit.edu Sun Dec 15 09:08:31 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA27650; Sun, 15 Dec 96 14:06:47 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27791; Sun, 15 Dec 96 14:08:31 EST Date: Sun, 15 Dec 96 14:08:31 EST Message-Id: <199612151908.AA27791@stork.lcs.mit.edu> To: djib@hematite.mit.edu In-Reply-To: Debajit Ghosh's message of Sun, 15 Dec 1996 12:57:36 -0500 (EST) Subject: polynomial inequalities Cc: 6044-forum Date: Sun, 15 Dec 1996 12:57:36 -0500 (EST) From: Debajit Ghosh X-Url: http://www.mit.edu:8001/people/djib/home.html A couple of us were wondering about this. In class, you had mentioned that polynomial inequalities were not even half-decidable. How do you get this? What is the basic reasoning behind thinking about polynomials and relating them to Scheme and/or 2CM? Thanks! -Jit Good question. It's easy to see that inequalities which are NOT valid, ARE half-decidable, so if we know that validity is undecidable, then it must be that the valid inequalities are not half-decidable. I think the undecidability of the validity problem for Diophantine polynomial inequalities is the coolest and best motivated undecidability result about "real" problems. But takes it about 2 lectures and development of some unfamiliar number-theorettic and polynomial algebraic lemmas to learn how polynomials can simulate 2-CM's. I had hoped to prove this, but decided it would be better to go slower and spend the time on some other, technically easier to prove, "real" undecidability results, namely, the semigroup word problem and the BNF equiv problem. A new text by Neil Jones which will soon be published in the MIT Press Foundations of Computer Science Series (edited by yours truly) contains the most polished elementary exposition of the proof found to date. It's 16 pages. Everyone in the class now has more than enough background to understand this exposition, though it takes some hours of study to go through. I'd be happy to make a copy of this section of the book for anyone in the class who is interested. (Even better, buy the book when it comes out so I get my editor's commission -- I think it's about 10 cents per copy :-) ) Regards, A. From meyer@theory.lcs.mit.edu Sun Dec 15 16:58:34 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA02952; Sun, 15 Dec 96 21:56:49 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA27844; Sun, 15 Dec 96 21:58:34 EST Date: Sun, 15 Dec 96 21:58:34 EST Message-Id: <199612160258.AA27844@stork.lcs.mit.edu> To: djib@hematite.mit.edu In-Reply-To: Debajit Ghosh's message of Sun, 15 Dec 1996 20:10:08 -0500 (EST) Subject: arithmetic sets Cc: 6044-forum Date: Sun, 15 Dec 1996 20:10:08 -0500 (EST) From: Debajit Ghosh Are we responsible for the arithmetic sets portion of the notes? NO If so, how do you porve that something is not arithmetic (Exercise 2)? You are NOT RESPONSIBLE for this, but I'll tell you: Use notation H^n for the set H''...'' with n jumps. Notice that script-J in exercise 2 has the property that H^n <=_T script-J , for ALL n >=0. No such set can be arithmetic. For suppose script-J was arithmetic. This means script-J <=_T H^k for some k. But since H^(k+1) <=_T script-J, we conclude H^(k+1) <=_T H^k. This contradicts the fact that H^k <_T H^(k+1). QED. From meyer@theory.lcs.mit.edu Sun Dec 22 18:46:27 1996 Return-Path: Received: from stork.lcs.mit.edu by theory.lcs.mit.edu (5.65c/TOC-1.2S) id AA18965; Sun, 22 Dec 96 23:44:33 EST From: meyer@theory.lcs.mit.edu (Albert R. Meyer) Received: by stork.lcs.mit.edu (5.65c/TOC-1.2C) id AA01919; Sun, 22 Dec 96 23:46:27 EST Date: Sun, 22 Dec 96 23:46:27 EST Message-Id: <199612230446.AA01919@stork.lcs.mit.edu> To: 6044-forum Subject: H28-grades You should have received personal email from me with your course grade. The sorted grades are on the course web-page (H28). Final grade distribution was: A 1 A- 1 B+ 1 B 2 B- 3 You can pick up your problem sets, and look over (but not keep) your final exam booklet from the course secretary David Jones, NE43-315, dmjones@theory.lcs.mit.edu, (617) 253-5936. Happy Holidays, A.