Samuel Schlesinger
  • Member for 5 years, 4 months
  • Last seen this week
4 answers
7 votes
299 views
What are semantic classes that have a syntactic equivalent?
2 votes

One of my favorites is $IND[t(n)] = FO[t(n)]$, where $IND[t(n)]$ is the class of problems decidable with an inductive definition which closes in less than or equal to $t(n)$ iterations and $FO[t(n)]$ ...

View answer
1 answers
4 votes
131 views
Which $SIZE$-$DEPTH(s, d)$ classes with $log(s(n))^{d(n) - 1} = o(n)$ can we not separate by known methods?
Accepted answer
2 votes

Lets say that we have $s, d$ where $log(s(n))^{d(n) - 1} = o(n)$. Let $d'(n)$ be arbitrary and $s'(n) = 2^{\sqrt[d'(n) - 1]{log(s(n))^{d(n) - 1}}}$. Then we have that $log(s(n))^{d(n) - 1} = log(s'(n))...

View answer
3 answers
14 votes
1k views
Checking formulas with two quantifiers ($\forall \exists$) - 2QBF
4 votes

To show satisfiability of $\exists x \forall y \phi$, we can play a game with two players A and B who each have access to a SAT solver. If we're working in a domain $D$, then at each iteration (...

View answer
2 answers
3 votes
168 views
Why is the multi-step reduction of semantics reflexive?
6 votes

The answer given is adequate but I'd like to mention that once you reduce a term to normal form, without reflexivity you're out of luck, with reflexivity you've hit a fixed point and thus you can use ...

View answer
2 answers
3 votes
549 views
Formally proving no algorithm exists
3 votes

What you are asking for is methods in proving lower bounds on the computational complexity (measured in space, time, etc) of given computational problems, and the answer is mostly that we have made ...

View answer
5 answers
33 votes
2k views
Evidence that PPAD is hard?
-1 votes

This paper is relevant to this, in that it attempts to show that PPAD = P: https://arxiv.org/abs/1609.08934

View answer
2 answers
11 votes
837 views
Subtypes as subsets of SML datatypes
1 votes

I can use GADTs, TypeFamilies, DataKinds, and TypeOperators (just for aesthetics) and create what you're after: data Term0 varb lamb letb where Lam :: lamb -> Term0 varb lamb letb -> Term0 ...

View answer