# Question
Title: Recurrent relation for algorithms with two stages
I am trying to do the recurrence relation for my algorithm, but it has two variables $T(n,m)$. For sufficiently small $n$, $m$ is practically the same as $n$, but $m$ cannot grow beyond some constant $k$. So once $n$ grows beyond $k$, $m$ turns to constant $k$. So it has two different stages.

I have done the relation in both cases: when $m$ is another variable, and when $m$ is a constant, but how do I put them together?

Using $a=2, b=2$ as an example: this recurrence relation with $m$ as a variable like $n$: $$T(1)=1$$ $$\begin{equation\*} \begin{split} T(n) & = 2T(\frac{n}{2})+m \\ & = 2T(\frac{n}{2})+n\\ & = n+nlog\_2n \end{split} \end{equation\*}$$

Treating $m$ as a constant: $$\begin{equation\*} \begin{split} T(n) &= 2T(\frac{n}{2})+m \\ &= n+mn-m \end{split}\end{equation\*}$$

Please feel free to check my math. Now how do I represent this as one recurrence relation? $m$ cannot grow beyond constant $k$.

# Answer
Just solve both cases separately. I.e., consider cases for $m \< k$ and $m = k$ separately. The solution for the first one (i.e., $T(n, k - 1)$) gives the starting point for the second recurrence (i.e., $T'(n) = T(n, k)$, presumably for $n \ge k$).
> 1 votes

---
Tags: algorithm-analysis, recurrence-relation
---


# Question
Title: What is the Purpose of Augmented Grammar in LR parsers?
I was reading the LR() parsers from the Dragon Book where I came across these lines:

> To construct canonical LR(0) collection for a grammar, we define an **augmented grammar** and 2 functions, CLOSURE and GOTO.

for example say if we have a grammar like--\>

S → BB
B → cB/d

Then in augmented grammar we define it as

S' → S

S → BB

B → cB/d

In the dragon book the reason for this is mentioned as,

> The purpose of this new starting state production is to indicate the parser when it should stop parsing and announce the acceptance of the input. That is acceptance occurs when only when the parser is about to reduce S' → S

I am unable to understand what this even means and how this augmented grammar is useful for parsing. Any help will be highly appreciated.

# Answer
The augmented grammar adds a new starting non-terminal $S'$ with the sole production $S' \to S$. This helps in detecting acceptance: If you reduce by this particular production (to the non-terminal $S'$), you are accepting. To reduce to the start non-terminal of the original grammar tells you nothing, it might appear on some right hand side.
> 3 votes

---
Tags: compilers, parsers
---


# Question
Title: Why is a subset of a undecidable language decidable?
I have problems with the understanding why a subset of a undecidable language is decidable. We've proved in the lecture that $HALT$$\_T$$\_M$$=${$\<M,w\>$|M is a TM and M halts on input w} is undecidable. Can someone give an example of a subset from $HALT$$\_T$$\_M$ and explain why it is decidable? Is $\Sigma^\*$ a valid subset of $HALT$$\_T$$\_M$?

# Answer
An undecidable language is necessarily infinite. A finite subset of it is always trivially decidable.
> 1 votes

---
Tags: turing-machines, undecidability, semi-decidability
---


# Question
Title: Number of logic gates for "reasonable" Turing completeness
Somewhere on stackexchage, I, or someone else asked what was the proper term for Turing completeness minus the infinite memory (e.g. a Turing machine that one can actually build, no bigger than your typical data center). Answer was inconclusive.

Also, someone else asked somewhere else on stackexchange about the number of gates for a Turing machine, but that got sidetracked into the useless infinite definition (that many quanta do not exist in the known universe).

So using the non-infinite Turing machine definition (\*), whatever that is, is there a known lower bound on the number of 2-input binary gates needed to produce a Turing complete computer? Or a reasonable guess or a minimum among known current published existing example implementations?

(\* If necessary assume the "tape" is external to the logic gate count, the gates just drive the tape read/write/move mechanism).

# Answer
As soon as you limit "memory" you are talking about machine models that are equivalent to finite automata. If you limit "memory" to input size, you are at linear bounded automata, which are easily seen to be limited to recognizing (some) recursive sets.
> 1 votes

---
Tags: turing-completeness
---


# Question
Title: What is the relation between the formal definition of strictness and its intuitive notion
I am currently reading *Functional Programming in Scala* and have encountered a statement in the book I cannot quite make sense of.

On page 67, we are told the formal definition of strictness:

"If the evaluation of an expression runs forever or throws an error instead of returning a definite value, we say that the expression doesn't *terminate*, or that it evaluates to *bottom*. A function f is *strict* if the expression f(x) evaluates to bottom for all x that evaluate to bottom."

This definition is somewhat puzzling because the discussion of strictness that comes before this definition has discussed strictness in relation to lazy evaluation. To say that an expression is strict is to say that it is completely evaluated, and not lazy. What is not clear is how this notion of strictness and laziness is at all related to the formal definition given.

# Answer
> 0 votes
The intuition: if executing `f(x)` causes `x` to be evaluated, and evaluating `x` doesn't terminate, then this will cause `f(x)` to fail to terminate (because evaluating `x` doesn't terminate, so the execution of `f(x)` never completes).

So, if executing `f(x)` always causes `x` to be executed, then `f` will be strict by the formal definition above. That's why "`f(x)` completely evaluates `x`" implies "`f(x)` evaluates to bottom for all `x` that evaluate to bottom".

In contrast, with a lazy function, evaluating `f(x)` doesn't necessarily trigger evaluation of `x`, so it doesn't necessarily terminate (even if evaluating `x` wouldn't terminate). Thus, for a function that is intuitively lazy, it won't meet the formal definition of strict.

---
Tags: functional-programming
---


# Question
Title: Is it possible to have high compression but low predictability?
Can you have a process that generates a binary sequence with high compression rate (low entropy) but impossible to predict next symbol?

'impossible to predict' - sequence cannot be predicted theoretically. But I was also asking about the real life example (no polynomial algorithm).

# Answer
> 2 votes
No. Let $x\_1,x\_2,\dots,x\_n$ be the bits of the binary sequence.

Suppose $\Pr\[x\_{i+1} | x\_1,\dots,x\_i\] = 1/2$ for all $i$. Then it is impossible to predict the next bit; however, it is also easy to see that $x\_1,\dots,x\_n$ is uniformly distributed on $\\{0,1\\}^n$, so has entropy $n$ (high entropy; no compression possible).

Alternatively, suppose $\Pr\[x\_{i+1} | x\_1,\dots,x\_i\] \ne 1/2$ for some $i$. Then it is possible to predict the next bit better than chance.

Those are the only two possible cases. In every case, either the next bit is predictable, or you can't compress.

This assumes you are talking about what is possible with infinite computing power (which isn't realistic, but is what is typically assumed in information theory).

# Answer
> 3 votes
Yes. A cryptographic stream cipher can generate an incredibly long string (e.g. ChaCha20 can generate $256 \times 2^{128}$ bits) from a single small key (e.g. 256 bits).

If you do not know the key that was used this stream is impossible to predict.

# Answer
> 1 votes
The accepted answer is plainly wrong.

It's not really low predictability. After the first 256 bits, the rest is perfectly predictable, it is just very hard. It's not *impossible* to predict. So the answer is wrong.

And the argument doesn't make sense. It's very hard to predict (but not impossible) without knowing the key. But it is equally very hard (but not impossible) to compress without knowing the key.

---
Tags: complexity-theory, information-theory, data-compression
---


# Question
Title: Smallest integer i stored as a float such that i+1=i
So I had an assignment which asked me to find the smallest integer $i$ which when represented as a float is such that $i+1=i$

My approach- By making a simple C++ program , we get $i=16777216$ or $i=2^{24}$ But if we want to do that theoretically, I am unable to arrive at this number.

So a float is 32 bit variable and the first bit represents sign of mantissa and the next 23 bits represent the number in Mantissa. The next bit represents sign of the exponent and the following 7 bits represent the value of exponent.

Now consider $2^{23}$. In Binary, it is represented as $1000,0000,0000,0000,0000,0000$ (the comma's are just to make things readable). Now if we add $1$ to it, it becomes $1000,0000,0000,0000,0000,0001$

Now we store these numbers as float in C++. Both the numbers $2^{23}$ and $2^{23}+1$ are stored as $0100,0000,0000,0000,0000,0000,00010111$ (the 1 in the end has to be scrapped in order to fit the number in 24 bits). So both of them are essentially the same for the computer.

But why does the computer give me answer as $2^{24}$?

The code that I used

```
#include<iostream>

using namespace std;

int main(){

    float i=1;
    while(1<2)
    {
        if(i+1==i)
            {cout << fixed << i << endl;
                break;}
        i=i+1;
    }

}

```

# Answer
Standard “float” has a 24 bit mantissa (the highest bit doesn’t get stored because it is always 1). Therefore all integers that fit into 24 bits - all integers less than $2^{24}$ \- can be represented exactly.

From $2^{24}$ onward only even numbers can be stored. So you take N = $2^{24}$, and carefully check what n+1 is according to the rounding rules.

BTW. It makes life a lot easier if you don't look at the exact bit representation of float, but just take it as "1 bit sign, 8 bit exponent, 23 bit mantissa + 1 implicit leading mantissa bit".
> 1 votes

---
Tags: floating-point
---


# Question
Title: Computer Vision Techniques to find Slope of beach in the 2D Images?
What I am planning to do is to calculate the height and estimate the slope of the segmented Object. The camera will be static and the Object of Interest is the slope of the beach. I am finding harder to use depth camera, as the minimum distance between slope and camera is 150 meters.

I have tried Unet Semantic Segmentation with two classes i.e. background and sand surface. After semantic segmentation what i left with is the sand surface, but i am struggling to find slope height; as one out of many options that i have tried is to run canny filter on 2D image and convert the segmented sand surface into 3D, but the distance between camera and sand surface is around 200 meters, therefore i am reluctant to use any of the 3D reconstruction approach.

And also i am not sure of any depth cameras which can cover up to 200 meters of range. Please see the attached Picture for more information. If you require more information please let me know, :) Thanks for your help !!!.

# Answer
As far as I understand you are trying to infer 3D position of the various points (i.e. height) on the beach using *single monocular RGB camera*.

I will try to give the best answer that with the CV knowledge that I have.

This is a difficult problem because you do not have the depth (distance from the camera) information, so you cannot infer full 3D structure from 2D image, i.e. the problem is ill-posed. Usually there are several other approaches that people do in order to extract 3D information:
1) having several cameras (e.g. stereo camera), then knowing the geometry of rig (its baseline), camera matrix one and doing disparity calculation one can find depth.
2) lidar, radar or other sensors that give depth directly. This information can either be fused to RGB camera or projected onto image space.
3) single monocular *moving camera* (can infer depth from structure-from-motion methods).

Additionally, one can perform monocular depth estimation but one would need:
1) to know camera matrix. In specific cases one can infer camera matrix (or some camera parameters) from parallel lines, circles or even from variability in focus, however in your case I don't see such artifacts.
2) depth map prediction algorithm (usually neural networks these days). There is lots of work on this, here's a sample paper one could start with. However, these methods do not understand the full 3d structure, they implicitly learn the relative size of objects and geometry of the scene, and of course you would need to devise a dataset for you task and train a neural net for that. And of course its depth accuracy will be much lower than the methods that I have described above.
> 1 votes

---
Tags: machine-learning, computer-vision, mathematical-programming, mathematical-analysis
---


# Question
Title: Algorithm to find a simple path with maximum weight less than a constant in DAG
Given a weighted directed acyclic graph $G=(V,E,W)$, where the weights are non-negative and are on the vertices. I am searching for a simple path of maximum total weight, but this total weight should not exceed a given constant $K$.

Perhaps my question is elementary but I cannot find any solution. Indeed, it is well known that finding a simple path with maximum weight in $G$ is polynomial, but by adding the fact that this total weight should not exceed a given constant $K$, will the problem remain polynomial? because we need to keep at each node the set of path lengths that can be reached by the next vertices.

# Answer
> 2 votes
Since there is no negative weight, you only need to keep at each node the set of path lengths no more than $K$. Because $K$ is a constant, you only keep a constant number of path lengths at each node. Hence, the algorithm remains polynomial-time.

---
Tags: algorithms, complexity-theory, graphs, np-hard
---


# Question
Title: Why does Bellman-Ford algorithm use < rather than ≤?
The Bellman-Ford Algorithm uses a less-than symbol rather than a less-than-or-equal-to symbol. How does this identify that there is a negative cycle?

For instance, say I have the below example going from initialization state through the first iteration and on to the second.

Initial state

```
    (0)S----(1)----B(inf)
        \         /
        (1)    (-1)
          \     /
           \   /
             C(inf)

```

First phase

```
...Check edges...
S->B
D[S] + 1 < D[B] = 0 + 1 < inf => True => Update D[B]

B->C
D[B] + (-1) < D[C] = 1 + (-1) < inf => True => Update D[C]

    (0)S----(1)----B(1)
        \         /
        (1)    (-1)
          \     /
           \   /
             C(0)

```

Second phase when checking for negative cycles

```
...Check edges...
...Skipping to check B->C...
B->C
D[B] + (-1) < D[C] = 1 + (-1) < 0 => False

    (0)S----(1)----B(1)
        \         /
        (1)    (-1)
          \     /
           \   /
             C(0)

```

Shouldn't the last check between `B->C` be true to detect the negative cycle? i.e. Shouldn't we use less-than-or-equal-to (≤) rather than (\<)?

# Answer
First of all, let me clarify a few points about your example:

* Bellman-Ford-Moore consists of two *phases*, *stages* or *steps*, each one consisting of a number of iterations as they are implemented with loops. The first *phase* computes the cost of the shortest-path to reach each vertex from the start vertex and it consists of two nested loops; the second one consists of a single loop which checks whether there are negative cycles or not. I mention this because it seems to me that you refer to the *phases* as *iterations*.
* Let me also note that in the first *phase* you skip the evaluation of reaching $S$ from $C$. I assume you just simply avoid making the computation because it is pointless for exemplifying your case, but let me just highlight that Bellman-Ford-Moore would also perform that evaluation. By the way, it is unclear whether you are considering a directed or undirected graph. I just assumed it is directed: $S\rightarrow B\rightarrow C\rightarrow S$.
* As noted in the comments by xskxzr, there is no negative cycle in your exmaple. A *negative cycle* is defined as a path which starts and ends in the same vertex whose overall cost (defined as the sum of all edge costs) is strictly negative. In your case, there is only one cycle from $S$ to it, but it has a cost which is is strictly positive: $c(S, B) + c(B, C) + c(C,S)=1-1+1=1\>0$.

I mention these points only to make the answer clearer (if possible) and more useful to other readers.

I will try now to address your question. Once the first *phase* is over, the distance of the shortest-path from the start vertex $S$ to all other vertices in your graph has been already computed. Let $d\_i$ denote the cost of the shortest path from $S$ to the $i$-th vertex.

Consider now any vertex of your graph, $v\_i$, and all incident edges to it. Clearly, at least one should be in the shortest-path from $S$, whereas all the others should not. Take any vertex $u$ which has an edge from it to $v\_i$:

* If the edge $\langle u, v\_i\rangle$ is part of the optimal path from $S$ to $v\_i$ then clearly $d\_u + c(u, v\_i)=d\_{v\_i}$
* Otherwise, $d\_u + c(u, v\_i)\>d\_{v\_i}$ as this is not part of the optimal path.

Thus, when starting the second *phase* (for detecting negative cycles), there is at least one edge for each vertex for which equality holds without the presence of negative cycles! This is just a consequence of the definition of shortest-path as shown above. This observation precludes the usage of $\leq$ for detecting cycles, as equality holds without negative cycles.

Let us now consider the case of negative cycles. Their essential property is that they decrease the value of reaching its final vertex indefinitely (as crossing it again would reduce the cost to reach its end vertex), i.e., negative cycles strictly *decrease* the cost of reaching its end vertex and hence, the only way $d\_u + c(u, v\_i) \< d\_{v\_i}$ is because there is at least one negative cycle.

In your specific example, make $c(C,S)=-1$. Now you have a negative cycle from $S$ to itself. Clearly, once the first *phase* is over, the cost of the shortest distances computed by Bellman-Ford-Moore would be: $d\_S = -2, d\_B = 0, d\_C = -1$. I assume the following order of edges: $\langle S, B\rangle$, $\langle B, C\rangle$ and $\langle C, S\rangle$ and recall that the first *phase* is ran as many times as edges minus 1, i.e., twice in your example. So far, after the first iteration (which considers updating the target vertex of all edges in the order given above) of the first *phase* $d\_S = -1, d\_B = 1, d\_C = 0$. Because Bellman-Ford-Moore dictates to run the first phase as many times as vertices minus one (the reason beig that the costs computed in the previous iteration should be propagated to the longest path whose number of edges is upper bounded by the number of vertices minus 1), a second iteration of the first *phase* is conducted and the cost of the shortest-path to all vertices gets decremented again, $d\_S = -2, d\_B = 0, d\_C = -1$.

Next, when running the second *phase* it turns out that $d\_S + c(S,B) = -2 + 1 = -1 \< d\_B = 0$ which reveals the presence of the negative cycle using $\<$.

Hope this helps,
> 1 votes

---
Tags: algorithms, graphs, algorithm-analysis
---


# Question
Title: Show that $L:=\{(a^{k}b)^{i}|i,k \epsilon \mathbb{N}_{+} \}$ is context-sensitve. (With context-sensitive/noncontracting grammar)
I am studying for an upcoming exam and this is an old exam question from two years ago (all exams were made available through our lecturer):

Show that $L:=\\{(a^{k}b)^{i}|i,k \epsilon \mathbb{N}\_{+} \\}$ is context-sensitve.

I could easily construct a LBA for this language. But since the notation/construction of LBAs weren't really explained, I would have to define it in the exam.

So I assume this task was expected to be done by constructing a context-sensitive grammar.

**NOTE:** In our lecture the definition of a context-sensitive grammar was in fact the definition of a noncontracting grammar. So any rule like this **x -\> y** is allowed if **|x| \<= |y|**

So this is allowed:

```
aAb -> bXaa

```

My best idea goes like this:

```
S  -> AB
B  -> bB | b
A  -> CA | C
Cb -> abC
Ca -> aC

```

so to generate `aaabaaabaaab` I do this:

```
S
AB
AbB
AbbB
Abbb
CAbbb
CCAbbb
CCCbbb
(let all C-Variables run through the word and leave an 'a' before every 'b')
CCabCbb
CCababCb
CCabababC
...
aaabaaabaaabCCC

```

But I can't make all the 'C'-Variables disappear.

# Answer
> 2 votes
Sems to be a decent approach.

The trick you need is to leave the last `B` marked, say you generate `bbX` rather than `bbb`. Now the final `X` can absorb the `C`'s using the production `CX -> aX`.

In the end you are left with the final `X` which can change into `b` again.

Of course the final production `X -> b` might be applied too soon, when there are still `C`'s around. This is harmless. Now the `C`'s cannot disappear and the derivation will not succesfully end.

In ordinary context-sensitive grammars one is usually not very interested in unsuccesful derivations, but it might be hard to consider all cases when writing formal proofs. It is some times possible to write more deterministic grammars by simulating linear bounded automata. In state `p` read `a` then write `b` move left to state `q` one would have the rewrite rule `xpa -> qxb` (for every letter `x`). Then the only problem is to make the final state disappear.

---
Tags: formal-languages, formal-grammars, context-sensitive
---


# Question
Title: Verifying connectivity of a graph in O(n^2)
I trying to solve the following problem in $O(n^2)$:

> We have vertices which represents cities and a textfile containing an edge on each line. How many roads do we need to build to make the graph connected - you can travel by road to each city?

Basically, at the start, we have just the vertices. As we read the textfile, we add a new edge each time we read a new line and we should decide after how many edges added is our graph now connected.

An example: An example: we have 5 vertices, A, B, C, D, E. In the textfile, we have defined these edges: A-B, B-C, A-C, B-D, C-D, A-D, B-E, C-E. The graph have been made connected after building 7 edges, while we have only 5 vertices when we start (5 components).

I solved it the following way: I'm calling the BFS algorithm after adding each edge to the graph until the graph is connected and counting the number of BFS calls. However, since the BFS itself has a time complexity of $O(n^2)$ and I'm calling it n-times, I have a worstcase time complexity near $O(n^3)$.

How would I solve this issue in $O(n^2)$?

# Answer
You can do one graph traversal to find all the connected components of your graph.

Then add an edge from each connected component to the next : the graph is fully connected and you did only one traversal, that's $O(n^2)$
> 2 votes

# Answer
I'm assuming that the problem is as follows. You're given the (ordered) list of edges in the input file and you read them one at a time and add them to the graph. You must stop as soon as the graph you've built is connected.

In that case, a simple $O(n^2)$ solution is to label each vertex with an integer that indicates what component it's in. Initially, the vertices are labelled $1, \dots, n$, since there are no edges so each vertex is its own component. Then, each time you add an edge, say between vertices $i$ and $j$ with labels $\ell\_i$ and $\ell\_j$, update every vertex with label $\ell\_i$ to have label $\ell\_j$. While you're doing that, check to see if there's some vertex that has a label different from $\ell\_i$ and $\ell\_j$. When every vertex has the same label, the graph is connected.
> 0 votes

---
Tags: algorithms, graphs, graph-traversal
---


# Question
Title: Finding partition with maximum number of edges between sets
Given a graph (say in adjacency list form), is there an algorithm to find a partition of vertices such that the number of edges between the two sets of the partition is the maximum possible?

For example, for the following set of edges of a graph with vertex set $\\{1, 2, 3, 4, 5, 6\\}$: $\\{(1, 2), (2, 3), (3, 1), (4, 5) , (5, 6), (6, 4)\\}$, one possible "maximum" partition is $\\{\\{1, 3, 4, 6\\}, \\{2, 5\\}\\}$ with $4$ edges between the sets $\\{1, 3, 4, 6\\}$ and $\\{2, 5\\}$.

# Answer
If your question really is "is there an algorithm", the answer is obviously yes: just try every possible partition and choose the one maximizing the number of edges with endpoints in different parts.

Otherwise, it's unlikely that there is a *polynomial-time algorithm*. Indeed, this problem is known as maximum cut and it is well-known to be NP-hard.
> 4 votes

---
Tags: graphs, partitions
---


# Question
Title: Floating point precision from rearranging equation
When I run $x^2 - y^2$ with x=8.8888888888 and y=9.9999999999 in python, I get the following result:

```
>>> 8.8888888888**2 - 9.9999999999**2
-20.9876543205679

```

However, if I rearrange it to $(x-y)(x+y)$ with the same x and y values, I get:

```
>>> (8.8888888888 - 9.9999999999) * (8.8888888888 + 9.9999999999)
-20.987654320567895

```

It seems that the two equations, though logically equivalent, give varying amounts of floating point precision by a difference of 2 digits. What could be causing this?

# Answer
> 4 votes
First of all, the different numbers of digits are misleading. The two numbers store the same amount of precision; Python is just leaving off final zeroes.

However, there *is* a loss of precision here, and it comes down to the intermediate results.

Floating-point values aren't infinitely precise, and the larger their absolute value, the fewer places they can store after the decimal point. (Hence the name "floating point": one way to think of floating point numbers is that they're a fixed number of digits long, but you can move the decimal point back and forth to represent both really big and really small values.)

When you compute `8.8888888888**2`, you're effectively using more of the available bits to store things before the decimal point. So there are fewer left over to store things after the decimal point. It gets less precise.

When you instead compute `8.8888888888 - 9.9999999999`, you're not using those extra bits before the decimal point, so they can all be devoted to the part after the decimal point.

*(Note: this is an intuitive explanation, not a technical one. The essence is correct, but the details are somewhat handwaved. If you want more technical details, look into how an IEEE float is stored.)*

# Answer
> 0 votes
You can roughly say that every floating point operation has an error proportional to the size of the result (with the notable exception of subtracting x - y when x/2 ≤ y ≤ 2x).

So in the first case, the errors per operation with $x^2 ≈ 80$, $y^2 ≈ 100$, are (very roughly) x^2 -\> 80 eps, y^2 -\> 100 eps, x^2 - y^2 = no error, total 180 eps. vs x - y -\> no error, x + y ≈ 19 -\> 19 eps, (x+y)(x-y) ≈ 21 -\> 21 eps, total 40 eps.

This is very simplified, but it shows the principle that by rearranging calculations in a clever way you can vastly reduce floating point errors.

---
Tags: floating-point
---


# Question
Title: Can I have a "dependent coproduct type"?
I'm reading through the HoTT book and I have a (probably very naive) question about the stuff in the chapter one.

The chapter introduces the **function type** $$ f:A\to B $$ and then generalizes it by making $B$ dependent on $x:A$ $$B:A\to\mathcal{U},\qquad g:\prod\_{x:A}B(x)$$ and that is called the **dependent function type**.

Moving on, the chapter then introduces the **product type** $$ f:A\times B$$ and then generalizes it by making $B$ dependent on $x:A$ $$B:A\to\mathcal{U},\qquad g:\sum\_{x:A}B(x)$$ and that is called the **dependent pair type**.

I can definitely see a pattern here.

Moving on, the chapter then introduces the **coproduct type** $$ f:A+B$$ and ... combobreaker ... there is no discussion of dependent version of this type.

Is there some fundamental restriction on that or it is just irrelevant for the topic of the book? In any case can someone help me with intuition on why function and product types? What makes those two so special that they get to be generalized to dependent types and then used to build up everything else?

# Answer
The dependent sum is a common generalization of both the cartesian product $A \times B$ *and* the coproduct $A + B$. It just so happens that the HoTT book introduces dependent sum by generalizing $A \times B$, because that does not require the boolean type to be defined first.

The coproduct is a special case of dependent sum. Given types $A$ and $B$, consider the type family $P : \mathtt{bool} \to \mathcal{U}$ defined by $P(\mathtt{false}) = A$ and $P(\mathtt{true}) = B$. The dependent sum $\sum\_{b : \mathtt{bool}} P(b)$ is equivalent to $A + B$. By the way, you can also get $A \times B$ as a dependent product $\prod\_{b : \mathtt{bool}} P(b)$.

You ask what is special about products and function types. There are many, many reasons why $\sum$ and $\prod$ are "necessary". In terms of logic, they are necessary because they correspond to $\exists$ and $\forall$ by the propositions-as-types correspondence (but that only shifts the question to "why are $\exists$ and $\forall$ necessary?"). In terms of category theory, $\sum$ and $\prod$ are necessary because they are the left and right adjoint to substitution. Ask a more secific question if you would like to know more.
> 20 votes

# Answer
I'll talk about this more software-engineering-ly.

Are you talking about a coproduct type whose latter **constructors** can refer to prior ones (which, looks pretty similar to a product whose latter *fields* can refer to prior ones)? This is possible in Agda after HIT is introduced (in version 2.6.0):

```
-- Auxiliary definition: Nat
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

-- The HIT I was talking about
data Int : Set where
  positive : Nat -> Int
  negative : Nat -> Int
  -- Note this constructor uses `positive` and `negative`.
  zeroPath : positive zero ≡ negative zero

```

By following this paper, if your type-checker checks definitions defined using the syntax presented in figure "(26)", I believe it's quite simple to support "dependent coproducts".
> 3 votes

---
Tags: type-theory, dependent-types, homotopy-type-theory
---


# Question
Title: Proving that $S_1+S_2 \leq f^{-\omega(1)}$
I am trying to show for every c, there exists $M\text{ such that }(x,y,z)\geq M$ then $S\_1(x,y,z) + S\_2(x,y,z) \leq ( f (x,y,z))^{-c} $ . For a particular $S\_1,S\_2,f$. Does it suffice to prove there exists M1, for corresponding $S\_1$, with $S\_1(x,y,z) \leq (f(x,y,z))^{-c} $ and $M\_2$ for $S\_2({x,y,z)} \leq (f(x,y,z) )^{-c} $?

This is in the same spirit as showing $O(S\_1+S\_2) \leq T$ can be done by showing individual upper bounds.

All functions are strictly positive increasing functions. In particular, $f$ is not a constant.

I am trying to show that there for large enough $x,y,z$, $S\_1 + S\_2$ is smaller than the inverse of any polynomial in $f$.

I am looking to solve it for a particular case of $f=x^2 y^2+xz\ log (xz)$ but general answers are also appreciated.

# Answer
Let's consider the simpler case in which $f$ only has one input — the general case is the same, given that you use the correct definitions.

Here is what we want to prove:

> Suppose that $\lim\_{n\to\infty} f(n) = \infty$.
>
> If for all $c \geq 0$ there exists $N$ such that for all $n \geq N$, $S\_1(n) \leq f(n)^{-c}$ and $S\_2(n) \leq f(n)^{-c}$, then for all $c \geq 0$ there exists $N$ such that for all $n \geq N$, $S\_1(n) + S\_2(n) \leq f(n)^{-c}$.

Let us be given $c \geq 0$. Let $N\_1$ be such that $f(n) \geq 2$ for all $n \geq N\_1$, and let $N\_2$ be such that for all $n \geq N\_2$, $S\_1(n),S\_2(n) \leq f(n)^{-(c+1)}$. Let $N = \max(N\_1,N\_2)$. Then for $n \geq N$, $$ S\_1(n) + S\_2(n) \leq 2f(n)^{-(c+1)} = \frac{2}{f(n)} f(n)^{-c} \leq f(n)^{-c}. $$
> 1 votes

---
Tags: asymptotics
---


# Question
Title: Does weak consistency allow reordering of events?
I am on studying a consistency model: weak consistency. weak consistency This model was first defined by Dubois et al. (1986), by saying that it has three properties:

1. Accesses to synchronization variables are sequentially consistent.
2. No access to a synchronization variable is allowed to be performed until all previous writes have completed everywhere.
3. No data access (read or write) is allowed to be performed until all previous accesses to synchronization variables have been performed.

And there is an example saying that the following sequence is weak consistent :

Here, S represents accessing synchronization variables.

But how is this possible ? I don't understand how can the event R(x)2 happens before R(x)1 of processor P3 while W(x) 1 happens before W(x)2 on processor P1.

# Answer
Weak consistency rather appears in distributed systems where changes to variables have to be transmitted via the network.
Before a synchronization there is no guarantee to the visibility of write operations.
On P2 the `W(x)1` could arrive before `W(x)2` and on P2 `W(x)2` could arrive before `W(x)1`.
> 1 votes

---
Tags: memory-access
---


# Question
Title: Finding closed forms for the return values
```

int coffee(int n) {
   int s = n * n;
   for (int q = 0; q < n; q++)
      s = s - q;
   for (int q = n; q > 0; q--)
      s = s - q;
   return s + 2;
}

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

int mocha(int n) {
    int r = 0;
    for (int i=0; i<=n; i = i+16)
        for (int j=0; j<i; j++)
            r++;
    return r;
}

int espresso(int n) {
    int j=0;
    for (int k = 16; coffee(k) * mocha(k) - k <= n; k+=16) {
        j++;
        cout << "I am having so much fun with asymptotics!" << endl;
    }
}
return j;

```

I am trying to find the returning value in terms of $n$ for `coffee`, `tea`, `mocha`, but I am stuck right now.

I know `coffee` will return 2 as the code follows:

$s = n^2$

$s = n^2 - \displaystyle\sum\_{q=0}^{n-1}q = n^2 - \dfrac{n(n-1)}{2}$

$s = n^2 - \dfrac{n(n-1)}{2} - \displaystyle\sum\_{q=1}^n q = n^2 - \dfrac{n(n-1)}{2} - \dfrac{n(n+1)}{2} = 0$

Then, $s = 0 + 2$.

However, I can't seem to figure out `tea`, `mocha`, and `espresso`, because they don't follow +1 increments. Could anyone help me out how to compute the return value in terms of $n$?

# Answer
For coffee, you can replace the less than with $$\leq n^3-1$$ and since you’re counting the number of doubling, the answer will be $$\lfloor(\log(n^3-1,2))+1\rfloor$$

For mocha firstly notice inner loop is equivalent to `r+=i` and the sum becomes $$16 \cdot \lfloor(n/16)\cdot(\lfloor(n/16)+1)/2 \rfloor \rfloor$$

I’m pretty sure you can work out the last function. Sorry if this is unclear. I’ll edit this better when I get my laptop
> 0 votes

---
Tags: algorithms, algorithm-analysis
---


# Question
Title: How is the right, root, left order traversal called in a binary search tree?
In a Binary Search Tree you have the following orders for traversal:

Left, Root, Right is called Inorder (or ascending order).

Root, Left, Right is called Preorder.

Left, Right, Root is called PostOrder.

But how is Right, Root, Left (or descending order) called?

# Answer
> 2 votes
As per wikipedia (Tree Traversal), it is called ***Out-order traversal***

Though, you could also find reference to *reverse in-order traversal*, which means the same.

---
Tags: algorithms, binary-search-trees
---


# Question
Title: Maximum-cardinality matching in unbalanced bipartite graphs
Let $G = (X+Y, E)$ be a bipartite graph, and suppose we want to find a maximum-cardinality matching in $G$. The Hopcroft-Karp algorithm runs in time $O(|E|\sqrt{|V|})$, where here $|V| = |X|+|Y|$. So if the graph is unbalanced and $|X|\<|Y|$, the run-time is $O(|E|\sqrt{|Y|})$.

Is there an algorithm that attains a better worst-case runtime complexity for the case of an unbalanced bipartite graph, where $|X| \in o(|Y|)$? In particular, if $|X|$ is constant, is it possible to get run-time $O(|E|)$?

# Answer
I just found the answer myself. In this paper:

> Lyle Ramshaw, Robert E. Tarjan (2012). "On minimum-cost assignments in unbalanced bipartite graphs". Technical reports, HP research labs.

in section 5, the authors show that the Hopcroft-Karp algorithm in fact solves the following problem: given an integer $s$, find matchings with $1,\ldots,s$ edges. The run-time is $O(|E|\sqrt{s})$. In particular, if $|X|\<|Y|$, we can take $s=|X|$ and the run-time is $O(|E|\sqrt{|X|})$.
> 2 votes

---
Tags: optimization, reference-request, runtime-analysis, bipartite-matching
---


title: Is JavaScript a homoiconic language?

text:
# Question
Title: Is JavaScript a homoiconic language?
I can't help but notice the uncanny resemblence JavaScript has to LISP. JSON (JavaScript Object Notation), for instance, is a data structure that can be reconstituted into an object by subjecting it to an eval() function. Likewise, LISP data can also be executed as code.

This leads to my question: Is JavaScript Homoiconic or at least partially so? If not, why?

# Answer
> 2 votes
Given your definition, the answer is "no". JavaScript syntax is not a subset of JavaScript's literal syntax. The fact that a value a literal represents can be produced by evaluating the literal is what makes a literal a literal and is true in any language. The only real difference is JavaScript has a richer literal syntax than many common programming languages, though this is certainly not a rare thing.

The answer is "no" for pretty much any reasonable definition that doesn't make practically every language "homoiconic".

My impression is there is not a clear consensus of what "homoiconic" means *within* the Lisp community. Part of that is it seems many Lispers are confused1 about "homoiconicity"2. I recommend this article which goes over the variety of possible definitions of "homoiconic" and the issues with each. As the title of that article is "Don't Say 'Homoiconic'", this suggests worrying about whether a language is "homoiconic" is not a great idea and you should be more specific about what it is you are care about.

If we use the definition referenced in the article, namely "having the internal and external representations be the same", then this definitely doesn't apply to JavaScript (to the extent that it even makes sense). It arguably doesn't apply to Lisp either, but there are various ways where Lisp gets closer to this. One small indicator is that Lisp's `eval` takes in Lisp lists while JavaScript's takes in strings. This separation holds for the actual Lisp implementation as well as parsing is viewed as conceptually outside of the implementation and so the implementation conceptually works upon Lisp lists. This has non-trivial consequences like being able to provide circular syntax and an abstract syntax graph in general.

1 Frankly, understandably so as the explanations tend to be vague. There is also, at this point, a lot of misinformation.2

2 There are many definitions floating around that whatever "homoiconic" should mean if anything doesn't mean these things such as "supports higher-order functions".

---
Tags: programming-languages, lisp
---


# Question
Title: Random restarts for unsatisfiable instances
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.

One technique used, that has shown good results in practice, is random restart. Intuitively, randomly restarting means there is a chance of getting luckier with guessing the right variable assignments that would lead to a quick solution.

The same intuition suggests this should be much more effective when the problem instance is in fact satisfiable (so you only need to guess a set of variable assignments that constitute a solution) than if it is not (so in principle you have to check all possible assignments anyway, modulo sections of the search space that can be skipped via techniques like unit propagation and non-chronological backtracking, which are at least not obviously sensitive to the initial guesses).

Is the second intuition correct? Are random restarts in fact much more effective, on average, in cases where the problem instance is in fact satisfiable?

# Answer
There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from knowledge gained about persistently troublesome conflict variables sooner than backjumping would otherwise allow the partial assignment to be similarly reset. In effect, restarts allow the discovery of shorter proofs of unsatisfiability on average.
> 10 votes

---
Tags: satisfiability, randomized-algorithms, 3-sat, sat-solvers
---


# Question
Title: How do we determine whether a heuristic is better than another in A* search Algorithm?
I am trying to solve a Maze puzzle using the A\* algorithm. I am trying to analyze the algorithm based on different applicable heuristics.

Currently, I explored Manhattan and Euclidean distances. Which other heuristics are available? How do we compare them? How do we know whether a heuristic is better than another?

# Answer
> 4 votes
A good heuristic should approximate the actual distance to the goal as closely as possible, without going over it.

If heuristic1 returns a greater or equal value than heuristic2 for every input (while still being valid), then heuristic1 is better. In your case, Manhattan distance is better than Euclidean distance because the value it returns is never smaller than Euclidean distance and is sometimes larger. (Unless you can move diagonally in the maze, in which case Manhattan distance is an invalid heuristic and Euclidean distance might be as well.)

If heuristic1 returns a larger value for some inputs, and heuristic2 returns a larger value for others (and both are valid), then heuristic3(x) = max(heuristic1(x), heuristic2(x)) is better than either of them.

If the heuristics are slow, it's more complicated. Since heuristic3 will be even slower than heuristic1 or heuristic2 alone, it could end up being worse overall if it doesn't improve the estimate by very much. There's no unambiguous way to choose the best heuristic in this case. You basically have to benchmark and decide how much cleverness you can afford.

---
Tags: algorithms, graphs, search-algorithms
---


# Question
Title: How do 2-3 FingerTrees generalize to bigger branching factors?
FingerTrees as implemented by Haskell's Data.Sequence use a branching factor of 2-3 for Nodes, and have Digits of size 1-4. Imagine we want to make the branching factor much wider -- perhaps to amortize per-node overheads better, or to improve lookup performance at the cost of update performance.

For example, we might want branching factors of 31-32 as in RRB-trees, or branching factors of 16-32 as in B-trees. How should the size of the Digits change to accommodate these branching factors? More generally, are there algebraic conditions on the size ranges of Nodes and Digits which are sufficient to guarantee the asymptotics (logarithmic access to the middle; constant-time access to the ends) of FingerTrees?

# Answer
Yes - if you read the original paper and assign the notions of *safe* and *dangerous* digits to the smallest and largest digits, the math should all go through.
> 1 votes

---
Tags: data-structures, trees
---


# Question
Title: How do we translate first order logic's universal quantifier (the $\forall$) and the existential quantifier (the $\exists$) to Prolog?
I'm trying to convert some English statements to first order logic statements and I'm trying to use Prolog to verify the translations. My question is: how do I convert a first order logic statement (having $\forall$ and $\exists$ quantifiers) into Prolog rules?

---

For example, there's this English statement:

> Every voter votes for a candidate which some voter doesn't vote for.

and here's my translation of the English statement into first order logic:

$$\forall x, y\[Voter(x) \land Candidate(y) \land Votes(x, y) \rightarrow \exists z\[ Voter(z) \land \lnot Votes(z, y) \] \]$$

Now I'm not sure if this translation is correct. That's what I want to find out. My question is: how do I convert this first order logic statement to a Prolog rule?

---

So first I'm trying to fill a Prolog database with some facts.

```
human(p1).
human(p2).
human(p3).
human(p4).
human(p5).
human(p6).
human(p7).
human(p8).
human(p9).
%humans who are neither voters nor candidates
human(p10).
human(p11).

%humans who are only voters
voter(p1).
voter(p2).
voter(p3).

%humans who are candidates and voters
voter(p4).
voter(p5).
voter(p6).
candidate(p4).
candidate(p5).
candidate(p6).

%humans who are only candidates
candidate(p7).
candidate(p8).
candidate(p9).

%some random votes
votes(p1, p6).
votes(p2, p6).
votes(p3, p6).
votes(p4, p7).
votes(p5, p8).
votes(p6, p5).

```

I'm using `human`, `voter`, `candidate`, and `votes`. Here are some attempts to model the statement into a Prolog rule:

```
rule1 :-
  foreach((voter(X), candidate(Y), votes(X, Y)),(voter(Z), \+votes(Z, Y))).

rule2 :-
  foreach((human(X), voter(X), candidate(Y), votes(X, Y)),(human(Z), voter(Z), \+votes(Z, Y))).

```

# Answer
> 4 votes
Prolog does not support arbitrary first-order logic but only a fragment of it known as Horn clauses. These are statements of the form $$\forall x\_1, \ldots, x\_n \\,.\\, P(x\_1, \ldots, x\_n) \Rightarrow q(x\_1, \ldots, x\_n)$$ where $P$ is built from atomic predicates and conjunctions, and $q$ is an atomic predicate. Not every statement in logic can be converted to this form.

You are suggesting use of `foreach`. Note that this is not properly a *logic quantifier* in Prolog, but rather a special-purpose routine which operates on lists. Pure prolog does not have any of this. If you are willing to use lists and to limit attention to only quantification over finite lists of elements, then you can just implement everything easily enough in Prolog using lists and functions on them. But that misses the point of logic programming, does it not?

# Answer
> 1 votes
If your intention is just to check if your translation from English to first order logic is correct, then I think you could put both your answer and the correct answer that is different from yours in CNF using Herbrand's theorem and compare if they are equal.

---
Tags: first-order-logic, prolog
---


title: NFA that accepts 0* or 1*

text:
# Question
Title: NFA that accepts 0* or 1*
Problem statement: Produce an NFA that accepts the strings 0\* and 1\*. So 000 and 11 would be accepted, while 101 would not be.

I'm a bit concerned about my idea because not all combinations of the alphabet are producible in it. Is this NFA legitimate?

My idea (updated to include the empty string):

# Answer
In a nondeterministic automaton, a given string may have multiple possible paths through the automaton, since the path may include $\varepsilon$-transitions and may reach nodes where there is more than one possible non-$\varepsilon$-transition. A given string may also have no possible path if all the ways to traverse the automaton reach a point where there is no outgoing transition with the correct letter. If there's no possible path through the automaton, the string is rejected, just as if there are paths but none of them reach an accepting state. To determine whether a string is accepted, what matters is only whether there is a way to reach an accepting state, not what happens on paths that don't lead to an accepting state.

You can add a sink state to your automata: add a state $q\_s$ which has outgoing transitions to itself (and only to itself) on all letters ($q\_s \xrightarrow{0} q\_s$, $q\_s \xrightarrow{1} q\_s$) and add transitions from other states wherever a letter is missing ($q\_0 \xrightarrow{0} q\_s$, $q\_0 \xrightarrow{1} q\_s$, $q\_1 \xrightarrow{1} q\_s$, $q\_2 \xrightarrow{0} q\_s$). Since there is no way to reach an accepting state via $q\_s$, adding this state and these transitions doesn't change the language that the automaton recognizes.

“Completing” the automaton in this way isn't very useful for a nondeterministic automaton. It lets you ensure that every string has at least one path, but note that some strings now have more paths — for example the string $0$ used to only have the path $(q\_0, q\_1, q\_1)$ but now also has $(q\_0, q\_s)$. The situation is different with deterministic automata. A deterministic automaton must have a transition at every state for every letter. There's a convention to allow some transitions to be missing. Such an incomplete automaton (with missing transitions, i.e. the “transition function” is only a partial function) is equivalent to a complete automaton (where the transition function is a function) which has one extra state, called a sink state, with the missing transitions leading to it and outgoing transitions only to itself. This is a useful convention with deterministic automata, where it's useful to draw automata without “useless” transitions but easier to reason on complete automata where all transitions are present. With nondeterministic automata, since a string doesn't have a unique path through the automaton, making an explicit sink state isn't particularly useful.
> 1 votes

---
Tags: finite-automata
---


# Question
Title: How to prove the performance, Big Omega ,of building a binary heap using recursive method is Ω(nlog(n))
We can learn the big-O of building a binary heap using recursive method is O(n log n) from wiki "This approach, called Williams’ method after the inventor of binary heaps, is easily seen to run in O(n log n) time: it performs n insertions at O(log n) cost each.\[a\]" we can also know if we build the heap using other methods. the big O could be better. Where should we begin if we would like to prove that the performance, Big Omega ,of building a binary heap using recursive method is Ω(nlog(n)), which is same as Big-O?

insert method from wiki

> To add an element to a heap we must perform an up-heap operation (also known as bubble-up, percolate-up, sift-up, trickle-up, swim-up, heapify-up, or cascade-up), by following this algorithm:
>
> Add the element to the bottom level of the heap. Compare the added element with its parent; if they are in the correct order, stop. If not, swap the element with its parent and return to the previous step

then we have the buildheap as

```
buildheap((1,1),(,))
   if n==1:
      return [(1,1)]
return insert(( ,),buildheap((1,1),...(−1,−1))

```

# Answer
> 1 votes
Suppose that your heap is a max-heap: a parent should be larger than its children. Consider what happens when you call `buildheap` with the numbers $1,\ldots,n$ in that order. Each time you add a new element to the bottom level of the heap, and the `heapify` procedure diffuses it all the way to the root. Since element $k$ is put at level $\Theta(\log k)$, inserting the $k$'th element takes time $\Theta(\log k)$. Overall, `buildheap` takes time $\Theta(\log 1 + \cdots + \log n) = \Theta(\log n!) = \Theta(n\log n)$.

---
Tags: heaps, performance, big-o-notation
---


title: Proving with co-induction principles

text:
# Question
Title: Proving with co-induction principles
I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the `stream_eq` predicate in Chapter 5.

Firstly, I'm used to induction schemes defined for data structures (`stream` in this case, if it were data and not codata). Yet, the co-induction principle being introduced seems to be defined for the predicate we're trying to prove itself, and how does it connect with the following (cursive ours)?

> Dually, a co-induction principle *ought to be parameterized over a predicate* characterizing what we mean to prove, as a function of the arguments to the co-inductive predicate that we are trying to prove.

Or should I parse this as implying parametrization over the predicate `R : stream A -> stream A -> Prop`, which, to me, seems like a reformulation of `stream_eq`, taking the following hypothesis into account?

```
Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).

```

Secondly, considering the quoted text again, we're trying to prove `stream_eq`. What would be the arguments to that predicate here? Looks like it should be the streams, but the hypothesis seem to be much more complex than that.

Lastly, all of this `stream_eq_coind` looks to me a like a somewhat generic way to do the `match` acrobatics on the streams to allow the simplifier to proceed (as Chlipala does in the version of the proof preceding this part). Is this correct or am I missing some deeper sense?

Oh, and what would be some good sources for me to read on co-induction? A few papers or tutorials I've found refer to some algebra or logic (i.e. Kripke models) quite beyond my current knowledge.

# Answer
> 3 votes
What likely makes it confusing is that you are doing very different things in inductive versus coinductive cases. This is somewhat alluded to by Chlipala's reference to "infinite proofs"1. (Another aspect that makes seeing what is really going on hard is the presentation that makes coinductive type declarations look similar to inductive type declarations.)

I'm going to set up some context starting with inductive types. This is motivated by the categorical understanding of inductive types via initial algebras, but I'm not going to elaborate on that too much

Since inductive types are modeled by initial algebras, this means if we define the behavior of a function on cases, which corresponds to providing an algebra, we get a unique algebra morphism from the initial algebra to our just defined algebra, and this unique algebra morphism is the recursor. The main thing to note here for our purposes is that we get an morphism *into* the type of our choosing. This is evident from the type of a recursor, e.g. the one for naturals is $\forall T.T\to(T\to T)\to\mathbb N\to T$ so we get to choose $T$. To get the inductive eliminator, we can essentially do the same story but instead of using a category of types and functions, we use a category of families of types and families of functions. This is a massively oversimplified summary of Fibrational Induction Rules for Initial Algebras. Again, the upshot for us is that we get to choose the family (represented by a $\mathsf{Prop}$-valued function) and the result is a function into this family. Since from a Curry-Howard perspective, to prove the predicate that the family represents, we want to produce values in the family, and this situation is ideal. Note that the predicates we're proving are not themselves inductive types (though they could be).

The categorical story for coinductive types is categorically dual. We talk about final coalgebras instead of initial algebras. The main point for us is that a final coalgebra provides a unique coalgebra morphism *from* a type of our choosing *into* our coinductive type. This leads to the duality that it's simple to create a value of an inductive type while consuming one is involved, meanwhile it is simple to consume a value of a coinductive type but producing one is involved. This is somewhat obscured by the presentation of coinductive types in Coq.2

The problem is that if we want to prove some predicate, we need to *produce* a value of the appropriate type, but coinduction is about how to produce values of the coinductive type.

The "solution" is to consider coinductively defined *predicates*, and then we can use coinduction to produce values of these predicates to prove them. And this is what's happening in the examples. We are not using coinduction on streams to show that `stream_eq` holds. Instead, `stream_eq` is *itself* a coinductive type. The fact that `stream` is also a coinductive type is irrelevant here. For example, would could define `stream_eq` to talk about functions $\mathbb N\to A$ instead of streams. Indeed, the `evalCmd` example is defining a coinductively defined predicate over inductive types.

As for why the coinduction rule takes the form it does for `stream_eq`, this follows from its definition fairly mechanically except the notation obscures things a bit. First, we can make the equality of the heads more apparent by, instead of using the same variable for both, using two variables and an explicit equality. Something like:

```
  CoInductive stream_eq : stream A -> stream A -> Prop :=
  | Stream_eq : forall h1 h2 t1 t2,
    h1 = h2
    -> stream_eq t1 t2
    -> stream_eq (Cons h1 t1) (Cons h2 t2).

```

A record-oriented rewriting would make things clearer still, e.g.:

```
coinductive StreamEq (A : Type) (xs ys : Stream A) : Prop where
     headEq : hd xs = hd ys
     tailEq : StreamEq A (tl xs) (tl ys)

```

The coalgebra (in a category of families) that we need to apply coinduction corresponds to producing a family of functions from $R$ to a record of the same form as `StreamEq` only with $R$ in the place of `StreamEq`. A function into a pair can be split into a pair of functions and this exactly what `Cons_case_hd` and `Cons_case_tl` correspond to.

1 I don't really like this reference to "infinite data structures" and "infinite proofs" as that's not what's happening.

2 If we used a more record-like declaration syntax it would be more obvious. Having something like:

```
coinductive Stream (A : Type) where
    hd : A
    tl : Stream A

```

with `corec` would be something like

```
corec : (S : Type) -> (S -> { hd : A, tl : S }) -> S -> Stream A

```

would make this a bit clearer. This record-/projection-oriented view of coinductive types helps explain the guardedness conditions. What we're *really* specifying in a `corec` is the behavior of `hd` and `tl`. If we don't *manifestly* present a `Cons` to Coq, so it can take the `hd` of it as the definition of `hd` and the `tl` as the definition of `tl`, then Coq doesn't know what those definitions should be, and, of course, they might not exist at all which means we don't have a coalgebra and can't apply corecursion.

---
Tags: proof-techniques, formal-methods, coq, coinduction
---


title: A* algorithm example explained

text:
# Question
Title: A* algorithm example explained
I am trying to understand A star algorithm. I am aware that it follows the sum of the current cost and heuristic, therefore `f(n) = c(n) + h(n)` in order to expand a new node. So every time the code with the smallest f(n) from the root is expanded. However, I am confused about the backtracking of the algorithm when it does not find the best solution. I tried to follow the example explained here. Therefore, by only using the f(n) the algorithm should have expanded: S-B-C-G. Firstly B then C and then G. Then declare that find a solution. How, the backtracking works?

The example is as follows:

In the left, there is the graph and in the table is the heuristic cost. What is going to be the a star expand in this graph?

# Answer
> 1 votes
A\* doesn't backtrack. It just keeps expanding the node with the least value of $f$ until it finds a solution. The properties of the heuristic used guarantee that the first solution found is optimal.

---
Tags: trees, search-algorithms
---


# Question
Title: How can $A \cup B$ be decidable if $B$ is undecidable?
My assignment says:

"Determine if the following statement is correct: If $A$ and $A \cup B$ are decidable, then $B$ is decidable."

The solution says:

"Incorrect. If $B = H\_0 \subseteq \\{0,1\\}^\*$ is the halting problem with input $\epsilon$ and $A = \\{0,1\\}^\*$, then $A$ and $A \cup B$ are decidable and $B$ is undecidable.

My question is:

How can $A \cup B$ be decidable if $B$ is undecidable? If for example $b \in B$ then $b \in A \cup B$ but a Turing Machine may not halt on $b$ because $B$ is undecidable, then how can $A \cup B$ still be decidable with $b \in A \cup B$ ?

# Answer
> 5 votes
If $A=\\{0,1\\}^\*$ then $A\cup B=\\{0,1\\}^\*$, regardless of what $B$ is. $\\{0,1\\}^\*$ is decidable, and choosing to express it as something involving undecidable things doesn't change that fact.

The question "Is $w$ in $A\cup B$?" is equivalent to "Is at least one of the following statements true? $w$ is in $A$; $w$ is in $B$; $w$ is in both $A$ and $B$?" In the case $A=\\{0,1\\}^\*$, we can answer "Yes, $w$ is in $A$" and the rest of the questions are irrelevant. It doesn't even matter if we can't answer "Is $w$ in $B$?", because we don't need to.

Here's a more practical example that might help. Suppose I give you a number $x$ and ask you "Is $x\in\text{Integers}\cup\text{Primes}$?" Figuring out if a large number is prime is quite difficult, but you can easily answer my question by checking if $x$ is an integer. You can ignore the "prime" part completely.

---
Tags: turing-machines, undecidability, sets
---


title: prove that {$↔,⊕$} is incomplete set?

text:
# Question
Title: prove that {$↔,⊕$} is incomplete set?
How do i prove that Is {$↔,⊕$} not a complete set ? I have no clue how to prove it .

# Answer
Prove by induction that any formula using only these connectives is affine, that is, has one of the following forms: $$ x\_{i\_1} \oplus \cdots \oplus x\_{i\_\ell}, \\ x\_{i\_1} \oplus \cdots \oplus x\_{i\_\ell} \oplus 1. $$ Then show that there are functions not expressible in this form.
> 1 votes

# Answer
The universal method to check whether a set of connectives is complete in this sense is Post's classes: there are 5 function classes such that a set of functions is complete iff it isn't a subset of any of these 5. One of the 5 is affine functions, as described in Yuval's answer; the rest are monotone, self-dual, 0-preserving, and 1-preserving functions.

It's pretty easy to show that all 5 classes are *closed*: any composition of functions from one of them will also belong to the same class. So if your set is a subset of a Post's class, it can't be complete. Showing the other direction is more complicated, but likely you'll learn the proof in the near future.
> 3 votes

---
Tags: logic, discrete-mathematics, propositional-logic
---


# Question
Title: Generate all combinations of values that are less than array's elements and have a sum = target
I want to find a way to generate sets that contain elements that sum to a certain target. Initially, I have an array that contains elements representing the maximum value that can be stored in that index.

For example, the input is \[8,6,1\] and the target is 10. The algorithm should produce all sets that have elements \[ (\<=8), (\<=6), (\<=1) \] such that their sum is equal to 10. Examples include: \[8,1,1\], \[8,2,0\], \[7,3,0\], ...

A major consideration for this algorithm is that it should work on any input length (the above example has a length of 3).

I think the solution is close to the subset sum problem, but I wasn't able to figure it out. Any help is appreciated.

Side note: python code is preferred, but Pseudo-code should be fine.

Thanks

# Answer
Where *subset sum* takes exponential time to find a solution, here you can find one solution quickly, but there are exponentially many solutions, and therefore it will take exponential time to find them all.

Or factorial really, on the length (let's call this $n$) of the array, as every time you have a set of $n$ numbers that add up to the target, all $n!$ permutations of this is a solution in the worst case, when they are within the maximum values (that is, \[6,4,0\] and \[4,6,0\] are not the same solution but both valid). So if the target can be summed from $n$ numbers in $k$ different ways, then we can have up to as many as $k * n!$ solutions in the worst case.

For small problems, you should be able to solve this using recursion. Here is a pseudocode representation that should work. Hope it all makes sense.

Pseudocode:

1:$\quad$ **function** RECURSE( *index* , *sum* , *value* , *array* )

2:$\quad\quad$ *sum* $\leftarrow$ *sum* \+ *value*

3:$\quad\quad$ **if** *sum* = *target* **and** *index* is last index in array **then** print result $\quad$// *it's a match*

4:$\quad\quad$ **if** *sum* $\gt$ *target* **or** *index* is the last index in array **then** return $\quad$// *no result here*

5:$\quad\quad$ **increment** *index*

6:$\quad\quad$ **for** $i = 0$ **to** $i =$ max allowed value on *index* **do**

7:$\quad\quad\quad$ *newArray* $\leftarrow$ copy of *array*

8:$\quad\quad\quad$ *newArray*\[*index*\] $\leftarrow i$

9:$\quad\quad\quad$ RECURSE( *index* , *sum* , *i* , *newArray* )

10:$\quad\quad$ **end for**

11:$\quad$ **end function**

$\\\$

12:$\quad$ **function** MAIN

13:$\quad\quad$ **for** $i = 0$ **to** max allowed value on index 0 i array **do**

14:$\quad\quad\quad$ *array* $\leftarrow$ new array

15:$\quad\quad\quad$ *array*\[0\] $\leftarrow$ $i$

16:$\quad\quad\quad$ **call** RECURSE( 0 , 0 , $i$ , *array* )

17:$\quad\quad$ **end for**

18:$\quad$ **end function**
> 2 votes

---
Tags: algorithms, subset-sum
---


# Question
Title: Why is it not possible to prove that two Turing Machines calculate the same function?
I was wondering why it is not possible. Is it because the corresponding language is not decidable, or because of the fact that it is not guaranteed that a Turing machine halts on every input?

# Answer
> 5 votes
Your exam question makes very little sense. The obvious reading would be this:

> Let $M$ and $N$ be two Turing machines. Why is it not possible to prove that $M$ and $N$ compute the same function?

More precisely:

> It is not the case that for all Turing machines $M$ and $N$ it is provable that $M$ and $N$ compute the same function.

Well, this is quite obvious: there exist two Turing machines that calculate *different* functions, say a Turing machine $M$ that computes the function $n \mapsto n + 1$, and a Turing machine $N$ that computes the function $n \mapsto 42 \cdot n$. Therefore, in general, $M$ and $N$ need not compute the same function, so in general we cannot prove that they do.

I am going to guess that whoever asked this question really wanted to ask:

> Show that there is no *decision procedure* which decides, given any Turing machines $M$ and $N$, whether they compute the same function.

This is a standard exercise in computability theory, but is completely different from the question. One should not mix up things like "prove" and "decide".

I suggest that you go back to the author of the question and ask them to participate in this discussion. Then perhaps we can clear up the confusion, and save some students from unnecessary suffering.

**Supplemental:** A hint on how to show that such comparison is not decidable: given a Turing machine $T$, produce a new Turing machine $M$ which on input $n$ outputs $1$ if $T$ halts in fewer than $n$ steps, and $0$ otherwise. Compare $M$ to the machine which always output $0$.

---
Tags: formal-languages, turing-machines, undecidability, halting-problem
---


title: Lack of Stack Pointer Register

text:
# Question
Title: Lack of Stack Pointer Register
Suppose a processor lacks STACK Pointer Register. But, It does have STACK. Then, in my opinion, a program will still be able to call subroutines but, will be unable to return back from the subroutines. Please do clarify me where I have made a wrong assumption. Also do mention the possible outcomes of the scenario.

# Answer
> 1 votes
Using a stack for function calls does not require any special support from the processor. It's up to the compiler to decide where to put the data relative to a function call (return address, parameters, possibly reserved space for the return value). A common convention is to designate one particular register as the stack pointer. This does not require any special processor instruction, it can be a general-purpose register. A function call looks like this:

* Write parameters to the memory region at address SP (stack pointer register)
* Decrease SP by the size of the parameters
* Write PC (program counter register) to the address SP
* Decrease SP by the size of PC
* Jump to the function entry point

Returning from the function looks like this:

* Load a PC-sized value from SP into a register A
* Increase SP by the size of PC
* Jump to A

Some processors have a particular register R with instructions to store a word in memory at the address designated by R and decrement R, and to load a word in memory at the address designated by R and increment R. In this case, the processor documentation typically describes R as the stack pointer register and compilers use it to store the address of the function call stack. But if the processor doesn't have such instructions, the compiler just emits separate instructions for load/store and for increment/decrement. The register doesn't need any special properties.

---
Tags: computer-architecture, operating-systems
---


# Question
Title: Examples of Regular, Context-free and Context-sensitive languages
Assume the languages:

$$ a) \\, L\_1 = \\{ w \in \\{b,c \\}^\* | \\, w \\, \text{contains 'bbc' as substring} \\} $$ $$ b)\\, L\_2 = \\{ 1^k 0^m 1^m | k,m \in \mathbb{N} \\} $$ $$ c)\\,L\_3 = \\{ w \in {0,1}^\* | \\, w \\, \text{is a multiple of 5 (binary system) }\\} $$ $$ d)\\,L\_4 = \\{ d^k e^m f^k | k,m \in \mathbb{N}, \\, k \< m\\} $$

$L\_1$: Since we could build an NFA which accepts its strings, it's **regular**.

$L\_2$: Using a single stack or PDA, by pushing $0$ to the stack for every $0$ in the string and then poping from the stack for every $1$ (after the $0$s) in the string, we can determine whether the string is in the language if the stack ends up empty. Thus, $L\_2$ is **context-free**.

$L\_4$: Same as above, but this time we need $2$ stacks (LBA). Push $0$s in the first stack for every $d$, push $1$s in the second stack for every $e$ and then pop from the two stacks for every $f$. If the first stack ends up empty and second ends up non-empty, then the string belongs to the language. Thus, $L\_4$ is **context-sensitive**.

Are the above conclusions correct? If so, please provide me with a hint for the classification of $L\_3$.

# Answer
$L\_1$, $L\_2$ and $L\_4$ are correct (notice that you are *not* showing that $L\_2$ is not regular and $L\_4$ is not context-free, which can be done using the appropriate version of the pumping lemma).

As far as $L\_3$ is concerned, let $x$ be the number that is encoded in binary and call $x\_i$ its $i$-th least significant bit, indexed from $0$. Then, counting modulo 5, we have:

$\displaystyle x = \sum\_{i=0}^\infty x\_i 2^i = \sum\_{i=0,4,8..} x\_i + 2 \sum\_{i=1,5,9..} x\_i + 4 \sum\_{i=2,6,10..} x\_i + 3 \sum\_{i=3,7,11..} x\_i$.

I.e., the least significant binary digit contributes $1$ to $x \bmod 5$, the next one contributes 2, then 4, 3, 1, 2, 4, 3, ... and this pattern repeats.

This means that you can create a DFA that recognizes $L\_3^R$ (and hence $L\_3$) using at most 20 states, namely $\langle i,j \rangle$ where $i \in \\{0,1,2,3\\}$ is the index, modulo 4, of the next character in the string, and $j \in \\{0,1,2,3,4\\}$ is the partial sum, modulo $5$, of the contributions of binary digits seen so far.

If the next bit is $0$ then: $\langle i,j \rangle \to \langle i+1 \pmod 5, j \rangle$.

If the next bit is $1$ then $\langle i,j \rangle \to \langle i+1 \pmod 5, j+ 2^i \pmod 5\rangle$. Writing this down explicitly:

* $\langle 0,j \rangle \to \langle 1, j+1 \pmod 5\rangle$;
* $\langle 1,j \rangle \to \langle 2, j+2 \pmod 5\rangle$;
* $\langle 2,j \rangle \to \langle 3, j+4 \pmod 5\rangle$;
* $\langle 3,j \rangle \to \langle 0, j+3 \pmod 5\rangle$.

The initial state is $\langle 0, 0 \rangle$ and the final states are all the ones of the form $\langle i, 0 \rangle$.
> 1 votes

---
Tags: regular-languages, context-free, finite-automata, classification, context-sensitive
---


# Question
Title: Algorithm to find longest path in a tree that is smaller than x
Suppose we have a weighted binary tree $G$ where the nodes are towns and edges are streets with edge weights being the travel time and we want to find out whether it is possible to travel from any town to any other town within some time $x$.

There are three paths to consider for each node $v$.

1. Path to the right subtree of $v$
2. Path to the left subtree of $v$
3. Path that goes from the left to the right subtree including $v$

My approach to solving this problem is to use dynamic programming and start at leaf nodes to calculate a travel time $T\_l$ for every leaf $l$ and set $T\_l = 0$. Then work my way up the tree and compute $T\_v = max(T\_c + w(v,c))$ for every other node where $c$ are the child nodes of $v$ and check if that value is smaller than the given $x$. This would cover the first two cases and would require us to iterate over every node and edge once which is in $O(V+E)$

Where Im not sure is how to cover the third case, i.e. if I wanted to compute the travel time from one leaf node to another. Is that still possible in linear time and how would I do that?

# Answer
> 2 votes
Your dynamic program is a step in the right direction. My idea would be to maintain *two* values for a node v:

1. $L\_v$: The longest path starting from v going downwards (these corresponds to your dynamic program and the first two cases)
2. $U\_v$: and the longest path in the subtree of v (i.e., case 3).

You already gave the formula for $L\_v$. For $U\_v$ you take the maximum of $U\_l$, $U\_r$ and $L\_l + w(lv) + w(rv) + L\_r$ where $l$ and $r$ are the left and right children of v resp. The last equation corresponds to the path which is formed by the longest paths to the left and to the right which are then joined.

---
Tags: dynamic-programming, shortest-path, binary-trees
---


title: What does valid method overriding mean?

text:
# Question
Title: What does valid method overriding mean?
In *Types and Programming Languages* by Pierce, from p257 to p258, about featherweight Java,

> The predicate `override(m, D, C→C0)` judges whether a method `m` with argument types `C` and a result type `C0` may be deﬁned in a subclass of `D`. In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

I am not sure what the predicate `override(m, D, C→C0)` means.

Does the predicate apply only to the case of overriding? (The first sentence doesn't imply so.)

Isn't it always possible to define a method with any name and any type in any class?

* In case of non-overriding, that is true.
* In case of overriding, that is also true.

Could you give examples where it is possible and where it isn't?

Figure 19-2: Featherweight Java (auxiliary deﬁnitions) says:

> Valid method overriding:
>
> If `mtype(m, D) = E→E0` implies `C = E` and `C0 = E0`, then `override(m, D, C→C0 )`

How can `mtype(m, D) = E→E0` imply `C = E` and `C0 = E0`? `mtype(m, D) = E→E0` only means that class `D` has a method `m` whose type is `E→E0`.

Why is "`mtype(m, D) = E→E0` implies `C = E` and `C0 = E0`" a condition for `override(m, D, C→C0 )`?

Thanks.

# Answer
> 1 votes
The important sentence in the first quote is

> In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

So if you have

```
class C1 { ... }
class C2 { ... }

class Cls {
    C1 foo(C2 x) { ... }
}

```

`override(foo, Cls, (C2)->C1)` holds but `override(foo, Cls, (C2)->C2)` doesn't; the subclass

```
class SubCls extends Cls {
    C2 foo(C2 x) { ... }
}

```

is illegal. In FJ, you can't have

```
class SubCls extends Cls {
    C2 foo() { ... }
}

```

either, unlike in Java.

> If `mtype(m, D) = E→E0` implies `C = E` and `C0 = E0`, then `override(m, D, C→C0 )`

This is implicitly quantified "for all `E` and `E0`". If `mtype(m, D)` is undefined, then `mtype(m, D) = E→E0` is always false, so it implies anything. If it's defined, then "`mtype(m, D) = E→E0` implies `C = E` and `C0 = E0`" is equivalent to `mtype(m, D) = C→C0`.

So it ends up being the same as

> > If `mtype(m, D) = C→C0` or `mtype(m, D)` is undefined, then `override(m, D, C→C0)`

(unless I went wrong somewhere)

---
Tags: programming-languages, type-theory, object-oriented, types-and-programming-languages
---


title: Grassfire vs BFS

text:
# Question
Title: Grassfire vs BFS
Expanding on this question :

Why is Dijkstra's Algorithm more popular compared to Grassfire algorithm?

What are the differences between grassfire and BFS? I'm surprised grassfire (supposedly) has a complexity of only $O(|V|)$, whereas BFS has a complexity of $O(|V| + |E|)$.

# Answer
> 1 votes
Grassfire seems to be simply a BFS in a 2D grid graph. Since $|E| = \Theta(|V|)$ in a 2D grid graph, this results in a complexity of $O(|V| + |E|) = O(|V|)$.

See also Wikipedia's page on the similar grassfire transform (https://en.wikipedia.org/wiki/Grassfire\_transform), a computation of the distance from some pixel(s) to the border of a region in an image, which can be used to yield descriptors such as the region's skeleton or medial axis.

---
Tags: algorithms, time-complexity, search-algorithms
---


# Question
Title: Algorithm Design: Efficient O(n) algorithm to get the ith to jth largest elements in an array
I am trying to design an efficient algorithm that retrieves the ith to jth largest elements in an array. For example, if the following array is the input:

```
[10, 14, 18, 3, 21, 25, 27]
i = 2
j = 4

```

The following array is returned:

```
[25, 21, 18]

```

18 is the 4th largest element in the array and 25 is the 2nd smallest element in an array. I've done a problem where you retrieve a list of the K largest elements in an array: in such a problem, the solution is pretty trivial (using a fixed-size minimum heap of size K to keep track of the K largest elements). In this case however, a heap seems out of reach to use because the minimum heap can only remove the smallest element from the heap (removing the kth smallest element within the heap seems really inefficient).

I could do QuickSelect (j - i) times to get all the elements, but that means doing a linear O(n) walkthrough (j - i) times, which yields a total time complexity of O((j-i) * n), but I was thinking about if it's possible to quicken the algorithm's time complexity to just O(n). Is there an O(n) algorithm to solve this problem?

---

# Answer
> 4 votes
> I could do QuickSelect (j - i) times to get all the elements

Overkill. Two calls to QuickSelect and one linear pass are sufficient.

# Answer
> 1 votes
If you don’t know quickselect: Just implement Quicksort, but every time Quicksort would sort a sub array, you don’t do it if you don’t need it to find out which items I to j are.

---
Tags: algorithms, algorithm-analysis, optimization, arrays, quicksort
---


# Question
Title: How can any non-primitive-recursive function like the Ackermann function be implemented on hardware?
If for-loops and function calls both boil down to jump instructions when implemented on a real machine, then how is "The Ackermann function isn't implementable with for-loops" a meaningful phrase?

# Answer
> 4 votes
Real machines have access to a stack, and so can implement recursion. This is all that is needed to implement the Ackermann function.

However, the Ackermann function grows very fast, so you would only be able to calculate a few of its values given realistic time and space constraints.

# Answer
> 3 votes
The phrase "The Ackermann function isn't implementable with for-loops" is shorthand for "The Ackermann function $A(m,n)$ cannot be implemented using bounded for-loops where an upper bound on the number of iterations in each loop is determined in advance from the values of the parameters $m$ and $n$". In other words the Ackermann function is not primitive recursive.

The Ackermann function can, of course, be implemented using while-loops (where a bound on the number of loop iterations is *not* fixed in advance). And while-loops can be reduced to simple logical tests and conditional jump instructions (this is what a compiler does).

Another way of expressing this is to say that the Ackermann function can be implemented in FlooP but not in Bloop.

# Answer
> 1 votes
I have an answer by demonstration; here's what x86-64 gcc 4.8.5 has to say on the issue. Here's the C code:

```
int ackermann(int m, int n) {
    if (m == 0) {
        return n + 1;
    }
    else if (m > 0 && n == 0) {
        return ackermann(m - 1, 1);
    }
    else if (m > 0 && n > 0) {
        return ackermann(m - 1, ackermann(m, n - 1));
    }
    return 1;
}
int main() {
    return 0;
}

```

And here's the assembly output:

```
ackermann:
        pushq   %rbp
        movq    %rsp, %rbp
        subq    $16, %rsp
        movl    %edi, -4(%rbp)
        movl    %esi, -8(%rbp)
        cmpl    $0, -4(%rbp)
        jne     .L2
        movl    -8(%rbp), %eax
        addl    $1, %eax
        jmp     .L3
.L2:
        cmpl    $0, -4(%rbp)
        jle     .L4
        cmpl    $0, -8(%rbp)
        jne     .L4
        movl    -4(%rbp), %eax
        subl    $1, %eax
        movl    $1, %esi
        movl    %eax, %edi
        call    ackermann
        jmp     .L3
.L4:
        cmpl    $0, -4(%rbp)
        jle     .L5
        cmpl    $0, -8(%rbp)
        jle     .L5
        movl    -8(%rbp), %eax
        leal    -1(%rax), %edx
        movl    -4(%rbp), %eax
        movl    %edx, %esi
        movl    %eax, %edi
        call    ackermann
        movl    -4(%rbp), %edx
        subl    $1, %edx
        movl    %eax, %esi
        movl    %edx, %edi
        call    ackermann
        jmp     .L3
.L5:
        movl    $1, %eax
.L3:
        leave
        ret
main:
        pushq   %rbp
        movq    %rsp, %rbp
        movl    $0, %eax
        popq    %rbp
        ret

```

A for-loop only compiles to a jump instruction; however, the instructions `movl %eax, %esi`, `movl %edx, %edi`, and `call ackermann` are relevant here. A call may behave like a jump, but it include the movement of parameters too, which a simple jump doesn't have.

---
Tags: computer-architecture, recursion
---


# Question
Title: DBMS: MINIMUM NUMBER OF TABLES REQUIRED TO REALIZE THIS ER MODEL
I was following a discussion on a forum where they have posted a question like this--\>

Some people are saying that we can merge A,B,C in a single table and m:n relation of A and C in another table having foreign key. Thus 2 tables are required. Where as another person is saying that A,B,C cannot be merged as if we merge A,B,C then it means that the A and C sharing the same row must have relation. So we need at-least 3 tables, one for AB another for BC and another one for AC. So which is correct? 2 tables or 3 tables. I am pretty much confused with this.

# Answer
> 1 votes
The issue is that it cannot really be answered unless you give more constraints.

It can be implemented using only one table. Ugly but doable. Each record would be the union o fields needed plus one “type” field. There will be very little of help from the database in keeping referential integritet.

---
Tags: databases
---


# Question
Title: I came up with a way to modify Dijkstra's Algorithm to handle graphs with negative edge weighs
1. Add a constant $c\geq |w\_{min}|$ to each edge of $G$, so that each edge now has non-negative weight.
2. Run Dijkstra's algorithm

Can anyone tell me if this is viable or if it fails?

# Answer
I'm afraid that this idea does not work (and I actually post this question as homework to my students, the reason being that at first glance it looks sound and complete).

Let $G(V, E)$ denote a graph with a cost function $c:e\in E\mapsto Z$, i.e., both positive and negative whole numbers, and no negative cycles. Let us assume there is an edge $e\langle v\_i, v\_j\rangle$ with a negative cost, i.e., $c(e\_{ij}) \<0$, so that $w\_{min}=c(e\_{ij})$.

Let $G'(V, E)$ denote a graph where the cost of each edge is now $c'(e\_{ij})=c(e\_{ij}) + w\_{min}, \forall v\_i, v\_j\in V$. Certainly, there are no negative edge costs in $G'$.

Running Dijkstra on $G'$ to find the shortest path between two arbitrary vertices $s$ and $t$ would return a path $\pi:\langle s=v\_0, v\_1, v\_2, ..., v\_n=t\rangle$ with a cost equal to $\sum\_{i=0}^{n-1}c'(e\_{i, i+1})=\sum\_{i=0}^{n-1}\left(c(e\_{i,i+1})+w\_{min}\right)=n\times w\_{min}+\left(\sum\_{i=0}^{n-1}c(e\_{i, i+1})\right)$ ---please note the usage of $c'$ and $c$ in these expressions. In other words, the overall cost of paths in $G'$ penalizes larger paths by the constant $w\_{min}$ and in the end, it might very easily return a different path.

It does not matter whether you correct now the cost of the path returned by running Dijkstra in $G'$, as it might be simply different.

Hope this helps,
> 2 votes

---
Tags: algorithms, graphs, weighted-graphs
---


# Question
Title: Does a Turing machine really need an infinite tape
Turing machines are usually described as having an infinite tape (i.e. a tape with infinitely many memory locations), but I think it only needs to have a tape that has a sufficient but finite number of memory locations for the problem it's working on, (although, of course, it is unknown in advance how many locations will be needed.) Am I right?

Alternative question: if and when a Turing machine halts, has it only used a finite portion of its tape?

# Answer
The answer to your alternative question is "yes". A Turing machine that halts, halts in a finite number of steps, and it can only move the head a finite distance from the starting position in a finite number of steps.

However, a Turing machine need not halt and may use up an ever growing number of tape positions as it executes. Further, we cannot in general tell how much tape a Turing machine will need to execute correctly.

Sometimes people speak of needing an "unbounded" or "ever extendable" tape rather than an "infinite" tape. About the only significance to this difference in wording is that the former wording makes it a bit clearer that the notion of a Turing machine should not be problematic to a finitist (though perhaps still for an ultrafinitist).
> 4 votes

# Answer
The answer to your first question is "no": a finite amount of tape may not be enough. At the same time, the answer to your alternative question is "yes": once it finishes, a Turing machine has never used more than a finite amount of tape.

The fundamental issue is that in general, it's impossible to tell in advance how much, or whether it will finish in the first place.

Do Turing machines contain an infinite tape? I would say the answer to that question is "no".

Reason one: a Turing machine doesn't contain any tape, it *uses* tape. You can see this in its mathematical definition, which doesn't contain any tape or tape contents. The definition doesn't imply anything about how or when the tape it uses is supplied. It makes no difference to the Turing machine.

Reason two: a Turing machine never uses more than a finite amount of tape, in the sense that at any point during its computation, it can never have used more tape cells than it has made computational steps. However, at the same time, a Turing machine may use an infinite amount of tape, in the sense that there may be no bound on the amount of tape it will eventually use. Therefore, if you should start with a given, finite amount of tape for it to use, no matter how much you supply, it may not be enough: you may need to extend it on the fly, and you may need to do that infinitely often.

Therefore, only if we think of the tape as pre-supplied with the Turing machine (which we don't need to do), the only choice we have is to supply an infinite tape (which is clearly impossible).

When Turing invented his Turing machine, a computer was a woman making calculations on pieces of scrap paper. The nature of computation is such that there is no fixed limit on the amount of scrap paper (or tape) a computation may require. Nobody would ever say that a human computer is a woman (or man) containing an infinite amount of scrap paper, and therefore cannot really exist. Then why do I keep reading that Turing machines contain an infinite tape, and therefore cannot exist? It is wrong, or at least misleading: I've seen misunderstandings arise as a result. Therefore, I would prefer if courses on Turing machines would stop saying it.
> 0 votes

# Answer
Couldn't we say "a tape of indeterminately many cells," or "an indeterminately long finite tape"? I know it's wordier, but it might be clearer?
> 0 votes

---
Tags: turing-machines
---


# Question
Title: Runtime-Analysis for single loop incremented by a factor of 3
So, I'm trying to understand how to get the run time of this loop:

```
for(int i = 1; i < n*n*n; i*=3) {...}

```

So, far I know:

* loop starts at 1
* finishes when $i \> n^3-1$
* that $i$ is multiplied by 3 each iteration.

Intuitively it seems like as $n$ gets larger the number of iterations decreases which makes me think that the run-time is $O(log$ $n)$. My question is if this is correct if it is what is a mathematical way I could derive that answer?

# Answer
> 1 votes
That's right. This for loop stops when: $$ 3^i \< n^3 \rightarrow i\<3\log(n) $$ Which implies the complexity of this for loop is $O(\log(n))$.

---
Tags: runtime-analysis, loops
---


# Question
Title: Types and Programming Languages - proof for theorem about principles of induction of terms
Types and Programming Languages book introduces a theorem about principles of induction on term (p. 31, theorem 3.3.4):

> Suppose P is a predicate on terms.
>
> Induction on depth:
>
> If, for each term s, given P (r) for all r such that depth(r) \< depth(s) we can show P(s), then P(s) holds for all s.

Proof of this theorem is left as the exercise for the reader. The solution to the exercise given in the book hints at defining a new predicate *Q(n)* on natural numbers such as:

> ∀s with depth(s) = n. P(s)

and apply the principle of complete induction on natural number (p. 19, axiom 2.4.2):

> If, for each natural number n, given P(i) for all i \< n we can show P(n), then P(n) holds for all n.

Since I lack experience in writing mathematical proofs, I'm struggling with applying the hint from the book and proving that theorem.

Given that:

* n = i + 1
* for all natural numbers i less than i + 1, the predicate *Q(i)* holds (from the induction axiom)

How do I prove that *Q(n)* (or *Q(i + 1)*) is true? Should I use *depth* function definition introduced previously for the simple arithmetic language?

# Answer
While you should get in the habit of providing definitions so your question is self-contained, especially when the original text is not easily accessible, the first thing to note is that the theorem doesn't actually depend at all on what "terms" are or how "depth" is defined.

Given *any* set $S$ and *any* function $f:S\to\mathbb N$, the theorem will hold. That is, $$(\forall s\in S.(\forall r\in S.f(r) \< f(s) \to P(r))\to P(s))\to \forall s\in S.P(S)$$

How useful this theorem is depends on $f$. For example, if $f$ is a constant function then this theorem simplifies to $(\forall s\in S.P(s))\to(\forall s\in S.P(s))$ which isn't very useful.

To prove this via complete induction, you should, as is always a helpful strategy, write out the definitions, in this case, of complete induction. Complete induction states: $$(\forall n\in\mathbb N.(\forall m\in\mathbb N.m \< n\to Q(m))\to Q(n))\to\forall n\in\mathbb N.Q(n)$$

So the bulk of the task is choosing an appropriate $Q$ to get the result that you want. As the hint states, the fairly obvious choice is $Q(n)\equiv\forall s\in S.f(s)=n\to P(s)$. If you stick this $Q$ into the formula for complete induction, you can simplify it into the first formula. All the work comes down basically to showing that $\forall n\in\mathbb N.\forall s\in S.f(s)=n\to P(s)\iff\forall s\in S.P(s)$ which is a simple and purely logical exercise. Indeed, we don't even need the fact that $\mathbb N$ is the naturals to prove this lemma, though we do need that fact to apply complete induction for the theorem overall.
> 2 votes

---
Tags: type-theory, types-and-programming-languages
---


title: Is inverse CNF polynomial?

text:
# Question
Title: Is inverse CNF polynomial?
Suppose we are given a CNF formula $F$ with $n$ variables and $m$ clauses. The question is whether we can represent $\lnot F$ as a CNF formula with the number of clauses polynomial in $n$ and $m$?

# Answer
No, not necessarily.

If $F$ is $(\neg X\_1 \lor \neg Y\_1) \land \dots \land (\neg X\_n \lor \neg Y\_n)$, then expressing $\neg F$ in CNF requires exponentially $2^n$ clauses. See, e.g., https://en.wikipedia.org/wiki/Conjunctive\_normal\_form#Conversion\_into\_CNF, Which CNF boolean formulas blow up exponentially at conversion to DNF?, and Formulas for which any equivalent CNF formula has exponential length.

However, if you allow introducing additional variables, then you can construct a formula $G$ that is equisatisfiable with $\neg F$ and such that $G$ can be represented in CNF with number of variables and clauses polynomial in $n$ and $m$.
> 1 votes

---
Tags: satisfiability
---


# Question
Title: How to check if DFA is actually a correct model of the intended system?
Suppose I have modeled a deterministic finite automaton of my system. How can I check if the traces generated by this system, actually represent the model I had in mind?

For example, say I have DFA A which models a vending machine. To ensure I did not model any wrong transitions, is coming up with (safety/liveness) specifications and performing verification the only method I can follow to ensure my model is correct? Many thanks.

# Answer
> 1 votes
If you want a guarantee, then yes, verification is the only approach. That's pretty much the definition of what verification means.

If you want a heuristic check, there are a number of testing methods based on synthesizing test cases (perhaps based on the DFA) and then checking that the vending machine's actual behavior on those test cases matches your DFA's.

# Answer
> 0 votes
For correctness proofs, you have to use induction. See here, correctness proof of DFA. For safety checking, you can check for words which belong to the language of the DFA and run it to see of it gets accepted. Also, check for words which do not belong to the language of the DFA and make sure they get rejected.

---
Tags: automata, finite-automata, software-verification
---


# Question
Title: Why is Dijkstra's Algorithm more popular compared to Grassfire algorithm?
Consider algorithms to find shortest paths in a graph. The grassfire algorithm has a complexity of `O(|V|)` where `V` is the number of nodes or vertices. The Dijkstra's algorithm has a complexity of `O((|V| + |E|) * log(|V|))` where `E` is the number of edges. Compared to A star, the Dijkstra's does not rely on properties of any heuristic which makes them popular. But I am trying to understand the advantage of Dijkstra's over Grassfire. Are there practical reasons why this is the case? Or am I simply seeing more cases of Dijkstra's compared to Grassfire due to the application areas such as navigation that I am working on?

# Answer
> 3 votes
In grassfire the distances are constant. All of your neighbors have equal length. In a weighted graph, grassfire will fail.

Graphfire is actually based on a small modification of BFS.

The Dijsktra works on weighted graphs, too.

**Note:** If all costs are equal, Dijkstra = BFS

Know the difference, and use them according to your need.

# Answer
> 1 votes
The Grassfire algorithm only works on a particular kind of graph; Dijkstra's algorithm works on any graph.

---
Tags: algorithms, graphs, time-complexity, shortest-path, greedy-algorithms
---


title: Non-Boolean SAT

text:
# Question
Title: Non-Boolean SAT
I was wondering about the complexity of SAT tests with variables $x\_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x\_i = a \implies x\_j \neq b$. When $n=2$, we have 2SAT, which has linear time algorithms. Meanwhile, if $n \> 2$, then if we can almost convert it to 2SAT by having Boolean variables $x\_{i,a}$ corresponding to the statement $x\_i = a$, however this allows for $x\_{i,1}=x\_{i,2}= \dots = x\_{i,n}=0$, which would leave $x\_i$ unassigned.

# Answer
> 1 votes
Your problem is NP-complete, even when the range of the $x\_i$ has size 3.

Consider a 3SAT instance with $m$ clauses. We will construct an instance of your problem with $m$ variables $x\_1,\ldots,x\_m$. The value of $x\_i$ will denote the literal satisfied in the $i$th clause. Correspondingly, if the $a$th literal in the $i$th clause is the negation of the $b$th literal in the $j$th clause then we will have the constraint $x\_i \neq a \lor x\_j \neq b$. This gives $O(m^2)$ constraints.

Given a satisfying assignment of the new instance, we can decode a satisfying assignment for the original one by reading the values of the satisfied literals in all clauses. By construction, each original variable is assigned at most one value in this way. Conversely, if the original instance is satisfiable, then a satisfying assignment naturally leads to a satisfying assignment to the new instance.

---
Tags: algorithms, propositional-logic, constraint-satisfaction, sat-solvers
---