title: Uniform sampling with constraints

text:
# Question
Title: Uniform sampling with constraints
Suppose one wants to uniformly sample a string $w$ of a given length over a finite alphabet, such $w$ satisfies a set of structural constraints (such as - "the third character has to be equal to the first character and the last character has to be equal to the second one").
The obvious method is to uniformly sample $w$, check if the constraints hold and return it if so. However, I am dealing with the case where there are many constraints, and the probability of random string to satisfy them is extremely low. Is there a way to sample uniformly from the set of all strings satisfying the set of constraints?

# Answer
If your constraints can be described using a small DFA, then you can use *sampling-by-counting*, which works in the following way. For each $\sigma \in \Sigma$, count the number of legal strings starting with $\sigma$ (as explained below), and use this to sample the first character, say $\sigma\_1$. Then, count the number of legal strings starting with $\sigma\_1 \sigma$ for all $\sigma \in \Sigma$, and use this to sample the second character; and so on.

It remains to explain how to count the number of strings of length $n$ with prefix $x$ accepted by a given DFA. Let me start with the case $x = \epsilon$. The idea is to use the *transfer matrix method*: construct a matrix $A$ in which $A(q\_1,q\_2)$ is the number of edges from $q\_1$ to $q\_2$ in the DFA (that is, the number of symbols $\sigma$ such that $\delta(q\_1,\sigma) = q\_2$). It is not hard to check that $A^n(q\_1,q\_2)$ is the number of words of length $n$ which carry the DFA from $q\_1$ to $q\_2$. Taking $q\_1$ as the initial states and summing over all final states for $q\_2$, we obtain the number of words of length $n$ accepted by the DFA.

Given a prefix $x$, we do exactly the same, only counting words of length $n-|x|$ that are accepted by the DFA when started at state $\delta(q\_0,x)$.

---

As a simple example, you can use this technique to sample a word of length $2n$ over $\\{a,b\\}$ having an equal number of $a$ and $b$. Although the corresponding infinite language isn't regular, you can construct a DFA for this language which has $O(n)$ states, making the above approach feasible. In this particular case there are also known closed formulas for the number of words of length $n$ with prefix $x$.

---

With some work, you can probably extend this approach to context-free grammars. One thing to try would be to extend the CYK algorithm so that it counts the number of words of given length with a given prefix.
> 2 votes

---
Tags: probability-theory, probabilistic-algorithms, sampling
---


title: Which word to pump in pumping lemma?

text:
# Question
Title: Which word to pump in pumping lemma?
Let say we have a Language $L = \\{0^m1^n \mid m,n \geq 0 \land m \neq n \\}$. If I want to use the pumping lemma to disprove that the language is regular or context-free, how do I choose the word in dependence of the number $n$? The problem is that I got an $m$ and an $n$ in the exponent and they cannot be equal. Can I choose $0^{n+1}1^n$ for the word?

# Answer
You can use any word in the language that lets you complete a proof. The pumping lemma says that, if a language $L$ is regular/context-free, then every long-enough string in the language can be partitioned in a way that generates an infinite set of strings that are also in $L$. So, if you can find any string in $L$ where the partition generates strings outside $L$, you're done.

Finding the right string to start with requires some thought and creativity; I'm not aware of any general method for doing it. I've not written anything out but I think that, if you start with $0^{n+1}1^n$, the proof won't work. However, you should try doing the proof with that string. Assuming that you don't make any mistakes, there are two possible outcomes:

* you win by successfully proving that the language isn't regular;
* you find that the proof doesn't work, and if the reason is the one I'm expecting, it should guide you straight to a better string to try to pump.
> 4 votes

---
Tags: formal-languages, pumping-lemma
---


# Question
Title: How are lookup tables described from the perspective of complexity theory?
Lookup tables can convert a piece of computational time into space. I remember that it was a part of a complexity theory course, but I cannot recall how it's called in its terms. I know how to use lookup tables in code to increase performance of my applications, so I don't need a definition of it in common sense.

I want to know a formal definition of an approach like lookup tables in complexity theory.

# Answer
In "Computational Complexity: A Modern Approach" by Sanjeev Arora and Boaz Barak I've found the term space-time tradeoff.
> 0 votes

# Answer
Lookup tables take a key, and either provide a value according to the key or tell you that there is no value under this key.

Time and space requirements will depend on the implementation. It's usually not further mentioned if it is obvious what kind of implementation a reasonable person would use.
> 0 votes

---
Tags: complexity-theory, terminology
---


title: Huffman Coding - probabilities

text:
# Question
Title: Huffman Coding - probabilities
I am having trouble understanding a question related to Huffman Coding. We haven't studied it a lot, so I am not even sure how to start.

Given $n ≥ 2$ characters, with probabilities $p\_{1} \geq p\_{2} \geq ... \geq p\_{n}$ Let $p\_{i} = 2^{k\_{i}}$ with $k\_{i} \in \mathbb{N}$ and $\sum\_{i=1}^{n} p\_{i} = 1$

Show that $p\_{n-1} = p\_{n}$ and that the minimum expected codelength amount to $$- \sum\_{i=1}^{n} p\_{i} \log p\_{i}$$

Help?

# Answer
> 0 votes
It's better to use the parametrization $p\_i = 2^{-k\_i}$. Multiply the equation $\sum\_{i=1}^n p\_i = 1$ by $2^{k\_n}$ to get $$ \sum\_{i=1}^n 2^{k\_n-k\_i} = 2^{k\_n}. $$ The right-hand side is even, so the number of $i$ such that $k\_i = k\_n$ must be even as well (why?). This implies that $p\_{n-1} = p\_n$.

For your second question, it is known that the minimum expected codeword length is at least $H(p) = \sum\_i p\_i \log (1/p\_i) = \sum\_i p\_i k\_i$. The converse to Kraft's inequality shows that there is a prefix code with codeword lengths $k\_1,\ldots,k\_n$, and so with expected codeword length $H(p)$.

---
Tags: huffman-coding
---


# Question
Title: High-level requirements for a Proof of "Saving to the Database"
This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the techniques and key points to watch out for. I understand it would take a lot of work.

In learning about formal proof and verification, I've come across Operational Semantics, Hoare Logic, and Matching Reachability Logic. All of them are pretty low-level and describe how to prove stuff such as a while loop with a few assignment / arithmetic operations, but that's it.

I am wondering what the **general** / high-level requirements are to prove something like "saving a record through some https API to the database", where it goes through the network (https) and through a bunch of servers finally arriving at an array of replicated databases like MySQL.

In unit testing, you would simply write a test that the method (let's say `save()`) creates the record. You would make a database query and see if the record matched the record you thought it would be.

I am wondering what it would entail to write a **proof** of this (at a high level, just a few sentence description is all). What things would need to be proven. If you can't write a proof, then what if you still wanted to at least *partially prove* the system's correctness. What it would take.

It seems like you could write a Hoare Logic statement such as:

```
{P}
save({ type: 'asdf', foo: 'bar', a: 'b' })
{fetch('asdf', 'latest') == { type: 'asdf', foo: 'bar', a: 'b' }}

```

That's at least better than nothing. But I'm not sure if you can write a proof with just that.

Then to know that it actually was in the *database* and not in some cache in the browser, you would have to know that `fetch` had a proof that it went through the network to some API, and that API request went to the database, and the database did whatever. That's basically what I'm wondering, if creating a proof for `save` starts off with the Hoare Logic statement like above, and then progressively you add more detail to the proof. In this way it's almost developed like via TDD. At some point, then, I'm wondering when you could say "it is proven".

# Answer
> 5 votes
The SoftwareEngineering.SE link gives the wrong answer for the right reasons. You can only ever prove anything with respect to a *formal* model. Verifying that that formal model accurately captures reality (or at least accurately captures the parts you care about for your purposes) is an informal process. In many applications of formal methods, one of the most time consuming and difficult parts is creating and validating the formal model. For example, for the CompCert project they had to make both a formal model for the behavior of C *and* a formal model for the behavior of the target processor (at least for the instructions they use). Both of these are massive undertakings on their own.

It makes no sense to "add more detail to the proof". Either a statement has a proof or it doesn't. It's proven if it has a proof. All proofs are equivalent for this purpose. What you *can* add more detail to is the formal model. Except "add more detail to" has the wrong connotations. You generally want the *least* detailed model that is accurate and for which you can prove your desired properties, e.g. correctness. The only reasons to change to a more detailed model is 1) you can't actually prove what you want with the original model, 2) the original model is wrong in which case your new model is not compatible with it, or 3) which is really a variant of (1), there is a different program that you *could* write that exploits those details to achieve the same functional behavior but different non-functional properties such as performance or implementation simplicity. In all these cases we need a new proof because we've changed the statement we're proving: either by changing the program or by changing the assumptions.

There are two aspects to the use of a formal model. First, as far as your program is concerned, it doesn't care if the database saves the data or even if the database exists. It only cares that the operations it uses behave as specified with respect to a given formal model. That formal model can be very high-level and abstract with no reference to any notion of "database" or "network" or "HTTP". However, it will likely be quite complicated to soundly capture the realities of the actual underlying systems. Second, at the systems level, you certainly *do* care whether the data was committed to the database as opposed to just being stored in some local cache. At the level of the program, there is absolutely no way for you to guarantee this. Your program could always be running in a sandbox that mimics any observable behavior. All you can prove at the program level is that your program will invoke some sequence of operations that putatively will lead to data being committed to the database. At some point you just have to accept based on empirical evidence that the chosen real world implementation faithfully implements the formal model. You can provide an implementation of the primitives of a high-level model with respect to a lower-level formal model that has been proven correct if you want to reduce how much you need to accept without (mathematical) proof.

The current state of play is that most *programming languages* lack publically available, normative (mechanized!) formal models let alone the underlying hardware. Ipso facto, most standard libraries, applications, operating systems, drivers, etc. are not proven correct since they have nothing with respect to prove their correctness. This is both in the sense that there isn't a formal model of what "correct" even means, nor is there a formal model of the implementation language so that you know what the implementations even do. In other words, in most cases we neither know what an implementation does nor what we even want it to do. This is why the artifacts (and tooling) produced by the CompCert projects and its related projects and by the $\mathbb K$ framework folks and several other groups are so important. Without these artifacts, you either use some massively over-simplified and weakly verified formal model that implicitly assumes millions of lines of codes are "correct" (spoiler: they aren't)1, or you invest man-centuries building a chain of trust. With luck, in the near-ish future some critical mass of formalization will be reached and proving the correctness of your program will become proportional to the complexity of your program and not the entire ecosystem.

1 While using an oversimplified formal model doesn't provide most of the benefits of "provable correctness", it does, in practice, do an excellent job of improving code quality by revealing mistaken assumptions in the code. Of course, the mistaken assumptions in your formal model have to be detected the old-fashioned way for the most part.

---
Tags: proof-techniques, formal-methods, software-verification
---


# Question
Title: Since physical memory is the RAM where is logical memory stored on the computer?
Since logical memory maps to the RAM (physical memory) it has be stored somewhere right and it will obviously take large bunch of memory of itself. Where is it stored?

# Answer
> 2 votes
I'm not sure what you mean by "logical memory"...

Memory is usually composed of physical memory and virtual memory. Physical memory is usually RAM, hard drives, solid-state drives, etc. It's the actual chips and stuff you plug into your computer (hence "physical").

However, it would be impractical if a larger scale OS is trying to run various applications at once and we only use this memory in a sequential manner, right? That's where virtual memory and virtual mapping comes into play. It's a matter of optimization used by the OS to improve performance.

"It" isn't exactly "stored" anywhere.

# Answer
> 1 votes
Logical memory is stored in physical memory, and in various places on your hard drive. The usual places are a swap file (stores data from logical memory that has been modified but not used for a while), and memory mapped files. For example, software playing an 8 GB video file may "memory map" that file, which means the logical memory is increased by 8 GB, and those 8 GB are stored in the video file.

---
Tags: operating-systems, memory-management, memory-access, c
---


# Question
Title: How to prove $c = a + b$ using Program Verification Techniques
I am trying to prove an elementary thing, but it seems at some point you get down to *atoms* where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an atom.

\begin{align} \\{a, b\\}\\ c = a + b\\ \\{a, b, c = a + b\\} \end{align}

This is my attempt at a Hoare assertion. It says "given $a$ and $b$, if I assign $c$ to $a + b$, then I end up with $a$ and $b$ unchanged, and $c$ assigned to $a + b$." That is, it's saying "if I do $c = a + b$, then I end up with $c = a + b$," which feels reduntant. In addition, this seems hard to formalize in programming. If the form is $\\{P\_1\\}\ Q\ \\{P\_2\\}$, then $Q$ and the $c$ part of $P\_2$ is the same code, namely $c = a + b$. So I don't see there being any need to write an assertion for addition, we can just state it's properties (that it returns a number) and it is proven *by definition*. That is, it's an axiom.

Wondering if this is true, or where I am missing something. Because when I tried writing this out in software I end up with basically what it looks like in that definition of the Hoare assertion above, $c = a + b$ twice.

# Answer
We can prove the Hoare triple

\begin{align} \\{{\sf true}\\}\\ c = a + b\\ \\{c = a + b\\} \end{align}

using the assignment rule. We take the postcondition $c = a + b$ and we substitute backwards $\\{(a+b)/c\\}$, so we get $(c = a + b)\\{(a+b)/c\\} = (a+b=a+b)$. That's the weakest precondition. Hence, we proved

\begin{align} \\{a+b = a+b\\}\\ c = a + b\\ \\{c = a + b\\} \end{align}

We can then use the weakening/strengthening/pre-post rule to rewrite $a+b=a+b$ as $\sf true$, since they are equivalent logical formulae.
> 1 votes

---
Tags: hoare-logic
---


# Question
Title: Proving that DFA equivalence is decidable
The following question is taken from Sipser:

> Prove that $EQ\_{\mathsf{DFA}}$ is decidable by testing the two DFAs on all strings up to a certain size. Calculate a size that works.

Here is the answer:

> For any DFAs $A$ and $B$, $L(A) = L(B)$ if and only if $A$ and $B$ accept the same strings up to length $mn$, where $m$ and $n$ are the numbers of states of $A$ and $B$, respectively. Obviously, if $L(A) = L(B)$, $A$ and $B$ will accept the same strings. If $L(A) \neq L(B)$, we need to show that the languages differ on some string $s$ of length at most $mn.$ Let $t$ be a shortest string on which the languages differ. Let $l$ be the length of $t$. If $l \leq mn$ we are done. If not, consider the sequence of states $q\_0,q\_1,\dots,q\_l$ that $A$ enters on input $t$, and the sequences of states $r\_0,r\_1,\dots,r\_l$ that $B$ enters on input $t$. Because $A$ has $m$ states and $B$ has $n$ states, only $mn$ distinct pairs $(q,r)$ exist, where $q$ is a state of $A$ and $r$ is a state of $B$. By the pigeon hole principle, two pairs of states $(q\_i,r\_i)$ and $(q\_j,r\_j)$ must be identical. If we remove the portion of $t$ from $i$ to $j-1$, we obtain a shorter string on which $A$ and $B$ behave as they would on $t$. Hence we have found a shorter string on which the two languages differ, even though $t$ was supposed to be shortest. Hence $t$ must be no longer than $mn$.

Unfortunately, I do not understand the sequence of steps in the answer. Could anyone explain the answer for me in a simpler way?

# Answer
> 5 votes
Here is a slightly different proof, along similar lines.

**Lemma 1.** Let $A$ be a DFA having $n$ states, and let $B$ be a DFA having $m$ states. There is a DFA $C$ having $nm$ states such that $L(C) = \[L(A) \setminus L(B)\] \cup \[L(B) \setminus L(A)\]$.

The proof uses the product construction (exercise).

**Lemma 2.** Let $C$ be a DFA having $p$ states. If $L(C) \neq \emptyset$ then $L(C)$ contains some word of length at most $p-1$.

**Proof sketch.** The language $L(C)$ is non-empty if some final state $q\_f$ is reachable from the initial state $q\_0$. The shortest path from $q\_0$ to $q\_f$ has length at most $p-1$, and this corresponds to a word of length at most $p-1$ in $L(C)$.

**Theorem.** Let $A$ be a DFA having $n$ states, and let $B$ be a DFA having $m$ states. Then $L(A) = L(B)$ iff for all words $w$ of length at most $nm-1$, either $w \in L(A),L(B)$ or $w \notin L(A),L(B)$.

**Proof.** If $L(A) = L(B)$ then the condition clearly holds. If $L(A) \neq L(B)$ then $\Delta := \[L(A) \setminus L(B)\] \cup \[L(B) \setminus L(A)\] \neq \emptyset$. According to Lemma 1, there is a DFA having $nm$ states whose language is $\Delta \neq \emptyset$. According to Lemma 2 (with $p = nm$), there exists a word $w \in \Delta$ of length at most $nm-1$. This is a word for which it *doesn't* hold that either $w \in L(A),L(B)$ or $w \notin L(A),L(B)$.

---
Tags: complexity-theory, turing-machines, computability, undecidability
---


title: Compression with random dictionary

text:
# Question
Title: Compression with random dictionary
Is the following scenario theoretically possible, or provably impossible?

Alice generates a 1 GiB file with random bits and sends it to Bob. This file is a shared dictionary they call Q. Now, Alice and Bob starts sending each other new files with arbitrary entropy, each of them \< 1 MiB, but they compress them with a clever algorithm that exploits information in Q, typically breaking the Shannon limit.

# Answer
This is provably impossible. The proof of Shannon's theorem goes through as usual.

As a simple example, suppose that are looking for an algorithm that compresses all $n$-bit strings to smaller strings. This is impossible since there are $2^n$ possible inputs, but only $2^n-1$ possible outputs. The proof of Shannon's theorem is very similar. Note how $Q$ makes absolutely no difference.

What happens if you choose a random 1 MiB window of $Q$ as your file? This can easily be compressed to 30 bits, by sending the location of the window. However, in this case the entropy of $Q$ is indeed at most 30 bits, since there are at most $2^{30}$ different windows.
> 1 votes

---
Tags: data-compression
---


# Question
Title: Print all subsets of a set ($a$) of $n$ positive integers, such that the product of their elements equals $p$
I have the following problem:

> Given a set *a* of *n* positive integers, write a *backtracking* C function that prints out all the subsets of *a* such that the product of their elements is *p*. Use an array for implementation of the set. What is the time complexity?

I have already solved the problem, both the idea and the C code is given below. *My questions are:*

1. How do I calculate the time complexity of my solution?
2. Is there a better way to solve this problem?

# My idea:

The function *f* takes *a*, *n*, *p*, and furthermore a variable *idx* for the current index in the array, and a boolean array *subset* which marks which elements in *a* are in the subset considered by this iteration of *f*.

First we iterate through *subset* and for each element in *a* currently in the subset, we multiply it by the product variable (initialized to 1).

If at any point during this iteration the product equals *p* we print out the elements in *subset*.

However if at any point the product becomes larger than *p* we return immediately. No further multiplication by positive integers could possibly bring the product down.

If the product is less than or equal to *p* after the iteration is done, we iterate through each of the elements in *a*, after *and including* *idx*, for each making a copy of *subset*, adding the element to it and calling the function recursively for the next *idx* and the copy of *subset*.

We have to do this even if the product is equal to *p* because I cannot assume the set is sorted; there may be a 1 down the road which would also give a result of *p* if added to the current subset.

What this means is that the function, called initially with an empty *subset* and *idx* of 0, will evaluate the possible subsets in the following order:

```
{}
{ 0 }
{ 0, 1 }
{ 0, 1, 2 }
..
{ 0, 1, 2 .. n-1 }
{ 0, 1, 2 .. n-1, n }
{ 0, 1, 2 .. n-2, n }
{ 0, 1, 2 .. n-3, n-1 }
{ 0, 1, 2 .. n-3, n-1, n }
{ 0, 1, 2 .. n-3, n }
{ 0, 1, 2 .. n-4, n-2 }
{ 0, 1, 2 .. n-4, n-2, n-1 }
{ 0, 1, 2 .. n-4, n-2, n-1, n }
{ 0, 1, 2 .. n-4, n-2, n }
{ 0, 1, 2 .. n-4, n-1 }
{ 0, 1, 2 .. n-4, n-1, n }
{ 0, 1, 2 .. n-4, n }
..
{ 0, 2 }
{ 0, 2, 3 }
..
{ 1 }
{ 1, 2 }
..

```

And so on, you get the picture.

# Time complexity?

I found both my idea and code too tough for trying to deduce the time complexity from, so I the first thought was that the time complexity must be $O(2^n)$ because it goes through all the $2^n$ subsets.

However, it *doesn't* go through all of them. If it detects a subset *s* the product of whose elements exceeds *p*, it immediately rejects both *s* and all other subsets of *a* that also have the offending *s* as a subset.

Does this impact the big O class, and if so, how? A rule of thumb I could apply to similar problems would be preferable to me instead of (or in addition to) any hard-to-digest theory.

# The code:

```
#include <stdio.h>
#include <stdbool.h>
#include <stdlib.h>

void
f(
    unsigned *a,
    int n,
    int idx,
    unsigned p,
    bool *subset
)
{
    unsigned product = 1;
    bool empty_subset = true;

    for(int i=0; i<n; i++) {
        if(subset[i] == true) {
            product *= a[i];
            empty_subset = false;
        }

        if(product > p)
            return;
    }

    if(product == p && !empty_subset) {
        for(int i=0; i<n; i++)
            if(subset[i])
                printf("%u, ",a[i]);
        printf("\n");
    }

    if(idx >= n) return;

    for(int i=idx; i<n; i++) {
        bool *newsubset = (bool*)malloc(sizeof(bool) * n);
        for(int j=0; j<n; j++)
            newsubset[j] = subset[j];

        newsubset[idx] = true;

        f(a, n, ++idx, p, newsubset);

        free(newsubset);
    }
}

```

# Answer
> 0 votes
Suppose the set is

$$a = \\{2,3,6\\} \cup \\{5,7,35\\} \cup \\{11,13,143\\} \cup \\{17,19,323\\} \cup \cdots \cup \\{p\_{2k-1},p\_{2k},p\_{2k-1}p\_{2k}\\}.$$

(Do you see the pattern? It has $3k$ elements, composed of $k$ groups of three. The $i$th group contains $p\_{2i-1}$, the $2i-1$th prime, and $p\_{2i}$, the $2i$-th prime, and their product.)

Also, suppose the product you want to hit is $p=p\_1p\_2 \cdots p\_{2k}$.

Then this set has at least $2^k$ subsets that multiply to this value. In particular, in each group, you can either pick the first two terms, or you can pick the third term.

So you'll need to output at least $2^k$ sets. This means the running time on an input of size $3k$ can be as large as $2^k$. Or, in other words, the running time on an input of size $n$ can be as large as $2^{n/3}$. This is exponential in the length of the input. Therefore, the worst-case running time is exponential. When we ask about the complexity, we usually implicitly mean the worst-case running time. Therefore, the complexity is exponential. Even though sometimes you might do much less work than that, sometimes you do fully exponential work, so we call the complexity exponential.

Unfortunately, I'm not aware of any simple rule of thumb that suffices for this case. Sometimes you have to figure out what's going on, and that might require a more deep analysis.

---
Tags: sets, backtracking
---


title: NFA accepting the empty string

text:
# Question
Title: NFA accepting the empty string
Suppose I have an NFA with accepting state q1(which is also an accept state) and non-accept state q2, with ε-transition from q1 to q2.

Also, suppose that empty string is inside the language. Then I want to know if the empty string is accepted by the above NFA following the standard definition:

Here, $\mathcal{P}(Q)$ denotes the power set of Q. Let $w = a\_1 a\_2 \ldots a\_m$ be a word over the alphabet $\Sigma\_\epsilon$. The automaton $M$ accepts the word $w$ if a sequence of states, $r\_0,r\_1, \ldots, r\_n$ exists in $Q$ with the following conditions with $m \>= n$ and $m\>=0$:

$r\_0 = q\_0$

$r\_i+1 \in \Delta(r\_i, a\_i+1)$, for $i = 0, \ldots, n−1$

$r\_n \in F$

I know it would be much easier to figure out whether the given string is accepted by NFA by visualizing what's going on in the NFA, but I find the formal definition above rather confusing because it's only checking the existence of one particular branch of computation that satisfies the above three conditions. I know that an empty string is w = ε or \[blank\]. By blank, I mean it has no symbols (where m = 0). But if I take w = ε, it would move from q1 to q2 via following ε-transition.But if I take w = \[blank\], then the sequence of state would be just q0, then it would be accepted. Is this the right way of thinking about it?

# Answer
> 1 votes
> Is this the right way of thinking about it?

No.

An NFA (with or without $\varepsilon$-transitions) accepts if there is any sequence of transitions that leads to an accepting state, regardless of whether there are other sequences that lead to non-accepting states. If the start state is accepting, then the empty string is accepted because the null sequence of transitions (no transitions at all) leads to an accepting state. It doesn't matter that there are other sequences that lead to non-accepting states.

$\varepsilon$-transitions are annoying to define formally. Informally (but completely accurately), they just allow the automaton to change state without reading an input character.

# Answer
> 0 votes
Perhaps the following alternative description of NFA with $\epsilon$-transitions would help clarify matters. The first step is to replace $\epsilon$ with some other symbol, say $\underline{\epsilon}$, in the NFA. We can now think of it as an NFA without $\epsilon$ transitions. The semantics of the NFA are as follows:

> For an alphabet $\Sigma$, let $h\colon \Sigma \cup \\{\underline{\epsilon}\\} \to \Sigma^\*$ denote the homomorphism which deletes $\underline{\epsilon}$: $h(\sigma) = \sigma$ for $\sigma \in \Sigma$, and $h(\underline{\epsilon}) = \epsilon$.
>
> An NFA with $\underline{\epsilon}$-transitions over $\Sigma$ accepts a word $w$ if and only if it accepts some word in $h^{-1}(w)$ \*as an NFA over $\Sigma \cup \\{\underline\epsilon\\}$.

In words, suppose that $A$ is a NFA with $\underline\epsilon$ transitions over an alphabet $\Sigma$. We can also consider it as an NFA $A'$ over $\Sigma \cup \\{\underline\epsilon\\}$ *without* $\underline\epsilon$ transitions. The automaton $A$ accepts a word $w$ iff $A'$ accepts some word $w'$ such that if we delete all $\underline\epsilon$ symbols from $w'$ then we obtain $w$.

---
Tags: automata, finite-automata
---


title: Context free languages

text:
# Question
Title: Context free languages
I have stumbled on this question:

Which of the following languages over the alphabet ${a,b,c,d}$ are context-free and which not ?

a) $L\_{1} = \\{wa^{3n+1}b^nw^{R} \mid w\in \\{c,d\\}^\*,\ n\>0\\}$;

b) $L\_{2} = \\{a^{3n+1}wb^nw^{R} \mid w\in \\{c,d\\}^\*,\ n\>0\\}$.

For a) I think this grammar solves it :

\begin{align\*} S&\to cMc \mid dMd \mid M\\ M&\to aN\\ N&\to aaaTb \mid\varepsilon\\ T&\to \varepsilon \end{align\*}

b) doesn't look so nice so I think that we might prove it with the pumping lemma,any suggestions what word to pick?

# Answer
I think you could use the Pumping Lemma for Contextfree languages to prove that the language (b) is not contextfree. Have a look at the word $a^{3n+1}cdb^ndc$, given n as the Pumping Length.
> 1 votes

---
Tags: context-free, formal-grammars
---


# Question
Title: A general question in type of computer science
Where can I find a source for questions/problems with data structures (like questions about avl trees , rank-trees, 2-3 trees, heap) and algorithms?

I will be happy for a references in these topics (I tried to search it in google,but I don't find appropriate something).

# Answer
> 0 votes
Here is a web portal that helps all computer scientists by selecting what level you're in i.e. Medium,expert... https://www.geeksforgeeks.org

Since data structures and algorithms are quite many,hoping you will do what best suits your computational problems.

---
Tags: algorithms, data-structures
---


# Question
Title: The difference between a Hoare Triple/Assertion and a Typed Function
I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function.

That is, say you have a typed function $f : A \to B$. The initial state for the function is thus $A$, and the final state is $B$. Similarly, in Hoare Logic, it would be like $\\{A\\}\ f\ \\{B\\}$. It's like the Hoare Triple is a typed function *application* or something, but I'm sure functional programming has those typed as well.

The types could be complex types such as dependent types that have constraints on the input as well, so you can handle things like $x \> y$ and the like. So I'm wondering, what the differences are between Hoare Triples and Typed Functions (in any type system) generally.

# Answer
> 4 votes
You are putting your finger on angular stone of program verification. At a very rough and high level you can think a derivation in Hoare logic as proving a property, thing which can somehow be translated in a type derivation.

More precisely you are almost (you're slightly limiting yourself with Hoare logic) rediscovering the very deep Curry-Howard correspondence with asserts that mathematical proof and type derivation are the same thing.

# Answer
> 3 votes
To be frank, it much more difficult to see how types and pre-/post-conditions are similar than how they differ.

In Hoare Logic, for the Hoare triple $\\{A\\}\ f\ \\{B\\}$, $A$ and $B$ would be predicates on the *entire program state* and $f$ would be a sequence of instructions, not a function. For example, $A$ might be something like $$\mathtt i = 0\land \mathtt s = 0\land\mathtt n \> 0\land\texttt{overflow\_flag} = \mathtt{false}$$ and $B$ might be $$\texttt{overflow\_flag} = \mathtt{true} \lor (\mathtt i = \mathtt n\land \mathtt s = \mathtt n(\mathtt n+1)/2)$$ You might use this to describe a the pre-conditions and post-conditions of a loop that sums increments $\mathtt i$ up to $\mathtt n$ and has $\mathtt s$ hold the running sum but may set $\texttt{overflow\_flag}$ if the numbers get to big at which point there are no guarantees about anything. However, the pre-conditions and post-conditions don't imply this code. *Any* code that produces the appropriate output (i.e. a program state matching the post-conditions) given the appropriate input (i.e. a program state matching the pre-conditions) would be just as valid. For example, a program that just immediately set $\texttt{overflow\_flag}=\mathtt{true}$ or one that just directly set $\mathtt{i := n}$ and $\mathtt{s := n}(\mathtt n+1)/2$. There is nothing in the specification I gave that indicates under what circumstances $\texttt{overflow\_flag}$ will be set. Also, unless I'm using some framing convention, there is nothing stated about what happens to all the other variables in the program state. *If you want to ensure/know that the other variables were not changed, you have to explicitly state that.*

There are many issues with the Hoare Logic approach. It has no real notion of scope, so recursion, higher-order functions, and objects are very difficult to deal with. Also, this makes it very non-modular. For Hoare Logic, in your example $f$ doesn't represent a function, it represents a sequence of instructions. Let's say you have two separate blocks of code proven to meet two separately developed specifications. You'd like to combine both in your program. You can't simply sequentially compose them. If they use the same variable names for different things, you'll need to rename them. You'll need to add framing conditions to state that neither mutates the variables of the other. God help you if you want to do a concurrent composition, because Hoare Logic won't.

Modern descendants of Hoare Logic such as separation logic and Hoare Type Theory address these deficiencies of the original Hoare Logic. ynot, mentioned by Andrej Bauer in a different answer, is based on separation logic.

If it isn't obvious yet, the above is not at all reminiscent of most type systems. Most type systems don't have any way of referring to run-time values in types. Even in most dependently typed systems, top-level types are generally meant to be closed, and certainly they refer to *values*, not mutable *variables*. Types usually don't allow arbitrary predicates of first-order logic, and type systems are usually designed not to require proving arbitrary theorems to type check. What you *can* do, though, and very roughly what ynot does, is make a tuple with all the program state and consider functions $S\times X\to S\times Y$ where $S$ is the type of the tuple of all the program state. You can then consider functions between subset types (perhaps represented by a dependent sum): $\Pi s:S.\\{x:X\mid P(s,x)\\}\to\\{(s',y):S\times Y\mid Q(s,s',y)\\}$. A function $f$ of this type would be akin to a Hoare triple $\\{P(s,x)\\}\ y\\, \mathtt{:=}\\, f(x)\ \\{Q(s\_{\text{old}},s,y)\\}$. Still, most function types (let alone arbitrary types) are not of this form. Going the other way, terms have types and, in particular, variables are assigned types. There is no analogue in Hoare Logic to assigning a type to a variable.

---
Tags: type-theory, hoare-logic
---


title: The halting problem for laymen

text:
# Question
Title: The halting problem for laymen
This line from Wikipedia made me want to ask this question:

> There is, however, no general procedure for determining whether an expression involving looping instructions will halt, even when humans are tasked with the inspection. The theoretical reason for this is the undecidability of the Halting Problem: there cannot exist some algorithm which determines whether any given program stops after finitely many computation steps.

Wondering what this is and what it means. Why is the Halting Problem undecidable. I don't understand, I feel like I could tell if a program terminates or not. Wondering what an example is of a program you can't tell will terminate or not.

# Answer
How about the Collatz Conjecture:

```
def f(n):
   if (n % 2 == 0):
      return n/2
   else:
     return 3*n + 1
n = read_input()
while (n != 1):
  n = f(n)

```

Will this program always halt? Nobody knows! It's an open problem in mathematics. You can run it for specific instances, and if it halts, you know that it halts. But if it doesn't halt, you never know when to quit. You could run it for 1000000 steps, but maybe it halts after 1000001 steps?

We may be able to intuitively determine which programs halt. This is because we write programs in ways that make their halting obvious: we write loops over finite numbers, we try to have recursion over strictly smaller arguments.

It turns out there is a large class of programs which are guaranteed to halt, and *almost* everything you can think of falls into this class. So most of the time, things you're running across on a daily basis will halt. But not every program is in this class.

The Halting problem says that there is no algorithm which can take *any* program which halts and return whether it halts or not. It doesn't mean that, given a *specific* program, we can never know if it halts.
> 4 votes

---
Tags: halting-problem
---


# Question
Title: How to prove a side effect in a function
I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and databases.

In this question I am wondering about a more middle-level proof, this time about transforming an object $f : A \to B$ with side effect $C$. Say I have as input a string $A$, and as output an Abstract Syntax Tree (AST) $B$. All of this happens in memory with a small string of say a few KB. Right now, ignoring all the details of the hardware implementation and all the details of any particular language.

I am wondering at a high level what it takes to prove something like this. Specifically I wanted to focus on **side effects** in this question. Say during the parse process, we create a global *symbol table* to store classes. Then as we are parsing through the code and we encounter the class, we add to the symbol table. So instead of $f : A \to B$, we really have:

\begin{align} f : A &\to B\\ &\downarrow\\ &C \end{align}

That is for the symbol table $C$ and AST output $B$. Somewhere in the function $f$ implementation there is another function $g : \\{C,c\\} \to C'$, which adds the new symbol $c$ to $C$.

What I would like to prove (in this question, just at a high level, some key points) is that the function generates the symbol table $C$, even though the *output* of the function is the AST $B$. In type theory, the proof for AST $B$ could possibly just be the sequence of type definitions and transformations, similar to Hoare Logic. But to prove that the function $f$ has side effect $C$ seems much harder/trickier.

It seems that you have to go and step through the algorithm one step at a time, and (assuming everything is strongly typed), figure out what the "current state" would look like at that point (of the whole program). Then you would compare your *pattern* (the assertion of the post-condition if it were Hoare Logic) with the current state of the program at that point, and see if it was a match. And see if that stayed true until the end of the function/algorithm. But this sort of seems like it's becoming Model Checking, which I only know the basics about, not sure if that is correct to assume though. Also, this one-step-at-a-time stepping through the algorithm seems like program *simulation*, so wondering if that is true or not or if simulation has a role here.

So I'm wondering, at a high level, what is required to prove that function $f$ generates a side effect $C$. As a specification, I would write "$f$ generates the symbol table $C$".

# Answer
> 3 votes
If the function has two outputs, a standard way to represent this is as a function $f: A \to (B \times C)$, i.e., $f$ outputs a pair of an AST and a symbol table.

If the function updates an existing symbol table, you could represent this as a function $f : (A \times C) \to (B \times C)$. It takes as an input a pair of a string and a symbol table, and outputs a pair of an AST and an updated symbol table.

You could also read about monads, which are a way to structure and reason about side effects in a functional programming language. They are notoriously challenging to understand.

You don't prove a side effect. You can prove a fact about the possible side effects, but you need to state what you are claiming; a side effect isn't something that can be proven or not. Similarly, you don't prove a function. You can prove the correctness of a function, if you specify what correctness means for that particular function, but you don't prove the function.

# Answer
> 3 votes
It depends on how you model the system and what proof approach you're using. For early versions of Hoare Logic, there isn't really any notion of "scope", so there's absolutely nothing special you need to do. You simply have a pre-conditions and post-conditions on the global state. For Hoare Logic, types have nothing to do with it.

In a bit more detail, in a Hoare triple like $\\{P\\}\ y\\,\mathtt{:=}\\,f(x)\ \\{Q\\}$, $P$ and $Q$ are predicates on the entire program state. If $f(x)$ updates some (global) variable, you simply include the appropriate condition in the post-condition $Q$. It's no different than $y$ or any of the other, presumably "local", variables $f(x)$ may mutate.

Most type theories have no notion of mutable state. If you want to talk about mutable state in such systems, you have to model it, e.g. via state passing (i.e. a state monad). In this case, a function $f:A\to B$ which may "mutate" some "global" state may be modeled as a function of type $S\times A\to S\times B$ where $S$ is a type representing "global" state. You can consider more refined versions of this type to capture the actual behavior.

---
Tags: proof-techniques, simulation, model-checking, hoare-logic
---


# Question
Title: Turing degree incomparable with any countable-ordinal jump of another Turing degree?
Among the Turing degrees are degrees of the form $0^n$, e.g. $0$, $0'$, $0''$, etc.

---

I'll just prove this quick for completeness' sake. Hopefully nobody has any qualms with this short proof:

Lemma: Any countable set of sets of natural numbers can be encoded as a single set of natural numbers, such that each original set can be decoded by a Turing machine.

Proof: Let $S$ be our set of sets, so that each $S\_n \in S$ is a set of natural numbers. Define $O = \\{k \cdot 2^{n+1} - 2^n | k \in S\_n \\}$.

Thus, $S\_n = \\{ k | k \cdot 2^{n+1} - 2^n \in O \\}$. Clearly, for each $S\_n$ there is a Turing machine that computes $S\_n$ given an oracle for $O$.

Minor Theorem: Any countable set of Turing degrees has an upper bound.

Proof: Let $D$ be our countable set of degrees. Thus, each $D\_n \in D$ is a countable set of sets of natural numbers. Let $E\_n$ be a set of natural numbers that encodes the elements of $D\_n$, and let $E$ be a set of natural numbers that encodes all $E\_n$.

Any set in any degree $D\_n$ can be computed by decoding $E$ twice in succession, so as Turing degrees, $D\_n \leq \[E\]$. Therefore $\[E\]$ is an upper bound of $D$.

---

Let $0^\omega$ be the upper bound of $\\{0, 0', 0'', ... \\}$ as described just above. Of course, we can take the Turing jump of $0^\omega$ to obtain $(0^\omega)'$ which we will write $0^{\omega + 1}$, and so on to obtain the countable set of Turing degrees, $0^{\omega + n}$. Taking the upper bound of these, we obtain $0^{2 \omega}$, and of course, furthermore taking the upper bound of $\\{ 0, 0^{\omega}, 0^{2 \omega}, ... \\}$ we obtain the Turing degree $0^{\omega^\omega}$. Generally for any countable ordinal $\beta$, we can define a degree $0^\beta$.

It is known that for every nonzero Turing degree $a$, there is a Turing degree $b$ with which it is incomparable. However, for any Turing degree $a$ (and I'm particularly interested in $0'$), is there a Turing degree $b$ that is incomparable with $a^\beta$ for all countable ordinals $\beta$?

# Answer
> 7 votes
The answer to your question is a resounding: **IT DEPENDS**! This takes us into some set theory, which - while interesting - is a bit off the beaten track perhaps for CS; to address this, I've made the first part of my answer strictly about the computability theory, and then added a separate section on the set theory side of things.

---

Before we can even address your question, it turns out that there is a surprising subtlety here:

> For $\alpha$ an arbitrary countable ordinal, it is not always clear how to define $0^{(\alpha)}$.

*This is treated variously at mathoverflow and math.stackexchange; what I've written below should be self-contained, however.*

The issue is that of **presentations** (or, essentially identically, **fundamental sequences**). In general, suppose $\lambda$ is a limit ordinal, we've defined $0^{(\alpha)}$ for each $\alpha\<\lambda$, and we want to define $0^{(\lambda)}$ as the set $$Z\_\lambda=\\{(i, \alpha):i\in\omega,\alpha\<\lambda, i\in0^{(\alpha)}\\}.$$ However, this set isn't a set of natural numbers. Fixing a map $f:\lambda\rightarrow\omega$, we can "interpret" $Z\_\lambda$ along $f$ in a natural way: $$Z\_\lambda^f=\\{(i, j): i\in\omega, j\in ran(f), i\in 0^{(f^{-1}(j))}\\}.$$ Here's the problem: what $f$ do we want to use? Different choices of $f$ will yield different sets, and potentially different Turing degrees. This wasn't an issue in cooking up $0^{(\omega)}$, since there was only one obvious thing to do, but when we try to go further the problem rears its head.

*As a quick aside, there's an alternate approach here which seems promising at first: simply define $0^{(\lambda)}$ for $\lambda$ a limit ordinal to be the least upper bound of $\\{0^{(\alpha)}:\alpha\<\lambda\\}$! Combined with the clause $0^{(\beta+1)}=(0^{(\beta)})'$, this would seem to give a recursive definition which works for all countable ordinals. However, it turns out that this entire attack is built on a false assumption: $0^{(\omega)}$ is not the least upper bound of $\\{0^{(n)}:n\<\omega\\}$ in the Turing degrees, and in fact **nontrivial least upper bounds never exist** (this is the "exact pair theorem" of Spector). So we do necessarily have to do some work.*

At this point it's a good idea to go back and try to develop a theory of iterated jumps "from scratch" as it were. This is **hyperarithmetic theory** due to Kleene, and is presented in detail in the beginning of Sacks' book; I'll just give a rapid (and ahistorical) gloss.

The sets $Z\_\lambda^f$ defined above are intuitively what we get if we iterate the jump not along a mere *ordinal* but along an explicit well-ordering of a set of natural numbers (that is, a copy of the ordinal "labelled" appropriately). To make this precise, suppose $R$ is a well-ordering of some set $D$ of natural numbers (note that $R$ determines $D$). It's easy to show that there is a unique set $J\_R$ of ordered pairs of natural numbers with the following properties:

* $(x,y)\in J\_R$ only if $x\in D$.
* If $u$ is the $R$-successor of $v$, then $(u, y)\in J\_R$ iff $\Phi\_y^{J\_R\[v\]}$ halts, where $J\_R\[v\]=\\{z: (v, z)\in J\_R\\}$.
* If $u$ is an $R$-limit, then $J\_R\[u\]=\\{(v, y): v\<\_Ru, y\in J\_R\[v\]\\}.$

This is what you get, intuitively, if you iterate the jump along $R$ starting with the emptyset *(the fact that we started with the emptyset was built in secretly to the last bulletpoint, since if $u$ is the $R$-least element then $J\_R\[u\]$ is forced to be empty; we can relativize by starting with a non-empty column)*.

If $R$ is "nice," this is extremely well-behaved:

> Suppose $R\_0, R\_1$ are well-orderings of sets $D\_0, D\_1$ of natural numbers such that each $R\_i$ is computable, their respective successor operations are computable, and their respective sets of limit elements are computable. Then if $R\_0$ and $R\_1$ have the same ordertype we have $J\_{R\_0}\equiv\_TJ\_{R\_1}$.

The conditions above are stronger than merely demanding that the orderings be computable, but in fact every computable well-ordering is (non-computably!) order-isomorphic to such a "nice" computable well-ordering. So based on this, it makes sense to define $0^{(\alpha)}$ for $\alpha$ a "computable ordinal" as the unique Turing degree of a "jump sequence" along a "nice presentation" of $\alpha$. More generally, for any Turing degree $d$ it makes sense to talk about the degree $d^{(\alpha)}$ for any ordinal $\alpha$ with an $d$-computable presentation.

The sets computable from $0^{(\alpha)}$ for some computable $\alpha$ are the **hyperarithmetic sets**; hyperarithmeticity has a number of equivalent characterizations and is one of the fundamental notions of modern computability theory, and is also very important in descriptive set theory. But this only gets us through countably many ordinals; most countable ordinals don't have computable presentations! The supremum of the computable ordinals is denoted "$\omega\_1^{CK}$" - it's much bigger than other popular ordinals like $\epsilon\_0$, $\Gamma\_0$, etc., but still countable, and indeed quite small among countable ordinals from various perspectives within logic. And it's not very hard to cook up two Turing degrees, neither of which is hyperarithmetic relative to the other, since we've only reached "countably high." Can we do better?

To go further, we need to get into set theory, so I'll put a horizontal line here:

---

Alright, let's talk about set theory. It turns out that we **can** continue the jump in a natural way past $\omega\_1^{CK}$. However, this gets complicated pretty quickly. The idea comes from Godel's constructible universe, the idea being that each additional step in the $L$-hierarchy is like taking $\omega$-many jumps of what you have so far (since you're looking at everything first-order definable in what you have so far). Teasing this out precisely gets us the notion of **mastercodes**. I won't define them precisely here, but Hodes has an excellent paper on the topic.

Now, mastercodes have many subtle and annoying features,$^\*$ but they let us unproblematically(ish) iterate the jump starting with the emptyset all the way up to $\omega\_1^L$, the first ordinal which the constructible universe thinks is uncountable. *(More generally, given a degree $d$ we can unproblemantically "do mastercodes" up to $\omega\_1^{L\[d\]}$, the first orderinal that the smallest inner model of ZFC containing $d$ thinks is uncountable.)*

If the constructible universe happens to be all there is - that is, if V=L \- then we're peachy:

> Every real in $L$ is computable from some $0^{(\alpha)}$ - in the sense of mastercodes - for some $\alpha\<\omega\_1^L$.

More generally, "reachable via mastercodes" just gives us the notion of **relative constructibility**: $x\le\_Ly$ iff $x\in L\[y\]$ iff $x$ is in every inner model containing $y$ iff $x$ is computable from some $y^{(\alpha)}$ for $\alpha\<\omega\_1^{L\[y\]}$.

However, it's quite possible - that is, consistent relative to ZFC - that $V$ is very far from $L$. For example, $\omega\_1^L$ might be countable, and indeed the "real" $\omega\_1$ could appear to be quite large from the perspective of $L$! Indeed, it turns out that strong set-theoretic hypotheses can prevent us from getting very far at all with this idea:

> Broadly speaking, if **large cardinals** exist then there are no easily-definable increasing $\omega\_1$-sequences of Turing degrees. (This is parameterized: ramp up the large cardinals and we get more and more necessary undefinability.)

Even assuming $\omega\_1^L=\omega\_1$ *and* ruling out anything (like large cardinals) that will bump up consistency strength, the $\le\_L$-degrees could still be quite wild, via **forcing**. In particular, if $c\_0, c\_1$ are mutually Cohen generic (say) over $L$, then $c\_0\not\in L\[c\_1\]$ and $c\_1\not\in L\[c\_0\]$; we can get Cohen generics without changing $\omega\_1$, so in this case neither is reachable from the other via countably many jumps, assuming we buy the "mastercode picture" (and if we don't, we need to cook up another picture!).

---

$^\*$They really only make sense at the level of *degrees*, not *sets of naturals*, so in that sense the "presentation issue" hasn't been avoided; see the middle of page 207 of Hodes' paper. More obnoxiously, Theorem 8 (and see the bottom of page 204 for the relevant definition) shows that ... OK, there's just no nice way to say this, and I can't put it off anymore: *mastercode-jumps aren't fully monotone*. We can have $\alpha\<\beta$ but $a^{(\beta)}=0^{(\alpha)}$ for some degree $a$. Aaargh.

---
Tags: computability, turing-machines
---


# Question
Title: Unclear logic notation for PFX program rules
I'm very new to this so please bear with me.

I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the result.

The image is supposed to be the rules describing the logic of a PFX program, but being very new to logical symbols, I can barely read it.

From what I understand, the top parts are suppositions and the bottom parts are conclusions. The first one, to me, reads, if i is different from n, then if either of the vk's implies i, the program declares an error. But I can tell my understanding is deeply flawed. I searched and have found close to no similar rules.

Also, the use of the letter "i" seems unclear to me mostly.

If someone can explain with words what the rules actually mean, it would help me a lot.

Thank you.

# Answer
> 4 votes
The "fraction"-style notation is an inference rule in natural deduction style. See What is this fraction-like "discrete mathematics"–style notation used for formal rules?.

$v\_1,\dots,v\_n\vdash \cdots$ means "in the environment $v\_1,\dots,v\_n$, such-and-such is true". (It's not an "or", and it doesn't mean "implies".) See What does ⊢ mean in operational semantics?.

I recommend finding a good textbook on programming language semantics, and reading it. It will give you some background that will help you understand that notation. It's probably too much to explain all of that in a single answer here.

---
Tags: logic, compilers, semantics, first-order-logic, haskell
---


# Question
Title: If A is reducible to B and B is reducible to A, and A is NPC, is B also NPC?
I was thinking about the max-clique problem and the k-independent set problem. You can show that k-independent set is reducible to max-clique easily and you can show that max-clique is reducible to k-independent set (with a simple for loop). And k-independent set is NPC, so wouldn't that mean max-clique is also NPC, but it's not because we can't create a verifier, so I'm terribly confused. What wrong assumption am I making?

# Answer
> 1 votes
First, note that there are two problems frequently called the "Maximum Clique Problem".

One of them is the Clique Decision Problem: given an undirected graph $G$ and a number $k$, does $G$ contain a clique with at least $k$ vertices? This is one of Karp's 21 Problems, the original list that made NP-completeness famous. The proof involved reducing to it from the Boolean Satisfiability Problem, the very first original NP-complete problem. And a verifier for this is easy to make: check whether the set given as a solution actually does contain $k$ or more vertices, and is actually a clique.

The other is the Maximum Clique Size Problem: given an undirected graph $G$, what is the size of the largest clique in $G$? This can be shown to be NP-hard by reduction from the Clique Decision Problem, by simply comparing the size of the largest clique with $k$. And as you mentioned, it can *apparently* be shown to be in NP by reduction to the Clique Decision Problem: for every integer from the number of vertices down to 1, check if there's a clique of that size, and if so return that number.

So it would seem that both versions of the problem are NP-complete. But be careful about the definition of NP. NP is defined as a class of *decision problems*, and the Maximum Clique Size Problem is not a decision problem.

Specifically, NP is the class of decision problems where, if the answer is yes, you can be given extra information of polynomial size that lets you verify that the answer is yes in polynomial time. (If the answer is no, you can't necessarily verify it, unless NP = co-NP.) So for problems which aren't answered with yes or no, trying to put them in NP just doesn't make sense.

So while the Maximum Clique Size Problem is indeed NP-hard, and can be reduced to an NP-complete problem in polynomial time, it is *not* in fact in NP. And thus it cannot be NP-complete. This is why you can't make a verifier for it (unless NP = co-NP, which is an open question).

---
Tags: complexity-theory, reductions
---


# Question
Title: Why Does the Fixed Point Theorem Apply to Quines?
A quine is a program that outputs its own source code without taking in any input. An example would be this (taken from here)

```
public class Quine {
    public static void main(String[] args) {
        char quote = 34;
        String[] code = {
"public class Quine {",
"    public static void main(String[] args) {",
"        char quote = 34;",
"        String[] code = {",
"        };",
"        for(int i=0; i<4; i++){",
"            System.out.println(code[i]);",
"        }",
"        for(int i=0; i<code.length; i++){",
"            System.out.println(quote + code[i] + quote + ',');",
"        }",
"        for(int i=4; i<code.length; i++){",
"            System.out.println(code[i]);",
"        }",
"    }",
"}",
        };
        for(int i=0; i<4; i++){
            System.out.println(code[i]);
        }
        for(int i=0; i<code.length; i++){
            System.out.println(quote + code[i] + quote + ',');
        }
        for(int i=4; i<code.length; i++){
            System.out.println(code[i]);
        }
    }
}

```

Running this produces exactly the same output as the source code. I've heard that the fixed point theorem applies, meaning that any turing-complete programming language will contain a quine. However, the more I thought about this the less it made sense.

The rules for the fixed point theorem in mathematics are that it must be continuous, bounded surface with no holes or 'cutting and gluing'. This seems to make no sense in terms of programming languages.

The first rule can be broken by the nature of characters as not continuous, for example there is no inbetween 'a' and 'b' in terms of ASCII encoding.

The second rule can be broken by stating that there can be infinitely many programs all equally valid, for example you could have `System.out.println("");`, `System.out.println("a");`, `System.out.println("aa");`...`System.out.println("aaaaaaaaaaaaaaaaaaaaa");`.

The third rule can be broken by saying that not all programs are valid, for example `abstract System out.println(23");"` is not valid, however the build output could be used as the output, ie

```
Main.java:2: error: class, interface, or enum expected
  public static void main(String[] args) {abstract System out.println(23");"
                                                   ^
Main.java:2: error: ')' expected
  public static void main(String[] args) {abstract System out.println(23");"
                                                                        ^
2 errors

```

If all but one of the rules are broken, then why does the fixed point theorem still apply?

# Answer
> 5 votes
The fixed point theorem you are mentioning is the Brouwer fixed-point theorem. It is possible that there is some way to give a topology to computer programs and use homotopy theory to derive the existence of a fixed point, but a way to do this does not immediately spring to mind. Your objections do not completely make sense in the language of topology:

1. A topological space is not described as continuous, but rather connected or path connected. It is possible for a two-point space to be path connected even though there are no "in between" points along the path.
2. The interval $\[0,1\]$ has infinitely many points yet is bounded. It is not clear that infinitely many programs with the same output is an issue.
3. Invalid programs can be considered valid by giving them well-defined output. For example, the compiler error message. Or we restrict to the subspace of valid programs.

Out of my own interest for understanding how Quines follow from a fixed-point theorem, I'm going to outline a proof. This is derived from this webpage.

Let $S$ be the set of all finite strings from some alphabet, say ASCII, and let $P\subset S$ be the subset of all valid programs for some specific Turing-complete programming language. Let $I:P\times S\to S\cup\\{\bot\\}$ be the function where $I(p,s)$ is the output from running program $p$ with input $s$, else $\bot$ if the program does not halt (think of $I$ as an interpreter). Define tuple functions like ${\times}:S\times S\to S$ by $x\times y = \`\`\mathrm{(}"+x+\`\`\mathrm{,}"+y+\`\`\mathrm{)}"$. We define them in such a way that you can recover $x$ and $y$, for the purpose of changing the number of arguments to a function.

The programming language is universal, meaning there is some program $i\in P$ such that $I(p,s)=I(i,p\times s)$ for all $p\in P$ and $s\in S$. This can be interpreted as saying that $I$ can be implemented in itself as $i$.

There is a partial evaluation function $\pi:P\times S\to P$ with the property that $I(\pi(p,s),t)=I(p,s\times t)$ for all $p\in P$ and $s,t\in S$. In fact, there is a program $p\_\pi$ implementing it in the sense that $\pi(p,s)=I(p\_\pi,p,s)$ for all $p\in P$ and $s\in S$. In Java, this can correspond to pasting in $s$ as a string literal.

**Fixed-point theorem.** *If $F:P\to P$ is a computable function, then there is a program $p\in P$ such that for all $s\in S$, $I(p,s)=I(F(p),s)$.*

*Proof.* Let $\Delta:P\to P\times P$ be the computable function $\Delta(p)=p\times p$. The composition $F\circ \pi\circ\Delta$ is the computable function $q\mapsto F(\pi(q,q))$, where $\pi(q,q)$ is the program from giving $q$ to itself as one of its inputs. Let $m\in P$ be the program for the composition $F\circ\pi\circ\Delta$, so $I(m,q\times s)=I(F(\pi(q,q)),s)$ for all $s\in S$ (\*). Let $p=\pi(m,m)$. Then, $$I(p,s)=I(\pi(m,m),s)=I(m,m\times s)=I(F(\pi(m,m)),s)=I(F(p),s)$$ where the third equality uses $q=m$ in (\*). QED

Now to prove that there is a Quine. Let $\eta:P\to P$ be a computable function such that $I(\eta(p),\emptyset)=p$ for all $p\in P$. That is, $\eta$ wraps a program text up in a print statement. Applying the fixed point theorem, there is a program $p\in P$ such that $I(p,\emptyset)=I(\eta(p),\emptyset)$. That is, $I(p,\emptyset)=p$, so $p$ is a Quine.

This is all very much constructive, so you can use it to create (inefficient) Quines.

# Answer
> 6 votes
As Discrete Lizard points out, there exist more than one "fixed point theorem." The one you're mentioning makes sense in terms of topology and geometry, but you're right to realize that it does not apply to programming languages.

It turns out, though, that a more general notion of continuity, called Scott Continuity, can give you something that is applicable, namely the Kleene fixed-point theorem:

> Any Scott-continuous function over a directed-complete partial order has a least fixed point.

An earlier, and easier to understand, version of this is given by Knaster-Tarski:

> Any monotone function over a complete lattice has a fixed-point. In fact, the fixed points of such a function form a complete lattice.

---
Tags: fixed-point
---


# Question
Title: Finding the number of squares by connected coordinates
If I have a list of lists as below ,

```
 [[1, 2], [3, 4], [1, 5], [2, 6], [4, 8], [5, 6], [6, 7],
 [7, 8], [6, 10], [7, 11], [8, 12], [10, 11],
 [10, 14], [12, 16], [14, 15], [15, 16]]

```

and

```
[[1, 2], [2, 3], [3, 4], [1, 5], [4, 8],
     [6, 7], [5, 9], [6, 10], [7, 11], [8, 12],
     [9, 13], [10, 11], [12, 16], [13, 14], [14, 15], [15, 16]]

```

The above 2 lists can be visualized as in the image, where each point is represented by a list.

I know there is a graph traversal where every visited node can be tracked as we traverse through the graph. But in this case, there is no direction mentioned.

How should I approach this problem? I am also interested in hints.

# Answer
> 2 votes
Let $b(p, \ell)$ be a boolean value denoting whether the horizontal segment whose left endpoint is $p$ and whose length is $\ell$ exists. Then the values of $b(p,\ell)$ for all possible $p$ and $\ell$ can be computed in $O(n^3)$ recursively using the fact that

> $b(p,\ell)$ is true iff $b(p,\ell-1)$ is true and $b(p+\ell-1,1)$ is true where $p+\ell-1$ denotes the point on the right side of $p$ and the distance between them is $\ell-1$.

Here $n$ is the length of the grid.

Similarly, you can do the same thing for vertical segments.

Now you can check each possible square by checking its four edge segments. The whole running time is $O(n^3)$.

---

As j\_random\_hacker said in the comment,

> You can drop the space usage to $O(n^2)$ by instead calculating the length $w(p)$ of the longest horizontal segment having left endpoint $p$ for all $p$. Then $b(p,\ell)=(w(p)\ge\ell)$.

# Answer
> 0 votes
A square is determined by the location of its upper-left corner and the length of its sides. You can enumerate all possibilities for that and check whether the picture does indeed contain that square or not.

---
Tags: algorithms, graphs, square-grid
---


# Question
Title: Famous hacker koan: who was it about, though?
Read this many years ago and can't remember who it was about. Nor can I remember the exact quote. The story goes:

> Famous computer scientist/professor is teaching a class. Student is having some problem w/ a machine and wants to reboot it, hoping to fix the issue. Professor chides him, saying something to the effect of "you can't expect rebooting to fix the problem unless you 'Truly Understand What Is Going On'". Professor then proceeds to reboot the computer and the issue resolves. ;)

Who was it?

# Answer
> 1 votes
Tom Knight

https://simple.m.wikipedia.org/wiki/Hacker\_koan

The item titled "Enlightenment"

Thanks to reinierpost.

---
Tags: education, history
---


# Question
Title: What the State is, and Where it comes from, when Generating Reachability Graphs
For Timed Automata, I found Figure 1 below. For Coloured Petri Nets I found Figure 2. Both are for "Reachability Graph Construction".

However, they don't describe where they got the *states* from (Figure 3), for generating the reachability graph. They assume you have "states" to generate a reachability graph, but I'm not sure what these states are. In the timed automata case, I'm not sure the automata "states" are what they are describing, it seems like by "state" they mean the *program state* after the automata runs (or on each step). Likewise for Petri nets, the state isn't the place or the transition, but the program state. At least that's what I'm getting.

Given that, my question is *how to construct the program state*, so that I can then construct the reachability graph. In addition, I'm wondering what the states actually are composed of. What the state *is* (boolean predicates, temporal logic expressions, data, etc.).

Some more detail. From here (on Petri nets):

> A marking $M'$ is reachable from a marking $M$ if $M\[s\rangle M'$ for some $s \in T^\*$... The reachability set Reach(N) of N is the set of all markings that are reachable from the initial marking. \[The markings have to do with the data associated to a place (a Petri net node)\]... A Petri net $N = (P, T, F, M\_0)$ induces several standard structures on which first-order logics may be interpreted... To specify properties of structures ... obtained from a Petri net $N$, we introduce a first-order logic FO with atomic predicates $x \to y$, $x \overset{\*}{\to} y$, $x \overset{+}{\to} y$ and $init(x)$. \[Then they go into the model checking part\].

That just demonstrates how the Reachability Graph Construction is left out. That is, what it is composed of (in some detail), and how to construct it.

---

Figure 1 $\downarrow$

Figure 2 $\downarrow$

Figure 3 $\downarrow$

# Answer
**Timed automaton case:** Here, a state is typically composed of the current *location* and the values of all *clock variables*. Thus, timed automata induce transition systems with an infinite number of states.

The usual approach in this context is thus to build a finite representation of this state set, which is a finite transition system. In the paper "An Efficient State Space Generation for Analysis of Real-time Systems" by Inhye Kang and Insup Lee that you linked to, the state set for this finite transition system is given on page 5, left column. The classical approach involves building a so-called *region graph*, which is referenced in column 2 of page 4.

Note that CTL model checking of the resulting transition system makes little sense, as the "next-time" operator of CTL does not have a usable semantic in this case. Rather, there are specialized logics (such as TCTL) to reason about properties of timed systems.

**Petri net case**: In the Petri net case, the states are the possible markings of the network. Note that the state set could be finite or infinite depending on the network. In paper that you referenced ("Petri Net Reachability Graphs: Decidability Status of First Order Properties" by Philippe Darondeau, Stéphane Demri, Roland Meyer, Christophe Morvan), the reachability graph is defined on page 4 as consisting of all markings and having a transition between a marking $M$ and $M'$ if we have $M\[t\rangle M′$ some $t$. This notation is in turn explained at the beginning of the page, in Definition 2.
> 2 votes

---
Tags: graphs, automata, model-checking, software-verification, petri-nets
---


title: Strassen's algorithm on unit vectors?

text:
# Question
Title: Strassen's algorithm on unit vectors?
I am trying to do a dot product of two vectors of each 128 dimension. I am just looping each member and calculating the sum.

```
public Double dotProduct(List<Double> v, List<Double> u) {
    Double dotProduct = 0;
    for (int i = 0; i < 128; i++) {
        dotProduct += v.get(i) * u.get(i);
    }
    return dotProduct;
}

```

Will strassen's algorithm perform better?

# Answer
> 2 votes
Strassen's algorithm is for multiplying square matrices, not vectors. Your algorithm already runs in (asymptotically) optimal time $O(n)$ (where $n$ is the dimension of the vector), and also uses the optimal number of multiplications.

---
Tags: optimization, matrices, linear-algebra
---


title: Generate all sub paths

text:
# Question
Title: Generate all sub paths
I have a path from node 1 to node n, which I can represent as a set: S = {1, 2, ..., n-1, n}. I want to efficiently generate the set of all subpaths from 1 to n. For instance, for n=5, we have S={1,2,3,4,5}.

So all the subpaths are as follows:

{{1,2},{2,3},{3,4},{4,5}, {1,2},{2,3},{3,4,5}, {1,2},{2,3,4},{4,5}, {1,2},{2,3,4,5}, {1,2,3},{3,4},{4,5}, {1,2,3},{3,4,5}, {1,2,3,4},{4,5}, {1,2,3,4,5}}

# Answer
Suppose that the path consists of edges $e\_1,\ldots,e\_\ell$. The following answer assumes that by "subpath" you mean a partition of $e\_1,\ldots,e\_\ell$ into intervals. Go over all possible values of $b\_1,\ldots,b\_{\ell-1} \in \\{T,F\\}$. If $b\_i = T$ then the edge $e\_i$ ends an interval. Otherwise it doesn't. Here is how this looks in your case, $\ell=4$: $$ \begin{array}{ccc|c} b\_1 & b\_2 & b\_3 & \text{subpath} \\\hline F & F & F & e\_1e\_2e\_3e\_4 \\ F & F & T & e\_1e\_2e\_3;e\_4 \\ F & T & F & e\_1e\_2;e\_3e\_4 \\ F & T & T & e\_1e\_2;e\_3;e\_4 \\ T & F & F & e\_1;e\_2e\_3e\_4 \\ T & F & T & e\_1;e\_2e\_3;e\_4 \\ T & T & F & e\_1;e\_2;e\_3e\_4 \\ T & T & T & e\_1;e\_2;e\_3;e\_4 \\ \end{array} $$
> 2 votes

# Answer
I am storing the nodes in an array and using recursion to generate the combinations of possible subpaths.

The method `generateSubPaths(int[] arr, int index)` takes an array and an index as input. The array `arr[]` contains the nodes and the `index` represents the current node.

We call this method recursively by updating `index` to `index - 1`. This will return us an array of strings. Each element of the returned array represents a combination of subpaths up to node `index - 1`. The number of combinations gets double if we increase the number of nodes by 1.

For n = 2 : Paths =\>

```
     (12)

```

For n = 3 : Paths =\>

```
     (12)(23)

     (123)

```

For n = 4 : Paths =\>

```
     (12)(23)(34)

     (123)(34)

     (1234)

     (12)(234)

```

For generating combinations after adding an extra node, repeat these steps for all existing combinations:

1. Create a new path between the previous node and current node.
2. Append new node to the last subpath in the combination.

Example :-

For n = 3 : One of the combinations is (12)(23).

For n = 4 :

1. Create a new path between node 3 and node 4 i.e. (34). Therefore, the new path is

(12)(23)(34).
2. Append node 4 to the last subpath in the combination. Therefore, the new path is

(12)(234).

Source Code :-

```
    import java.util.Scanner;

    public class SubPaths {

        public static void main(String[] args) {
        Scanner sc = new Scanner(System.in);

    // Input number of nodes (>1)
        System.out.println("Enter number of nodes (>1) :");
        int n = sc.nextInt();
        int[] arr = new int[n];

    // Initialize the array of nodes
        for (int i = 1; i <= n; ++i) {
            arr[i - 1] = i;
        }

        String[] result = generateSubPaths(arr, n);

    // Print each combination in a separate line
       for (String str : result) {
            System.out.println(str);
       }
       sc.close();
    }

    /*
    * This method will return an array of Strings , where each String
    represents a
    * possible combination of subpaths
    */
    private static String[] generateSubPaths(int[] arr, int index) {
    /*
     * If there are only two nodes, only 1 combination is posssible.
     */
        if (index == 2) {
            String[] result = new String[1];
       // Join node 1   and node 2
            result[0] = "(" + arr[0] + arr[1] + ") ";
        return result;
        }
    /*
     * smallResult[] stores all the combinations of subpaths where
     * maximum node is represented by 'index'
     */
       String[] smallResult = generateSubPaths(arr, index - 1);
       int x = smallResult.length;
    /*
     * If one new node is added i.e. the current node, the possible
     * combinations will be double of the previous ones.
     */
        String[] result = new String[x * 2];
        String temp;
        for (int i = 0; i < x; ++i) {
            temp = smallResult[i];
    // Create a new path between current node and previous node.
            result[i] = temp + "(" + temp.charAt(temp.length() - 2) +
                    arr[index - 1] + ")";
    // Append current node to the last subpath in the combination
            result[x + i] = temp.substring(0, temp.length() - 1) +
            arr[index - 1] + ") ";
        }
    return result;
    }
    }

```
> 0 votes

---
Tags: graphs, enumeration
---


# Question
Title: How strong "Consistent Guessing Problem" is?
I saw "Rosser’s Theorem via Turing machines" at:

https://www.scottaaronson.com/blog/?p=710

The modified halting problem (Consistent Guessing Problem) CGP is used in the proof:

```
CGP(M) - accepts if M accepts on a blank tape
CGP(M) - rejects if M rejects on a blank tape
CGP(M) - either accepting or rejecting if M runs forever on a blank tape

```

It's shown in the proof TM which solves CGP doesn't exist. Consider I have CGP as oraculum. Does it allow me to solve halting problem?

# Answer
> 2 votes
Andy Drucker, in a comment (with follow-up) to Scott Aaronson's blog post, shows that

> HALT does not reduce to Consistent Guessing (CG).

Here is his proof (copied verbatim), which uses diagonalization:

> We’ll build a language $L$ that’s a solution (i.e., refinement) of CG. On stage $i$ we’ll try to set finitely many bits of $L$ so as to ensure that the $i$th machine $M\_i$ doesn’t solve HALT when given oracle access to $L$.
>
> If this works, then we’re done! So assume for contradiction’s sake that we get stuck on some stage $i$. We’re going to use this premise to solve HALT — without an oracle. This absurdity will prove the result.
>
> So — say we’re stuck at stage $i$, and we have some finite setting $L\[i\]$ to some of the bits of $L$, consistent with CG.
>
> Let $L^\*$ be $L\[i\]$ augmented with all of the bits ‘forced’ by CG: i.e., $L^\*(M) = 0$ whenever $M$ halts with output $0$, and similarly for $1$. So, $L^\*(M)$ still is undefined for all but finitely many of the machines $M$ that run forever.
>
> Now, for each input $M$ to $M\_i$, by our assumption we have that
>
> $$ M\_i^{L’}(M) = HALT(M) $$
>
> whenever $L’$ is an extension of $L^\*$. An application of König’s lemma tells us that for each $M$ there is a number $n = n(M)$ such that any extension of $L^\*$ with arbitrary values up through input lengths $n$, causes $M\_i(M)$ to output $HALT(M)$.
>
> So, here’s how we can determine the value $HALT(M)$: we dovetail simulations of all Turing machines. On stage $j$ we simulate the first $j$ machines for $j$ steps each. Whenever a machine halts with output ($0$ or $1$), we extend our finite approximation of $L^\*$. (This approximation begins with the finitely many values of $L\[i\]$, hard-coded into the algorithm). Let $L^\*\[j\]$ be the finite approximation to $L^\*$ on the $j$th stage.
>
> On the second part of stage $j$, we simulate $M\_i(M)$ on all extensions of $L^\*\[j\]$ up to length $j$. That is, we take the values we have so far, and we try extending them in all possible ways. We then simulate $M\_i(M)$ on all of these extensions as oracle, for $j$ steps each. If on all such simulations, the machine halts with some output $b$, without ever trying to access an undefined oracle bit, then we output “$HALT(M) = b$”.
>
> The claim is, this always halts with the right answer. Using our earlier analysis with König’s lemma (and the fact that $L^\*\[j\]$ converges to $L^\*$), we find that for large enough $j$, we will output the correct bit, *if* we reach stage $j$.
>
> So we just need to argue that we never output a wrong bit earlier. But this is easy: at every stage $j$, at least one of our simulations is an initial segment of a correct simulation of $M\_i(M)$ on a valid CG oracle. Thus that simulation always either halts with the correct output, or doesn’t halt, or tries to access an undefined oracle bit. So we never get a unanimous incorrect vote.

---
Tags: halting-problem
---


title: Grammar ambiguous or not?

text:
# Question
Title: Grammar ambiguous or not?
So I've been struggling for the past hour with $G=(\\{S\\},\\{a,b\\},P,S)$ with productions $S\to aaSb | abSbS | \varepsilon$. I need to prove whether this grammar is ambiguous or not. Thus far I think it is ambiguous, possibly cuz of abSbS, but not sure (mainly since I have no idea how to prove it's not) . Can anyone help? I tried several words to no avail.

# Answer
Here is an outline of a parsing procedure. To prove that the grammar is unambiguous, you have to show that it works (parses the string), and furthermore that the parsing tree it produces is the unique one generating the string. If this question came up in the context of a course on compilers, then you should have learned the necessary tools.

The parser is a DPDA. The stack starts initialized with `S`, and then works according to the following rules, reading the input from left to right.

1. If the top-of-stack is `S`:

* If the string starts `aa`, replace `S` with `AS` (`S` on top).
    * If the string starts `ab`, replace `S` with `BS`.
    * If the string starts and ends `a`, reject.
    * If the string ends, accept.
    * If the string starts `b`, delete `S` and process `b` again.
2. If the top-of-stack is `A`:

* If the string starts `b`, delete `A`.
    * Otherwise, reject.
3. If the top-of-stack is `B`:

* If the string starts `b`, replace `B` with `S`.
    * Otherwise, reject.

(Unless explicitly stated, the automaton consumes the characters it reads from the string.) At the end of parsing, the automaton rejects unless the stack is empty.

I'll let you figure out how to construct the actual parse tree. You'll also have to figure out how to prove that this parsing tree is the unique one (if it is indeed the case).
> 2 votes

# Answer
To show that this CFG is unambiguous you can try convert it into a LL(1) (preserving ambiguity). Then, if you can do it, the original CFG will be unambiguous too (o course, if you cannot, you won't show anything about ambiguity). If you use left-factoring on S → aaSb|abSbS|ε you get: S → aT|ε, T → aSb|bSbS. Show that this CFG is LL(1) and you will get your prove (because all LL(1) grammars are unambiguous and left-factoring preserves ambiguity).
> 1 votes

---
Tags: context-free, formal-grammars, ambiguity
---


# Question
Title: computably defined function with non computable range
Are there examples of functions that can be defined computably, though the existence of their range is not computable?

# Answer
> 5 votes
Your question is a bit unclear, but you're probably looking for this example: $$ A(x,n) = \begin{cases} x & \text{ if program $x$ halts within $n$ steps}, \\ \bot & \text{ otherwise}. \end{cases} $$ This is a computable function whose image is the set of halting problems (together with $\bot$).

# Answer
> 3 votes
I believe you're asking:

> Is the range of a computable function necessarily computable?

(The phrase "the existence of" is throwing me off a bit.)

If so, the answer is **no**. The intuitive explanation of why we should expect it to be negative is that in order to tell whether $a$ is in the range of $f$, we seem to have to do an infinite search *(does $f(0)=a$? does $f(1)=a$? does $f(2)=a$? ... and this is even worse if $f$ is not total, in which case asking whether $f(0)=a$ itself requires an infinite search in case $f(0)$ doesn't hatl!)* in case $a\not\in ran(f)$. This doesn't prove that the answer is negative, but it definitely suggests it.

A set $X$ which is the range of a partial computable function is called **computably enumerable** (or c.e. - also "recursively enumerable" and "r.e."). This is equivalent to being the domain of a partial computable function, and - as long as $X$ is nonempty - to being the range of a total computable function. *(These are good exercises. Incidentally, the analogues of these facts can fail in generalized computability theory.)* It turns out that there are **lots** of different kinds of c.e. sets.

* The Halting Problem $K$ - the set of all pairs $(e, n)$ such that the $e$th Turing machine halts on input $n$ *(this is slightly wrong - usually $K$ is defined as the set of $e$ such that $\Phi\_e$ halts on input $e$ - this doesn't change anything, and the definition I've given is slightly easier to work with)* \- is the most famous example of a c.e. set. It is *maximally complicated* amongst the c.e. sets: if $X$ is c.e., then $X$ is Turing reducible (even $1$-reducible - that is, injectively many-one reducible) to $K$.

The proof that $K$ is not computable is a nice diagonal argument: if $\Phi\_e$ were to compute $K$, consider the machine $\Phi\_c$ which, on input $(d, n)$, runs $\Phi\_e(d,n)$ and $(i)$ halts if the output is "No" and $(ii)$ loops endlessly if the output is "Yes" *(the existence of such a machine follows from the existence of a universal Turing machine)*. Now can $\Phi\_c(c, c)$ halt?

* Following this, Post asked whether there were any c.e. sets of "intermediate" complexity. This was answered by Friedberg and Muchnik, who showed in fact that there are c.e. sets of *incomparable* Turing degree. This was the invention of the **priority argument**, which would over time be developed to increasingly extreme levels of complexity (Friedberg-Muchnik is an instance of the *finite injury* type of priority argument; Sacks developed the basic *infinite injury* priority method, and after extensive development Lachlan went one step further with a technique so complicated that it was known for a while as the *monster theorem*).
* Primarily - but not exclusively - via priority arguments, a detailed picture of the c.e. sets has emerged. There are far too many fundamental facts about them to mention here; I'll just point the interested reader to Soare's text on the subject, which also functions as a good introduction to computability theory in general. (This paper of Soare, with the same title, may also be of interest - and is definitely shorter! Note that both book and paper are rather old, and no longer represent the state of the art in the field.)
* Interestingly, although c.e. sets of Turing degree strictly between the computable and that of $K$ are known to exist, no *natural* examples are known (those constructed by priority arguments are quite artificial). There is a general body of heuristic evidence that in fact no natural examples exist at all, but this gets technical very quickly.

---
Tags: computability
---


title: Two dimensional 3 bit parity check

text:
# Question
Title: Two dimensional 3 bit parity check
Can someone explain how do we find these parity bit errors?

# Answer
> 1 votes
I'm assuming that your code works in the following way:

* The input is an $n \times m$ bit matrix.
* You add a parity bit to each row, chosen so that the parity of the new row is even.
* You add a parity bit to each column, chosen so that the parity of the new column is even.
* You end up with an $(n+1) \times (m+1)$ bit matrix in which the parity of each row and column is even.

Suppose now that between 1 and 3 errors occurred. There must be either a row or a column in which *exactly* 1 error occurred (I'll let you figure out why). This row or column will have odd parity, and so you will be able to detect that an error occurred.

---
Tags: computer-networks, digital-circuits
---


# Question
Title: Prove that the TM which would go over the leftmost position is not decidable
Let $M$ be a one-band TM and $w$ a word. We say that *M tries to move the head over the left margin of the band* if, while the head is in the leftmost position of $w$, the TM $M$ tries to move to the left.

Show that the language

$ LEFT\_{TM} = \\{\<M,w\> | $ M is a TM of the type above $\\}$

is not decidable.

How can I show that such a language is not decidable?

I was thinking about using the TM $A$ which accepts any input and reduce it to $LEFT\_{TM}$, but I'm not sure how. I would appreciate a nudge in the right direction.

# Answer
> 2 votes
You can reduce the halting problem to your problem. Roughly speaking, the reduction goes along the following lines:

> Given a Turing machine $T$, construct a Turing machine $T'$ which simulates $T$ but never ventures to the left of the starting symbol. If $T$ halts, it then proceeds to go all the way to the left, until it goes beyond the starting symbol.

If you can do this, then you will have shown that LEFT is undecidable.

So how do you construct the machine $T'$? The difficult part is to somehow arrange that it never goes to the left of the starting symbol. Fortunately, this is essentially equivalent to showing that Turing machines with a one-sided infinite tape are equivalent to Turing machines with a two-sided infinite tape. You can look this up in many sources, or come up with a simulation of your own. There are many different ways to do it. Be creative!

---

One thing which might be unclear is what it means to simulate $T$ without going to the left of the starting symbol. What if $T$ wants to go to the left of the starting symbol? We are not looking for a *literal* simulation. Rather, we want to simulate each step of $T$ using a series of steps in $T'$, in such a way that the state of $T$ can be read from the state of $T'$. As a simple example, you can think of a Turing machine over the tape alphabet $\\{0,1\\}$ which simulates a Turing machine with tape alphabet $\\{00,01,10,11\\}$ by using two cells to store each symbol. We are looking for something similar: simulating a two-sided infinite tape using a one-sided infinite tape.

---
Tags: turing-machines, reductions
---


title: What is a not-well-founded cotree?

text:
# Question
Title: What is a not-well-founded cotree?
I'm reading the paper "Dual of substitution is Redecoration". And I'm struggling with understanding the usage of the word "not-well-founded cotrees".

1. what is a cotree compared to a tree ? I suspect it is a tree for which all relations are inverted, but it is just my assumption.
2. what it is to be "well-founded" for a tree, for a cotree.

Probably, to have an insight, it would be helpful to give me examples of a well-founded and of a not-well-founded tree/cotree.

# Answer
I'm not sure what you mean by "all relations are inverted" (what's the relation of a tree?), but perhaps I can provide some insight.

In Haskell, one might write the type of binary trees as such:

```
data Tree = Leaf | Node Tree Tree

```

in the terminology of the paper, the type of "incomplete trees" would then be

```
data ITree a = Leaf | Node ITree ITree | Var a

```

allowing for an "incomplete" tree with holes marked by an instance of `Var a`. The paper observes that the type `ITree a` forms a monad, where a `Var a` can be "substituted" with `f a` given a suitable function `f :: a -> ITree b`.

Now our intuition is that the type `Tree` is the type of finite, or **well-founded** binary trees, of which an example is

```
 myTree :: Tree
 myTree = Node (Node Leaf Leaf) (Node Leaf Leaf)

```

However, it is untrue in a language like Haskell that *all* trees are of this form. Indeed, following definition is perfectly acceptable:

```
infTree :: Tree
infTree = Node infTree infTree

```

intuitively, this tree represents the infinite "full" binary tree. So really the type `Tree` may contain either finite binary trees, or trees which may contain infinite paths. **Such trees are called non-well founded trees**.

So, in Haskell, the type `Tree` is *in reality* the type of co-trees, which allows such elements as `infTree`. This may be a bit confusing, since we rarely think about such elements when considering that type.

Hopefully this provides useful intuition.

The main observation of the paper, is that the type of co-trees has a construction dual to that if `ITree`, which one might call `DTree`, defined as

```
 DTree a = DLeaf a | DNode a (DTree a) (DTree a)

```

such that we can define a *comonad structure*:

```
extract :: DTree a -> a
extract (DLeaf a) = a
extract (DNode a _ _) = a

duplicate :: DTree a -> DTree (DTree a)
duplicate (DLeaf a) = DLeaf (DLeaf a)
duplicate (DNode a l r) = DNode (DNode a l r) (duplicate l) (duplicate r)

```

The paper goes on to explain some intuition about this structure and why it should be considered as interesting.

---

Oh by the way, the paper you are reading seems pretty heavy in abstract nonsense, and if you're coming from the CS side of things, you might want to take a look at these blog posts first:

https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/

http://5outh.blogspot.com/2013/01/comonads.html
> 4 votes

---
Tags: trees, category-theory, duality
---


# Question
Title: Impossibility of Distributed Consensus with One Faulty Process
I'm reading Fischer et al.'s *Impossibility of Distributed Consensus with One Faulty Process*, and I don't quite follow 2 points:

The first is in the proof of Lemma 3, pg. 378:

> Otherwise, $e$ was applied in reaching $E\_i$, and so there exists $F\_i ∈ \mathscr{D}$ from which $E\_i$ is reachable.

Why does there exist $F\_i ∈ \mathscr{D}$ from which $E\_i$ is reachable?

The second is more general: what does having at most one faulty process have to do with the theorem that "no consensus protocol is totally correct in spite of one fault"? In the part where

> We now show that it is always possible to run the system in a way that avoids such steps, leading to an admissible nondeciding run.

I don't see anything depending on having at most one faulty process. In fact, what would change if *no* process was faulty?

# Answer
Adding context:

> If $E\_i\in\mathscr C$, let $F\_i = e(E\_i)\in\mathscr D$. Otherwise, $e$ was applied in reaching $E\_i$, and so there exists $F\_i \in \mathscr D$ from which $E\_i$ is reachable.

Of course, without the definitions of $E\_i$, $e$, $\mathscr C$, and $\mathscr D$, this isn't much use either. We're given a configuration $C$. $e$ is by assumption an event applicable to $C$. $\mathscr C$ is the set of all configurations reachable from a given configuration $C$ where event $e$ has *not* been applied. $\mathscr D$ is all the configurations you get when you apply $e$ to the configurations in $\mathscr C$. $E\_i$ is a(n $i$-valent) configuration reachable from $C$.

The first paragraph of the lemma shows that $e$ is applicable to all configurations in $\mathscr C$. Given this, if $E\_i\notin \mathscr C$, then, by definition of $\mathscr C$ and the fact that $E\_i$ is reachable from $C$, $E\_i$ must be reachable via some configuration that applies $e$. Any run from $C$ to $E\_i$ must have a first time where $e$ is applied. Any configuration before that is in $\mathscr C$ by definition. The configuration at the point $e$ is applied is in $\mathscr D$ by definition and the fact that $e$ is applicable to all configurations in $\mathscr C$. That configuration is $F\_i$.

Again, your second quote lacks context. The "such steps" mentioned in it are the steps from a bivalent configuration to a univalent configuration. Avoiding "such steps" is only relevant if we must start from a bivalent initial configuration, which is what Lemma 2 establishes. Lemma 2 critically depends on allowing up to one faulty process. If the protocol did not have to work correctly in the face of up to one faulty process, then Lemma 2 would not apply.

The idea of Lemma 2 is that if we have two configurations that differ only in how the input register is set for a single process, then if they can both reach a decision without ever executing that process (i.e. that process is faulty), then they must reach the same decision, since, once we remove that process, they have the same set of processes with the same initial state receiving the same messages. If we assume there are no bivalent initial configurations (for contradiction), then by partial correctness it is necessarily the case that there are two configurations that would make different decisions, but differ from each other only by a single process' input. Thus a contradiction.

It's trivial to make a consensus protocol when no processes are faulty. Simply pick one process (via setting its initial state appropriately) to be the Decider. It copies its input to its output. All other processes do nothing. Clearly this scheme won't work if the Decider is faulty.
> 1 votes

---
Tags: distributed-systems, consensus
---


# Question
Title: Is there an efficient algorithm for WEAK-PARTITION?
Suppose that we are given a list of non-zero integers $(a\_1,...,a\_n)$ and we want to decide whether there exist $(x\_1,...,x\_n)$ such that

$x\_1a\_1 + x\_2a\_2 + ... + x\_na\_n = 0$,

$x\_i$ $\in$ $\\{-1,0,1\\}$, with at least one $x\_i \neq$ 0.

Note that this is not the same as PARTITION, where the restriction $x\_i \in \\{-1,1\\}$ would give a solution. Of course we should also be aware that with $x\_i \in \\{0,1\\}$ is the NP complete problem SUBSET-SUM. I don't see any obvious way of reducing SUBSET-SUM or PARTITION to this problem. For example, attempting to reduce a 0-1 problem to $\\{-1,0,1\\}$ problem by appending the list with negative elements appears to accomplish nothing.

The closest problem that I found was described this post, calling the problem WEAK-PARTITION. However, the link that the original poster provided is currently broken.

I would like to know whether there is an efficient (i.e. polynomial time) algorithm known for this problem and whether anyone knows of further references to this problem.

# Answer
> 3 votes
Your problem is NP-complete, as proved by Adi Shamir in his paper On the cryptocomplexity of knapsack systems.

---
Tags: partitions
---


# Question
Title: Does selecting the same arm has the same reward?
In multi-armed bandit problem, we have a set of $K$ arms. In each round $t$, a bandit selects an arm $k$ and receives a reward $r\_{kt}$. The objective is to maximize the rewards after $T$ rounds.

My question: Does selecting the same arm in two different rounds leads to the same reward? Or the rewards are completely different?

It is surprising to me if one could select the same arm but receives a different reward and still has a sublinear regret.

# Answer
> 4 votes
In the version of the Multi-Armed Bandit problem I'm familiar with, there is a fixed list of distributions $B = R\_1, R\_2 \cdots R\_n$, and the reward for pulling lever $k$ is chosen from the distribution $R\_k$.

So pulling the same lever twice might lead to different rewards, but the rewards are connected through the distribution $R\_k$.

---
Tags: machine-learning, learning-theory
---


# Question
Title: Finding independent set of size n in an undirected graph
Is there an algorithm that, given an undirected graph, finds an independent set of size n (where n is less than or equal to the total number of vertices)?

# Answer
> 2 votes
(Note: for the sake of standardization, I'm using $n$ for the number of vertices in the graph, and $k$ for the number you want in your independent set.)

The problem of whether such a set even exists is actually NP-complete, by reduction from the clique problem (since an independent set is a clique in the complement of the graph). So unless P=NP, you're not going to get any better than exponential time. This limits you to rather small graphs in practice.

The easiest algorithm for this is simple brute force: run through all sets of $k$ distinct vertices, and check whether each one is independent. If it is, return it. As expected for brute force, this runs in $O(n^2 2^n)$. An improvement was found by Xiao and Nagamochi in 2017, which brings this down to about $O(1.2^n)$. (Unfortunately, I don't have access to their paper, so I can't summarize their algorithm here.)

---
Tags: graphs
---