Advisors: Fabian Kunze and Gert Smolka
In recent years, a lot of effort has been concentrated on reaching polynomial time lower bounds on algorithms for solving various well-known problems. A useful method for showing such lower bounds is to prove them conditionally based on well-studied hardness assumptions such as P != NP, SETH, ETH, OVH, etc. This area of research helps us to better understand the structure of class P.
One can consider a simple problem of deciding whether two sets of size n each containing d-dimensional vectors have a pair of orthogonal vectors (OV Problem). There is a trivial algorithm working in time O(n^{2} poly(d)) which simply tests all the possible pairs of vectors and checks whether one of these pairs is orthogonal. The question is whether it is possible to find an algorithm solving OV that works in time O(n^{1.999} poly(d))? The assumption about P != NP turns out to be too coarse. However, under SETH we can show that any algorithm solving OV has runtime at least O(n^{2} poly(d)).
Reasoning about complexity bounds is not as easy as one would hope and might implicitly rely on a computational model or other complexity assumptions (such as e.g., time-constructability). Therefore, we would like to do such reasoning in a mechanized fashion using Coq proof assistant. In this work, we aim to formalize the basic hardness assumptions such as SETH, ETH, OVH and prove conditional lower bounds such as "SETH implies OVH" in weak call-by-value lambda-calculus as computational model using Coq proof assistant.