Karim:
In August, several team members took some well-deserved personal time off. But nonetheless we’ve managed to have several important milestones especially on the TML side. First on the Agoras Live side, Andrei was working mainly on the reviewing system for user and teacher reviews. He got that working and we’re in the process of testing that. He always continues to fix some small issues that come here and there, but the platform in general. He also installed another video conferencing server, so we can use that for a dedicated team server for testing these calls.
Juan continued his work on first order logic together with Umar. Most importantly, he’s close to wrapping up a first iteration of the second order logic solution. We’re all looking forward to seeing that next week. He’s going to demo it internally. Umar continued his great work on the conversion to a universe of size 2, and he included handling of inequalities and he’s making improvements to the arithmetic. He continues to improve the type system with the nested type environments. Tomas continued his work on the IDE and especially the syntax highlighting in Visual Studio code and the Vim editor. He most importantly also helped Umar test the conversion to binary size universe.
Murisi as usual has delivered some great features, where most importantly he actually fixed some old code that Ohad had written a long time ago for the proof of extraction. I cannot overestimate the importance of that feature. He also continued working on the safety checking and performance improvements and Z3 containment as well.
Prof. Benzmüller:
This month in the academic discussions, we were looking at the proposal by Ohad on a solution for our language and the knowledge representation framework. We assessed it again with some concrete examples and compared it with an alternative solution, we are currently also looking at. By the comparison, I think we in particular will make further progress on the pros and cons of both approaches and now how far exclusivity reaches here. It’s an interesting stage of development. I think by this mixture of theory development or theoretical ideas and looking at the same time at concrete examples. This is actually an enabler for hopefully a finite pick in the end.
On the side of tier improving development or reasoning system development, I’ve been looking this month a lot into equational reasoning. I improved my program a lot, the system I developed I mentioned in the meetings before it’s a team improving system and the model finding respectively counter model finding system that’s also capable of reasoning modulo varying domain cardinalities. This makes it relatively complicated in combination with equational reasoning to get these things right. I’m at the moment still in a final debugging phase. Setting up examples and then checking whether they run. But already by comparing for instance also my developments with the alternative developments by others in the project. We also can exchange very useful insights about not only how to debug the systems but also debugging them on a concrete basis.
I think it has been very fruitful. For instance in today’s meeting and already last week when we presented the work here. I guess I will make the code very soon publicly available that I’ve reduced on and then also can offer a better prepared demo if people are interested. I think that are the main points to report here for this month. I have been also a bit slowed down by a lot of conference organization work as a co-chair of a major conference, but I leave these things aside here.
Murisi:
So, this month, I identified and fixed bugs in some of the transformations within the TML engine and yes, these were kind of discovered through extensive testing. These are kind of corner cases we hadn’t run into yet. I also worked on improving the safety checking mechanism in TML. I did this with a particular focus on the uniqueness quantifiers. I was kind of making sure that the uniqueness quantifiers passed through the safety check without any complaints.
Juan:
This month we are reaching a better situation with the second order logic feature. Where we are as we describe this strategy a couple of months ago where we are handling dual sets of constraints for each second order variable. So, with that in mind, we are able to create an Algebraic structure that represents all of these constraints for the second order variables. We are also starting to quantify over this structure in order to get the models which are fulfilling or satisfying the second order formulas that we are currently handling. This mechanism is of course very related with all hat’s Boolean Algebraic developments and exposition that have been doing for the team for many months before.
Also, borrowing ideas from Professor Benzmüller: Acquisitions about the relevance of unification and particularly the relevance of having a solid first order logic feature in order to get into the second order logic. That’s why I also put some further effort into improving the test suite for first order logic, clearing some issues that were still there. I would say the general approach that we are following is to dig deeper into our problems to figure out how we can integrate these capabilities into the overall TML framework, into the TML language. Once we confirm that our strategy is somehow feasible in our environment, of course we need to gain confidence on the implementation by expanding the test suite and clearing any remaining issue back that we do not clear from scratch or we don’t design from scratch.
That’s how the first order logic feature happened to be. We just started with a couple of very basic tests which we were able to handle with our primitive solvers. And for second order logic that’s more or less the same strategy, we started with a few numbers of the second order formulas that we are handling right now in the proper way. And we expect to enlarge or grow the capabilities of this solver in the coming future to get a fully functional solution. This development is at least from my understanding it will be eventually very relevant for the Tau system. That’s why we have been putting so much energy on this.
So, that’s looking forward to demoing it first internally for the team during this month and eventually do demos as we did for the community, as we did for first order logic before. And I also have been doing some work on our blockchain backend expanding our wallet capabilities and reviewing some stuff related to our blockchain backend.
Andrei:
Summer has gone but a very productive platform is waiting ahead of us. Finally, better late than never we’ve come to the very edge of giving away our Agoras Live platform to external testing. As I’ve covered all basic parts of the platform with necessary improvements and fixed all visible issues we had on the platform. [ https://youtu.be/MmTt1UrwZfA?t=739 ] This August, I remade the review system of Agoras Live. Now the review system is forcing you to review your past experiences, no matter where on the platform you browse or you may close the platform and later come back and it will ask you. This review system stores all reviews in a separate database and it asks you for a review based on your permissions.
For example, a teacher can’t review his own group call. A teacher can review his experience with the students and students can review the teacher and a group call they’ve had. Next necessary improvement was the ability to end the call outside the session. For example, you close your video conferencing with the teacher or teacher closes the video conferencing with you. And you now can end this conference call from within Agoras Live platform with this button. Next small improvement is to join the group call. If you are a teacher then I made sure that all necessary controls over your calls over your appointments are located in one place and now you make your calls with students from your account sessions here.
Last thing I created a separate video conferencing platform for better testing. Now we have a platform for active development and the platform for better testing. More or less everything is ready for testing finally.
Tomas:
In August, I’ve been working on making TML’s rapl work in a browser and making it work as a backend for the editor. Which would allow running TML programs by steps. This is to make debugging of TML programs a little bit easier. I’ve been working on fixing bugs in the TML online editor. I’ve updated the ‘node.js’ libraries and fixed new issues with building the web application. I also fixed build issues of a JavaScript version of the latest TML. I’ve also spent some time on testing new features like bit universe. So, that’s all from me this month.
Umar:
This month I have been working on improving the types checking and type inference in a way that now we can have types of different nested programs connected. So, if you search for a type in the nested program, the search will try to find it in the parent scopes as well. And similarly, if you search a type in the parent scope, it will go towards a nested scope as per the desired bit sizes or the number of AGRS. So, this is important because then this allows you to be able to return your facts that are derived from the BDD, back to the original program while keeping these types available during the conversion. Other than that, I’ve been looking into improving some of the contextual information that is available for the arithmetic terms.
When we are trying to determine the number of bits for a number, that doesn’t have a type but we derive a type based on the context of the wires where it’s surrounded by. There was a bug we improved on there. Then there were several tests and fixes that were made. So, the overall workflow of converting the program to the bit universe and then converting it down to the raw level then to the term level and then down to the BDDs. And then reconstructing the facts from the terms and from the BDD back to the original program. That workflow is complete except that there is some handling that is related to arithmetic terms and first order logic. They are in the pipeline. I’ll be working with other developers to ensure that the expectation is met there.
In future, this was one way of handling the bit universe transformation; a cleaner and a faster and optimized way could be. To not express this transformation at the raw level, but instead just add this information within the tables and within the signature of the tables directly. So, that is still a concept, but I will share that with the lead developers and the peer developers.
Ohad:
Last time, I spoke about a logic which offers a lot of new stuff and solves a lot of problems at the scope of Tau. And from there, we continue into forms. First, it is not one logic, it can take large families of languages and extend them to support their self-referential methodological features. We need to choose which logics to extend and that’s based on the theoretical front and ongoing discussion with the academic partner. And in the practical font, I started writing the code implementing this language and it is much more complex than TML. Both from the point of point of view and also from the backend point of view. Just writing a parser for that language is terrible. So, instead I just wrote a generic parser for any grammar and it’s a kind of parser called an early parser. The parser already works; at least the recognizer part works. Now I just need to finish the part of BDDs to parse these.
That’s an advancement also as now we can replace TML parser with this parser, which will be much faster and much easier to maintain. I look forward to finishing this. One thing I forgot to say is that the logic I spoke about last time is just a logic, but Tau is about programs. So, how do we connect it to programs? We decided to follow the common practices from the world of functional programming languages. It will be a functional programming language with the major twist that functions including higher order functions are restricted to be what is called only Boolean functions.
Many people understand the term Boolean functions differently. Here I am in a function that takes an element from Boolean Algebras of several elements and an internal element from any Boolean algebra by means of the Boolean Algebraic operations. It is a much broader definition than the one that is commonly used that speaks only about two values zero and one. We are now working on turning this logic into such a functional programming language. And by that, we will be able to speak and reason about programs.
