Transcript S - University of Virginia

Class 19:
Computability
Halting Problems Hockey Team Logo
CS200: Computer Science
University of Virginia
Computer Science
David Evans
http://www.cs.virginia.edu/evans
Menu
• Quiz Answers (Questions 1-6)
• Review:
– Gödel’s Theorem
– Proof in Axiomatic Systems
• Computability:
Are there some problems that it is
impossible to write a program to
solve?
12 March 2003
CS 200 Spring 2003
2
Quiz Answers
12 March 2003
CS 200 Spring 2003
3
1. How far have you read in GEB?
– Through Ch 5 or less: 3
– Through Ch 6 or 7: 10
– All of Part I: 16
– Beyond Part I: 2, Whole Book: 1
• Reading GEB might not be necessary to get
a good grade in this class, but I really hope
you will read it and enjoy reading it!
• Ch 13 is the last assigned reading in it for
this class (but I hope you’ll read the rest
during your summer vacation!)
12 March 2003
CS 200 Spring 2003
4
2. Should Exam 2 be:
─ Similar to Exam 1
(“but should be harder”)
─ Like Exam 1, but allow DrScheme
─ In class, open notes
─ In class, closed notes
─ There shouldn’t be another Exam
17
10
0
0
10
Exam 2 will allow use of DrScheme, but probably not
expect it (unlike last year’s Exam 2, which you can
see on the web site).
12 March 2003
CS 200 Spring 2003
5
3. So far, class is going:
–Way too fast
–Too fast
1
11
“in a good way”
–Just about right
–Too slow
–Way too slow
12 March 2003
22
1
0
CS 200 Spring 2003
6
4. How far have you gotten in PS5:
– Finished
– Question 7
– Question 5
– Question 3
– Question 1
– Read it
– Haven’t started
12 March 2003
0
1
4
2
6
13
9
CS 200 Spring 2003
7
5. What should be different?
• “A couple fewer problem sets, but slightly more difficult ones
would be nice.”, “Less problem sets or less questions per
problem set. The problem sets are very time consuming (I
spend 20 hr/ps) for a 3-credit class.”, “shorter problem sets”
• “More help from TA’s”, “please have more TA hours. I wish
we’d have lab hours at least 2 hours a day, 4 days a week if
possible.”
– PS’s are long but they are as short as possible
– But many of you seem to think they are too short
and there are too many lab hours:
• 22/35 of you had not started PS5 14 days after it was
handed out!
• Only one person came to the 2 lab hours the first
week PS5 was out
12 March 2003
CS 200 Spring 2003
8
5. What should be different?
“Use more examples to explain concepts”, “clearer explanation of
Scheme code”, “More hands-on examples”, “Now that we know we can
code everything, use less coding and more theory and explanation”, “Go
slower and explain new concepts slower and throughout lecture since
each lecture builds on info already taught. If the first thing taught made
no sense to us, either will anything else.”, “The theoretic basis is
interesting and exciting, but the Scheme is slightly lacking”, “sometimes
confusing but that seems to be part of the plan”, “Breaking down info
more”, “Less fast”, “we tend to go a little bit too fast on certain concepts
and I think incorporating some more of the concepts that we learn into
real life examples would be helpful”, “More use of GEB into lecture
(relevance)”, “Maybe include questions from GEB on the problem sets.”,
“Something different than powerpoint, it is getting old”
Best way to get more examples, clarifications,
slower lectures: ask questions!
12 March 2003
CS 200 Spring 2003
9
6. What is Computer Science?
• A liberal art covering a wide range of disciplines
• Computer science encompasses all 7 of the liberal arts and
focuses on the manipulation of language and thought.
• Computer science is the epitome of a “liberal art”! It
combines rhetoric, logic, geometry, grammar, etc.
• A combination of all the components in liberal arts.
• In between science and liberal arts.
• A huge overall topic that is really hard to define in one sentence, but
brings in all parts of classical liberal arts.
• Not science, a liberal art.; A true liberal art.
•
•
•
A liberal art involving a lot of theory on logic and information and a bit on the
limitations of real systems or “computers”
Everything in fine arts and beyond…to a certain degree the way ideas are put
into code and expressed to the real world.
The study of problem-solving techniques.
Reasonable statements, but not really useful definitions.
12 March 2003
CS 200 Spring 2003
10
6. What is Computer Science?
• Imperative knowledge practically employed
• Study of “how” things are done, rather that “what”.
Understanding concepts deeper than the surface with
programs, etc…
• Study of the use of problem-solving strategies to manipulate machines
and systems to execute a given task.
• A way of creating logical systems to solve problems.
• Study of imperative knowledge.
• A science on the processing of information and its representation;
manipulation of the representations of information.
•
•
•
•
•
Study of systems of language and code. Also, the application of these.
Ways of manipulating information.
Study of the manipulation of systems and problem solving using formal
languages.
The study of processes and how they are written, understood and carried out.
Study of mechanical reasoning and its applications.
Good answers, similar to my definition in Lecture 1
12 March 2003
CS 200 Spring 2003
11
6. What is Computer Science?
• A study of how computers function, operate in a logical programmed way.
• The study of how to use a computer-like system and make it do what you
want it to.
• An attempt to solve real world problems with application of computers and
reason.
• The manipulation of computer memory to achieve a goal. The study of
logic.
• The use of language to represent any idea or procedure which can cover
topics from almost any discipline.
• Study of isomorphic mappings that yield discernable results to an
interpreter.
• Neither computers nor science, but the study and theory of formal
systems.
• I used to think it was the study of the software in computers, but now I’m
not really sure.
Interesting answers, but hard to defend.
12 March 2003
CS 200 Spring 2003
12
6. What is Computer Science?
Recursively speaking,
computer science is
the study of computer
science.
12 March 2003
CS 200 Spring 2003
13
What is Computer Science?
• My answer would be:
“Study of ways to describe procedures and
reason about the processes they produce.”
• My alternate answer:
“Playing with procedures.”
12 March 2003
CS 200 Spring 2003
14
5. What should be different?
“We should have some competitions, such
as writing a program to play tic-tac-toe.”
– PS6 is sort of a game; take CS201J for real
competitions
“We should have class in
different places more often,
maybe even outside”, “More
field trips!”, “More trips to the
AFC, so that we can be hassled
again.”, “More field trips.”
12 March 2003
CS 200 Spring 2003
15
Field Trip
12 March 2003
CS 200 Spring 2003
16
Review
• Axiomatic System
– Set of axioms
– Set of inference rules
• Example: MIU-System from GEB
– Axioms: MI
– Inference rules: 4 rules for making new strings
• An axiomatic system is a formal system
where the string we can generate are
meant to represent “true theorems”
12 March 2003
CS 200 Spring 2003
17
Proof
• A proof of S in an axiomatic system is
a sequence of strings, T0, T1, …, Tn
where:
– The first string is the axioms
– For all i from 1 to n, Tn is the result of
applying one of the inference rules to Tn-1
– Tn is S
• How much work is it to check a proof?
12 March 2003
CS 200 Spring 2003
18
Proof Checking Problem
• Input: an axiomatic system (a set of
axioms and inference rules), a statement
S, and a proof P containing n steps of S
• Output:
true if P is a valid proof of S
false otherwise
How much work is a proof-checking procedure?
We can write a proof-checking procedure that is  (n)
12 March 2003
CS 200 Spring 2003
19
Finite-Length Proof Finding Problem
• Input: an axiomatic system (a set of
axioms and inference rules), a statement
S, n (the maximum number of proof steps)
• Output: A valid proof of S with no more
then n steps if there is one. If there is no
proof of S with <= n steps, unprovable.
At worst, we can try all possible proofs:
How r inference rules, 0 - n steps ~ rn possible proofs
much Checking each proof is  (n)
work? So, there is a procedure that is  (nrn)
but, it might not be the best one.
12 March 2003
CS 200 Spring 2003
20
Proof Finding Problem
• Input: an axiomatic system, a statement S
• Output: If S is true, output a valid proof. If
S is not true, output false.
How much work?
It is impossible!
Gödel’s theorem says it cannot be done.
12 March 2003
CS 200 Spring 2003
21
Gödel’s Statement
G: This statement of number
theory does not have any proof in
the system of Principia
Mathematica.
G is unprovable, but true!
12 March 2003
CS 200 Spring 2003
22
What does it mean for an axiomatic
system to be complete and consistent?
Derives all true
statements, and no false
statements starting from a
finite number of axioms
and following mechanical
inference rules.
12 March 2003
CS 200 Spring 2003
23
What does it mean for an axiomatic
system to be complete and consistent?
It means the axiomatic system is
weak.
Its is so weak, it cannot express
“This statement has no proof.”
12 March 2003
CS 200 Spring 2003
24
Computability
12 March 2003
CS 200 Spring 2003
25
Algorithms
Question 5 answer:
“Perhaps we could try to look at other elements of computer science
like digital logic, algorithms, discrete math, etc.”
(CS230)
(CS202, CS302)
• What’s an algorithm?
A procedure that always terminates.
• What’s a procedure?
A precise description of a process.
12 March 2003
CS 200 Spring 2003
26
Computability
• Is there an algorithm that solves a problem?
• Decidable (computable) problems:
– There is an algorithm that solves the problem.
– Make a photomosaic, sorting, drug discovery,
winning chess (it doesn’t mean we know the
algorithm, but there is one)
• Undecidable problems:
– There is no algorithm that solves the problem.
There might be a procedure, but it
doesn’t always terminate.
12 March 2003
CS 200 Spring 2003
27
Are there any
undecidable problems?
The Proof-Finding Problem:
• Input: an axiomatic system, a
statement S
• Output: If S is true, output a valid
proof. If S is not true, output false.
12 March 2003
CS 200 Spring 2003
28
Any others?
How would you prove a problem is undecidable?
12 March 2003
CS 200 Spring 2003
29
Undecidable Problems
• We can prove a problem is undecidable by
showing it is at least as hard as the prooffinding problem
• Here’s a famous one:
Halting Problem
Input: a procedure P (described by a Scheme
program)
Output: true if P always halts (finishes
execution), false otherwise.
12 March 2003
CS 200 Spring 2003
30
Alan Turing (1912-1954)
• Published On Computable Numbers … (1936)
– Introduced the Halting Problem
– Formal model of computation
(now known as “Turing Machine”)
• Codebreaker at Bletchley Park
– Broke Enigma Cipher
– Perhaps more important than Lorenz
• After the war: convicted of homosexuality
(then a crime in Britain), committed suicide
eating cyanide apple
12 March 2003
CS 200 Spring 2003
31
Halting Problem
Define a procedure halts? that takes the
code for a procedure and an input
evaluates to #t if the procedure would
terminate on that input, and to #f if would
not terminate.
(define (halts? procedure input) … )
12 March 2003
CS 200 Spring 2003
32
Examples
> (halts? ‘(lambda (x) (+ x x)) 3)
#t
> (halts? ‘(lambda (x)
(define (f x) (f x)) (f x))
27)
#f
12 March 2003
CS 200 Spring 2003
33
Halting Examples
> (halts? `(lambda (x)
(define (fact n)
(if (= n 1) 1 (* n (fact (- n 1)))))
(fact x))
7)
#t
> (halts? `(lambda (x)
(define (fact n)
(if (= n 1) 1 (* n (fact (- n 1)))))
(fact x))
0)
#f
12 March 2003
CS 200 Spring 2003
34
Can we define halts??
• We could try for a really long time, get
something to work for simple examples,
but could we solve the problem – make it
work for all possible inputs?
• Could we compute find-proof if we had
halts?
12 March 2003
CS 200 Spring 2003
35
find-proof
I cheated a little here –
we only know we can’t
do this for “true”.
(define (find-proof S axioms rules)
;; If S is provable, evaluates to a proof of S.
;; Otherwise, evaluates to #f.
(if (halts? find-proof-exhaustive
S axioms rules))
(find-proof-exhaustive S axioms rules)
#f))
Where (find-proof-exhaustive S axioms rules) is a procedure that tries all
possible proofs starting from the axioms that evaluates to a proof if it
finds one, and keeps working
if it doesn’t.
12 March 2003
CS 200 Spring 2003
36
Another Informal Proof
(define (contradict-halts x)
(if (halts? contradict-halts null)
(loop-forever)
#t))
If contradict-halts halts, the if test is true and
it evaluates to (loop-forever) - it doesn’t halt!
If contradict-halts doesn’t halt, the if test if false,
and it evaluates to #t. It halts!
12 March 2003
CS 200 Spring 2003
37
This should remind you of…
Russell’s Paradox
• S: set of all sets that are not members of
themselves
• Is S a member of itself?
– If S is an element of S, then S is a member of
itself and should not be in S.
– If S is not an element of S, then S is not a
member of itself, and should be in S.
12 March 2003
CS 200 Spring 2003
38
Undecidable Problems
• If solving a problem P would allow us to
solve the halting problem, then P is
undecidable – there is no solution to P,
since we have proved there is no solution
to the halting problem!
• There are lots of practical problems like
this.
Example: why virus detectors will never really work!
12 March 2003
CS 200 Spring 2003
39
Virus Detection Problem
Problem 7. Melissa Problem
Input: A Word macro (like a program, but
embedded in an email message)
Output: true if the macro will forward the
message to people in your address book;
false otherwise.
How can we show it is undecidable?
12 March 2003
CS 200 Spring 2003
40
Undecidability Proof
Suppose we could define is-virus? that
decides the Melissa problem. Then:
(define (halts? P input)
(if (is-virus? ‘(begin (P input)
virus-code))
it is a virus, we know virus-code was
#t Since
evaluated, and P must halt (assuming P wasn’t a virus).
#f))
12 March 2003
Its not a virus, so the virus-code never executed.
Hence, P must not halt.
CS 200 Spring 2003
41
Undecidability Proof
Suppose we could define is-virus? that
decides the Melissa problem. Then:
(define (halts? P input)
(is-virus? ‘(begin ((vaccinate P) input)
virus-code))
Where (vaccinate P) evaluates to P with all mail
commands replaced with print commands (to
make sure (is-virus? P input) is false.
12 March 2003
CS 200 Spring 2003
42
Proof
•
•
•
•
If we had is-virus? we could define halts?
We know halts? is undecidable
Hence, we can’t have is-virus?
Thus, we know is-virus? is undecidable
12 March 2003
CS 200 Spring 2003
43
Charge
• PS 5
– Even if you take into account Hofstadter’s
Law and Byrd’s Law, it may be longer than
you think so get cracking!
• Friday, Monday:
Object-Oriented Programming (PS6)
• Wednesday, Friday (next week):
More about complexity (measuring
work) and computability.
12 March 2003
CS 200 Spring 2003
44