Functional Data Structures

Prof. Tobias Nipkow, Dr. Mohammad Abdulaziz, Summer semester 2020

• Module: IN2347 SS20
• Lectures: 2 lecture hours per week, Fri 8:30-10:00 MI Hörsaal 2
• Tutorials: 2 lecture hours per week, Fri, 12:15-13:45 MI Hörsaal 2
• Start of lectures: first week (April 24). Start of tutorials: first week (April 24)
• Tutors: Mohammad Abdulaziz

The course introduces students to the design and analysis of data structures for functional programming languages. It assumes that the students are familiar with functional programming and with running time analysis of algorithms. The course covers a range of functional data structures with an emphasis on their precise analysis. Proofs of both functional correctness and complexity will be a core part of the course. Proofs are carried out with the help of a computer-based proof assistant Isabelle. An introduction to Isabelle is part of the course.

There is an emphasis on search trees and priority queues, but the syllabus is still evolving.

At the end of the course students should be familiar with a number of efficient functional data structures and algorithms and should be able able to prove both functional and complexity properties about them with the theorem prover Isabelle.

On this page: Important notices News Written Material Lectures Homework Literature

Final Exam

General Format

The exam will take place online: you will receive exercises, solve them on your own at home, and then submit the solutions to the Isabelle submission system used for the homework. You must have an account in the system and send the tutor Mohammad Abdulaziz an e-mail from your TUM account with your submission system username before the exam.

You must work on the exam on your own. The exam is open book (including the internet), but you must not, in any way, get help by someone else (in person, chat, forum, discussion group, etc.). Doing so is classified as cheating ("Unterschleif") and leads to consequences as mentioned in the APSO ("Allgemeine Prüfungs- und Studienordnung"). In particular, the exam will be marked as failed with cheating.

If we have reasons to doubt that you solved the exercises yourself, we may schedule an additional oral exam on short notice. Failing the oral exam means failing the whole exam with cheating.

There will be a dry run closer to the exam date.

Further details will be published here and sent by email to all students registered for the exam.

Exam Instructions

We expect valid Isabelle proof scripts to be submitted as a solution to the questions of this exam. Major proof steps, especially inductions, need to be stated explicitly. The use of "sorry" may lead to the deduction of points but is preferable to spending a lot of time on individual proof steps.

Please submit your solution via the submission system and ALSO via email to mansour@in.tum.de. You have to include your final answer to all questions in one email. If you do not submit the exam by the deadline (10 minutes after the official end of the exam) either via the submission system or via email you will have failed the exam (X = no show = 5,0). The solutions you send by email are primarily intended as a backup in case of technical problems. Unless you state explicitly that we should grade the email submission (and it was submitted in time), we will grade the submission on the submission system.

In the unlikely event that you discover a mistake in one of the questions you should communicate this to nipkow@in.tum.de and mansour@in.tum.de. We will communicate any corrections to the exam questions by email to you. Thus you do need to watch your email at regular intervals.

Also, if you encounter unforeseen technical problems during the exam, you can send an e-mail to nipkow@in.tum.de and mansour@in.tum.de.

Important notices

Prerequesites

• You must be familiar with some functional programming language like Haskell, Objective Caml, Standard ML or F# (e.g. Functional Programming and Verification (IN0003)).
• You must have taken a first course on data structures and algorithms (e.g. Fundamentals of Algorithms and Data Structures (IN0007)).
• You must have taken some basic course in discrete mathematics where you learned about sets, relations and proof principles like induction (e.g. Discrete Structures).
• You need not be familiar with formal logic but you must be motivated to learn how to write precise and detailed mathematical proofs that are checked for correctness by a machine, the theorem prover Isabelle.

Homework, exam, grading:

Throughout the course there will be homework assignments. They will involve the use of Isabelle and will be graded. At the end of the course there will be a written or oral examination, depending on the number of students. The final grade will combine the grades from the examination (60%) and the homework (40%).

Plagiarism:

Discussing ideas and problems with others is encouraged. When working on homework problems, however, you need to solve and write up the actual solutions alone. If you misuse the opportunity for collaboration, we will consider this as cheating.
Plagiarizing somebody else's homework results in failing the course immediately. This applies for both parties, that is, the one who plagiarized and the one who provided his/her solution.

Language:

All lectures are in English.

Isabelle:

Please install Isabelle 2020 on your computer. You will need Isabelle for (almost) everything, in particular tutorials and homework.

News

• Until further notice, all lectures and tutorials take place online only. In particular the lectures will be replaced to a large extent by recorded material. Also, every Friday at 13:00 we will:
  • Upload a tutorial video online and provide its link on this webpage.
  • Add a sheet that contains the tutorial exercises and the homework to the github repository. Homework solutions should be uploaded to the competition system in the link below by the next Friday at 10:00.
  After watching the uploaded video lecture and tutorial, you can ask questions on the Piazza course page. We will answer most of the questions you post textually on Piazza. For questions about the lecture that cannot be answered textually, Prof. Nipkow will upload a video answering them. He will upload these videos every Tuesday, and they will concern the lecture uploaded on the preceding Friday. For some questions about the tutorial, we might ask you to join this BBB meeting room so that an instructor interactively answers you.

Written Material

All written material (lectures notes, slides, demo material, exercises, homework, ...) will be provided via a github repository, such that you can easily keep up to date.

Lectures

Until we can all meet safely in the classroom again, all lectures are will be replaced by video recordings of the same. We will use a mixture of TTT recordings from previous years (2018, 2019) and new recordings. For each Friday (when the lecture would take place) we list which recordings to watch and what to read up to that date: <.ul>

24.4.: Watch #01 from 2018, read up to/incl 2.2.5 in prog-prove.pdf.
Note: at the very end of the lecture I could not demo the last proof (because of a problem with the projector). Do look at the full proof in Demos/List_Demo.thy.

1.5.: Watch #02 from 2019, read up to/incl 2.5.3 in prog-prove.pdf
Note: May 1st is a holiday, but we ignore this because classes do not take place on a fixed day at the moment. Promise: we will not cover more material than last year and most likely we can finish one week earlier as a result.

8.5.: Watch #03 from 2019, read up to/incl 3.3 in prog-prove.pdf

15.5.: Watch #04 from 2019, read up to/incl 4.1 in prog-prove.pdf

22.5.: Watch #05 from 2019, read up to the end of prog-prove.pdf

This is the beginning of Part II of the course: Functional Data Structures. In addition to the videos there are the slides slides-fds.pdf and a textbook-in-progress book-fds.pdf.
NB: The videos are of last year, but a few details have changed since then, for example in red-black trees. The definitive references are the 2020 theories, the slides and the textbook.
29.5.: Watch #06 and #07 from 2019 (there is an interruption after 10 minutes), read book-fds.pdf up to the end of 2.4 but without 2.3.

5.6.: Watch #08 from 2019, read chapters 4, 5 and 6 in book-fds.pdf restricted to the material covered in the lecture.

12.6.: Watch #09 from 2019, read chapters 7 and 8 in book-fds.pdf restricted to the material covered in the lecture.
Note that the deletion function on red-black trees shown in the lecture is the one in 8.2.3. Instead of studying the details of deletion in red-black trees read 5.2.1 on two general methods of deletion in trees.

19.6.: Watch #10 from 2019, read chapter 13 in book-fds.pdf.

26.6.: Watch #11 from 2019.

3.7.: Watch #12 from 2019.

10.7.: Watch #13 from 2019.

17.7.: Watch #1 from 2020.

• The slides for this topic have been extended. Please get the latest version.
• This topic has moved to the end of the course by accident. It does not mean that it is unimportant, quite the opposite!

Tutorials

• 24.4.: Watch this video
• 1.5.: Watch this video
• 8.5.: Watch this video
• 15.5.: Watch this video
• 22.5.: Watch this video
• 29.5.: Watch this video
• 5.6.: Watch this video
• 12.6.: Watch this video
• 19.6.: Watch this video
• 26.6.: Watch this video
• 3.7.: Watch this video
• 10.7.: Watch this video
• 17.7.: Watch this video
• 24.7.: Watch this video
• Mini-Project Presentations: Watch this video

Homework

Homework is the heart and soul of this course. It is provided in the repository and needs to be carried out with Isabelle.

• Solved homework should be uploaded to the submission system according to the following instructions.
  • Register an account in the system and send the tutor an e-mail with your username.
  • Select the competition "FDS2020" and submit your solution following the instructions on the website.
  • The system will check that your solution can be loaded in Isabelle2020 without any errors and reports how many of the main theorems you were able to prove.
  • You can upload multiple times; the last upload before the deadline is the one that will be graded.
  • If you have any problems uploading, or if the submission seems to be rejected for reasons you cannot understand, please contact the tutor.
  General hints:
  • If you cannot prove a lemma, that you need for a subsequent proof, assume this lemma by using sorry.
  • Define the functions as simply as possible. In particular, do not try to make them tail recursive by introducing extra accumulator parameters -- this will complicate the proofs!
  • All proofs should be straightforward, and take only a few lines.
• Make sure that your submission gets a "Passed" status in the system. We will not grade it otherwise!
• The latest submission date is given on each exercise sheet. Late submissions will not be graded! If you have a good excuse (such as being very sick), you should contact the tutors before the deadline.
• Discussing ideas and problems with others is encouraged. When working on homework problems, however, you need to solve and write up the actual solutions alone. If you misuse the opportunity for collaboration, we will consider this as cheating.
  Plagiarizing somebody else's homework results in failing the course immediately. This applies for both parties, that is, the one who plagiarized and the one who provided his/her solution.
• Important: all homework is graded and contributes 40% towards the final grade.

Literature

There is currently no book that covers the material of the course. However, this is the canonical reference to functional data structures:

• Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999.