Martin Escardo @MartinEscardo@mathstodon.xyz
Public

For some reason I am going to find out tomorrow, my about-to-be 16-year son asked me to explain this paper to him:

Round-Based Public Transit Routing
microsoft.com/en-us/research/w

Of course I don't understand this paper because I haven't read it yet.

I promised to have a look at it together tomorrow (it is 10pm now).

But we had a preliminary look together.

For instance, there is a definition in Section 2, preliminaries, of a certain 5-tuple. I tried to begin explaining to him what all that means, and this worked to some extent with him, but we will continue tomorrow when I have a clearer head earlier in the day.

In any case, I want to say this. If my Computer Science students learning Agda manage to write down in Agda the definition given in the first paragraph of Section 2 (preliminaries) precisely, I will be very happy.

(I will be even happier if they can reason with it in their head and/or Agda, even more with respect the algorithms described rigorously in that paper.)

www.microsoft.com

0
0
0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/MartinEscardo/statuses/115929701451651483 on your instance and quote it. (Note that quoting is not supported in Mastodon.)