How to get an element from an existential proposition in Type theory proof assistant (Lean prover) I am trying to implement set theory in type theory from scratch, just for self pedagogical purposes. Specifically, I'm using the Lean Prover, and defining the element-of relation from scratch using the symbol $\epsilon$, just for pedagogical purposes.

What I'm trying to do

However, I'm unsure how to even define the notion of inductive set in this way. I am using the definition of inductive set:

  a set $S$ is inductive if $\emptyset \in S \land \forall x\in S, x\cup \{x\} \in S$.
  The axiom of infinity then states that there exists an inductive set.

Where I'm getting stuck is at even defining the set $\{x\}$ in Lean. I know from the axiom of pairing, that there exists a set, which we denote by $\{x\}$, which is shorthand for $\{x,x\}$, such that $\forall u, (u\in \{x,x\} \iff u = x \lor u = x)$.

What goes wrong

However, in type theory this axiom doesn't give me the actual set, it gives me an inhabitant of the existential proposition type. I've tried to use the "let" command to extract from this the actual set, but I get the error: "invalid match/convoy expression, expected type is not known".
This makes me suspect I shouldn't be using this command here at all (I think it's only intended for proofs).

Maybe instead I should be using the axiom of choice?

My code

constant Set : Type
constant In : Set → Set → Prop
infix  `ε`:50  := In

axiom pairing : ∀X:Set, ∀Y:Set, ∃S:Set, ∀u, u ε S ↔ u = X ∨ u = Y
axiom union : ∀X, ∀Y, ∃S, ∀u, u ε S ↔ u ε X ∨ u ε Y
infix `U`:49 := union

definition inductiveset (S:Set) : Prop := ∀x:Set,
let ⟨ (Q:Set), (h: ∀u, u ε S ↔ (u = x ∨ u = x) ) ⟩ := (pairing x x) in
     x ε S → (x U Q) ε S

axiom infinity : ∃S, inductiveset S

Summary

So basically:

How do I actually define the inductive set property in Lean?
Can I just extract a function $f:X\to Y$ from proof of a proposition $\forall x:X,\exists y:Y, ...$?
should I use the axiom of choice here?

Edit: Defining an operation from an existence theorem.

unique existence case.
Suppose I have the following:

constant T:Type
constants P:T → T → Prop
axiom ....
......
%Now, after 5 pages of lemmas, I prove:
theorem uniqueexistence : ∀t:T, ∃u:T, ( P t u ∧ ∀v:T, ¬v=u → ¬(P t v) )
                        := λ t:T, complicated_proof lemma238 t

Suppose I have a Lean file like the one above, How do I then create an operator F:T → T together with a theorem that ∀t:T, P t (F t)?

nonuniqueness case.
Similarly, if instead I don't have uniqueness, how do I randomly pick such an operator?

theorem nonuniqueexistence : ∀t:T, ∃u:T, P t u
                        := λ t:T, complicated_proof lemma238 t

How do I randomly (using the axiom of choice) pick an operator F:T → T together with a theorem that ∀t:T, P t (F t)?

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (only $\in$ relation). But even just stating the axioms of set theory without any constants and operation symbols is pretty haunting, see this gist of mine.

If you want a workable set theory you will have to rephrase your axioms so that they are not existential statements but rather operations. For example, define a union : Set → Set → Set operation and an axiom which states that u ε union X Y ↔ u ε X ∨ u ε Y. Formally, set theory does not have these operations, but every single development of set theory relies on the meta-theorem which says that introducing such constants is conservative (they can be eliminated). Also for the inductive set, introduce a constant S : Set and the axiom inductiveset S.

As a general advice, when formalizing mathematics in a proof assistants, one has to be quite flexible about organization of material. Traditional organization is good for teaching and writing textbooks, and so it may not align well with the demands of formalization.

For example, it looks to me at first sight that you would benefit by formalizing not only sets, but also classes. The class comprehension notation $\{ x \mid \phi(x) \}$ is very expressive and convenient, and easily formalized in terms of propositional functions on $\mathsf{Set}$. With it, you can define many operations on classes and then state that they are sets in terms of axioms. For example, rather than axiomatizing a union operation we just define union X Y to be the class {u | u ε X ∨ u ε Y} and then state that this class is a set. I suppose you could look at Von Neumann–Bernays–Gödel set theory.


what is the time complexity for binary division by repeated subtraction? The divisor and dividend are of length n and m bits respectively.

According to Wikipedia article,
https://en.wikipedia.org/wiki/Output-sensitive_algorithm
division by substraction is an output sensitive algorithm and has the time complexity of Θ(Q). Can the time complexity be calculated in terms of length of input bits?

If you calculate Z = floor (X / Y) by repeated subtraction, then you will perform Z subtractions. If you divide exactly n bits by exactly m bits, then there are at least $1/2 \cdot 2^{n-m}$ and at most $2 \cdot 2^{n-m}$ subtractions, so it's $\theta (2^{n-m})$ subtractions.

If you divide at most 2 bits by at most m bits, then Y might be 1 and in the worst case there are almost $2^n$ subtractions, so $O(2^n)$ subtractions.


Given a set of intervals on the real line, find a minimum set of points that "cover" all the intervals I've been trying to find an efficient way to solve the problem of finding a minimum (not minimal) set of time points that cover a given family of intervals on the real line, that is, for each interval $I$ there should be some time point $t$ from the chosen set such that $t \in I$. However, I am not sure if it's that straightforward. I tried modeling it as a minimum edge cover problem ("P" polynomial time complexity: intervals are vertices and intersection between intervals is an edge), but that doesn't work because for 1 time point in optimum solution there can be multiple edges.

I developed a greedy solution: have intervals sorted in increasing order of their end times. Then iterate over the intervals in the order. If a time point hasn't been inserted into the solution that covers the current interval, then insert it and remove all intervals that are covered by it from consideration. Continue till no intervals remaining.
Example:
(0, 10), (3, 12), (11, 15)

Add time 10 to the solution.
Remove (0, 10) and (3, 12) from consideration.
Add time 15 to solution.
Remove (11, 15) from consideration.
Final solution is of size 2. (time 10 and 15).

I can't prove it's optimum because it's not modeled as edge cover or vertex cover or known graph problem. I tried modeling it as "minimum clique cover problem" but not sure if it works.

How to model it properly to understand its complexity (P vs NP complexity)?
How to know if the above solution is optimum?

The problem is in $\mathbf{P}$.

In fact, there is even a (very) efficient algorithm for it:

Let $[a_1, b_1], \dots, [a_n, b_n]$ be the input intervals and assume $a_i \le b_i$ for all $i$. Additionally, let us assume (for now) that the intervals are given in sorted order as a list, sorted firstly respective to the $a_i$ and secondly to the $b_i$.

An optimal solution can be found as follows: Set $r$ to $a_1$. Then, starting with $i = 1$, check if $a_{i+1} \le b_i$; if that is the case, set $r$ to $a_{i+1}$ and increment $i$; otherwise, add $r$ to the solution and eliminate all intervals from $[a_1, b_1]$ up to $[a_i, b_i]$. Repeat until no more intervals are left.

Why is this an optimal solution? $[a_1, b_1]$ must be covered, so there must be some $r \in [a_1, b_1]$ in the solution. Then, either $r$ covers all $n$ intervals or there is $i$ such that $r < a_{i+1}$. The way our solution is constructed, $r$ is chosen so as to cover a maximal number of intervals while preserving these two conditions for $r$ (i.e., $a_1 \le r \le b_1$ and $r < a_{i+1}$). Apply induction on the remaining intervals (i.e., $[a_j, b_j]$ with $j \ge i + 1$).

The above procedure runs in linear time in $n$. The bulk of the time complexity, thus, lies in sorting the intervals, which can be done in $O(n \log n)$. I do not believe there is a better solution than this (though how to prove it does not occur to me at the moment).

A note

After some thought, the solution you have given also seems to be optimal (in fact, the only significant difference is you pick end times instead of start times). Proving it is optimal is analogous to the argument above: Set $r$ to $b_1$; if $a_2 \le b_1$, then $r$ already covers $[a_2, b_2]$, so disconsider it; otherwise, $a_2 > b_1$ and there is no $r$ covering both $[a_1, b_1]$ and $[a_2, b_2]$. Apply induction.

The time complexity is still $O(n \log n)$, though, since you require sorting the end times first.


Are all undecidable/uncomputable problems reducible to the Halting problem? Theory of computation tells us that there are some languages that cannot be recognized by a Turing machine. That is, there are well-defined problems for which no Turing machines can provide an algorithm which solves the problem.

Many problems that are undecidable seem to have a reduction to the Halting problem: Matyasevich's proof of the undecidability of Diophantine equations uses the Halting problem, the machine equivalence problem uses the Halting problem as well...

The question is: are all undecidable problems (in the sense of Turing) reducible to the Halting problem?

If so, is there a proof of this? If not, is there a counterexample of such a problem that provably cannot be reduced or mapped to the Halting problem.

No. As I recall a practical example can be made out of a function inequivalence statement. More abstractly, there is something called Turing-degree in undecidability and infinite levels of "hardness".  Each level has it's own Halting Problem strictly harder than those at every level lower.  Check out the first section of this Scott Aaronson lecture and what he calls a "Super Halting Problem".


What would a formal grammar for a binary file format look like? Binary structures often feature length specifiers; the parser is supposed to read them and then consume the specified amount of symbols. Because of this, the grammar is context-sensitive.

What would a context-sensitve grammar for a simple binary format look like?

For example, let's consider a length-prefixed array with the following layout:

64 bits | [size * 8] bits
size    | data

I suppose the language that corresponds to this format would be:

$$n b^n \\
n \in [0, 2^{64}[ \\
b \in [0, 2^8[$$

Left-context-sensitive grammars have the following structure:

$$\alpha A \rightarrow \alpha \gamma$$

I don't understand how this formalism could generate or be used to parse a language which contains part of the grammar itself in it. Does the following grammar make any sense?

\begin{align}
Bit & \rightarrow 0 \\
Bit & \rightarrow 1 \\
Octet & \rightarrow Bit^8 \\
Size & \rightarrow Octet^8 \\
Size \; Data & \rightarrow Size \; Octet^{Size} \\
Array_s & \rightarrow Size \; Data \\
\end{align}

I reason that the grammar above matches the structure of left-context-sensitive grammars. It seems clear to me that the next-to-last line of the grammar directly corresponds to the definition above:

\begin{align}
\alpha & = Size \\
A & = Data \\
\gamma & = Octet^{Size} \\
\end{align}

The trickiest non-terminal seems to be $Size$. It is not clear to me exactly how it influences the grammar's semantics. It is simultaneously part of the input and the grammar, serving as the number of repetitions for $Octet$.

I have seen many grammar-based approaches to parsing binary file formats. They include formalisms such as attribute grammars,[1][2] adaptive grammars, the recently introduced data-dependent grammars,[1][2] parser combinators [1][2][3][4][5] and even scattered context grammars.[1]

All these tools go beyond the definition above, so I keep wondering about the nature of binary file formats. If it is not possible to describe their language with a context-sensitive grammar, does that mean they are more powerful in the Chomsky hierarchy?

The Chomsky hierarchy is a hierarchy of grammars described by a given formalism.  The other grammar descriptions that you are giving (attribute grammars, ...) are not part of that formalism so they are outside the Chomsky hierarchy (and if I'm not mistaken are able to recognize some languages of higher level in the hierarchy while being unable to recognize other languages at a lower level).
Context-sensitive grammars are not at the top of the Chomsky hierarchy, unrestricted grammars are.
Context-sensitive grammars can generate what you are asking for, but it's painful to write.  Here is a grammar which generate a s followed by a binary number, followed by as many p as determined by the binary number.

\begin{align}
S & \rightarrow \text{s} \; C \\
\text{s} \; C & \rightarrow A \\
\text{s} \; C & \rightarrow \text{s} \; B \; \text{p} \\
\text{s} \; C & \rightarrow \text{s} \; B \; C \; \text{p} \\
A \; C & \rightarrow A \; D \\
A \; D & \rightarrow B \; D \\
B \; D & \rightarrow B \; \text{p} \\
B \; D & \rightarrow B \; C \; \text{p} \\
B \; C & \rightarrow B \; E \\
B \; E & \rightarrow X \; E \\
X \; E & \rightarrow X \; \text{p} \\
X \; E & \rightarrow X \; C \; \text{p} \\
A \; X & \rightarrow A \; F \\
A \; F & \rightarrow B \; F \\
B \; F & \rightarrow B \; A \\
B \; X & \rightarrow B \; G \\
B \; G & \rightarrow X \; G \\
X \; G & \rightarrow X \; A \\
\text{s} \; X & \rightarrow \text{s} \; B \; A \\
 A & \rightarrow 0 \\
 B & \rightarrow 1 \\
\end{align}

Yes that's a lot of rules (I may have missed some shortcuts, but on the other hand I may have missed some cases where unwanted strings are generated which could be avoided only with a more complex grammar).  Some explanations:

I'm using $A$ and $B$ for temporary place holder for $0$ and $1$ because context sensitive rules do not allow to modify terminals.  The last two rules replace them by the terminals they were acting for.
the first three rules are pretty obvious.
the fourth is starting the count
the next four are transforming a count ending by a $0$ in a count ending by a $1$ and a $\text{p}$
the next four are transforming a count ending by a $1$ in a count ending by a $X$ (meaning a carry to be propagated) and a $\text{p}$
the last seven rules are doing the carry propagation.


State of variables in dynammic programming I would like to know  what a state variable is in simple words, and I need to give a lecture about it.

I have chosen the Longest Common Subsequence problem
I found a similar question but it has no answers. I was told that I need to use the "states of variables" (not sure if variable of a state and state variable are the same) when explaining the pseudocode.

I think it has something to do with Hoare logic and state variables but I'm a very confused.

If you can provide useful links or maybe a clear explanation would be great.

Dynamic programming was
invented/discovered by Richard Bellman as an optimization technique.
The notion of state comes from Bellman's original presentation of
Dynamic Programming (DP) as an optimization technique. This is
presented for example in the Bellman equation entry of Wikipedia.

The technique was then extended to a variety of problems.

You might usefully read the Wikipedia presentation, I think. The
concepts you are interested in, including that of states and state variables, are described there. It may still be
some work to see how it fits the algorithm you have to explain.


Converting S->aTbS|epsilon T->aTb|epsilon to chomsky normal form The grammar have the following producitons,

\begin{align}
S&\rightarrow aTbS \mid\epsilon\\
T&\rightarrow aTb\mid\epsilon
\end{align}

Already turned this homework in, but I need to convert this grammar to chomsky normal form. Our teacher didn't go over this very well and all the documentation doesn't make sense to me and they almost all over the same example. Can someone please help? I only understand the first step which is making a new start state go to $S$. I have a vague understanding that I have to remove the null terminations next.

Our grammar $G$ has following two production where $S$ is start symbol.

$S\rightarrow aTbS \vert\epsilon$

$T\rightarrow aTb|\epsilon$

Now to convert it to chomsky normal form (CNF) we have to perform following steps:

If there is some production having $S$ in it's right side($S\rightarrow aTbS$ in this example) then add new start symbol $S_0$ and production rule $S_0 \rightarrow S$ to $G$.
Then remove null production from $G$:
So, after removing null production $G$ will have following productions:

$S_0 \rightarrow S$

$S \rightarrow aTbS|abS|aTb|ab$

$T \rightarrow aTb|ab$
Now we have to remove unit production from $G$. But there are none of them.
Then if there is production containing both terminal and nonterminals on RHS then introduce new non-terminal for the terminal appearing there and replace occurence of terminal in that RHS by this non-terminal. example will make this clear.

we, have this $S \rightarrow aTbS$ production. So we add production $A \rightarrow a$
and $B\rightarrow b$ to G. and then rewrite production $S \rightarrow aTbS$ as $S \rightarrow ATBS$

Doing same for all production we will have production set of $G$ as follow:

$S_0 \rightarrow S$

$S \rightarrow ATBS|ABS|ATB|AB$

$T \rightarrow ATB|AB$

$A \rightarrow a$

$B \rightarrow b$
Now we handle the case where RHS of production contains more than 2 non-terminals.
What we do is simple. We just keep first non-terminal as it is and introduce new
nonterminal for remaining part. Again example will make this clear.

We have this $S \rightarrow ATBS$ production. So we introduce new non-terminal $C$
and add production $C\rightarrow TBS$. Then modify original production as
$S\rightarrow AC$.

Note here that now we have to do this process for newly introduced production also.
i.e $C\rightarrow TBS$ will be converted to $C\rightarrow TD$ for instance and we
have to add $D \rightarrow BS$

Now after this step $G$ will contain following productions:

$S_0 \rightarrow S$

$S \rightarrow AC|AD|AE|AB$

$C \rightarrow TD$

$D \rightarrow BS$

$E \rightarrow TB$

$T \rightarrow AE|AB$

$A \rightarrow a$

$B \rightarrow b$

So now grammar is in CNF. But one thing is still remaining. Original grammar produces empty string but this grammar does not. For that add production $S_0 \rightarrow \epsilon$ to $G$.


Finite representations and programming languages Countably inifite I'm going over some of the pre-requisite math regarding Automata theory, and finite representations.

I read the following:

If ∑ is a finite alphabet the set of all strings over the alphabet
(∑*) is countably infinite.
The set of all possible languages over an alphabet ∑ is uncountably
infinite.

How can the set of languages possible from ∑ be uncountably infinite, yet the possible application of that alphabet to a language be countably infinite?

Can I ask those replying to not use too much complex notation, as I'm not a mathematics wizz.

Here is a simpler situation highlighting the difference. The set of finite binary strings is countable. The set of infinite binary strings is uncountable.

Another example: the set of numbers with finite decimal expansion is countable. The set of numbers with infinite decimal expansion is uncountable.

The reason that the number of languages is uncountable is that you have infinitely many choices: for each word, you can decide whether it's in the language or not. That's why it's like that infinite binary string considered above.


Integer Problems are NP-HARD I studied that Integer problems are properly NP-HARD problems. I know that NP-HARD include problems that arent solvable, like the halting problem.
This mean that there are instances of Integer problems that arent solvable ?

No, it doesn't mean that.

The set of NP-hard problems is upward-closed in the sense that there is no upper bound on the hardness of problems in it. You are correct to say that the class of NP-hard problems contains undecidable problems.

That does not imply, however, that every NP-hard problem has "unsolvable instances".

There is no such thing as an "unsolvable instance" in integer programming. There always is an answer, true or false (considering the decision version). Every finite set of instances is trivially computable. Only infinite sets can be undecidable.
We do know upper bounds on integer programming. For the decision version, we know that it's in NP; the optimization version is in NPO. Therefore, we know IP is decidable.


Is the union between a regular language and a random language also a regular language? If not can we draw any conclusion about the newly fromed language, the language that represents the union between a regular language and a non regular language  (not context free but a truly random language ).

The empty language is certainly regular. Take its union with any non-regular language $N$. What's the result?


Correctness of proof by induction Suppose a person states the following: $n^2 = (n * n), \forall n > 0$. One can check such equality by saying, via proof by induction, that:

for $n := 0:\ 0^2 = (0 * 0)$;
for $n := 1:\ 1^2 = (1 * 1)$;
and for $n := n + 1:$

$\ (n + 1)^2 = ((n + 1) * (n + 1))$

$n^2 + 2n + 1 = n^2 + 2n + 1$

As far as I understand, this states that:

$P(n)$ is valid for some $n$ within a range, say integers greater than 0;
$P(n)$ must be valid for the successor of any $n$ within the previous range;

Of course, it is not commonly necessary to prove such things as $n^2 = (n * n)$. And, proving it seems rather like considering that, eventually, there could be a mysterious value for $n$ that would make $n^2 \neq (n * n)$.

First question: is this interpretation correct?

Now, if one could prove $P(n): n^2 = (n * n)$ via the base and the induction cases:

$P(n)$ is valid for $n := 0$;
$P(n)$ is valid for $n := n + 1$;

One should also be allowed to prove it by saying that:

$P(n)$ is valid for $n := 0$;
$P(n)$ is valid for $n := n + 2$;
and via $P(n)$ is valid for $n := n + 3$;
and via $P(n)$ is valid for $n := n + 4$;
and, in fact, via $P(n)$ is valid for $n := n + m,\ \forall m > 0$.

Second question: is this inference correct?

So, if we are fine thus far, it should be the case that, eventually, a mysterious value $m$ could make proof by induction fail. And here comes the final question.

Third Question: how to prove the correctness of proof by induction?

Short answer: Proof by induction is correct because we define the natural integers as the set for which proof by induction works.

On your interpretations and examples

Your understanding seems broadly correct, though there are a few places where your statements are not fully rigorous. Given that we're talking about logic, getting things precisely right is important.

You should mention that you're working in the domain of integers (naturals, to be precise, which are the nonnegative integers). Induction doesn't work on many larger domains such as real numbers.
When proving a property of the form $\forall n \gt 0, \ldots$, the case $n=0$ does not come up. The basic induction principle applies to all natural numbers: if $P(0)$ and $\forall n \in \mathbb{N}, (P(n) \to P(n+1))$ then $\forall n \in \mathbb{N}, P(n)$. Other statements such as “if $P(1)$ and $\forall n \in \mathbb{N}, (n \ge 1 \to (P(n) \to P(n+1)))$ then $\forall n \in \mathbb{N}, (n \ge 1 \to P(n))$” are also true (and easy to derive from one another).
“$P(n)$ is valid for $n:=n+1$” is not a rigorous statement since the last occurrence of $n$ is not covered by any quantifier. The proper way to write this is “for any natural $n$, if $P(n)$ holds then $P(n+1)$ holds”.
Regarding your second question, it isn't clear what you mean by “and, in fact, …”. It is not the case, for example, that $P(0) \wedge (\forall n \in \mathbb{N}, P(n) \to P(n+2))$ implies $\forall n, P(n)$ — these hypotheses only prove that the property holds on even integers.
Finally, this isn't a matter of rigor, but your choice of example is odd, as $n^2$ is normally defined as $n*n$ — so after expanding the definition, the property to prove becomes $\forall n \gt 0, n * n = n * n$, which doesn't need induction. A better elementary example would be $\forall n \in \mathbb{N}, n + 1 = 1 + n$.

The Peano axioms

Now, to turn to why proof by induction works. It is impossible to answer this question rigorously without explicitly stating how the natural numbers are defined, or what properties of the natural numbers we define. Many definitions exist.

One definition of the natural numbers is the Peano axioms. There are many minor variants of the Peano axioms; one (which assumes equality as a preexisting notion) is:

$0$ is a natural.
For every natural $n$, $S(n)$ is a natural.
For every natural $n$, $0 \ne S(n)$.
For every natural $n$ and $m$, if $S(m) = S(n)$ then $m = n$.
Let $P$ be any unary predicate over the naturals. Suppose that $P(0)$ is true and that for every natural $n$, if $P(n)$ is true then $P(S(n))$ is true. Then for every natural $n$, $P(n)$ is true.

The first two axioms describe ways to build naturals. The next two axioms state that naturals built in different ways are distinct. (Exercise: find a model where all the axioms hold except for #3. Maybe a bit harder: find a model where all the axioms hold except for #4.)

As you can see, with this axiomatisation of the naturals, the induction principle is an axiom.

If you try to define the naturals as a subset of the reals, you'll run into foundational trouble: where do the reals comes from, and how do you prove properties of them? For example, it's difficult to reason about sequences of reals (or anything else) without induction.

The most common foundation of mathematics is set theory, specifically, ZF (Zermelo-Fraenkel). From ZF, a common way to define naturals is as Von Neumann ordinals:

$0$ is the empty set: $0 := \varnothing$
the successor of an ordinal is the union of that ordinal with the singleton containing it: $S(n) := n \cup \{n\}$.

The existence of the empty set is guaranteed by any set theory that proves the existence of at least one set and even a weak version of the axiom of comprehension. The existence of a successor is guaranteed by pairing to prove the existence of $\{n\}$ (which is an abbreviated notation for the pair $\{n,n\}$), and one to prove and union to deduce the existence of $n \cup \{n\}$. This suffices to prove the existence of all the natural numbers.

In order to prove that all the natural numbers form a set, an additional axiom is needed. It can be stated as “the natural numbers form a set”. Usually, the axiom is formulated as “the exists an inifinite set”. This more general formulation does not guarantee that the natural numbers obtained by this construction form a set — there are models of ZF where the smallest infinite set contains more than just zero and its successors, called non-standard models. I won't dwell on these models; doing logic in these models tends to be somewhat non-intuitive, but they are nice in that they allow rigorous reasoning about “infinitesimally large” integers, and from there about infinitesimally small numbers such as the $\mathrm{d}x$ in $\dfrac{\mathrm{d}x}{\mathrm{d}t}$ beloved of physicists.

Let's call a set $x$ supernatural (this is not standard terminology) if it contains $0$ and if for any $y \in x$, $S(y) \in x$. A supernatural set contains all the naturals, and perhaps more. A common formulation of the axiom of infinity is that there exists a supernatural set; we'll assume that. Let $\mathbb{O}$ be a supernatural set.

Now let $\mathbb{N}$ be the intersection of all the supernatural subsets of $\mathbb{O}$. Since all the supernatural sets contain $0$ and there is at least one element in the family ($\mathbb{O}$ itself), $0 \in \mathbb{N}$. For any $n \in \mathbb{N}$, $n$ is a member of each supernatural subset of $\mathbb{O}$, therefore (by definition of supernatural sets) so is $S(n)$. Thus $\mathbb{N}$ itself is supernatural. We'll call this set the set of naturals. Intuitively speaking, $\mathbb{N}$ is the smallest set containing the naturals (though without further axioms it is not necessarily unique, e.g. in nonstandard models).

$\mathbb{N}$ satisfies the induction principle. To see this, consider a predicate $P$ over the naturals, such that $P(0)$ is true and for all $n \in \mathbb{N}$, $P(n)$ implies $P(n+1)$. Let $\mathbb{N}_P$ be the set of naturals that satisfy $P$, i.e. $\mathbb{N}_P = \{n \in \mathbb{N} \mid P(n)\}$. Then $\mathbb{N}_P$ is a supernatural set, so $\mathbb{N} \subseteq \mathbb{N}_P$ by definition of $\mathbb{N}$.

Other foundations of mathematics

There are foundations of mathematics that are not based on set theory. What you consider the foundations vs derived theorems is not important: as long as you prove that your foundations are equally consistent with one of the commonly accepted ones, you're doing the same mathematics as everyone else. The definition of $\mathbb{N}$ as a set of ordinals is merely one way to construct it. The Peano axioms (or any equivalent formulation) are the specification of the naturals, and it is this specification that defines $\mathbb{N}$, rather than any particular construction.

In particular, constructive foundations of mathematics tend to treat the naturals as the most fundamental notion, and the induction principle on naturals, or on some more general structures, as a foundational axiom. For example, in homotopy type theory, the Peano axioms are a consequence of the rules for constructing functions by recursion. In intuitionistic type theory with inductive types (e.g. in the calculus of inductive constructions, which is the foundation of the Coq proof assistant), the induction principle on naturals is an instance of the more general induction principle that holds on any constructed type.


Practical Applications of regular grammars A regular grammar is a mathematical object, $G$, with four components, $G = (N, Σ, P, S)$, where. $N$ is a nonempty, finite set of nonterminal symbols, $Σ$ is a finite set of terminal symbols , or alphabet, symbols, $P$ is a set of grammar rules, each of one having one of the forms. $A → aB$.

I want to know what's Practical Application of these grammars.  I mean where and how do we use these in real world?

Also it may be helpful if someone tells me about the weaknesses of regular grammars.

Thanks in advance.

Regular grammars are more-or-less the same as NFAs, so you might as well ask what applications these have. Finite automata are used in compilers, for performing lexical analysis. Any course on compilation will contain ample information on this.

As for the weaknesses of regular grammars, they only describe regular languages. In particular, they're not enough to parse programming languages, even superficially. We use context-free grammars for that. Any course on formal languages and automata will explain all of that very clearly.


Why doesn't the Floyd-Warshall algorithm work if I put k in the innermost loop The Floyd-Warshall algorithm is defined as follows:

   for k from 1 to |V|
      for i from 1 to |V|
         for j from 1 to |V|
            if dist[i][k] + dist[k][j] < dist[i][j] then
               dist[i][j] ← dist[i][k] + dist[k][j]

Why doesn't it work if I simply use

for i from 1 to |V|
  for j from 1 to |V|
     for k from 1 to |V|
        if dist[i][k] + dist[k][j] < dist[i][j] then
           dist[i][j] ← dist[i][k] + dist[k][j]

In this case, the intermediate node k is iterated in the innermost loop. I expect it will make the same comparisons, but maybe different order. Why is the result different and incorrect?

Take $i - 1$ and $j = 2$. The algorithm is trying to find the shortest path between $1$ and $2$, by considering intermediate vertices. But at this point, most of the array dist is infinity, so we don't even find that $2$ is reachable from $1$ unless the distance is $1$ or $2$.


Findind The n/lgn intermidiate values in an unsorted array with asymptotic run time of $\Theta(n)$ SELECT algorithm Let $A[1..n]$ be an unsorted array, we want to find the $n/lgn$ intermidiate numbers in the array.

Namely the $(n/2)+1$ biggest number and the $(n/2) + 2$ biggest number and so on... until the $(n/2) + (n/lgn)$ biggrst number.

We are studing on the select algorithm and sortings.

I think it should go somehow with select algorithm as it has an efficiency of $\Theta(n)$

But its not that simple. As just making a loop will get us to \Theta(n^2)$

Just a remainder - the select algorithm compute nad finc the median of the medians in order to find the $i$ value in the array with run tie of $\Theta(n)$

Any suggestions?

Thank you.

You can find a $k$-th order statistic of an array using a selection algorithm in $\Theta(n)$ time. It means that you can also find the $k$ least (and the $k$ greatest) elements of an array in $\Theta(n)$ time by first finding the $k$-th ordering statistic and then comparing it with each element of an array.
So in your case we can find $n / 2$ (median) and $n/2 + n / \log(n)$ order statistics and then find all suitable elements by scanning an array and comparing its elements with both statistics.


Algorithm for generation of Canonical represented integers Is there a way to get canonical representation of an integer by algorithm?
I can get primes, but I don't know how to represent, for example, 1000 as 2^3×5^3. How can I compute the power of each prime number?

The simplest algorithm to do this is to divide repeatedly by the prime, until the division no longer yields an integer.


Clock page replacement policy vs LRU page replacement policy, is Clock more efficient? I'm currently learning about database systems and they mention a buffer management system which brings in pages from disk to memory. This buffer manager allows higher layers to operate as if the entire database on disk is actually in memory.

The video I am watching talks about LRU and Clock as the page replacement policies when a page doesn't exist in the buffer pool.

However what I am confused about is that this video mentioned that LRU was log n in efficiency, but Clock is a better algorithm.

Specifically, imagine the buffer pool being a hash table with page id as the key. The value is dependent on if we are doing LRU or Clock.

If LRU was implemented with a heap data structure, maintaining this structure would be O(log n). ie A read of a page is constant to see if it's in the hash table. If it is, the value points to somewhere on the LRU data structure, which needs an update since the 'last used' time has changed. This means every read, updates the LRU so this is O (log n).

For a clock page replacement policy, modifying a page's last used bit to 0 is constant time, because the page id is a key in the hash table and modifying it's value is O(1).

However for a clock replacement policy, finding a page with a last used bit = 0 requires scanning the buffer pool. That is o(n). For LRU, we just grab the root node which is O(1) and delete it which is log(n) and insert a new node which is log(n). So LRU should be O(log n) to replace a page.

So I'm confused why people would use a Clock page replacement policy and believe it is better than a LRU page replacement policy? Did the educational video I watch make an error in stating Clock is more efficient?

Or am I missing something?

If I understand correctly I think you are confusing the cache and the cache hit data structure. The structure isn't used to access the page, its used to store the hit count. For LRU, the OS needs to examine the hit count for every page in the cache memory to find the least recently used. When a page is hit, it is moved up in the list to prevent it from being evicted. I don't see how this would translate to a hash map.

The clock algorithm, only keeps track of a set of the most recently used pages (typically since the time since a new page was requested). The clock algorithm acts as an approximation of LRU without the maintenance of the linked list.


walk / traverse a disjoint set that has union rank and path compression I'm studying CLRS section 21.3, which introduces a union rank + path-compressed implementation of disjoint set. The implementations of MAKE-SET, UNION, LINK, and FIND-SET on p 571 of the book all work with nodes themselves, where each node has a parent pointer and rank.
Exercise 4 in that section claims that if you wanted to traverse all the nodes in the set (e.g. to print them) you only need a single extra attribute for each node, and the book claims that you can implement this without sacrificing the asymptotic complexity of union rank + path compression.
The data structure that immediately comes to mind is a circular list with single (not double) links. In this case, the "single extra attribute" the exercise asks for would be the next pointer of each node. We could just maintain that list in parallel with the disjoint-forest + union rank + path-compression.
However, the problem is that when trying to merge two sets, you would also need to merge their circular lists, and for a singly linked circular list, I'm pretty sure you cannot combine them into one without traversing through one of them first. This traversing would certainly destroy the asymptotic efficiency of union rank + path compression here.
Of course, you could slightly augment the circular list by keeping track of both its head and the node before the head, i.e. the tail. However, in order to do this, you can no longer work directly with the nodes, but would need to maintain a circ-list object (one for each set) with head and tail pointers. This would also mean that you can no longer call UNION on two nodes directly, but rather need to maintain a set object that has a pointer to its circ-list object as well as its root. All this seems to be somewhat more than the "exactly one extra attribute for each node`, since you also need O(1) extra attributes for each set.
Is what the exercise asking for actually possible, or do I need to make one of the concessions above?

None of the hacks in the question are necessary, since it's definitely possible to merge two singly linked circular lists without maintaining any additional tail pointers.
Suppose you have heads x and y of two separate circular lists. We first save xn = x.next. Then, set x.next = y.next. Then, set y.next = xn. After these, it's easy to see that the two circular lists have been merged.


find the minimum number of vertices in a directed graph from which the other vertices are reachable In a directed graph i want to call bfs on some of the vertices so that all of the vertices will be met.

(in other words all of the other vertices are reachable from these chosen vertices.)

I want to find the minimum number of such vertices.

Actually this problem arises in social networks when we want to find the minimum number of people to which if we send a message then all of the network members will get that.(suppose that we know when someone gets the message he/she will send that to all of his/her followers.)

Can anyone help?

The problem can be reduced to finding "sources" (opposite of "sinks", nodes with in-degree zero) in the graph. Suppose there is an optimal solution in which $B$ is one of the chosen nodes and there is an edge $A\rightarrow B$. Then we can put $A$ instead of $B$ in the solution and still cover the whole graph ($A$ can reach $B$, so it can reach all the nodes reachable from $B$). On the other hand, "sources" have to be chosen because they are not reachable from any other node. Then we should repeatedly find "source" nodes, chose them and mark all the vertices reachable from them as covered.

If there are no "source" nodes, then the graph must have cycles. All the nodes in a cycle are equivalent in terms of the nodes they can reach. Thus, they can be simplified into a "supernode". If eventually the supernode becomes a "source" and hence chosen by the algorithm, that means an arbitrary node of the cycle can be chosen.

So the algorithm repeatedly performs iterations of "finding source nodes" and "simplification" until the whole graph is covered.


Identifying the Equivalence Classes of a Language with equal number of 10 and 01 strings I'm doing a problem where I need to find the equivalence classes of the language below:

Let A = {x ∈ {0, 1}* | #(01, x) = #(10, x)}, where, for a, b ∈ {0, 1}*, #(ab, x) is the number of places in x where an a is immediately followed by a b.

So I can start to see some equivalence classes. 1* and 0* both are in A, because they both have zero 10's and 01's, so the condition holds. I don't really know how I would describe the other equivalence classes?

Any help would be great!

It's a trick question.

They try to make you think that you have to count how many 01 strings and how many 10 strings there are, but you don't have to.

Say the first letter is 0. So far, no 01 and no 10 strings. This doesn't change if there are more zeroes. But if we find a 1, we now have got a 01 string. Nothing changes until we get a zero, and we have one 01 and one 10 strings. Again, more zeroes don't change this, the next 1 means the number of 01 strings is one higher than 10, and the next 0 after that makes the number equal again.

You can see that if we start with a 0 and process more letters, every time the string ends with a 1 the 01's are one ahead of the 10's, and when the string ends with a 0 their counts are equal.

You do the same for the case that the string starts with a 1. Again the counts are equal every time the last digit is a 1 and unequal every time the last digit is 0. Counts are equal every time the first and last digits are the same.


Why is DTIME(n) not equal to NP, and consequently, DSPACE(n) not equal to NP? Intuitively it would seem like these equalities are false since DTIME(n) and DSPACE(N) are in terms of deterministic Turing machines and NP is non-deterministic, but I'm struggling to come up with a convicing argument as to why this is. I'm assuming that both the Time and Space Hierarchy Thoerems must be used but I'm just not quite sure how. I'm hoping someone can lead me in the right direction.

$DTIME(n^2) \subseteq \mathcal{P} \subseteq \mathcal{NP}$ and by the Time Hierarchy Theorem  $DTIME(n^2) \nsubseteq DTIME(n)$
Therefore $\mathcal{NP} \neq DTIME(n)$


Two's complement 8-bit subtractor? Please help me! I've been asked to make a circuit using only Logic Gates to implement an 8-bit 2's complement subtractor.

I was thinking of somehow modifying an 8-bit adder, but I figured it isn't 2's complement so it won't be of much use to me.

Any help is greatly appreciated, even if it's a pointer to the right approach to take in this.

It may seem at first as though computing the two's complement of b would cost you a whole separate incrementer, but you can easily merge it into the adder that you need anyway: just set the carry-in.

Alternatively (for example if you are somehow forced to use an adder without carry-in, or if it just works out better in combination with other logic) you may used that a - b = ~(~a + b), which obviously only ever needs inverters and a normal adder. This does put inverters before and after though, whereas to calculate the two's complement of b you'd only need inverters before the adder (and a carry-in but that's almost free).


Is it decidable whether a Turing Machine will visit every non-end state from input x? L = {w#x | w,x ∈{0,1}∗ and Turing Machine Mw with input x visits every non-end state at least once}

I believe this problem is undecidable.

My proof would consist of me reducing L to a Halting Problem; however, the structure of these proofs seem incosistent and inconclusive. I would appreciate if I could have some constructive feedback.

My understanding of the proof:

Create R which decides L
Construct algorithm S, which decides Atm (which we reduce to L)
Contradiction because Atm is undecidable

This is the skeleton to most Turing Machine dicidibility related  proofs I have read on the internet.

It's undecidable because you could use it to decide halting.

Because the number of states in a Turing machine is finite you can enumerate all $2^n$ combinations of possible non-end states. Run the algorithm against all of them.

If the algorithm returns yes for a group of states that includes an original end state then the machine halts.

Halting problem is undecidable so the algorithm cannot be executed by a Turing machine.


How to determine likely connections in a social network? I am curious in determining an approach to tackling a "suggested friends" algorithm.

Facebook has a feature in which it will recommended individuals to you which it thinks you may be acquainted with. These users normally (excluding the edge cases in which a user specifically recommends a friend) have a highly similar network to oneself. That is, the number of friends in common are high. I assume Twitter follows a similar path for their "Who To Follow" mechanism.

Stephen Doyle (Igy), a Facebook employee suggested that the related newsfeed that uses EdgeRank formula which seems to indicate that more is to valued than friends such as appearance is similar posts. Another user suggested the Google Rank system.

Facebook states their News Feed Optimization as $\sum u_{e}w_{e}d_{e}$ where

$u_{e}$ = affinity score between viewing user and edge creator
$w_{e}$ = weight for this edge (create, comment, like, tag, etc)
$d_{e}$ = time decay factor based on how long ago the edge was created

Summing these items is supposed to give an object's rank which I assume as Igy hinted, means something in a similar format is used for suggested friends.

So I'm guessing that this is the way in which connections for all types are done in general via a rank system?

What you're looking for is a heuristic. No algorithm can say, given a graph of friends as the only input, whether two individuals not directly connected are friends or aren't; the friendship/acquaintance relation isn't guaranteed to be transitive (we can assume symmetry, but that might even be a stretch in real life). Any good heuristic will therefore need to be based on an understanding of how people interact, rather than some mathematical understanding of the nature of graphs of relations (although we will need to quantify the heuristic in these terms).

Suggesting friends of friends with equal probability is a relatively cheap but inaccurate heuristic. For instance, my father has friends, but I wouldn't say I'm friends with any of them (although I'd probably say I'm a friend of my father's for the purposes of, e.g., a social network). Having a person at a relatively close distance doesn't necessarily make them a great candidate.

Suggesting people to whom you have a great many extended connections also seems like a poor choice in general, because this will tend to lead to exponential growth of friends of people who pull ahead early on (the seven degrees of separation from Kevin Bacon game is an example of this).

I suggest a circuit-based model. Assume that each link is a resistor of resistance $R$. Then the best candidate for a new friend might be the individual with the lowest equivalent resistance. Here's a poorly-executed ASCII graphics example:

  _____
 /     \
a---c   f
|   | /
b   d---e
| \ |
g   h   i

Say we want to find new friends for a. a's current friends are b, c, and f. We evaluate the net equivalent resistance between a and each of d, e, g, h, and i:

pair   resistance
(a,d)   6/7
(a,e)  13/7
(a,g)   7/4
(a,h)   1/1
(a,i)   inf

According to this heuristic, d is the best candidate friend, followed closely by h. g is the next best bet, followed closely by e. i can never be a candidate friend by this heuristic. Whether you find the results of this heuristic to be representative of real human social interactions is what's important. Computationally speaking, this would involve finding a subgraph containing all paths between two individuals (or, perhaps interestingly, some meaningfully selected truncation of this), then evaluating the equivalent resistance between the source and sink nodes.

EDIT: So what's my social motivation for this? Well, this might be a rough model of how hard it is to get in touch with, and subsequently communicate possibly significant amounts of information through, intermediaries (friends). In CS terms (rather than physics terms), this might be construed as bandwidth between two nodes in a graph. Extensions of this system would be to allow different kinds of links between people with different weights (resistance, bandwidth, etc.) and proceed as above.


Proving that Every Full Prefix-Free Language is Maximal I'm practicing a problem where I need to prove that every full prefix-free language is maximal.

I know a prefix-free language A is maximal if it is not a proper subset of any prefix-free language, where a prefix-free language is full if,

$$\sum_{x\in A} 2^{-|x|} = 1$$

Furthermore, I know that a language A ⊆ {0, 1}* is prefix-free if no element of A is a prefix of any other element of A and that the Kraft inequality says that for every prefix-free language A,

$$\sum_{x\in A} 2^{-|x|} \leqslant 1$$

I'm pretty sure that a full prefix free language is maximal, since it belongs to the maximal prefix-free set. I don't know, however, how to formally prove this. Should I be doing induction with Kraft's Inequality and with what I know about the relationship between maximal and prefix-free sets?

Any help would be appreciated!

Suppose that $A$ is a full prefix-free language, that is,
$$
\sum_{x \in A} 2^{-|x|} = 1.
$$
Assume, for the sake of contradiction, that $A$ is not maximal. Then there is a word $y$ such that $A \cup \{y\}$ is also prefix-free. According to Kraft's inequality,
$$
\sum_{x \in A \cup \{y\}} 2^{-|x|} \leq 1.
$$
However, this implies that
$$
1 \geq \sum_{x \in A} 2^{-|x|} + 2^{-|y|} = 1 + 2^{-|y|} > 1,
$$
and so we reach a contradiction. This shows that $A$ is maximal.

The more interesting direction is the converse: if $A$ is maximal then $A$ is full. Let me give two proofs of this fact.

The first proof is by induction on the length of the maximal word in $A$ (note that if $A$ is maximal then it cannot be empty). If $A = \{\epsilon\}$ then $A$ is indeed full. Now suppose that $A$ contains some word of positive length. Since $A$ is prefix-free, $\epsilon \notin A$. Hence we can write
$$
A = \{ 0x : x \in A_0 \} \cup \{ 1x : x \in A_1 \},
$$
where $A_0,A_1$ are prefix-free, and have shorter maximal words. It is easy to check that $A_0,A_1$ are maximal: for example, if $A_0 \cup \{y\}$ were prefix-free, then $A \cup \{0y\}$ would be prefix-free. Applying the induction hypothesis, we see that
$$
\sum_{x \in A} 2^{-|x|} = \sum_{x \in A_0} 2^{-|0x|} + \sum_{x \in A_1} 2^{-|1x|} = \frac{1}{2} \sum_{x \in A_0} 2^{-|x|} + \frac{1}{2} \sum_{x \in A_1} 2^{-|x|} = \frac{1}{2} + \frac{1}{2} = 1.
$$

The second proof uses a probabilistic argument, though for the sake of presentation I will present it as a counting argument. Let $A$ be a prefix-free code which is not maximal, and let $n$ be the length of the maximal word in $A$. For a word $x$ of length at most $n$, let $B_n(x)$ denote all words of length $n$ of which $x$ is a prefix, and note that $|B_n(x)| = 2^{n-|x|}$. Since $A$ is prefix-free, the sets $B_n(x)$ for $x \in A$ are all disjoint. Therefore
$$
\left| \bigcup_{x \in A} B_n(x) \right| = \sum_{x \in A} |B_n(x)| = \sum_{x \in A} 2^{n-|x|} = 2^n \sum_{x \in A} 2^{-|x|} < 2^n.
$$
Therefore there is some word $w$ of length $n$ which has no word in $A$ as a prefix. So $A \cup \{w\}$ is also prefix-free, and we conclude that $A$ is not maximal.

Both proofs we presented above actually show the following stronger fact: every prefix-free code is a subset of a maximal prefix-free code. Let me quickly outline how to obtain this result using both proofs.

In the first proof, we prove the claim by induction. If $A = \emptyset$ then we can extend it to $A = \{\epsilon\}$, and if $A = \{\epsilon\}$ then $A$ is already maximal. So suppose that $A = 0A_0 \cup 1A_1$. The induction hypothesis shows how to extend $A_0,A_1$ to maximal prefix-free codes $B_0,B_1$ (respectively), and then $B = 0B_0 \cup 1B_1$ is maximal.

In the second proof, we obtain a maximal prefix-free code by adding to $A$ all words in
$$
\overline{\bigcup_{x \in A} B_n(x)}.
$$

In both proofs, one way to check that the extended code is maximal is by verifying that it is full.

For extra credit, the reader can try extending the ideas above to infinite prefix-free codes, that is, prefix-free codes containing countably many words.


Why is the run time with a loop of this structure considered O(log n) I used the search function and a good amount of google searches, but wasn't able to get a straight answer on how a loop of the form below, is translated to a proper summation where the function derived from the summation is:  $O(\log n)$.

Example of the for loop:

int j = 0;
for (int i = 2; i <= n; i *= 2) {
    j = j + n * 2;
}

So I understand within the loop we have 3 operations (multiplication, addition, then assignment).

I understand that the index $i$ ranges from $[1, 2, 4, 8, 16, 32, 64, 128, 256]$... ($i$ is only equal to powers of 2, up to $n$).

So essentially the range of $i$ seems to be from $[2^m, n]$ and $m \in [0, \log_2n]$ right?

Also, $i^m < n$ so the loop executes $\log_2n - 0 + 1 = \log_2n + 1$ times right? How do we go about expressing this in summation notation?

Is it this (just taking a guess, not sure if it's right):

$$\sum\limits_{i = 0}^{log_2n + 1} 3$$ since we have 3 operations? If this is the answer, why do we keep the upper bound of the summation to $\log_2n$ instead of $n$? Also, I know typically we'd use $\log n$ but just put in the base 2 to help clear things up in my own head.

Could someone please show how the summation of the for loop is properly written?

Assuming the model of computation is RAM(Random Access Machine). Which means the cost of addition, multiplication,division etc is constant. Now your program is

int j = 0;
for (int i = 1; i <= n; i *= 2) {
    j = j + n * 2;
}

Inside the loop, you are doing addition, multiplication, comparison etc which takes constant time. Let $k$ denotes the number of iterations of the loop. Let $c_i$ denotes the cost at $i$th iteration of loop.
The total cost is

$$ = c_1+c_2+\ldots + c_{k}$$
$$ = \sum_{ j =1 \text{ to } k}c_i$$

It is easy to see that above summation gives $\mathcal{O}(\log n)$.


What are appropriate isomorphisms between formal languages? A formal language $L$ over an alphabet $\Sigma$ is a subset of $\Sigma^*$, that is, a set of words over that alphabet. Two formal languages $L$ and $L'$ are equal, if the corresponding sets are extensionally equal as subsets of $L\cup L'$. One can use languages in complexity theory to formalize the concept of a "problem." One could complain that "in general" extensional equality is undecidable, but I believe this would be misguided.

I'm pondering the following problem since some time: Two languages $L$ and $L'$ over alphabets $\Sigma=\{a,b\}$ and $\Sigma'=\{c,d\}$ (where $a$, $b$, $c$ and $d$ are distinct letters) can never be equal, even if they describe "exactly" the same "problem." But they should be isomorphic, if they really describe "exactly" the same "problem." What I would like to know are possible notions of isomorphism appropriate for complexity theory. I initially thought a computationally weak "translator" like a finite-state machine could be used to define the allowed isomorphisms, but this already seems to break down for trivial syntactic translations between equivalent logical formulas. (See for example this table with the syntactic definition of the dual $A^\bot$ in linear logic.)

Today I had the following idea: A definition of the language corresponding to a certain "decision problem" often has two parts: (1) An encoding of the allowed problem instances as finite strings of symbols, and (2) a definition of the "accepted" problem instances which belong to the language. If the checking whether a given finite string of symbols is an encoding of an allowed problem instance already requires a machine computationally stronger than a finite-state machine, then this stronger machine should also be used for the definition of the allowed isomorphisms.

  Questions: Has this line of reasoning any chance of "resolving" my problem? Has my problem already been solved, so that I just need to read the right references? Does my problem itself makes any sense, or is this just as misguided as complaining about undecidability of extensional equality?

Edit (not an answer yet) I noticed that "(1) An encoding of the allowed problem instances as finite strings of symbols" already contains the (hidden) assumption of a normalized input. Without this assumption, two different finite strings might correspond to the same problem instance. Instead of checking whether a given finite string is valid, the checking might produce a normalized input (and map invalid strings to a special string).

This setting has the advantage that the machine doing the checking/normalization is already equipped with means to transform finite strings to other finite strings. The allowed machine (complexity class) for this task could be part of the problem definition, and the (iso)morphisms would use the same machine (complexity class). (The suggestion of "poly-time many-one reductions" from Raphael's comment would then indeed be one possibility for problems in $\mathsf{P}$.)

A drawback is that this way of specification might only be appropriate for deterministic machines. Non-deterministic machines might require more flexible ways to specify/decide whether two input strings correspond to the same problem instance.

Has my problem already been solved, so that I just need to read the right references?

The theory of abstract family of languages is relevant. For example, the morphisms defined by finite state transducers lead to the cone family. Eilenberg's short ICM talk from 1970 nicely explains this framework, see also chapter 11 "Closure properties of families of languages" from Introduction to Automata Theory, Languages, and Computation (1st ed.) by J. Hopcroft and J. Ullman from 1979. However, only nondeterministic languages fit into this framework1. In the end, the book Theory of codes by J. Berstel and D. Perrin from 1985 helped me to come up with reasonable solutions for my problem. Codes and Automata by J. Berstel, D. Perrin and C. Reutenauer from 2009 is a major revision of this book with a much broader coverage.

  Has this line of reasoning any chance of "resolving" my problem? Does my problem itself makes any sense, or is this just as misguided as ...?

The assumption that there is one correct category for modeling isomorphisms between languages to "formalize the concept of a problem" is misguided. There are many different categories which can be interesting in the context of formal languages.

Here are three interesting categories related to many-one reductions, which will be referred to as total, partial, and relational. The objects of the categories are pairs $(\Sigma, L)$ of a finite alphabet $\Sigma$ and a language $L\subset\Sigma^*$ of words over $\Sigma$. For total, the morphisms between the source object $(\Sigma, L)$ and the target object $(\Sigma', L')$ are total functions $f : \Sigma^* \to \Sigma'^*$ with $L=f^{-1}(L')$. For partial, the morphisms are partial functions $f : \Sigma^* \to \Sigma'^*$ with $L=f^{-1}(L')$, where two partial functions $f$, $g$ are considered equal (as morphisms) if $f(x)=g(x)$ for all $x\in L$. For relational, the morphisms are relations $R\subset \Sigma^* \times \Sigma'^*$ with $L=R^{-1}(L')$, and any two morphisms between the same source and target are considered to be equal. The set of allowed functions or relations can be restricted to various simple "translators" to get categories with interesting isomorphisms.

The monoid homomorphisms from $\Sigma^*$ to $\Sigma'^*$ give a very basic total category. The isomorphisms of this category are basically just the bijections between $\Sigma$ and $\Sigma'$. Any reasonable family of languages should better respect these isomorphisms, i.e. be closed under inverse homomorphisms.
The partial functions defined by deterministic log-space Turing machine translators give a quite natural partial category. It is able to perform many trivial syntactic transformations (like applying De Morgan's laws to move negations to the atoms), includes the morphism defined by functional finite state transducers1, and also can sort. Still it won't identify two completely unrelated languages as isomorphic, because equality of the composition of two morphisms to an identity morphism is a much stronger requirement than just existence of many-one reductions in both directions.
The relations defined by nondeterministic log-space Turing machine translators give an interesting relational category. SAT is isomorphic to HORNSAT in this category, but it is an open question whether TAUTOLOGY or any other co-NP-complete problem is isomorphic to HORNSAT.

  Two languages $L$ and $L'$ over alphabets $\Sigma=\{a,b\}$ and $\Sigma'=\{c,d\}$ (where $a$, $b$, $c$ and $d$ are distinct letters) can never be equal, even if they describe "exactly" the same "problem." But they should be isomorphic, if they really describe "exactly" the same "problem."

The very basic total category described above solves this problem.

The problem becomes more interesting if "exactly the same" is replaced by "nearly the same for most practical purposes": Let $L$ be a language over $\Sigma=\{U,C,A,G\}$ and let $L'$ be the language over $\Sigma'=\{0,1\}$ obtained from $L$ by the substitution $U \to 00$, $C \to 01$, $A \to 10$, and $G \to 11$. Note that in any total category, $L$ and $L'$ are not isomorphic for $L=\Sigma^*$. The same would be true for partial categories, if the part "where two partial functions $f$, $g$ are considered equal (as morphisms) if $f(x)=g(x)$ for all $x\in L$" were omitted from the definition.

The quite natural partial category described above is sufficient for making $L$ and $L'$ isomorphic. It would be nice to have a more basic (i.e. more restrictive) category that makes them isomorphic. The following (successively more restrictive) categories look reasonable to me:

The partial functions realized by unambiguous finite state transducers2 where the only accepting state is the initial state. The isomorphisms of this partial category are (a subset of the) bijections between recognizable variable length codes.
The partial functions realized by deterministic finite state transducers where the only accepting state is the initial state. The isomorphisms of this partial category are (a subset of the) bijections between prefix codes.
The partial functions realized simultaneously by both a forward and a backward deterministic transducer where the only accepting state is the initial state. The isomorphisms of this partial category are (a subset of the) bijections between bifix codes.
Further restriction of the partial functions such that the isomorphisms are (a subset of the) bijections between block codes could also make sense.

  One can use languages in complexity theory to formalize the concept of a "problem."

Even before I learned about category theory, I have wondered about whether there are "more faithful" ways to formalize the concept of a "problem". After becoming familiar with category theory, I sometimes tried to come up with possible solutions, but always quickly gave up at the first stumbling block (because nobody cares anyway). I know that Yuri Gurevich has solved some related questions, but his solutions are practically applicable, whereas I was looking more for something nice and abstract, independent of practical applicability.

Most of my spare time for the last three weeks went into finally making some progress on this problem. Most often the time was spend finding annoying issues in the possible solutions I had in mind. The sense of making progress arose from reading (old) books and articles, and learning many basic concepts and facts about transducers and rational sets.
Finally I learned the notions of a prefix code and a bifix code (formerly biprefix code in Berstel's book), which allowed me to come up with the reasonable3 categories described above.

It may be hard to appreciate those (code related) categories, without having seen some issues of the more obvious categories. A general issue is that closure under composition can make it hard to define a nicely restricted class of partial functions. Another issue is related to the fact that addition of one (or multiplication by a constant) is an "easy to compute function" if the digits of the number are given in low-endian order, but not if the digits are given in big-endian order.

1
A functional finite state transducer is a nondeterministic finite state transducer that realizes a partial function. These partial functions cannot be realized by deterministic finite state transducers. They can be realized by deterministic bimachines, but those may need $O(n)$ forward and backward scans over the input, if they want to operate in $O(1)$ space.

2
An unambiguous finite state transducer is a nondeterministic finite state transducer with at most one accepting path for each input. It realizes a partial function, hence it is also a functional finite state transducer. It is decidable whether a given finite state transducer is unambiguous.

3
I'm not sure how reasonable the total and the relational categories introduced above really are. I just wanted to show straightforward alternatives to the partial category. More alternatives are easy to come up with, for example co-relational, where the morphisms are relations $R\subset \Sigma^* \times \Sigma'^*$ with $L=R^{-1}(L')-R^{-1}(\Sigma'^*-L')$, and any two morphisms between the same source and target are considered to be equal.


Shortest directed path connecting given subset of vertices Given

weighted directed graph $G = (V,E,w)$, where $w : E \to \mathbb R^+$
source vertex $v \in V$
vertex subset $U \subset V$

how to find a shortest directed path from $v$ containing all vertices from $U$? Note that such path may contain vertices that are not in $U$.

Does such problem have a name?
How to find a solution?

This problem is NP-complete, by reduction from Hamiltonian path. Given an instance $G=(V,E)$ of Hamiltonian path, add a new vertex $s$ connected to all original vertices; this edges are directed from $s$, and all the original graph edges are bidirectional. Give all edges unit weight. There is a path from $s$ visiting all of $V$ of weight $|V|$ if and only if $G$ has a Hamiltonian path.


Greedy Algorithm Proof Min Swaps Problem to get the min. no. of swaps required for arranging pairs togethe.

There exists an array of size 2N with integers ranging from 0 to 2N-1 arranged at random. Each integer is paired with another
i.e. 0 paired with 1, 2 paired with 3,...2N-2 paired with 2N-1. What is the minimum number of swaps required to have
all pairs next to each other.
E.g. : [5,4,2,6,3,1,0,7] -> [5,4,2,3,0,1,6,7] Output 2 swaps needed

Solution: Greedy Approach

for i from 0 to 2N-2:
    if array[i] and array[i+1] does not constitute a pair:
        find the pair for the ith one and swap position with i+1 element

What is the proof for why the above greedy algorithm is optimal?

The algorithm in the question can be stated more clearly in the following form since considering the odd $i$ does not have any effect once $i-1$ has been take care of.

for even i from 0 to 2N-2:
    if array[i] and array[i+1] does not constitute a pair:
        find the pair for the i-th one and swap position with i+1 element

Here is an outline of the proof.

Given an array $A$ of size $2N$ with integers ranging from $0$ to $2N-1$, let us construct a graph $G$. Replacing $2i-1$ with $2(i-1)$ for all $i$, we will have a new array $B$ of even integers from $0$ to $2(N-1)$, each of which appears twice. Let $G$ have vertices $0, 2, \cdots, 2(N-2)$.

If $B[0]=2i$ and $B[1]=2j$, we will add an edge between $2i$ and $2j$ in $G$.
If $B[2]=2i$ and $B[3]=2j$, we will add an edge between $2i$ and $2j$ in $G$.
$\cdots$
If $B[2N-2]=2i$ and $B[2N-1]=2j$, we will add an edge between $2i$ and $2j$ in $G$.

Please note since $2i$ might be the same as $2j$, $G$ may have self-loops. Since each even number appears twice in array $B$, the degree of each of vertices of $G$ is 2 (2-regular graph). That means $G$ is a disjoint union of cycles.

Define a function $s$ from arrays which are permutations of $0, 1, \cdots, 2N-1$ to $\Bbb N$, $s(A)=$ the number of cycles in $G$, where $G$ is obtained from $A$ by the above deterministic construction.

Claim (at most 1 increase with one swap). Suppose an array $A$ is changed to $A'$ by a swap of two elements. Then $s(A')\le s(A)+1$.

Suppose we have proved the claim. Notice that $s(A)=N$, the maximum value of $s$ if and only if all pairs are next to each other. Since you can only increase at most 1 to $s(A)$ by each swap and the greedy algorithm does increase $s(A)$ by 1 with each of its swaps, the greedy algorithm must be optimal.

I will leave the gaps in the above proof as two easy exercises.

Exercise 1: The greedy algorithm increase the value of $s$ by 1 with each of its swaps.

Exercise 2: Prove the claim of at most 1 increase with one swap.


Minimize a sum with a weight constraint We are given N sets, each of which has a finite number of pairs $(x_i,y_i)$.

$M_1=\{(0,0), (x_{1,1},y_{1,1}), ...\}$

...

$M_N=\{(0,0), (x_{1,N},y_{1,N}), ...\}$

The problem is to select one and only one item from each set such that

$Min \{\displaystyle\sum_{j=1...N}(x_{i,j})\}$

s.t. $\displaystyle\sum_{j=1..N}(y_{i,j}) > R$

where $R$ is a given constant.

Is there any classic problem similar to this? or what is known about this class of problems?

The problem you have given is similar to KNAPSACK as Yuval Filmus mentioned.

KNAPSACK problem is defined as:

maximize $\sum_{i=1}^n v_i x_i$
subject to $\sum_{i=1}^n w_i x_i \leq W$ and $x_i \in \{0,1\}. $

I assume the pair (0,0) is used so that you may not choose pairs for some of the $M_j$'s. Otherwise (0,0) pair is irrelevant in the problem.

If this is so, then your problem can be easily shown to be NP-complete. We can reduce KNAPSACK to your problem by taking $N=n$ and have each $M_j$ as a copy to the KNAPSACK instance (after negating $v_i$'s and $w_i$'s of course).

If pair (0,0) is not used in a way that I described above, then too you can circumvent the issue by adding $N$ pairs $(x_{N+i,j},y_{N+i,j})$, for $1\leq i \leq N$ in set $M_j$ for $1 \leq j \leq N$, so that each $M_j$ has now additional $N$ pairs (total of $2N+1$). Each $x_{N+i,j} = y_{N+i,j} = 0$ for all $i$'s and $j$'s.

If you say that each pair need to be distinct, then we can take $x_{N+i,j} = y_{N+i,j} = \epsilon_{i}$ to make each pair distinct, where $\epsilon_{i} \ll 1$ is an arbitrarily very small quantity. We also replace $R$ by $R+\Sigma_i \epsilon_i$.


What is the difference between classical crypto and post-quantum crypto? Will there be a need to change the definitions of security if we have quantum computers? What cryptographic constructions will break? Do you know a survey or an article that explains what will be needed to change?

Summary of this paper providing a (partial) answer.

There are two kinds of traditional public-key cryptographic methods: those based on integer factorization, and those based on the discrete logarithm, including elliptic-curve-based methods. These models are believed to be hard in the classical models, but have been shown that neither is hard in the quantum model.

Although Grover developed a quantum algorithm providing quadratic speedup for searching, Bennet, Bernstein, Brassard and Vazirani showed that the quantum model couldn't allow exponential speedup for search problems. This suggests symmetric encryption algorithms, one-way functions and cryptographic hashes should resist quantum-based attacks. The focus, then, should be on developing secure public-key methods.

Lamport signatures may provide a one-time signature mechanism secure against quantum attacks. Lattice problems may form the basis for public-key methods which are resistant to quantum attacks; in particular, the NP-Hard shortest-vector and closest-vector problems are attractive. For both the classical and quantum models, these problems are believed to be hard for lattices of high dimension. The NTRU family of cryptographic algorithms, based on lattice problems, may provide a practical means of achieving public-key cryptography resistant to quantum attacks. Another problem which might serve as a basis for secure public key methods is the syndrome decoding problem. The McEliece encryption system is based on this problem, and variants may provide a way forward.


The complexity class FP I have a hard time understanding the following lines from our lecture notes:

$f \in \text{FP}$ iff there is a transducer T that computes $f$ and there exists a polynomial $p$ such that $TIME(T(x)) \leq p(|x|).$

Note: If $f \in \text{FP},$ then $|f(x)| \leq p(|x|)$ holds for a fixed polynomial $p.$

Examples:

$f(x) = x^2$ ($x$ is a binary number)

$f(x) = $ Table of the shortest paths from a start node s in a directed graph $G,$ where $G$ and $s$ are coded as $x.$

$f(x) = 2^x$ is not in $\text{FP}.$

Can somebody please explain the examples in a dummy-friendly way?

Recall that Turing Machines are often defined to output only a yes/no answer. Transducers are used to extend this to a general output, which is sometimes more appropriate for a certain task (e.g. defining mapping-reductions).

When we use transducers, we can also analyze their runtime, and in this case they compute functions, so we are interested in which functions can be computed using a transducer that runs in polynomial time.

In this context, running in polynomial time means that, as you state, the transducer is allowed to run for $p(|x|)$, where $p$ is a fixed polynomial, and $x$ is the input to the transducer. Finally, the transducer outputs the binary representation of the function that it computes.

Let's consider the first example: $f(x)=x^2$. A transducer that computes it takes as input a binary number, for example $11$ (3 in binary). It then needs to output $1001$. To actually compute this value, we can use the long-multiplication algorithm from preschool. What we need to notice is that this algorithm is indeed polynomial in $|x|$ - the length of the binary representation of $x$. It is not hard to verify that the algorithm runs in  quadratic time of this length.

So we have a polynomial-time transducer for $f(x)=x^2$, so it is in FP.

Now let's consider example 3: $f(x)=2^x$. Consider an input $x$. What is the size of the binary representation of $f(x)$? Well, it's $\log f(x)$. But
$$\log f(x)=\log 2^x=x$$
and $x$ is exponential in $|x|$ - indeed, the size of the representation of $x$ is $\log x$.

So we have that $\log(f(x))$ is exponential in $|x|$, or in other words, $|f(x)|$ is exponential in $|x|$, and in particular, $|f(x)|>|p(x)|$ for every polynomial $p$ and for large enough $x$ (because $2^n\in \omega(p(n))$ for every polynomial $p$).

So it is no possible to even write down $f(x)$ in polynomial time, let alone compute it. This is why $2^x\notin FP$.

Finally, the second example is just an emphasis on the relation between FP and P: Given $G,s$ in some representation (e.g. a "text file" encoded in binary) it is easy to compute the shortest path from $s$ to all the vertices using BFS, which runs in polynomial time. So essentially, once you run BFS on the graph and mark all the shortest paths, you get some binary string which represents it. You then output this binary string.

The important thing to take from the second example is the concept that if you are looking for a solution which is not a yes/no answer (e.g. shortest path, result of an arithmetic expression, etc.) and you can solve a related decision problem using TMs in polynomial time (e.g. "is there a path shorter than $k$?", "is the result of this expression smaller than $v$?"), then in many cases you can use the TM that solves the decision problems to actually obtain a transducer that runs in polynomial time, so the problem will be in FP.


Filling bins with pairs of balls A bin is called full if it contains at least $k$ balls. Our goal is to make as many bins as possible full.

In the simplest scenario, we are given $n$ balls and may arrange them arbitrarily. In that case, obviously the best we can do is pick $\lfloor n/k \rfloor$ bins arbitrarily and put $k$ balls in each one of them.

I am interested in the following scenario: we are given $n$ pairs of balls. We have to put the two balls of each pair in two different bins. Then, an adversary comes and removes one ball from each pair. What can we do to have the maximum possible number of full bins after the removal?

A simple strategy is: pick $\lfloor n/(2k-1) \rfloor$ pairs of bins. Fill each bin-pair with $2k-1$ ball-pairs (each bin contains $2k-1$ balls, one ball from each pair). Then, regardless of what our adversary removes, we have in each bin-pair at least one full bin.

Do we have a strategy that achieves a larger number of full bins (more than $\lfloor n/(2k-1) \rfloor$)?

TL;DR -- No, there is no better strategy than the simple strategy.  Here is the main idea of the proof. When there are not enough balls, there will be a "ball path" from a $k$-full bin to a bin with at most $k-2$ balls. The adversary can pass a ball from that full bin to that less full bin along that path, which can be done repeatedly until the number of $k$-full bins is reduced.

Reformulation in Graph theory

Suppose we are given a simple finite graph $G(V,E)$ with a function $w: E\to\Bbb Z_{\ge 0}$. We say there are $w(e)$ balls in edge $e$. Let $E_2$ be the (end-marked edge) set $\{(e,v)| e\in E, v\in e\}$. If $d:E_2\to\Bbb Z_{\ge 0}$ satisfies $w(e)=d(e,v_1) + d(e,v_2)$ for every edge $e=\{v_1,v_2\}$, we say that $d$ is $w$-distributing. Any $w$-distributing function $d$ induces a function, which we use the same symbol, $d:V\to\Bbb Z_{\ge 0}$, $d(v) =\sum_{v\in e}d(e,v)$. We say that $d(v)$ balls are in $v$. Given $k\in\Bbb Z_{\gt0}$, let $F_k(d)=\#\{v\in V|d(v)\ge k\}$, the number of $k$-full vertices by $d$.

(Erel-Apass Theorem) For any simple finite graph $G(V,E)$ and $w:E\to\Bbb Z_{\ge0}$, we have $\sum_{e\in E}w(e)\geq (2k-1) \min_{w\text{-distributing }d}F_k(d)$

Imagine each vertex is a bin. For each edge $e=\{v_1,v_2\}$, $w(e)$ ball-pairs are put into $v_1$ and $v_2$, each of which getting $w(e)$ balls. Among these $w(e)$ ball-pairs, the adversary may take away $d(e,v_2)$ balls from $v_1$ and $d(e,v_1)$ balls from $v_2$. The end result is the same as if, given all empty bins initially, for each edge $e=\{v_1, v_2\}$, $w(e)$ balls are put into it and, then, $d(e,v_1)$ and $d(e,v_2)$ balls are distributed to $v_1$ and $v_2$ respectively by the adversary.  Hence, Erel-Apass theorem says that in order to ensure $t$ k-full bins after a smart adversary's removal, at least $(2k-1)t$ pairs of balls are needed. In another word, an optimal strategy to have the maximum possible number of full bins left is indeed the "simple strategy", which repeatedly fills a different pair of bins with $2k-1$ ball-pairs until we do not have enough balls to repeat.

Proof of the theorem

For the sake of contradiction, let $G(V,E)$ and $w$ be a counterexample whose number of vertices is the smallest among all counterexamples. That is, there is $w$-distributing $m$ such that $F_k(m)$ is minimal among all $F_k(d)$ of $w$-distributing function $d$. Furthermore,
$$\sum_{e\in E}w(e)\lt (2k-1)F_k(m)$$

Let $V_s=\{v\in V | m(v)\le k-2\}$. Let $V_\ell=\{v\in V|m(v)\geq k\}$. So $F_k(m)=\#V_\ell$.

Claim one: $V_s\neq\emptyset$.
Proof of claim one. Suppose otherwise that $V_s$ is empty.
$$ \sum_{v\in V}m(v)= (k-1)\#V +\sum_{v\in V}(m(v)-(k-1))
                    \ge (k-1)\#V + \#V_\ell \gt (k-1)\#V$$
Let us also reuse $w$ as a function from $V$ to $\Bbb Z_{\ge 0}$ such that $w(v)=\sum_{v\in e}w(e)$ for any $v\in V$.
$$\begin{align}
\sum_{v\in V}w(v) &=\sum_{v\in V}\sum_{v\in e }w(e)
                  =\sum_{e\in E }\sum_{v\in e}w(e)
                  =\sum_{e\in E}2w(e)
                  =2\sum_{e\in E}w(e)\\
                  &=2\sum_{e\in E }\sum_{v\in e}m(e,v)
                  =2\sum_{v\in V}\sum_{v\in e }m(e,v)
                  =2\sum_{v\in V}m(v)\\
                  &\gt 2(k-1)\#V
\end{align}$$
So there must be a vertex $b$ such that $w(b)\ge 2k-1$.

Consider the induced setup $G'(V', E')$ and $w'$, where $V'=V\setminus\{b\}$, $G'(V', E')$ is the induced graph $G[V']$ and where $w'=w|_{E'}$. For any $w'$-distributing function $d'$, we can extend it to a $w$-distributing function $d_{d'}$ where $d_{d'}$ is the same as $d'$ on $E'$ while $d_{d'}(e, b)=w(e)$ for every edge $e$ adjacent to $b$. Note that $F_k(d_{d'})= F_k(d') + 1$ since $d_{d'}(b)=\sum_{b\in e}d_{d'}(e,b) = \sum_{b\in e}w(e)=w(b)\ge 2k-1\ge k$. Then
$$\begin{align}\sum_{e\in E'}w'(e)&\le\sum_{e\in E}w(e) - w(b)\\
  &\lt (2k-1)F_k(m) -(2k-1)\\
  &=(2k-1) \left(\min_{w\text{-distributing }d}F_k(d) -1\right)\\
  &\le (2k-1) \left(\min_{w'\text{-distributing }d'}F_k(d_{d'})-1\right)\\
  &\le (2k-1) \min_{w'\text{-distributing }d'}F_k(d')
\end{align}$$
So, $G'(V', E')$ and $w'$ is a counterexample whose number of vertices is smaller than the number of vertices in $G$. That cannot true by our assumption about $G(V,E)$ and $w$. So claim one is proved.

For any vertex $v$, define $v$ $d$-reachable from vertex $u$ if there is a path $u_0= u, u_1, u_2, \cdots, u_m, u_{m+1}=v$, $m\ge0$ such that $d(\{u_i, u_{i+1}\}, u_i)>0$. Let $V_r=V_\ell\cup \{v\in V|\exists u\in V_\ell \text{ and } v\text{ is } m\text{-reachable from } u \}$.

Claim two: $V_r = V$
Proof of claim two: Suppose $V_r\neq V$. For any vertex $v\in V_r$ and $u\notin V_r$, since we cannot reach $u$ from $v$,  if $\{v, u\}$ is an edge, then $w(\{v, u\}, v) = 0.$ Consider the induced setup $G'(V', E')$ and $w'$, where $v'=V_r$, $G'(V', E')$ is the induced graph $G[V']$ and where $w'=w|_{E'}$. For any $w'$-distributing function $d'$, we can extend it to a $w$-distributing function $d_{d'}$ where $d_{d'}$ is the same as $d'$ on $E'$ and the same as $m$ on other edges. Note that $F_k(d_{d'})= F_k(d')$ since all vertices with no less than $k$ balls inside are in $V_\ell\subset V_r$. Then
$$\begin{align}\sum_{e\in E'}w'(e)&\le\sum_{e\in E}w(e)\\
  &\lt (2k-1)F_k(m)\\
  &=(2k-1) \min_{w\text{-distributing }d}F_k(d)\\
  &\le (2k-1) \min_{w'\text{-distributing }d'}F_k(d_{d'})\\
  &\le (2k-1) \min_{w'\text{-distributing }d'}F_k(d')
\end{align}$$
So, $G'(V', E')$ and $w'$ would be a counterexample whose number of vertices is smaller than the number of vertices in $G$. That cannot be true by our assumption about $G(V,E)$ and $w$. So claim two is proved.

Now let us prove the theorem.

Since $V_r=V$ and $V_s\neq\emptyset$, there is a path $u_0= u, u_1, u_2, \cdots, u_m, u_{m+1}=v$, $m\ge0$ with $m(u)\gt k$, $m(v)\leq k-2$ and $d(\{u_i, u_{i+1}\}, u_i)>0$. Let us construct a new $w$-distributing function $r(m)$ from $m$ so that
$$r(m)(e, u)= \begin{cases}
    m(\{u_i, u_{i+1}\}, u_i) -1 & \text{ if } (e,u)=(\{u_i, u_{i+1}\},u_i)\text { for some } 0\le i\le m\\
    m(\{u_i, u_{i+1}\}, u_{i+1}) +1 & \text{ if } (e,u)=(\{u_i, u_{i+1}\},u_{i+1})\text { for some } 0\le i\le m\\
    m(e,u) &\text{ otherwise }
  \end{cases}$$

$m$ and $r(m)$ agrees on all vertices except $v$ and $u$, $m(v)\lt r(m)(v)\le k-1$ and $r(m)(u)\lt m(u)$. We can apply this procedure on $r(m)$ to get $r^2(m)$. Repeating this $i$ time for some large enough $i$, we will obtain a $w$-distributing function $r^i(m)$ with $F_k(r^i(m))=0$. However, we have assumed that $F_k(m)>0$ is the minimum among $F(d)$ of $w$-distributing function $d$. This contradiction shows that we have proved the Erel-Apass theorem.


Why must a function with polymorphic type `forall t: Type, t->t` be the identity function? I am new to programming language theory. I was watching some online lectures in which the instructor claimed that a function with polymorphic type forall t: Type, t->t be the identity, but did not explain why. Can someone explain to me why? Maybe a proof of the claim from first principles.

The first thing to note is that this isn't necessarily true. For example, depending on the language a function with that type, besides being the identity function, could: 1) loop forever, 2) mutate some state, 3) return null, 4) throw an exception, 5) perform some I/O, 6) fork a thread to do something else, 7) do call/cc shenanigans, 8) use something like Java's Object.hashCode, 9) use reflection to determine if the type is an integer and increment it if so, 10) use reflection to analyze the call stack and do something based on the context within which it is called, 11) probably many other things and certainly arbitrary combinations of the above.

So the property that leads to this, parametricity, is a property of the language as a whole and there are stronger and weaker variations of it. For many of the formal calculi studied in type theory, none of the above behaviors can occur. For example, for System F/the pure polymorphic lambda calculus, where parametricity was first studied, none of the above behaviors above can occur. It simply doesn't have exceptions, mutable state, null, call/cc, I/O, reflection, and it's strongly normalizing so it can't loop forever. As Gilles mentioned in a comment, the paper Theorems for free! by Phil Wadler is a good introduction to this topic and its references will go further into the theory, specifically the technique of logical relations. That link also lists some other papers by Wadler on the topic of parametricity.

Since parametricity is a property of the language, to prove it requires first formally articulating the language and then a relatively complicated argument. The informal argument for this particular case assuming we're in the polymorphic lambda calculus is that since we know nothing about t we can't perform any operations on the input (e.g. we can't increment it because we don't know if it is a number) or create a value of that type (for all we know t=Void, a type with no values at all). The only way to produce a value of type t is to return the one that is given to us. No other behaviors are possible. One way to see that is to use strong normalization and show that there is only one normal form term of this type.


Bucket computation, cutting array with lines Given an NxN array, drawing a line from the edge's midpoint to the opposite field how can the N buckets be found covering the majority of the line's path?

A visual aid:

Is there a better way to this than computing the linear equation and iteratively advancing in tiny steps to check which bucket we fall on? If not what is the lower limit step size to choose?

For the considered line you know the start position (xs, ys) and the end (xe, ye). For instance on the N=7 visual you provide, let's take the first upper left line:

xs = 0
ys = 4.5
xe = 7
ye = 2.5
(I use coordinates right, down starting from upper left corner).

Let's take a parameter t of the linear position on the line with t=0 on start and t=1 on end. You know how many verticals or horizontals your line crosses and at which t value. In our exemple:

6 verticals crossed at t = v/7 with v=1 to 6 (not counting outlines).
2 horizontal crossed at t = 0.25 and t = 0.75.

Now just sort t increasing all these crossings:

(1/7, V), (0.25, H) (2/7, V), (3/7, V), (4/7, V), (5/7, V), (0.75, H), (6/7, V).

They correspond to cell change starting in cell (1, 5) to cell (7, 3). So you can compute the relative length of the line in each cell. For instance:

cell (1, 5) L = 1/7-0 = 1/7
cell (2, 5) L = 0.25-1/7
...

And you know how to select the X pixels now.


Distinguishability given black box access to the distribution Consider two probability distributions $D$ and $U$, over $n$-bit strings, where $U$ is the uniform distribution. We are not given an explicit description of $D$: we are only given black-box access, ie, we are only given a sampling device that can sample from $D$. Consider a sample $z \in \{0, 1\}^{n}$, taken from either $D$ or $U$. We want to know which one is the case, and to do that, we consider polynomial-time algorithms that use the sampling device.
Let the best distinguisher algorithm use the black-box sampling device a polynomial number of times (at most) and get samples $z_{1}, z_{2}, \ldots, z_{k}$ from $D$, for some polynomial $k$. My intuition is that, if this best algorithm decides that $z$ indeed came from $D$, then it must be true that $z_{i} = z$ for at least one $i \in [k]$. In other words, since we know nothing about $D$ or its support, we have to "see" $z$ at least once in the samples we collect from $D$ to ascertain that $z$ indeed came from $D$. How do I mathematically formalize this statement?
Also, does this same intuition hold if we are given a polynomial number of samples as input (taken from either $D$ or $U$) instead of just one and are also given access to a black-box sampler for $D$?

You can't.  Your intuition is wrong.  I will give an explicit counter-example.  Actually, I'll give you two: two for the price of one.
Suppose $n=1$, the distribution $D$ always outputs 1, and $U$ is uniform on $\{0,1\}$.  The following algorithm is an optimal distinguisher:

Never use the black box.  If the input $z$ is 0, guess that it came from $U$, otherwise guess that $z$ came from $D$.

Suppose we run this algorithm on an input $z$ and it guesses that $z$ came from $D$.   Then it's not true that $z$ must be equal to one of the queries to the black box; the algorithm didn't make any queries to the black box.
If you're not happy with that, you can obtain another explicit counterexample by considering the following algorithm, with $U$ being the uniform distribution and $D$ a distribution that outputs $1$ with probability $3/4$ and $0$ with probability $1/4$:

If the input $z$ is 0, get a sample $z_1$ from the black box, ignore $z_1$, and guess that $z$ came from $U$.
Otherwise, get a sample $z_1$ from the black box, ignore $z_1$, and guess that $z$ came from $D$.

Notice that if this algorithm guesses that $z$ came from $D$, it is not necessarily true that $z=z_1$ (it can happen that $z=1$ but $z_1=0$), so your claim is not true about this algorithm either; yet this algorithm is an optimal distinguisher.
It's often useful to test your intuition on some simple examples.
I suspect what you're missing is that the adversary is assumed to know the distributions $D,U$ in advance and then choose an algorithm based on knowledge of $D,U$ -- a different distinguisher algorithm for each different $D$.  There's no requirement to choose a single algorithm that works for all $D,U$.


Is it possible to find the nth term  of a Fibonacci sequence using a definitive for loop? I'm using the book Introduction to Computer Science by John Zelle and at the end of Chapter 3 (Computing with numbers), I'm asked to find the nth term of a Fibonacci sequence presumably using a definitive for loop, as no other decision structure has been introduced yet.

Is this possible? I've tried everything I could think of.

**I know how to solve it using if statements and such. But the book hasn't yet covered decision structures, yet it asks me to find the nth term(given by the user). So I can only presume to know how to do this using "for" loops as this is all that has been covered so far

If it is only the third chapter, I doubt the authors have covered dynamic programming, but I will illustrate what is going on when a for loop is used to compute the $n^\text{th}$ Fibonacci number, $F_n$.

Recall the definition,
$$F_n = \begin{cases} 0 & n = 0\\
1 & n = 1\\
F_{n-1} + F_{n - 2} & \text{otherwise}
\end{cases}$$

We could naively compute this using a recursive function defined in Python as,

def fib(n):
    if n < 2:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

However by recomputing the same sub-problem many times, this function requires exponential time to compute (illustrated below)!

There is a fix, though. We can use dynamic programming to do "smarter" recursion and keep our previous results around. This way, we don't need to recompute $F_i$. Our function call "tree" will collapse to a list and and will compute $F_n$ from the "bottom-up".

def fib2(n):
    if n < 2:
        return n
    else:
        if not results[n]:
            results[n] = fib2(n - 1) + fib2(n - 2)
        return results[n]

Now we have our $O(n)$ time algorithm to compute $F_n$, but if you notice, we require $O(n)$ additional space (one spot in the array for each $F_i$). This can be cut down to $O(1)$ additional space because each $F_i$ requires only two other fibonacci numbers, namely $F_{i-1}$ and $F_{i-2}$.

def fib3(n):
    if n < 2:
        return n
    f_0 = 0
    f_1 = 1
    f_n = 0
    for _ in range(n - 1):
        f_n = f_0 + f_1
        f_0 = f_1
        f_1 = f_n

    return f_n


Relating a proof to a Haskell program I am trying to relate the following integer square root theorem

$\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land  (x < (y+1)^2))$

and its proof to its role as a specification of the Integer Square Root isqrt ($\lfloor \sqrt{x} \rfloor$) function in a Haskell program.

Below is a inductive proof of the theorem and the related Haskell program.
The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $\leq$ in Fitch.

For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving  $\exists$-Elimination and $\lor$-Elimination.

I used Quickcheck as a reasonable check that the theorem holds in the code.

I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement  the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.

Is there a technical name for this form of proof to program relation?
I would be grateful for an explanation or pointer to the literature.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z
x *@ S y = (x *@ y) +@ x
-- square
sqr x = x *@ x
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n
_=@ _  = False

-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False
Z <@ x | not(x =@ Z) = True
x <@ Z | not(x =@ Z) = False
(S x) <@ (S y) = x <@ y

-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False

-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x

-- test with Quickcheck
instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.

Your goal is to “prove”  --I'm using bullets “•” for syntactic separators--
$$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x < (y+1)²$$

Proof Methods

In the natural deduction style, one proves “∀ x : ℕ • P x” by proving
two statements:

Base case      :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function

Where, in this case,
$$P x \;\;≡\;\; ∃y \;•\; y² ≤ x < (y+1)²$$

In the constructive fashion, one proves “∃ y • Q x” by
actually finding such a $y$ using whatever data is available.

Base case

For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.

Inductive step

For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).

However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a < (b+1)²$ --which looks really close to the goal (*).
To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a < (b + 1)²$$
So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$

But from (1) we also have $a < (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$
Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).

Curry-Howard: Proving ≅ Programming

The above was a proof [sketch] which corresponds to the a program.

A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program

-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0  = “the y found in the base case of the proof”
prog n  = “the y found in the inductive step,
             along with any conditionals and recursive calls”

Applying this to our above proof yields,

prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
         in
           if   a + 1 <= (b + 1) * (b + 1)
           then b
           else b + 1

Hope that helps :-)