| Week 1 | | | Week 5 | | | Week 9 | |
| Week 2 | | | Week 6 | | | Week 10 | |
| Week 3 | | | Week 7 | | | Week 11 | |
| Week 4 | | | Week 8 | | | Week 12 |
In our first session, Eric gave us the primary intuitions of computation and programs. For our best understanding, he explained some of Gödel’s incompleteness theorems' implications and shortly exposed the Berry’s Paradox to show us some of the problematics involved in expressive languages. He also explained the Turing’s and Church’s responses and took the opportunity to teach us the correct notion of computability, very related to sets of numbers. We demonstrated Cantor’s diagonal argument, which shows that we can’t enumerate the set of infinite binary sequences, because there will always be a sequence not included in the enumeration. Returning to Turing’s proposes, we saw an encoding of programs with a sequence of prime numbers, and we looked more closely at how it involves the Halting problem.
This session was divided in two parts. The first one was led by Gina and was focused on proofs in mathematics. We recalled we can make a direct proof by assuming the antecedent and showing the consequent, by contraposition and by reduction ad absurdum. However, our target was induction, hence we did some exercises regarding induction on the natural numbers. Gina also explained how the recursive functions work and introduced “natlists”. The second part of the session was led by Eric. He began explaining the origin of λ-Calculus and Combinatory logic and introduced Untyped λ-Calculus, defining its terms and notation as well as other important concepts like “multi-set” or the different kinds of variables.
Eric used this week’s session to provide us with the definitions of the necessary notation for λ-calculus so we can, in the next session, begin the more interesting questions apart from syntax. We saw the corresponding definitions of the strict-equivalence, the α-conversion or α-equivalence (=α), the variable substitution , the λ-terms substitution (named simply 'substitution'), the one-step β-reduction (→β) and the β-reduction (zero-or-more-step). Finally, to expand our knowledge about the ß-reduction, he explained what’s a reducible expression (also known as a Redex), a ß-normal-form (usually abbreviated as ß-nf) and the ß-equivalence.
This session was led by Eric. He began introducing some important notions related to β-reduction, like the Church-Rosser Theorem. Later he defined the Church numerals and showed us its relation with the “successor” function. In order to get better understanding about the basic functions that take Church numerals as arguments, like “successor”, “add” and “mult”, Eric asked us to find ourselves the formulation of these λ-terms, with satisfactory results. Finally, we talked about fixed points in λ-Calculus, analysing the Fixpoint theorem and presenting the Curry fixed-point combinator and the Turing fixed-point combinator. Eric anticipated us the fact that every λ-terms had a fixed point is a crucial feature for the computable results.
Guillem exposed partially the Benedetto Intrigila and Richard Statman's article Fixed points in lambda calculus. First, he shows us that the fixed point theorem needs to be understood as a restrictive principle, and how this turns us to another problem. Second, he demonstrated the existence of a fixed point by an interpretation of λ-calculus as a programming process. Then, Eric quickly explained us how to form the factorial product within λ-terms, using the recursive processes and the fixpoint. Finally we put in common the ideas emerged from the investigation, the principal objective of this week meeting and for what we did not do the session of the course.
We had a work meeting, for this reason we didn't a session with theoretical content.
We didn't take this week's class. We went to the Law Faculty of the UB to listen a series of presentations about the emergent problem of the Artificial Intelligence and Software for lawyers. The Joost's one was titled The Logic Road to Software Homologation.
(no class.)
The session was led by Eric. He began explaining the problems associated with the untyped λ- Calculus to indicate is justified study the typed λ-Calculus. He showed us the Barendregt's Cube and specified the new goal: understand simply typed λ-Calculus. Then he proceeded to define the variables, the terms, the types and the notation in the simply typed λ-Calculus, as well as the derivation rules associated. We also saw some concrete propositions in order to apprehend better the consequences of the typed λ-Calculus. Finally, Eric mentioned the decidable problems of simply typed λ-Calculus.
We continued the Simply typed λ-calculus' theory: first, we demonstrated that any term M has not more than one type, by induction on the construction of M; then we played with our intuitions and tried (and did so) to find the appropriate terms for a set of types; we also saw some general properties of λ→; and, finally, we took the last minutes to practice derivation by natural deduction.
The session was led by Eric. He began introducing the BHK interpretation of Intuitionistic Propositional Calculus (IPC). Then he presented the Curry-Howard Isomorphism and we tried successfully to proof it. In the second part of the session we enlarged the language of simply typed λ-Calculus, as well as the derivation rules associated. To conclude the temary we saw in concrete the parallelism between simply typed λ-Calculus and IPC reduced to the conditional. Finally, anticipating the next session, Eric showed what is the Calculus of inductive Constructions, used in Coq.
Eric, Gina and Aleix showed us the basic notions for Coq program. Firstly, we used the Inductive command to define the sets of natural numbers, of natural numbers' lists and of Booleans. Secondly, we introduced the Fixpoint command and used the previous definitions, with which we described some functions, by one side, on the set of natural numbers and, by another side, on the set of natural numbers' lists.
This session was directed by Eric. First, we saw how to declare variables and distinguish sections in Coq. Then Eric explained how to define the induction principle with a “Fixpoint” function, and we remembered that we can check the induction principle of any Type defined in Coq. In the second part of the session we worked with propositions, like “False” and “True” propositions, and observed some consequences involved with the Curry-Howard Isomorphism. Finally, Eric showed some new tactics.
Final task for grading. It consisted in solving some longer Coq exercises which were designed to exemplify a fragment of the process of developing formally verified software.
Website maintained by Júlia Pla, Guillem Muñoz, Eric Sancho and Joost Joosten.