2020 Lambda-Calculus and Type Theory Revisited (Official course code: 361146)

Organisation

The organizers of the course are Aleix Solé Sánchez, Eric Sancho and Joost Joosten. The course content is heavily based on the, 2019 edition, which in turn was based on the excellent 2017 edition, prepared and delivered by Ana Borges and Nika Pona, and incorporates their kind suggestions and help. The lecturer of the course is Eric Sancho.

The aim of the course is to learn what is behind the scenes when using proof-assistants. This course is part of the apprenticeship project of the UB and as such the students will have to develop notes that can be used for future hires of the company. Apart from taking notes and learning the material and challenging the lecturers, there are several other company-oriented tasks to be performed by the students. This project constitutes for 6 European Credits so that the students are to dedicate 120 hours to it. As usual, we decided to spread this out in 12 weeks of 10 hours dedication per week. However, due to the COVID19 pandemic, this year most of the course took place in dialogue form via online communication and through assembled lecture notes for the students to work with and study, as well as a heavier load of homework and feedback than other years. However, a minimum of online lectures was considered essential and have thus been held during lock-down.

Lecture 1

(Week: Mar 02 -- Mar 6)

The lecture was kicked off by Joost, with an introduction to the aim of the company and the applicability of complex mathematical theories. It has been talked, inter alia, about Russell Paradox, isomorphisms, and type theory, that is, the kind of formal system with which Formal Vindications works. The rest of the session was led by Eric, who began by giving an outline of the evaluation methodology and schedule of this internship. Then, he followed with an exposition aimed to answer the fundamental question: “what is computation?” Three keywords were given: information, transformation and instructions. To give a bit of background, the origins of computation stems from a matter that was addressed some time ago: thinkers like Descartes, Hegel or Hilbert believed in the equivalence between truth (as adaequatio) and demonstrability. However, in 1931 Gödel ends with this conception by showing that (i) if we have a formal system that is expressive enough and consistent, then it isn't complete (there are some mathematical truths that can't be demonstrated); (ii) the own consistency of this system is indemonstrable. To reinforce this idea, we have seen Berry's Paradox. Next, Eric defined computation as a science that studies everything that belongs to the range of calculability and mentioned another approximation given by Church and Turing (Church-Turing Thesis). It states that a function on the natural numbers can be calculated by an effective method if and only if it is computable by a Turing machine. Finally, we ended the session by an explanation of Cantor’s diagonal argument to see that there are infinite sets with different cardinalities (for instance, the set of real numbers is bigger than the set of natural numbers).

Lecture 2

(Week: Apr 06 -- 10)

Due to Covid-19 pandemic and the subsequent restrictions we are unable to have face-to-face meetings, but we managed to do an online class. Today’s lecture was led by Eric and it revolved around the topics we have been working on via e- mail for the last two weeks: inductive definitions, inductive demonstrations, recursive demonstrations and lambda-calculus. We solved our doubts on those subjects and we reviewed the theory related to them.

Lecture 3

(Week: May 11 -- 15)

By means of online class, we have had today a class that has let us clarify the most important definitions of the lambda-calculus. First, we treated the beta-equivalence, concluding that its meaning is that both parts of it are the same, always respecting the free and bound variables. In addition to equivalence, we also talked about substitution, looking for the difference between a necessary reduction and an unnecessary one. After that, Eric introduced us some new concepts like the number’s concept, showing us the definition of succession trough an exercise. Finally, we learned how lambda-calculus models the behaviour of functions, but always with lambda-terms that have a fix point. With this information, we can make a beta-reduction that let us make recursive functions in lambda-calculus.

Lecture 4

(Week: Jun 22 -- 26)

The last online lecture was led by Eric and started with a quick doubt resolution on the content we have been working on since last class, that is, Booleans and type theory. Then, we have been introduced to intuitionistic logic and the Brouwer-Heyting-Kolmogorov interpretation to subsequently get a grasp on the Curry-Howard interpretation. Afterward, to close the theory part of the course, Eric has pointed out the different theoretical systems that constitute the lambda-cube as a way to give us a bigger image of logic (indeed, lambda-calculus) and its multiple paths. Eventually, we've discussed and agreed that it would be great to extend our internship (even though, in the end, it has not been possible) and shared our thoughts about this experience, giving some feedback to Eric and vice-versa.


Website maintained by Robert Carles Marqueño, Carlos Cantero de Arriba, Laia Barceló Moll, Eric Sancho and Joost Joosten.