The following list goes through the course, summarizing the things you should know (i.e. memorize), and the things you should be able to do if asked in a question.

Things to know | Things to do |
---|---|

Register machine definition | Write short programs for RMs |

Argue for the Church-Turing thesis | |

concepts of Pairing functions and coding functions | design a coding function for some datatype |

simulate one machine by another | |

the Halting Theorem | prove the theorem |

Turing machine definition | sketch TM programs |

argue the equivalence of TMs and RMs | |

defn of computable function | |

defn of (decidable) decision problem | |

oracles | |

defn of many-one reduction | |

reduction from undecidable problem shows undecidability | prove the theorem; use the theorem on simple examples |

Uniform Halting | prove undecidable |

defn of (co-)semi-decidable | |

preservation of (co-)semi-decidability by m-reductions | prove this |

defn of computably enumerable | show that H and similar problems are c.e. |

Looping Problem | prove L is co-semi-decidable |

semi-dec and co-semi-dec => dec | prove this; prove L is not semi-decidable |

preservation of (co-)semi-decidability by reductions | prove UH or similar problems not (co)-semi-decidable |

big/little O and omega notation | simple analyses |

definition of P | show that algorithms/problems are in P |

argue for/against P as a good defn of tractable | |

defn of PTime-reduction | |

defn of P-bounded machines; redefn of P using these | |

defn of non-deterministic machines | write simple programs |

show that NRMs compute same functions as RMs | |

defn of NP by PTime-bounded RMs | |

guess-and-check defn; equivalence thereof | show problems in NP by guess-and-check |

defn of NP-hard/complete | |

preservation of NP-hard by reduction | prove this; use it in simple examples |

HPP, Timetabling as NP-complete | |

defn of SAT | |

Cook-Levin Theorem | prove in outline |

defn of 3SAT | reduce from 3SAT to other problem |

defn of CLIQUE | reduce from CLIQUE to similar problems |

NP-hardness of CLIQUE by redn from 3SAT | |

P=?=NP | |

ExpTime believed strictly bigger than NP | |

lambda-calculus syntax | write simple lambda-expressions |

alpha,beta,eta-conversion | do these |

call-by-name and call-by-value reduction strategies | use these |

simple extensions: if, arithmetic | |

concept of recursion | use Y operator if given |

simple types | |

typing rules | write types for lambda-expressions |

write a formal derivation tree for the type of an expressoin | |

properties of simple types (slide 85) | |

fix typing rule | write simple recursive functions with fix |

general scheme for extending language | write typing and evaluation rules for a new extension |

defns of let and letrec as syntactic sugar | use these |

concept of type inference | infer types `by hand' |

outline of type inference using variables | do inferences in outline |

type schemes/polytypes as quantified variable types | give polytypes `by hand' |

let(rec) as primitives | |

Hindley-Milner algorithm in outline |

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh |