Computability and Logic 2008

Turing machines and languages

Martin, chapter 9

Familiarity with terminology

• Martin 9.2 (use http://ironphoenix.org/tril/tm to check your solution)
• Martin 9.11
• Martin 9.35

Describe computability classes

• Martin 9.5
• Martin 9.6(b), 9.15 (a, b) (notice that the language from 9.6(b) is non context-free - for these exercises use again a one-tape TM and use http://ironphoenix.org/tril/tm to check your solution)
• Martin 9.18 and 9.19 (for these exercises you are encouraged to use multitape TMs)

Describe properties of computability classes

• Martin 9.33 (see the use of non-determinism: informal arguments only)

Slides:

[pdf]

Computability

Martin, chapters:

• 10.1-10.2 (365-371),
• 10.5 (387-397),
• 11.1-11.2 (407-416)

Describe properties of computability classes

• 10.1: show closure properties of R
• 10.3: RE closed under infinite union?
• 10.5: show that R is the same as "TM canonical enumeration"
• 10.35: RE closed under Kleene *

Describe countability properties

• 10.24: show that countability is closed under subsets
• 10.27: L uncountable, M countable -> L\M uncountable
• 10.29: alternative proof of countability of RE
• 10.31 (b,d,e,h): (un)countable sets?

Describe properties of non-computable problems

• 10.33: uncountably many "difficult" languages!

Analyze properties of non-computability

• 10.39: Non-existence of virus-tester!!

Competition

Construct a (deterministic) Turing Machine with

• three states
• a tape which is infinite "both ways"
• tape-alphabet {1}

Do the same for four states.

Test your solution on the TM simulator from last week.

Slides:

[pdf]

Unsolvable problems

• Martin, chapter 10.3 (without proofs)
• Martin, chapter 11.3-11.6 (without proofs of theorems 11.14 and 11.15)

Describe (un)decidability

• 11.3 Reduction theorem for RE
• 11.5 Fermat's last theorem
• 11.15 A non-trivial problem solvable for TMs
• 11.18 Example of PCP

Explain algorithmic approaches to computability

• 11.9 A TM reduction
• 11.13 Unsolvable problems for C-programs
• 11.19 PCP unsolvable for binary alphabets
• 11.20 PCP solvable for unary alphabets
• 11.21 Unsolvable problems for CFG (hint: use Thm 11.15)
• Slide 13 week 3: Show Busy Beaver function is non-computable, what happens if the output should be represented in binary? What about the input?

Slides:- [pdf]

Propositional logic

Kelly, chapters:

• 1 (1-26),
• 4 (65-93).

Describe the semantics of propositional logic

• Kelly page 14: 1.10 (i)-(ii): expressibility of nor and nand
• Kelly page 25: 1 (i)-(v), 2, 5 (i)-(ii), 6, 7: truth tables

Describe and construct deductions in AL

• Kelly page 92-93: 2 (i)-(ii), 3 (iv)-(v)

Analyze proof of completeness of AL

• Kelly page 90: 4.11

Slides:

[pdf]

Predicate logic

• Kelly chapter 6.1-6.7.4 (112-139), 6.9-6.10 (144-150)
• Kelly chapter 7.1-7.4 (153-165)
• Note: Limitations of Program Verification, Sections 1-3 (pages 1-10)

Lecturer: Gudmund Frandsen

Describe the semantics of predicate logic

• Kelly page 123 6.7 (scope rules)
• Kelly page 130 6.9 (expressiveness)
• Kelly page 136 6.12 (satisfaction)
• Kelly page 138 6.19 (satisfiability, truth, validity)

Describe and construct deductions in FOPL

• Kelly page 160 7.1 (i) (ii)

Describe and construct deductions for Hoare triples

• LimProVer page 10 Exercise 1

Slides:

[pdf]

Handouts:

Limitations of Program Verification (nu med referencer!)

Limitations of Program Verification, Sections 4-8 (pages 10-29)

All exercises in the following referring to the note Limitations of Program Verification [LiProVer08].

Describe representations of numbers

• [LiProVer08] 2 (p 16), 3, 4 (p 17) : understanding number representations
• [LiProVer08] 9 (p 23): understanding selection predicate

Prove limitations of formalization

• [LiProVer08] 5, 6, 8 (p 21): understanding the reduction to Hoare specifications
• [LiProVer08] 10 (p 27): understanding the reduction to predicate logic over the natural numbers

Slides:

[pdf]

dBerLog: A Summary and the Exam

Slides:

[pdf]