1David Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceClass 24: ComputabilityHalting ProblemsHockey Team Logo2CS150 Fall 2005: Lecture 24: ComputabilityMenu• Review: – Gödel’s Theorem– Proof in Axiomatic Systems• Computability:Are there some problems that it is impossible to write a program to solve?3CS150 Fall 2005: Lecture 24: ComputabilityGödel’s ProofG: This statement of number theory does not have any proof in the system of PM.If Gwere provable, then PM would be inconsistent.If Gis unprovable, then PM would be incomplete.PM cannot be complete and consistent!4CS150 Fall 2005: Lecture 24: ComputabilityWhat 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.5CS150 Fall 2005: Lecture 24: ComputabilityWhat 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.”6CS150 Fall 2005: Lecture 24: ComputabilityWhy is an InconsistentAxiomatic System less useful than an IncompleteAxiomatic System?27CS150 Fall 2005: Lecture 24: ComputabilityInconsistentAxiomatic SystemDerives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules.some false statementsOnce you can prove one false statement,everything can be proven! false ⇒ anything8CS150 Fall 2005: Lecture 24: ComputabilityProof• A proof of S in an axiomatic system is a sequence of strings, T0, T1, …, Tnwhere:– The first string is the axioms– For all i from 1 to n, Tnis the result of applying one of the inference rules to Tn-1– Tnis S• How much work is it to check a proof?9CS150 Fall 2005: Lecture 24: ComputabilityProof 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 Sfalse otherwise How much work is a proof-checking procedure?We can write a proof-checking procedure that is θ(n)10CS150 Fall 2005: Lecture 24: ComputabilityFinite-LengthProof 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.How much work?At worst, we can try all possible proofs:r inference rules, 0 - n steps ~ rnpossible proofsChecking each proof is θ(n)So, there is a procedure that isθ(nrn) but, it might not be the best one.11CS150 Fall 2005: Lecture 24: ComputabilityProof 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! “It might take infinite work.”Gödel’s theorem says it cannot be done.12CS150 Fall 2005: Lecture 24: ComputabilityComputability313CS150 Fall 2005: Lecture 24: ComputabilityAlgorithms• What’s an algorithm?A procedure that always terminates.• What’s a procedure?A precise (mechanizable) description of a process.14CS150 Fall 2005: Lecture 24: ComputabilityComputability• 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.15CS150 Fall 2005: Lecture 24: ComputabilityAre 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.16CS150 Fall 2005: Lecture 24: ComputabilityAny others?How would you prove a problem is undecidable?Hint: how did we prove 3-SAT was NP-Complete (once we knew Smiley Puzzle was?17CS150 Fall 2005: Lecture 24: ComputabilityUndecidable Problems• We can prove a problem is undecidable by showing it is at least as hard as the proof-finding problem• Here’s a famous one:Halting ProblemInput: a procedure P (described by a Scheme program) and its input IOutput: true if executing P on I halts (finishes execution), false otherwise.18CS150 Fall 2005: Lecture 24: ComputabilityAlan Turing (1912-1954)• Codebreaker at Bletchley Park– Broke Enigma Cipher– Perhaps more important than Lorenz• Published On Computable Numbers …(1936)– Introduced the Halting Problem– Formal model of computation (now known as “Turing Machine”)• After the war: convicted of homosexuality (then a crime in Britain), committed suicide eating cyanide apple5 years after Gödel’s proof!419CS150 Fall 2005: Lecture 24: ComputabilityHalting ProblemDefine a procedure halts? that takes 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) … )20CS150 Fall 2005: Lecture 24: ComputabilityExamples> (halts? ‘(lambda (x) (+ x x)) 3)#t> (halts? ‘(lambda (x)(define (f x) (f x)) (f x))27)#f21CS150 Fall 2005: Lecture 24: ComputabilityHalting 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)#f22CS150 Fall 2005: Lecture 24: ComputabilityCan 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?23CS150 Fall 2005: Lecture 24: Computabilityfind-proof(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.I cheated a little here –we only know we can’tdo this for “true”.24CS150 Fall 2005: Lecture 24: ComputabilityAnother Informal Proof(define (contradict-halts x)(if (halts? contradict-halts