21 votes
Accepted

Applications for set theory, ordinal theory, infinite combinatorics and general topology in computer science?

One major application of topology in semantics is the topological approach to computability. The basic idea of the topology of computability comes from the observation that termination and ...
user avatar
16 votes

Data structure to determine if sets are disjoint in o(n) time

The communication complexity of the set disjointness problem is $\Omega(n)$. The communication complexity is a lower bound on the time complexity of testing whether the two instances are disjoint. ...
user avatar
  • 10.5k
10 votes
Accepted

Universal and existential types

Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science. Forget the intersections and unions. People get ...
user avatar
  • 26.7k
9 votes

In the context of regular languages, must the alphabet be finite?

It makes sense in some contexts in mathematics to consider strings or languages over infinite alphabets. For instance, this concept is used in the strong version of Higman's lemma. But a finite ...
user avatar
9 votes
Accepted

Cantor's theorem in type theory

Short answer: yes! You don't need that much machinery to get the proof to go through. One subtlety: it seems on the face of it that there is a use of the excluded middle: one builds a set $D$ and a ...
user avatar
  • 13.2k
8 votes

In the context of regular languages, must the alphabet be finite?

The usual convention in formal languages and automata theory is that an alphabet is finite. However, there are certainly some cases where it's useful to think of an alphabet being infinite. For ...
user avatar
8 votes
Accepted

What are the issues with a set-like interpretation of quantifiers in type theory?

I think there may be a little nuance that can be applied to the situation, where 2 different possible hats may be applied, and which both are valid views of type systems. View 1: Types are intrinsic ...
user avatar
  • 13.2k
7 votes
Accepted

Order notation quirk

The identity is provable in ZF (or even in $\mathrm{RCA}_0^*$). The $\subseteq$ inclusion is trivial. For the $\supseteq$ inclusion, let $f\notin O(n)$. Define an integer sequence $\{n_k:k\in\mathbb N\...
user avatar
6 votes

Data structure to determine if sets are disjoint in o(n) time

This is not an answer to the exact question you pose, because the $n$ is different and the set instances are not separate. But there's a data structure for representing subsets of an $n$-element ...
user avatar
6 votes
Accepted

How can I formalize key value stores with set theory?

You did not say why you want a formalization, but presumably you want to do things with it, for instance prove properties of dictionaries and operations on them. In fact, your question can be ...
user avatar
  • 26.7k
6 votes
Accepted

Which formalism is best suited for automated theorem proving in set theory?

There are numerous ways of formalizing set theory: ZFC uses first-order logic and a primitive relation $\in$ NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$ ...
user avatar
  • 26.7k
6 votes

Are there presentations of set theory in terms of lambda-calculus?

There is a really interesting approach to a set theory-like foundational system that I am rather fond of: Grue's Map Theory. The basic idea is to take the (untyped!) $\lambda$-calculus as a base ...
user avatar
  • 13.2k
5 votes

Variation on partial Set Cover with penalties

This answers question (2): The greedy heuristic for Set Cover / Maximum Coverage always picks the set which contains the maximal number of uncovered elements. Assuming your modification for the ...
user avatar
  • 9,378
5 votes

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Some of the work of Olivier Finkel seems related to the question---though not necessarily explicitly about the Axiom of Choice itself---and in line with Timothy Chow's answer. For instance, quoting ...
user avatar
  • 3,324
5 votes
Accepted

Do we know a specific $L_{ZFC}$ such that $K(s) \ge L_{ZFC}$ is unprovable in ZFC for all strings $s$?

(Note: This answer works for most any consistient theory, not just $ZFC$.) We will define a machine $p$ based on the universal algorithm. $p$ does a search, looking for a string that represents a ...
user avatar
  • 471
4 votes

What are the issues with a set-like interpretation of quantifiers in type theory?

Cody's answer very nicely describes an important distinction. I would just like to point out a specific thing about the interpreation of $\forall$ as $\bigcap$. A typical way to get $\forall$ ...
user avatar
  • 26.7k
4 votes

Applications for set theory, ordinal theory, infinite combinatorics and general topology in computer science?

The 2004 Gödel Prize was shared between the papers: The Topological Structure of Asynchronous Computation. By Maurice Herlihy and Nir Shavit, Journal of the ACM, Vol. 46 (1999), 858-923 Wait-Free k-...
user avatar
  • 2,319
4 votes

Applications for set theory, ordinal theory, infinite combinatorics and general topology in computer science?

Behavior of a reactive system is often modeled using infinite structures ( infinite traced and infinite computation trees) and their Temporal properties (safety and liveness properties) have also been ...
user avatar
3 votes

Universal and existential types

Regarding question 1): the variable $Y$ must not appear in $Y$, indeed it needs to be unconstrained. If you want to have any hope of the lhs being equal to the rhs, certainly you should have the same ...
user avatar
  • 13.2k
2 votes

Given a partition and an element, find the subset that includes this element

It is unlikely to have a "name" because it is trivial: it can be solved with a hashtable, array, self-balanced binary search tree, or any other data structure that maps $x$ to $X_i$.
user avatar
  • 10.5k
2 votes

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

My impression reading this question is that no suitable example of a problem that requires more than just PA (let alone ZF) has been given, and the excellent answer by Timothy Chow explains why it's ...
user avatar
2 votes

Variation on partial Set Cover with penalties

Sorry for answering my own question, but I found the answer quite clearly. To question 1: It turns out that this problem has been studied by Pauli Miettinen not too long ago. The intuitive name given ...
user avatar
  • 171
2 votes
Accepted

Minimum order of partite in a bipartite graph

This is an upper bound on $N$ for the second formulation: Assume that I pick $N$ uniformly random sets. The probability of a pair of elements not to be covered by a specific set is $$1-\left(\frac{a}...
user avatar
  • 9,378
1 vote
Accepted

A Combinatorial Problem on Extremal Set Theory

This is arguably trivial, but maybe good enough for you: For any $a,b,c$ with $b \le a \le c$ (in particular $a=b=c$), if $\mathcal{F}$ is maximal subject to (i) and (ii), then it satisfies (iii) for ...
user avatar
1 vote

A Combinatorial Problem on Extremal Set Theory

Did you want some condition to make $\mathcal{F}$ a large collection? Because the current definition allows for the following, presumably trivial, case. Consider $\mathcal{F}=\{S_1,S_2\}$, where $S_1=[...
user avatar
  • 10.1k
1 vote

Is there a set theoretic way to look at SQL?

A co-Relational Model of Data for Large Shared Data Banks by Erik Meijer and Gavin Bierman, http://queue.acm.org/detail.cfm?id=1961297 Good article describing SQL and No-SQL databases as categorical ...
user avatar
1 vote

Is there a set theoretic way to look at SQL?

It is common wisdom that database field is firmly grounded in the two math disciplines: predicate logic and set theory. However, this is very fuzzy observation, and reality is more subtle. The ...
user avatar
1 vote

Universal and existential types

I suggest not to give up on the operational intuition. Operational is primary, all semantics are derived, and are but proof techniques for operational semantics. The key ideas are as follows. A ...
user avatar
1 vote
Accepted

Explanation of Cantor's diagonal argument?

It's actually more trivial. Suppose that $s$ occurs in the enumeration. Then it occurs at some specific index. Let's call this index $n$. This means that $s = s_n$. But this is impossible, because ...
user avatar
1 vote
Accepted

Rings and the set of all minimum s-t-cuts

Here I'll show that the statement is true, assuming that $V=U\cup\{s,t\}$, i.e. source and sink are not elements of $U$. Let $S=\bigcap\limits_{R\in\mathcal R}R$, $P=\bigcup\limits_{R\in\mathcal R}R\...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible