Principal Type algorithm and correctness. Type substitutions and unification, Robinson's algorithm, the matching problem. Pointer to literature on PCF as the obvious extension of simple types to cover all computable functions. Consequences: no fixed point combinators, poor definability power. Briefly, a system with type invariance under equality. Subject Construction Lemma, Subject Reduction Theorem and failure of Subject Expansion. Simple type assignment a la Curry using Hindley's TA lambda system. Abstraction algorithm, combinatory completeness, translations to and from untyped lambda-calculus, mismatches between combinary logic and lambda-calculus, basis. Second Recursion Theorem, Scott-Curry Theorem, undecideability of equality in lambda beta. Statement, without proof, of Genericity Lemma, and simple applications.Ĭhurch numerals, definability of total recursive functions. Proof that leftmost reduction is normalising. Reduction strategies, head and leftmost reduction. Inconsistency of equating all terms without beta-normal form. beta-reduction, proof of the Church-Rosser property (via parallel reduction), connection between beta-reduction and lambda beta, consistency of lambda beta. Compatible closure, reflexive transitive closure, diamond and Church-Rosser properties for general notions of reduction. Terms, free and bound variables, alpha-conversion, substitution, variable convention, contexts, the formal theory lambda beta, the eta rule, fixed point combinators, lambda-theories. Preparation for use of inductive definitions and proofs. understand how to deduce types for terms, and prove correctness of a principal type algorithm.learn about simple type systems for the lambda-calculus, and how to prove a strong normalization result.see the connections and distinctions between lambda-calculus and combinatory logic.see the connections between lambda-calculus and computabilty, and an example of how an undecidability proof can be constructed.learn techniques for analysing term rewriting systems, with particular reference to beta-reduction.be exposed to a variety of inductive proofs over recursive structures.understand the syntax and equational theory of the untyped lambda-calculus, and gain familiarity with manipulation of terms.The course is an introductory overview of the foundations of computer science with particular reference to the lambda-calculus. Some basic knowledge of computability would be useful for one of the topics (the Models of Computation course is much more than enough), but is certainly not necessary. There are no prerequisites, but the course will assume familiarity with construting mathematical proofs. As such, the course will also function as a brief introduction to many facets of theoretical computer science, illustrating each (and showing the connections with practical computer science) by its relation to the lambda calculus. Topics covered include the equational theory, term rewriting and reduction strategies, combinatory logic, Turing completeness and type systems. This course introduces the terminology and philosophy of the lambda calculus, and then covers a range of self-contained topics studying the language and some related structures. It is folklore that various forms of the lambda calculus are the prototypical functional programming languages, but the pure theory of the lambda calculus is also extremely attractive in its own right. The lectures for this course will be pre-recorded and can be found here.Īs a language for describing functions, any literate computer scientist would expect to understand the vocabulary of the lambda calculus. MSc in Mathematics and Foundations of Computer Science Schedule S1(3rd years) - Computer Science
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |