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).
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.
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.
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.