Title: PSPACE-completeness of Rush Hour and Modeling Computation as Games
Chair: Roy Willems
Advisor: Anton Golov
Gary William Flake, Eric B. Baum, Rush Hour is PSPACE-complete, or "Why you should generously tip parking lot attendants", 2002.
Erik D. Demaine, Robert A. Hearn, Constraint Logic: A Uniform Framework for Modeling Computation as Games, 2008.
Abstract:
Rush Hour is a children's puzzle game played on a 6x6 grid where the goal is to get the target car to the exit. If we generalize the game by allowing the grid to be of arbitrary size, it is possible to construct a machine capable of emulating a finite memory random access machine. This implies that deciding rush hour is PSPACE-complete. Another approach of proving that a game is complete in their corresponding complexity class is by reducing Constraint Logic into it. Constraint Logic is a game family where players reverse edges on a directed graph while following some rules. The games comprising this family have been shown to be complete in the complexity classes of their respective game categories. Due to the simplicity of the different Constraint Logics, they can be reduced into other games particularly easily.
Title: Higher-order Rewriting
Chair: Mirja van de Pol
Advisor: Cynthia Kop
F. van Raamsdonk, Outermost-fair rewriting, in: Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications (TLCA '97), Nancy, France, April 2-4, 1997, Proceedings, P. de Groote, Ed., Lecture Notes in Computer Science, vol. 1210, pp. 284–299, Springer, 1997.
T. Nipkow, Higher-order critical pairs, in: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pp. 342–349, IEEE Computer Society, 1991.
Abstract:
First-order rewrite systems can be extended to allow for higher-order functions and bound variables, resulting in higher-order rewrite systems (HRSs). Things like lambda calculus, logic, and functional programming languages come to mind as areas that can benefit from such an extension. After a quick recap on first-order rewrite systems, we will discuss how such an extension to HRSs can be made. We also look at critical pairs and the results about confluence they imply. Finally, we discuss a strategy for normalising terms and in which cases it is guaranteed to succeed.
Title: Erdös conjecture, Riemann hypothesis and Goldbach's conjecture have one thing in common: busy beaver functions
Chair: Menno Bartels
Advisor: Wieb Bosma
[no slides]
Tristan Stérin and Damien Woods. On the hardness of knowing busy beaver values BB(15) and BB(5, 4), 2021.
Scott Aaronson. The Busy Beaver Frontier, 2020.
Abstract:
n-state busy beavers are turing machines that take the most steps before halting among all the n-state turing machines. The busy beaver function, BB(n), returns the amount of steps the n-state busy beaver takes. This function has significant implications that can determine whether we can prove certain theorems such as the Erdös conjecture or even the Riemann hypothesis. By making n-state turing machines that halt when finding a counter example, we are able to verify the theorem by running the turing machine for BB(n) + 1 steps. Unsurprisingly, the busy beaver function is non-computable. How far can we go in knowing the values of the busy beaver function?
Title: Using Nondeterministic Constraint Logic to prove 1 x 1 Rush Hour is PSPACE complete
Chair: Steven Bronsveld
Advisor: Wieb Bosma
Erik Demaine, Nondeterministic Constraint Logic (NCL), Lecture 17 from: 6.890 Algorithmic Lower Bounds: Fun with Hardness Proofs, MIT Computer Science and Artificial Intelligence Laboratory, Fall 2014.
Josh Brunner, Lily Chung, Erik D. Demaine, Dylan Hendrickson, Adam Hesterberg, Adam Suhl, Avi Zeff, 1 × 1 Rush Hour with Fixed Blocks is PSPACE-complete, in: Proceedings of the 10th International Conference on Fun with Algorithms, FUN 2020.
Tags: Game Complexity, Complexity Theory, Reversible Logic
Abstract:
We define 1×1 Rush Hour in the setting of n2 − 1 unit-square blocks in an n × n square board, where each block is labeled as movable horizontally (only), movable vertically (only), or immovable – a variation of Rush Hour with only 1×1 cars and fixed blocks. The paper by Brunner et al. demonstrates that it is PSPACE-complete to decide weather a block can each the left edge of a board. We begin with introducing Nondeterministic Constraint Logic, and demonstrate that it reduces to 1×1 Rush Hour by constructing an intermediate problem called 2-color Oriented Subway Shuffle, effectively proving hardness in PSPACE (while also showing membership of 1×1 Rush Hour in PSPACE).
Title: Robust Markov decision process with k-Rectangular Uncertainty
Chair: Danish Alvi
Advisor: Nils Jansen, Marnix Suilen
Shie Mannor, Ofir Mebel, Huan Xu, Robust MDPs with k-Rectangular Uncertainty, 2016.
Jean-François Raskin, Ocan Sankur, Multiple-Environment Markov Decision Processes, August 30, 2018.
Abstract:
Markov decision processes are a tool for modeling planning problems under uncertainty. At each stage of the MDP an action is chosen and the next state of the MDP is determined with a probability distribution. These probabilities are not known and belong to an uncertainty set. The goal is to obtain a policy that achieves maximal performance under the most adversarial parameter in the uncertainty set. The paper focuses on coupled uncertainty sets and defines a new class of uncertainty sets, "k-rectangular uncertainty sets".
Title: Learning from soft evidence: A mathematical view on Jeffrey's rule and Pearl's rule
Chair: Markel Zubia
Advisor: Marnix Suilen, Nils Jansen
B. Jacobs, The Mathematics of Changing one's Mind, via Jeffrey's or via Pearl's update rule, Journal of Artificial Intelligence Research 65, pp. 783–806, 2019.
B. Jacobs, Learning from What's Right and Learning from What's Wrong, arXiv preprint arXiv:2112.14045, 2021.
Abstract:
We constantly form beliefs and when learning new evidence, we have to update these beliefs. Hard evidence states that some event occurred with certainty, whereas for soft evidence there is some uncertainty in whether the event occurred. Two ways to deal with soft evidence, Jeffrey's rule and Pearl's rule, give widely different results for updating beliefs based on soft evidence. In this talk a common mathematical framework for Jeffrey's rule and Pearl's rule is explained. Moreover, it is discussed how Jeffrey's rule can be interpreted as correcting beliefs with evidence taking into account existing evidence, and how Pearl's rule can be interpreted as improving beliefs with evidence not taking into account existing evidence. Finally, two mathematical properties are given, describing how these rules bring the updated beliefs closer to the evidence one updates with.
Title: Bounded natural functors, and their application to describe binding-aware syntaxes
Chair: Bálint Kocsis
Advisor: Freek Wiedijk
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette, Foundational, Compositional (Co)datatypes for Higher Order Logic: Category Theory Applied to Theorem Proving, LICS 2012.
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel, Bindings as Bounded Natural Functors, POPL 2019.
Abstract:
Bounded natural functors (BNFs) are a class of functors that include many familiar functors (e.g. product, list, function space). In the first part of my talk, I will introduce BNFs and discuss some of their nice properties. I will motivate the use of BNFs as a basis of a datatype package in Isabelle/HOL allowing mixed inductive and coinductive definitions. In the second part of the talk, I will focus on a concrete application of BNFs: describing a binding-aware syntax of lambda-calculus in higher order logic. The framework used applies a categorically inspired approach to describe and reason about syntaxes, but is still concrete enough to formulate many fundamental operations on terms. These include for example free variables, checking for alpha-equivalence and capture-avoiding substitution.
Title: Morphic and mix-automatic sequences
Chair: Suzan Erven
Advisor: Hans Zantema
Endrullis, Jörg, Clemens Grabmayer, Dimitri Hendriks, Mix-automatic sequences, International Conference on Language and Automata Theory and Applications, Springer, Berlin, Heidelberg, 2013.
Ehrenfeucht, Andrzej, Kwok Pun Lee, and Grzegorz Rozenberg, Subword complexities of various classes of deterministic developmental languages without interactions, Theoretical Computer Science 1.1, pp. 59–75, 1975.
Abstract:
k-automatic sequences are infinite sequences that are generated by a deterministic and finite automaton with output where the input consists of strings representing the natural numbers in base k. This definition can be expanded to mix-automatic sequences by making the input alphabet of the deterministic finite automaton with output and the base of the strings representing the natural numbers variable. We will introduce another class of infinite sequences, called the morphic sequence. We will look at subword complexity of morphic sequences and find out that they do not exceed quadratic order. This will be used to compare morphic and mix-automatic sequences and prove that neither class is a subset of the other.
Title: Martin Hofmann's Case for Non-Strictly Positive Data Types -- A breadthfirst algorithm using a non-strictly positive data type
Chair: Wietze Koops
Advisor: Herman Geuvers
Ulrich Berger, Ralph Matthes, Anton Setzer, Martin Hofmann's Case for Non-Strictly Positive Data Types, TYPES 2018.
Herman Geuvers, Inductive and Coinductive types with Iteration and Recursion in a Polymorphic Framework, 1992.
Abstract:
Most of the data types that are used, such as lists or trees are so-called strictly positive data types. These data types are used to implement algorithms such as breadthfirst traversel through a binary tree. Martin Hofmann's suggested a non-strictly positive data type, which could be used to implement a functional algorithm for breadthfirst traversal algorithm. The paper discusses the correctness and termination of this suggested algorithm. The correctness proof we will considers, follows a proof sketch given by Martin Hofmann himself. The termination is done using the fact that the algorithm can be implemented in a strongly normalizing extension of System F.
Title: GhostCell: a library for implementing data structures with internal sharing in Rust
Chair: Márk Széles
Advisor: Robbert Krebbers, Ike Mulder
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer, GhostCell: Separating Permissions from Data in Rust, in: Proc. ACM Program. Lang. 5, ICFP, Article 92, 30 pp., August 2021.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer, RustBelt: Securing the Foundations of the Rust Programming Language, Proc. ACM Program. Lang. 2, POPL, Article 66, January 2018.
Abstract:
Rust is a general-purpose programming language that encourages safe systems programming. Armed with a strong, ownership-based type system, it guarantees memory-safety by statically ruling out programs that would cause data-races. It achieves this by prohibiting the mutation of aliased state. This, however, makes it impossible to implement mutable data structures with internal sharing, such as graphs or doubly-linked lists. Although the Rust standard library provides ways to circumvent this limitation, they often incur unnecessary performance penalties.
GhostCell is a Rust library that enables one to implement data structures with internal sharing without introducing runtime overhead. In the first part of the presentation, we will learn the basics of Rust by covering some of its most characteristic features. After that, we will take a look at how the GhostCell library manages to overcome the aforementioned disadvantages of Rust. In the second part, we will shortly discuss RustBelt, a semantic soundness proof of the Rust language, as well as how it is extended to verify the soundness of GhostCell.
Title: Nominal automata theory
Chair: Robin Holen
Advisor: Jurriaan Rot
M. Bojańczyk, B. Klin, S. Lasota, Automata theory in nominal sets, Logical Methods in Computer Science, 10 (3), 2014.
Joshua Moerman, Matteo Sammartino, Residual Nominal Automata, the 31st International Conference on Concurrency Theory, CONCUR 2020.
Abstract:
In this talk I present the basics of nominal automata theory. Nominal automata recognizing languages over infinite alphabets with some symmetries. I will define these automata using basic group theory and show how we can generalize the Myhill-Nerode theorem for characterizing regular languages to the nominal setting. Next we will add more properties to these nominal automata and show that they recognize different sets of languages. Finally we look at a characterizing theorem that determines whether a language is accepted by a residual automaton.
[link to the old page with descriptions of the projects by the teachers]