http:^^www.cs.washington.edu^education^courses^431^96s^bboard.shtml

来自「This data set contains WWW-pages collect」· SHTML 代码 · 共 1,486 行 · 第 1/4 页

recently, you should.

Cheer,
	Michael <[e-mail]>
<hr size=4><a name="830643569001">Date: 27 Apr 1996 15:10 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>exercise</b>
</a>

At the end of class on friday, I suggested you think about , before
monday's class, what questions about C programs are decidable
vs undecidable.  As another slant on this, what programming errors
could you catch at compile time?  The following talk announcement
that happened to come out yesterday may give you some food for
thought.  Don't worry if you don't understand all the buzz words in
this; I don't either.

PS: Nelson's a good guy; the talk might be interesting (but I'm
certainly not suggesting that it's part of your 431 homework).
  &gt;  _________________________________
  &gt; From voting-faculty-request@june Fri Apr 26 11:09:28 1996
  &gt; Date: Fri, 26 Apr 1996 10:33:06 -0700 (PDT)
  &gt; From: Scott Dakins &lt;[e-mail]&gt;
  &gt; To: [e-mail]
  &gt; Subject: UW-CSE Colloq / 5-7-96 / Nelson / DEC Systems Research Center 
          / Extended Static Checking
  &gt; 
  &gt; UNIVERSITY OF WASHINGTON
  &gt; Seattle, Washington 98195
  &gt; 
  &gt; Department of Computer Science and Engineering
  &gt; Box 352350
  &gt; [phone]
  &gt; 
  &gt; COLLOQUIUM
  &gt; 
  &gt; SPEAKER:	Greg Nelson
  &gt; 		DEC Systems Research Center
  &gt; 
  &gt; TITLE:		Extended Static Checking
  &gt; 
  &gt; DATE:		Tuesday, May 7, 1996
  &gt; 
  &gt; TIME:		3:30 pm	
  &gt; 
  &gt; PLACE:		134 Sieg Hall
  &gt; 
  &gt; HOST:		Anna Karlin
  &gt; 
  &gt; ABSTRACT:
  &gt; 
  &gt; I'll describe a system for detecting at compile time certain programming
  &gt; errors that are not normally detected until run time, and sometimes
  &gt; not even then.  For example, array bounds errors and NIL dereferences.
  &gt; A special novelty of the system is its ability to detect race conditions
  &gt; and deadlocks in multi-threaded programs.  
  &gt; 
  &gt; The system requires the programmer to annotate procedure declarations 
  &gt; with simple preconditions and postconditions.  These annotations 
  &gt; are much less onerous than the annotations that would be required 
  &gt; for a full program correctness proof.  
  &gt; 
  &gt; The checking is totally automatic. The checker reports errors by line number. 
  &gt; 
  &gt; The system is implemented for Modula-3, and handles essentially 
  &gt; all features of the Modula-3 safe language, including references, 
  &gt; objects with single inheritance, and concurrency.  Many parts of 
  &gt; the standard library for Modula-3 have been checked with the system, 
  &gt; including the object-oriented input-output stream library and the 
  &gt; generic sequence library. 
  &gt; 
  &gt; 
  &gt; Refreshments to follow.
  &gt; 
  &gt; 
  &gt; Email: [e-mail]
  &gt; 
  &gt; Info: http://www.cs.washington.edu
  &gt; 
  &gt; 
<hr size=4><a name="831090259001">Date: Thu, 2 May 1996 19:24:14 -0700 (PDT)
From: <b>Larry Roske &lt;[e-mail]&gt;</b>
To: [e-mail]
Subject: <b>HW #3 Problem 5.7</b>
</a>

Since A_TM is enumerable, can't we just use Theorem 5.22 which
says that if A &lt;=m B, and B is enumerable, then A is enumerable?

--Larry

<hr size=4><a name="831098472001">Date: 2 May 1996 21:39 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: Larry Roske &lt;[e-mail]&gt;
Subject: <b>Re: HW #3 Problem 5.7</b>
Cc: [e-mail]
</a>

theorem 5.22 is an &quot;If&quot;, not an &quot;If and only if&quot;.

  &gt; Date: Thu, 2 May 1996 19:24:14 -0700 (PDT)
  &gt; From: Larry Roske &lt;[e-mail]&gt;
  &gt; To: [e-mail]
  &gt; Subject: HW #3 Problem 5.7
  &gt; 
  &gt; Since A_TM is enumerable, can't we just use Theorem 5.22 which
  &gt; says that if A &lt;=m B, and B is enumerable, then A is enumerable?
<hr size=4><a name="831269855001">Date: Sat, 4 May 1996 21:17:28 -0700 (PDT)
From: <b>Larry Roske &lt;[e-mail]&gt;</b>
To: [e-mail]
Subject: <b>HW Solution Questions</b>
</a>

Jayram, 

After more careful reading of the homework solutions I 
wanted to clarify a couple of things:

HW #1 Solution:  (just errata I think)
  1. For Problem 4, part a., first sentence:  0,1* should be {0,1}* ?

  2. For same problem, part b., 4th line:  u^R should just be u ?

HW #2 Solution:
  1. Problem 5:  You used a^t instead of just a number t.  Is this
     because you wanted to encode the number as a string?

HW #3 Solution:
  1. 5.7:  How would we write the solution using the format used
     in text and lecture--as follows?

     The following machine F computes a reduction f:
     F = &quot;On input x:
       1. If x != &lt;M, w&gt; for any TM &lt;M, w&gt;, then output some fixed
          y0 not_in A_TM.

       2. Otherwise, build M' and output &lt;M', w'&gt;, where

          M'(M_L) = &quot;On input w:
            1. Run M_L on w
            2. If M_L accepts, then accept; else reject.

     Where M'(M_L) means M' is parameterized with M_L, a TM that
     accepts any enumerable language.

Thanks,

--Larry


<hr size=4><a name="831493913001">Date: 7 May 1996 11:30 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>talk today</b>
</a>

A reminder, on the off chance that you were interested in the talk I
mentioned...
  &gt;  _________________________________
  &gt; From voting-faculty-request@june Tue May  7 11:21:55 1996
  &gt; To: cs-grads@geoduck, uw-systems@geoduck, faculty@geoduck
  &gt; Subject: Colloquium reminder
  &gt; Date: Tue, 07 May 1996 11:19:37 PDT
  &gt; From: Anna Karlin &lt;[e-mail]&gt;
  &gt; 
  &gt; 
  &gt; Greg Nelson from DEC Systems Research Center is giving a colloquium
  &gt; today at 3:30 on Extended Static Checking.
  &gt; He's a really good guy, who's done great work in numerous areas
  &gt; of computer science including programming languages, theorem
  &gt; proving and distributed systems.
  &gt; It should be a really interesting talk.
  &gt; 
  &gt; 
<hr size=4><a name="831499402001">Date: 7 May 1996 13:02 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: Kestutis Sereiva &lt;[e-mail]&gt;
Subject: <b>Re: talk today</b>
Cc: cse431@cs
</a>

in 134 Sieg.
<hr size=4><a name="832005486001">Date: 13 May 1996 09:35 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>book review</b>
</a>

I think I told you I will be sending the publisher a review of
Sipser's book (in preparation for his final edition).  I'll probably
compose it next weekend.  If you have comments about the book,
please send them to me and I'll forward them.
<hr size=4><a name="832218048001">Date: Wed, 15 May 1996 20:40:43 -0700 (PDT)
From: <b>Larry Roske &lt;[e-mail]&gt;</b>
To: [e-mail]
Subject: <b>HW #4</b>
</a>

FYI, in problem 7.13, the A refers to some language in P.

--Larry

<hr size=4><a name="832309764001">Date: Thu, 16 May 1996 22:09:20 -0700 (PDT)
From: <b>Larry Roske &lt;[e-mail]&gt;</b>
To: [e-mail]
Subject: <b>HW 4 Prob. 7.30</b>
</a>

I'm trying to polynomially reduce 2SAT to PATH, and then
by Theorem 7.25, (if A &lt;=P B, and B is in P, then A is in P)
2SAT would be in P as desired, but am having difficulty.
Any suggestions/insight, or would another strategy be easier?

Thanks,

--Larry

<hr size=4><a name="832360862001">To: Wade Barrett &lt;[e-mail]&gt;
Cc: ruzzo@cs, cse431@cs
Subject: <b>Re: NP vx. NP </b>
In-reply-to: Your message of &quot;Fri, 17 May 1996 11:45:15 PDT.&quot;
             &lt;[e-mail]&gt; 
Date: Fri, 17 May 1996 12:20:50 PDT
From: <b>&quot;Jayram S. Thathachar&quot; &lt;[e-mail]&gt;</b>
</a>

&gt;&gt;&gt;&gt;&gt; &quot;WB&quot; == Wade Barrett &lt;[e-mail]&gt; writes:

WB&gt; Could you please tell me exactly what was being proved at the end
WB&gt; of class?  I would like to try to prove it myself.

The two formulations of NP were

L is in NP if

(*) There is a poly-time verifier for L.

(**) There is a poly-time NTM that decides L.

Proof:
(*) ==&gt; (**)

Suppose there is a verifier V for L that takes a pair &lt;x,y&gt; and
accepts/rejects in time |x|^k then the poly-time NTM that
decides  L works as follows:

On input x:
  Guess y of length |y|^k.
  Accept iff V accepts &lt;x,y&gt;.

(**) ==&gt; (*)
Suppose the NTM N decides L in time n^s.
The poly-time verifier V should take a pair &lt;x,y&gt; and accept/reject
&lt;x,y&gt; in time polynomial in |x| so that

a. If x is in L, then for some y, V accepts &lt;x,y&gt;
b. If x is not in L, then for all y, V rejects &lt;x,y&gt;

Hint: Use the simulation of NTMs by DTMs (I'm not sure but I think it
is Theorem 3.7) to do this.

If you recall, this is similar to the HW problem that showed that a
language C is enumerable if and only if there is a decidable language
D such that
a. if x is in C, then for some y, &lt;x,y&gt; is in D
b. if x is not in C, then for all y &lt;x,y&gt; is not in D.

Thus the DTM that decides D is the verifier for the enumerable language
C (with no restrictions on running time). In some sense, the class of
enumerable languages are to NP as the class of decidable languages to P.
<hr size=4><a name="832397386001">Date: 17 May 1996 22:27 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>late HW policy</b>
</a>

Just got back to town, to find several messages asking about late
homework.  My usual policy is -10% for late papers, so if you didn't
turn anything in today, or only turned in part of the assignment,
it's certainly worth your while to try to finish it over the weekend.
<hr size=4><a name="833343977001">Sender: [e-mail]
Date: Tue, 28 May 1996 21:26:13 -0700
From: <b>Jayram Thathachar &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>Re: Proofs</b>
References: &lt;[e-mail]&gt;
</a>

The language U in Problem 1(Ex 7.23) is very similar to ATM, in the
sense it is &quot;universal&quot;. Use what you know about ATM to figure this one
out.

&gt; On problems 1 and 2 we need to show:
&gt; (a) that some language L is in NP
&gt; (b) that every other language in NP is &lt;=p L, either directly or
&gt;     indirectly by reduction from some known NP-complete language.
&gt; 
&gt; I'm having no problem with part (a), but I'm having a really difficult
&gt; time trying to find suitable reductions for part (b).  None of the
&gt; NP-complete languages we've covered in class seem suitable.
-- 
Jayram S. Thathachar                  [e-mail]
Department of CSE              http://www.cs.washington.edu/homes/jayram
University of Washington              [phone] (vox)
Box 352350, Seattle, WA 98195         [phone] (fax)
<hr size=4><a name="833384953001">Date: 29 May 1996 08:37 PDT
From: <b>Larry Ruzzo &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>Re: Handout 6</b>
</a>


  &gt; Date: Wed, 29 May 1996 08:25:45 -0700 (PDT)
  &gt; Subject: Handout 6
  &gt; 
  &gt; In Handout 6, problem 3c, I am getting a little lost in the notation.
  &gt; A few questions:
  &gt; 
  &gt; A)  Each x(i) seems to be each unique variable, made even more unique
  &gt;     by whether it is negated or not?

yes, there are m different variables.

  &gt; B)  &quot;Suppose 'x(i)' occurs in clauses numbered i(1),...,i(j)....&quot; 
  &gt;     Does this mean that the variable MUST occur in each clause 
  &gt;     between i and j, inclusive?  (Obviously, the same question applies
  &gt;     for the negated version.)

No, not &quot;inclusive&quot;: if x3 appears (not negated) in clauses 2, 3, 12
and 17, then j=4 and i1=2, i2=3, i3=12 and i4=17 and
a3=2+3+12+17=34.  (Really I should have used double subscripts or
something, because j and the the i_k's will likely be different for
each xi, but I was trying to keep it simple.); 

  &gt; C)  &quot;Let a(i) = (Summation from k=1 to j) i(k).&quot;  Does this mean that
  &gt;     a(i) is the number of times that a unique variable appears, including
  &gt;     p[Aossible repeats in a clause?  (Once again, same question for the
  &gt;     negated variable.)

as above, it's the sum of the clause numbers in which the variable
appears.

  &gt; D)  &quot;Let s = (Summation from i=1 to q) i.&quot;  Is this just the number
  &gt;     of clauses in f?

no.  s=1+2+3+...+q, where q is the number of clauses.

  &gt; Sorry about all the questions, but obviously I can't answer the 
  &gt; question if I don't understand the details!

No problemo.
<hr size=4><a name="833393843001">Sender: [e-mail]
Date: Wed, 29 May 1996 11:17:15 -0700
From: <b>Jayram Thathachar &lt;[e-mail]&gt;</b>
To: cse431@cs
Subject: <b>hws etc.</b>
</a>

I will hold special office hours tomorrow(Thursday) from 1-2 in Sieg
326(undergraduate lounge)for those  who need help on the problems due
Friday. 
Here is the plan for returning hws.

The graded hw4 will be handed back tomorrow during my office hours. I
will post the solutions today on the class web and also have copies of
it tomorrow. On Friday, I'll return hw5(whichever part was handed in
today) with the solutions to all the hw5 problems. Note that I also have
office hours on Friday from 1-2.

Since I will be moving to a new place, I will not be in school this
weekend. If you send me e-mail about clarifications, I'll try as much as