Thesis on Lean and Relational Algebra

Stream: new members

[Rick van Oosterhout]

Hello everyone,

My name is Rick van Oosterhout, I am a Master’s student in Computer Science and Engineering at the University of Technology Eindhoven. I have recently started my thesis on formalizing the relational algebra using Lean. The main goal of this thesis will be to prove the equivalence between first-order logic and the relational algebra. Given that I am currently working on my literature survey and initial experiments, I thought it would be helpful to reach out to more experienced Lean users.

For me this will be my first project using Lean. I have worked with Coq and Haskell before, so many concepts should not be new to me. However, I have noticed that there is a lot to learn, before I can work on the implementation of the project.

If anyone has any relevant sources, useful suggestions and starting guides or immediate feedback, feel free to join in on this conversation. I have already collected a number of resources and set up some initial experiments. But I would love to get some more insights from those who are more experienced with Lean.

[Johan Commelin]

Welcome! Do you already know about #tpil ? That's one of the standard sources.

[Marcus Rossel]

I also had to learn Lean for my Bachelor's thesis, and going through #tpil was very helpful!

[Rick van Oosterhout]

Thanks for the suggestion! I definitely came across that book a few times already during my literature survey and first experiments. It indeed seems very useful to get started with my thesis.

[Martin Dvořák]

Is https://github.com/AviCraimer/relational-calculus-library-lean4 related?

[Rick van Oosterhout]

Martin Dvořák said:

Is https://github.com/AviCraimer/relational-calculus-library-lean4 related?

This seems very interesting and definitely related to what I will be working on. I will look into this and see how usefull it will be when I get more hands-on with Lean. Thanks!

[Rick van Oosterhout]

After a closer look at the repository you mentioned, I figured that it might not be as useful as I thought initially. The term relational calculus has a very different meaning in database theory, which made me optimistic initially. However, I am afraid that the calculus of relations does not really relate with the database theory concepts.