# Question
Title: Research on evaluating the performance of cache-obliviousness in practice
Cache-oblivious algorithms and data structures are a rather new thing, introduced by Frigo et al. in Cache-oblivious algorithms, 1999. Prokop's thesis from the same year introduces the early ideas as well.

The paper by Frigo et al. present some experimental results showing the potential of the theory and of the cache-oblivious algorithms and data structures. Many cache-oblivious data structures are based on static search trees. Methods of storing and navigating these trees have been developed quite a bit, perhaps most notably by Bender et al. and also by Brodal et al. Demaine gives a nice overview.

The experimental work of investigating the cache behaviour in practice was done at least by Ladner et al. in A Comparison of Cache Aware and Cache Oblivious Static Search Trees Using Program Instrumentation, 2002. Ladner et al. benchmarked the cache behaviour of algorithms solving the binary search problem, using the classic algorithm, cache-oblivious algorithm and cache-aware algorithm. Each algorithm was benchmarked with both implicit and explicit navigation methods. In addition to this, the thesis by Rønn, 2003 analyzed the same algorithms to quite high detail and also performed even more thorough testing of the same algorithms as Ladner et al.

**My question is**

> Has there been any newer research on *benchmarking* the cache behaviour of cache-oblivious algorithms in *practice* since? I'm especially interested in the performance of the static search trees, but I would also be happy with any other cache-oblivious algorithms and data structures.

# Answer
You've already covered background research on cache-oblivious algorithms quite well. In terms of benchmarking and practical results, I see this recent paper by Intel as an interesting read:

A Synergetic Approach to Throughput Computing on x86-based Multicore Desktops
> 5 votes

---
Tags: algorithms, data-structures, computer-architecture, reference-request, cpu-cache
---


title: Error-correcting rate is misleading

text:
# Question
Title: Error-correcting rate is misleading
In coding theory, 'how good a code is' means how many channel errors can be corrected, or better put, the maximal noise level that the code can deal with.

In order to get better codes, the codes are designed using a large alphabet (rather than binary one). And then, the code is good if it can deal with a large rate of erroneous "symbols".

**Why isn't this consider cheating?** I mean, shouldn't we only care about what happens when we "translate" each symbol into a binary string? The "rate of bit error" is different than the rate of "symbol error". For instance, the rate of bit-error cannot go above 1/2 while (if I understand this correctly), with large enough alphabet, the symbol-error can go up to $1-\epsilon$. Is this because we *artificially* restrict the channel to change only "symbols" rather than bits, or is it because the code is actually better?

# Answer
> 7 votes
Many widely used codes for binary data are concatenated codes, which are composed by using two error-correcting codes. The *inner code* is over a binary alphabet, and the *outer code* is over an alphabet whose symbols correspond to the codewords of the inner code. This allows you to use the superior power of larger alphabet sizes to encode binary messages without "cheating".

The standard definition of minimum distance is a natural one to use when considering concatenated codes, as well as in the theory of codes over large alphabet sizes. It would only be "cheating" if you used these numbers to compare a binary code with a large-alphabet code that encodes binary input without using an inner code as well; coding theorists are clever enough not to do this (and I believe that since concatenated codes were invented, large-alphabet codes have often been used along with an inner code, but large-alphabet codes are also very good for correcting error in bursty channels such as CDs, since a large number of consecutive bit errors will only affect a few "symbols").

---
Tags: information-theory, coding-theory
---


# Question
Title: Could quantum computing eventually be used to make modern day hashing trivial to break?
Simply put, if one were to build a quantum computing device with the power of, say, 20 qubits, could such a computer be used to make any kind of modern hashing algorithm useless?

Would it even be possible to harness the power of quantum computing in a traditional computing application?

# Answer
> 13 votes
Quantum computers might have some advantage over classical computers for some cases. The most remarkable example is Shor's Algorithm which can factor a large number in polynomial time (while classically, the best known algorithm takes exponential time). This completely breaks schemes like RSA, based on the hardness of factorization.

This is not necessarily the case for hash functions. First, we need to define what it means to break a hash function. One way to break it is called *pre-image attack*: you give me hash value $v$, and I need to find a message $m$ such that $\operatorname{hash}(m)=v$. Another attack is the *collision attack*, in which you give me nothing, and I need to come up with two different messages $m\_1, m\_2$ that have the same hash $\operatorname{hash}(m\_1)=\operatorname{hash}(m\_2)$. This is easier than finding a preimage, since I'm not bound to the a specific $v$.

What can Quantum computers do? The main result is Grover's search algorithm: a method for a quantum computer to search in an unsorted database of size $N$ with time $O(\sqrt{N})$ (while classically it will take an expected time of $N/2$).

With Grover's algorithm, finding a preimage of a hash function whose output is $k$-bits takes $O(2^{k/2})$ time, rather than $O(2^k)$.

*Is this a problem*? Not necessarily. Hash functions are **designed** such that time $2^{k/2}$ is considered "safe" (in other words, the hash designers always double $k$). This is due to the Birthday paradox with which finding a *collision* is possible with time $O(2^{k/2})$ by a classical computer.

The nice thing about Grover's algorithm that it is optimal - every other quantum-algorithm to find an element in an unsorted database will run in time $\Omega(\sqrt{N})$.

*Can quantum-computers perform better collision attacks*? Actually I'm not sure about it. Grover's algorithm can be extended, such that if there are $t$ items (that is, preimages), the time to find one is reduced to $O(\sqrt{N/t})$. But this gives no collision - running the algorithm again might return the same preimage. On the other hand, if we choose $m\_1$ at random, and then use Grover's Algorithm, it is probable that it will return a different message. I'm not sure if this gives better attacks.

<sub>(this answers the more general question, without restricting the computer to 20 qubits, which will not be enough to break the current 1024-bit hashes).</sub>

# Answer
> 1 votes
From what I understand, quantum computing does have the power to easily break today's hashing algorithms. However, in the long run we will also be able to use more complex hashing algorithms, and generally it is easier to encrypt than decrypt something. I think the biggest issues to consider are when quantum computing is available only to a select few, giving them easy access to stuff protected by today's algorithms long before more advanced algorithms or even consciousness of the threat are widespread.

See here for an actually technical answer to the question on Stack Overflow.

---
Tags: cryptography, quantum-computing, hash
---


# Question
Title: Does every large enough string have repeats?
Let $\Sigma$ be some finite set of characters of fixed size. Let $\alpha$ be some string over $\Sigma$. We say that a nonempty substring $\beta$ of $\alpha$ is a *repeat* if $\beta = \gamma \gamma$ for some string $\gamma$.

Now, my question is whether the following holds:

> For every $\Sigma$, there exists some $n \in \mathbb{N}$ such that for every string $\alpha$ over $\Sigma$ of length at least $n$, $\alpha$ contains at least one repeat.

I've checked this over the binary alphabet, and this is quite easy for that case, but an alphabet of size 3 is already quite a bit harder to check, amd I'd like a proof for arbitrarily large grammars.

If the above conjecture is true, then I can (almost) remove the demand for inserting empty strings in my other question.

# Answer
> 16 votes
No, unfortunately not. There are even infinite *square-free* words if your alphabet has at least three symbols.

This apparently natural border (two-element alphabets have only finitely many square-free words) is observed in many places, for instance:

* $\\{xyyz \mid x,y,z\in \Sigma^+\\}$ is co-finite for $|\Sigma|\leq 2$ but not context-free for $\Sigma\>2$.
* The class of languages generated by terminal-free patterns can be learned in the limit if $|\Sigma|\>3$ but not so if $|\Sigma|=2$ \[Reid2004\].

---
Tags: combinatorics, strings, word-combinatorics
---


# Question
Title: Are two elements always in a relation within a partially ordered set?
In a partially ordered set, am I always able to order two arbitrary elements out of the set? Or is it possible that two elements within the set have no order relation to each other?

For example if there are three elements $\\{a, b, c\\}$ and $a \leq b$ and $a \leq c$, does either $b \leq c$ or $c \leq b$ have to hold?

I need this to understand the fixed point theory for semantics of programming languages (denotation of while loops).

# Answer
In a partially ordered set, there may be members which are not comparable. A partial order where all elements are comparable is called a total order.

We say $a$ and $b$ are comparable when at least one of the following holds:

* $a\leq b$,
* $b \leq a$.
> 8 votes

# Answer
In a partially ordered set (poset for short), you can have $a \le b$ and $a \le c$ without $b$ and $c$ being comparable (i.e. neither $b \le c$ nor $c \le b$ holds). That's what makes it a partial order and not a total order. Mathematicians often mean a total order when say “order”, because the primary example of an ordered set is the real numbers (or subsets such as the natural integers); computer scientists use more partial orders at an elementary level, so in CS, assume partial unless told total.

A typical example of poset is set inclusion: $\\{x\\} \subset \\{x,y\\}$ and $\\{x\\} \subset \\{x,z\\}$, but neither of $\\{x,y\\}$ and $\\{x,z\\}$ is a subset of the other.

Posets often arise in denotational semantics to represent an amount of knowledge about a program. $a \le b$ means that $b$ is a better approximation of the behavior of the program than $a$. For example, if $a$ is “the program is a function from the integers that terminates for all inputs”, $b$ is “the program calculates the successor function” and $c$ is “the program calculates the double function”, then $a \le b$ and $a \le c$ but $b$ and $c$ are not comparable.
> 7 votes

---
Tags: terminology, discrete-mathematics, order-theory
---


title: Error in the use of asymptotic notation

text:
# Question
Title: Error in the use of asymptotic notation
I'm trying to understand what is wrong with the following proof of the following recurrence

$$ T(n) = 2\\,T\\!\left(\left\lfloor\frac{n}{2}\right\rfloor\right)+n $$ $$ T(n) \leq 2\left(c\left\lfloor\frac{n}{2}\right\rfloor\right)+n \leq cn+n = n(c+1) =O(n) $$

The documentation says it's wrong because of the inductive hypothesis that $$ T(n) \leq cn $$ What Am I missing?

# Answer
Let's say the final goal is to prove $T(n) = \mathcal{O}(n)$. You start with the induction hypothesis:

$T(i) \leq ci$ for all $i \< n$.

And to complete the proof, you have to show that $T(n) \leq cn$ as well.

However, what you're able to deduce is $T(n) \leq (c+1)n$, which is not helpful to complete the proof; you need *one* constant $c$ for (almost) all $n$. Therefore, we cannot conclude anything and $T(n) = \mathcal{O}(n)$ isn't proved.

Notice that you are confused between the result and the proof process. And one more point, $T(n)$ is actually $\Theta(n \log n)$ in this case so you may consider an appropriate induction hypothesis to be able to prove it.
> 12 votes

# Answer
You've omitted a few steps. It looks like you're attempting to prove by induction that $T(n) = O(n)$, and your proof goes:

> Suppose $T(k) = O(k)$ for $k\<n$. This means $T(k) \le c \\, k$ for some $c$. Then $T(n) = 2 T(\lfloor n/2\rfloor) + n \le 2 c \lfloor n/2\rfloor + n\le (c+1) \\,n$, so $T(n) = O(n)$.

This proof goes wrong right from the start: “$T(k) = O(k)$ for $k \lt n$” does not make sense. Big oh is an asymptotic notion: $T(k) = O(k)$ means that there is some constant $c$ *and a threshold N* such that $\forall k \ge N, T(k) \le c \\, k$. And again at the end, you can't conclude that “$T(n)=O(n)$”, because that says something about the function $T$ as a whole and you've only proved something about the particular value $T(n)$.

You need to be explicit about what $O$ means. So maybe your proof goes:

> Suppose that $T(k) \le c \\, k$ for all $k \< n$. Then $T(n) = 2 T(\lfloor n/2\rfloor) + n \le 2 c \lfloor n/2\rfloor + n\le (c+1) \\,n$.

This does not prove an inductive step: you started from $T(k) \le c \\, k$, and you proved that for $k=n$, $T(k) \le (c+1) \\, k$. This is a weaker bound. Look at what this means: $T(k) \le c \\, k$ means that $c$ is a bound for the rate of growth of $T$. But you have a rate $c$ that grows when $k$ grows. That's not a linear growth!

If you look closely, you'll notice that the rate $c$ grows by $1$ whenever $k$ doubles. So, informally, if $m=2^p k$ then $c\_m = c\_k + p$; in other words, $c\_k = c\_0 \log\_{2} k$.

This can be made precise. Prove by induction that for $k \ge 1$, $T(k) \le c \log\_2(k)$.

The recurrence relation is typical for divide-and-conquer algorithms that split the data in two equal parts in linear time. Such algorithms operate in $\Theta(n\\,\mathrm{log}(n))$ time (not $O(n)$).

To see what the expected result is, you can check the recurrence relation against the master theorem. The division is $2T(n/2)$ and the extra work done is $n$; $\log\_2(2) = 1$ so this is the second case for which the growth is $\Theta(n\\,\log(n))$.
> 8 votes

# Answer
I'm extending the answer already given, perhaps only by explaining my comment in more detail.

As guessing can clearly be difficult and tedious, sometimes better methods exist. One such method is the Master Theorem. Our recurrence is now of the form $T(n) = a T(n/b) + f(n)$, where $a \geq 1$ and $b \> 1$ are constants and $f(n)$ a function. Note that in our case $\lfloor n/2 \rfloor$ can be interpreted to mean $n/2$. To be technically exact, our recurrence might not be well-defined because $n/2$ might not be an integer. However, this is allowed since it will not affect the asymptotic behaviour of the recurrence. Therefore, we often find it convenient to drop floors and ceilings. The formal proof of this is a bit tedious, but the interested reader can find it for example from the Cormen et al. book.

In our case, we have $a = 2$, $b = 2$, $f(n) = \Theta(n)$. This means that we have $n^{\log\_b a} = n^{\log\_2 2} = n$. The second case of the Master theorem applies since $f(n) = \Theta (n)$, and we have the solution $T(n) = \Theta (n \log n)$.
> 7 votes

---
Tags: algorithms, landau-notation, asymptotics, recurrence-relation
---


# Question
Title: Understanding $\text{handle}$ in parsing problem
*Originally https://math.stackexchange.com/questions/22614/help-understand-texthandle-in-parsing-problem but unaswered there*

The BNF is defined as followed:

```
S -> aAb | bBA
A -> ab | aAB
B -> bB | b

```

The sentence is:

```
aaAbBb

```

And this is the parse tree:

**Phrases:** aaAbBb, aAbB, bB
**Simple Phrases:** bB
**Handle:** ?

From the book, `handle` is defined as followed: `B` is the handle of the right sentential from $y = aBw$ if and only if:
$S \to\_{rm} \cdot aAw \to\_{rm} aBw$

So in my case, what's the handle? Any idea?

# Answer
I'll assume you talk about the 'handle' as often defined in the context of LR-parsing. I'm not entirely sure if the definition you use is the proper definition: $A$ and $B$ seem to stand for nonterminals, but $B$ should really stand for some string of terminals and nonterminals (as the right hand side of a production of $A$, to be precise) to have a proper meaning.

Let's parse your example using LR machinery, and illustrate what happens. In particular, we'll find multiple handles during the parse. The dot '$\bullet$' will show where in the parse we are at the moment. We're looking for suffixes of the part to the left of the bullet that exactly match productions of our grammar.

* $\bullet aaAbBb$ - we're starting at the beginning.
* $a \bullet aAbBb$ - moving on, '$a$' is not a handle as it is not a production.
* $aa \bullet AbBb$ - moving on, '$aa$' or '$a$' is not a handle as it is not a production.
* $aaA \bullet bBb$ - '$A$', '$aA$' and '$aaA$' are not productions.
* $aaAb \bullet Bb$ - '$b$' and '$aAb$' are candidate handles (they are right-hand sides of productions), but your parse tree shows that neither gets reduced, so we ignore them.
* $aaAbB \bullet b$ - '$bB$' is a handle! We reduce it to $B$.
* $aaAB \bullet b$ - '$aAB$' is a handle! We reduce it to $A$.
* $aA \bullet b$ - '$A$' and '$aA$' are not productions.
* $aAb \bullet$ - '$aAb$' is a handle! We reduce it to $S$.
* $S \bullet$ - Oh hey, we're done: the input was part of the grammar.
> 4 votes

# Answer
We talk about **handles** when we talk about **bottom-up parsing**. Bottom-up parsing during a left-to-right scan of the input constructs a rightmost derivation in reverse. Informally, a **handle** is a substring that matches the body of a production, and whose reduction represents one step along the reverse of a rightmost derivation.

In other words, **handles** are substrings of sentential forms:

1. A substring that matches the right hand side of a production
2. Reduction using that rule can lead to the start symbol
3. The rule forms one step in a rightmost derivation of the string

The most common bottom-up parsers are the shift-reduce parsers. These parsers examine the input symbols and either shift (push) them onto a stack or reduce elements at the top of the stack, replacing a right-hand side by a left-hand side. A shift-reduce parser is most commonly implemented using a stack, where we proceed as follows:

* start with an empty stack
* a "shift" action corresponds to pushing the current input symbol onto the stack
* a "reduce" action occurs when we have a **handle** on top of the stack. To perform the reduction, we pop the **handle** off the stack and replace it with the nonterminal on the LHS of the corresponding rule.
> 3 votes

# Answer
As stated in the comments of the original question, This "handle" means the left-most variable in left-most derivation according to the definition which is 'B' in this case. It means from which variable you should start simplifying a sentence of the grammar.
> 1 votes

---
Tags: formal-languages, compilers, parsers
---


# Question
Title: Fine-grained security models for XML data
Access control models are typically very coarse-grained, allowing one access to a resource (possibly with some combination of read/write/execute permission) or exclude such access. Some models of database security allow access to be granted on a per row basis (though I don't have a reference handy).

Have fine-grained access control models been designed to limit access to *parts of* an XML document? What could/should a model look like? Has any work been done in this area? Are other security models applicable in this context?

For example, one could imagine that the model prevents access to a particular subtree. The subtree could either be removed or encrypted.

*Note that this need not explicitly apply to XML. Any models devised for semi-structured data are also interesting.*

# Answer
The conversion between SQL access control policies and XML-specific access control models has been studied in:

"Preserving SQL Access Control Policies Over Published XML Data" by G. Leighton (2009)

According to the author:

*... To the best of our knowledge, our work represents the first attempt to formulate an SQL-to-XML access control policy translation framework, capable of expressing the entirety of the SQL access control model, and carrying the semantics of the original ACP over to the chosen XML ACP formulation language. ...*
> 5 votes

# Answer
*I'm no expert on access control for structured data. This is a 10000-foot view. Don't assume a correlation between what my answer covers, what is scientifically interesting and what is significant in terms of deployment.*

Take any access control or permission mechanism and slap some angle braces around it, and you have an XML access control mechanism. It's been done a lot, but it looks like each effort has had little visibility outside the community it originated in.

XACML is a standard (that some people actually use) for specifying access control policies. Some of these policies control data access. I believe the model it uses for actors (PAP, PDP, PEP, PIP) is common in distributed access control systems (for managing data access and otherwise).

XACL (not to be confused with XACL or XACML) is a rich model for access control over elements or subtrees, allowing redaction, encryption and other transformations of content as well as logging.

There's a 2006 survey by Mark J. Estlund. It covers both XML for access control and access control of XML. It's nowhere near complete.

*Access Control in Data Management Systems* by Elen Ferrari (2010) has a section on XML.
> 4 votes

---
Tags: security, access-control, structured-data
---


title: How does Stack Inspection work?

text:
# Question
Title: How does Stack Inspection work?
*This is precursor to my other, more advanced question about Stack Inspection.*

Stack Inspection is a security mechanism introduced in the JVM to deal with running code originating from locations having different levels of trust. This is question aims at finding a simple description of its functionality. So:

> How does stack inspection work?

# Answer
See

From the paper:

... The stack inspection algorithm used in current Java systems can be thought of as a generalization of the following **simple stack inspection** model:

In this model, the only principals are “system” and “untrusted”. Likewise, the only privilege available is “full.” This model resembles the stack inspection system used internally in Netscape Navigator 3.0.

In this model, every stack frame is labeled with a principal (“system” if the frame is executing code that is part of the virtual machine or its built-in libraries, and “untrusted” otherwise), and contains a privilege flag which may be set by a system class which chooses to “enable its privileges,” explicitly stating that it wants to do something dangerous. An untrusted class cannot set its privilege flag. When a stack frame exits, its privilege flag (if any) automatically disappears.

All procedures about to perform a dangerous operation such as accessing the file system or network first apply a stack inspection algorithm to decide whether access is allowed. The stack inspection algorithmsearches the frames on the caller’s stack in sequence, from newest to oldest. The search terminates, allowing access, upon finding a stack frame with a privilege flag. The search also terminates, forbidding access and throwing an exception, upon finding an untrusted stack frame (which could never have gotten a privilege flag). ...
> 7 votes

---
Tags: terminology, security, stack-inspection
---


# Question
Title: Is there an abstract machine that can capture power consumption?
When reporting algorithmic complexity of an algorithm, one assumes the underlying computations are performed on some abstract machine (e.g. RAM) that approximates a modern CPU. Such models allow us to report time and space complexity of algorithms. Now, with the spread out of GPGPUs, one wonders whether there are well known models where one can take into account power consumption as well.

GPUs are well known to consume considerable amount of power and certain instructions fall into different categories of power consumption based on their complexity and location on the sophisticated chip. Hence instructions, from an energy of view, are not of unit (or even fixed) cost. A trivial extension would be assigning weights to operation cost, but I'm looking for a powerful model where an operation/instruction might cost *non-constant* units of energy, e.g. polynomial amount (or even more complex e.g.: function of time elapsed since start of the algorithm; or taking into account probability of failure of cooling system, which will heat up the chips, and slow down the clock frequency etc.)

Are there such models where non-trivial costs and faults can be incorporated?

# Answer
There isn't an established model yet, but this is an area of active research right now. One of the experts on the algorithms side of things is Kirk Pruhs. His papers have more information, and you can also browse this presentation.
> 8 votes

# Answer
**Models for energy consumption**

Speed scaling is one of the most used model (recently) when considering energy consumption. It consists in modifying the supply voltage. By lowering supply voltage, or processor clock frequency, it is possible to achieve important reductions in power consumption; faster speeds allow for a faster execution, but they also lead to a much higher (supra-linear) power consumption.

More precisely, a processor running at speed $s$ dissipates $s^3$ watts per unit of time, hence it consumes $s^3 \times d$ joules when operated during $d$ units of time.

However speed scaling is not the only energy considered. It is what is called the *dynamic* energy. The *static* energy is the power that is due to the processor being 'on'. It is possible to get rid of this *static* power by shutting down the processor during idle time. However it has a cost. There has been a lot of work done on this subject which is very close to the ski rental problem.

Usually the energy consumption is the sum of the static and dynamic power consumption times the execution time. However, most paper focus on either one of these problems.

**Introducing faults in this model**

I think this is the most surprising part of the speed-scaling model. Usually one would think that the faster you execute a task, the more likely you are to fail the execution. On the contrary, it was shown that reducing the speed of a processor increases the number of transient fault rates of the system; the probability of failures increases exponentially, and this probability cannot be neglected in large-scale computing.

Intuitively, there is the fact that the more time you spend on a task the more chances you have to fail during the execution of that task. However there is more than that: Shatz and Wang in this, stated that the fault-model followed a Poisson distribution. The parameter $\lambda$ of the Poisson distribution is then:\ $$ \lambda(f)=\lambda\_0 e^{d\frac{fmax-f}{fmax-fmin}}, $$ where $f$ is the processing speed comprised in $\[fmin,fmax\]$, and $\lambda\_0$ and $d$ are constant dependent on the systyem. If you consider a task of weight $w$, executed at speed $f$, the reliability of the execution for that task is $R(f)=e^{-\lambda(f)\times\frac{w}{f}}$.

This is self reference so I do not know if it is appreciated here, however if you are interested, you can find more information in this paper on the *dynamic* part of the energy consumption.
> 7 votes

# Answer
There have been attempts to analyse energy consumption of algorithms in theory (using real-life costs per operation, of course); see e.g. \[1\]. While the results are surprising enough---the fastest algorithm is not always the one using the least energy---some obstacles remain.

In particular, modern platforms switch off certain features so that operation energy cost spikes when they are turned on again. While in principle possible to incorporate in rigorous analysis, it becomes technically (too?) hard. Also, the effect of cache misses on total energy consumption has not been studied well.

It appears that huge differences between platforms oppose rigorous analyses which can (for once) not ignore specifics because general models (i.e. before plugging in concrete constants/functions) have limited significance.

---

1. Hannah Bayer and Markus E. Nebel: *Evaluating Algorithms according to their Energy Consumption*, Computability in Europe, 2009
> 3 votes

---
Tags: complexity-theory, computer-architecture, power-consumption, machine-models
---


title: Limitations of Stack Inspection

text:
# Question
Title: Limitations of Stack Inspection
*This is a follow up to the How does Stack Inspection work? that explores the notion in more detail*

Stack inspection is a mechanism for ensuring security in the context of the JVM and CLR virtual machines when externally downloaded code modules of different levels of trust may be running together. That system libraries need some way of distinguishing between calls originating in untrusted code and calls originating from the trusted application itself. This is done by associating with code the principal corresponding to its origin. Then access permissions are recorded on the stack and whenever a call to a sensitive, system method is made, the stack is traversed to see whether the appropriate permissions for the principal making the call are present on the stack.

> What are the limitations of stack inspection? What mechanisms have been proposed to replace it? Have any significant changes been made to the model since it was introduced in the late 90s?

# Answer
Stack inspection is necessary because programs on the JVM and CLR have default access to dangerous operations, so something must be done to prevent disasters. For example an untrusted program can reference an I/O library and call it:

```
using IO;
...
IO.DeleteFile("/home/foo/bla");

```

So on each dangerous operation made, we need to check whether it is allowed. With stack inspection it is generally complicated to understand who gets access to what. It also makes optimizations such as inlining and tail calls difficult.

A superior mechanism is to not give each program automatic access to dangerous operations in the first place. In this model there is no way to import an IO library. The only way to get access to an IO library is if somebody else gave it to you. This is called capability security. An introduction can be found here.

Instead, we would write the previous program like this:

```
Main(IOLibrary IO){
  IO.DeleteFile("/home/foo/bla");
}

```

The IO library is a parameter to the entry point of the program, and this is called a capability (because it gives use some capability, in this case to do IO). To be able to run this program, we must have access to an IO capability ourselves, and run the program by calling `Main(ourIOlibrary)`. If we are running an untrusted program, we simply do not pass our IO library to it, since it might use that library to delete our files. In some cases we want to give an untrusted program limited access to the filesystem. In that case we create a wrapper around our own IO library that only allows access to a certain directory, and pass that one to the untrusted program instead of the full IO library

So if we need an IO capability to invoke a program that needs an IO capability, that also means that whatever invoked our program needed to have access to an IO capability to be able to give it to us. So where did its IO capability come from? Well, eventually there is a point where the human operating the computer invoked a program. This human has access to all the system capabilities, so he was able to pass the IO capability on. If this human does not trust the program he is running, then he simply will not pass his IO capability to it.

You can probably easily imagine other kinds of capabilities: internet access, access to draw stuff on your screen, etc. For example a secure browser plugin system might give a graphics capability to an untrusted plugin that only allows it to paint graphics in a predefined rectangle on the page.
> 6 votes

# Answer
One limitation of stack inspection as traditionally implemented is that it breaks proper tail calls. In particular, typical implementations need to keep the entire "stack" around at all times. Clements and Felleisen show how this problem can be remedied using a technique called "continuation marks" in their paper *A Tail-Recursive Semantics for Stack Inspections* in ESOP 2003.
> 6 votes

---
Tags: security, stack-inspection
---


# Question
Title: Are the Before and After sets for context-free grammars always context-free?
Let $G$ be a context-free grammar. A string of terminals and nonterminals of $G$ is said to be a *sentential form* of $G$ if you can obtain it by applying productions of $G$ zero or more times to the start symbol of $S$. Let $\operatorname{SF}(G)$ be the set of sentential forms of $G$.

Let $\alpha \in \operatorname{SF}(G)$ and let $\beta$ be a substring of $\alpha$ - we call $\beta$ a *fragment* of $\operatorname{SF}(G)$. Now let

$\operatorname{Before}(\beta) = \\{ \gamma \ |\ \exists \delta . \gamma \beta \delta \in \operatorname{SF}(G) \\}$

and

$\operatorname{After}(\beta) = \\{ \delta \ |\ \exists \gamma . \gamma \beta \delta \in \operatorname{SF}(G) \\}$.

> Are $\operatorname{Before}(\beta)$ and $\operatorname{After}(\beta)$ context-free languages? What if $G$ is unambiguous? If $G$ is unambiguous, are $\operatorname{Before}(\beta)$ and $\operatorname{After}(\beta)$ also describable by an unambiguous context-free language?

This is a followup to my earlier question, after an earlier attempt to make my question easier to answer failed. A negative answer will make the encompassing question I'm working on very hard to answer.

# Answer
> 9 votes
Let us get a feeling for $\operatorname{Before}(\beta)$ and $\operatorname{After}(\beta)$ first. Consider a derivation tree which contains $\beta$; "contains" here means that you can cut away subtrees so that $\beta$ is a subword of the tree's front. Then, the before (after) set are all potential fronts of the tree's part left (right) of $\beta$:

<sup>\[source\]</sup>

So we have to build a grammar for the horizontally lined (vertically lined) part of the tree. That seems easy enough as we already have a grammar for the whole tree; we just have to make sure all sentential forms are words (change the alphabets), filter away those that do not contain $\beta$ (that is a regular property as $\beta$ is fixed) and cut away everything after (before) $\beta$, including $\beta$. This cutting should also be possible.

---

Now to a formal proof. We will transform the grammar as outlined and use closure properties of $\mathrm{CFL}$ to do the filtering and cutting, i.e. we perform a non-constructive proof.

Let $G = (N, T, \delta, S)$ a context-free grammar. It is easy to see that $\operatorname{SF}(G)$ is context-free; construct $G'=(N',T',\delta',N\_S)$ like this:

* $N' = \\{N\_A \mid A \in N\\}$
* $T' = N \cup T$
* $\delta' = \\{\alpha(A) \to \alpha(\beta)\mid A\to\beta \in \delta \\} \cup \\{N\_A \to A \mid A\in N\\}$

with $\alpha(t)=t$ for all $t \in T$ and $\alpha(A)=N\_A$ for all $a\in N$. It is clear that $\mathcal{L}(G')=\operatorname{SF}(G)$; therefore the corresponding prefix closure $\operatorname{Pref}(\operatorname{SF}(G))$ and suffix closure $\operatorname{Suff}(\operatorname{SF}(G))$ are context-free, too¹.

Now, for any $\beta \in (N\cup T)^\*$ are $\mathcal{L}(\beta(N\cup T)^\*)$ and $\mathcal{L}((N\cup T)^\*\beta)$ regular languages. As $\mathrm{CFL}$ is closed under intersection and right/left quotient with regular languages, we get

$\qquad \displaystyle \operatorname{Before}(\beta) = (\operatorname{Pref}(\operatorname{SF}(G))\ \cap\ \mathcal{L}((N\cup T)^\*\beta))\\,/\\,\beta \in \mathrm{CFL}$

and

$\qquad \displaystyle \operatorname{After}(\beta) = (\operatorname{Suff}(\operatorname{SF}(G))\ \cap\ \mathcal{L}(\beta(N\cup T)^\*))\\,\backslash\\, \beta \in \mathrm{CFL}$.

---

¹ $\mathrm{CFL}$ is closed under right (and left) quotient; $\operatorname{Pref}(L) = L / \Sigma^\*$ and similar for $\operatorname{Suff}$ yield prefix resp. suffix closure.

# Answer
> 9 votes
Yes, $\mbox{Before}(\beta)$ and $\mbox{After}(\beta)$ are context-free languages. Here's how I would prove it. First, a lemma (which is the crux). If $L$ is CF then:

$\mbox{Before}(L,\beta) = \\{ \gamma \ |\ \exists \delta . \gamma \beta \delta \in L \\}$

and

$\mbox{After}(L,\beta) = \\{ \gamma \ |\ \exists \delta . \delta \beta \gamma \in L \\}$

are CF.

Proof? For $\mbox{Before}(L,\beta)$ construct a non-deterministic finite-state transducer $T\_{\beta}$ that scans a string, outputting every input symbol it sees and simultaneously searches non-deterministically for $\beta$. Whenever $T\_{\beta}$ sees the first symbol of $\beta$ it forks non-deterministically and ceases outputting symbols until either it finishes seeing $\beta$ or it sees sees a symbol that deviates from $\beta$, stopping in either case. If $T\_{\beta}$ sees $\beta$ in full, it accepts upon stopping, which is the only way it accepts. If it sees a deviation from $\beta$, it rejects.

The lemma can be jiggered to handle cases where $\beta$ could overlap with itself (like $abab$ -- keep looking for $\beta$ even while in the midst of scanning for a prior $\beta$) or appears multiple times (actually, the original non-determinisic forking already handles that).

It's fairly clear that $T\_\beta(L) = \mbox{Before}(L,\beta)$, and since the CFLs are closed under finite-state transduction, $\mbox{Before}(L,\beta)$ is therefore CF.

A similar argument goes for $\mbox{After}(L,\beta)$, or it could be done with string reversals from $\mbox{Before}(L,\beta)$ , CFLs also being closed under reversal:

$\mbox{After}(L,\beta) = \mbox{rev}(\mbox{Before}(\mbox{rev}(L),\mbox{rev}(\beta)))$

Actually, now that I see the reversal argument, it would be even easier to start with $\mbox{After}(L,\beta)$, since the transducer for that is simpler to describe and verify -- it outputs the empty string while looking for a $\beta$. When it finds $\beta$ it forks non-deterministically, one fork continuing to look for further copies of $\beta$, the other fork copying all subsequent characters verbatim from input to output, accepting all the while.

What remains is to make this work for sentential forms as well as CFLs. But that is pretty straightforward, since the language of sentential forms of a CFG is itself a CFL. You can show that by replacing every non-terminal $X$ throughout $G$ by say $X^\prime$, declaring $X$ to be a terminal, and adding all productions $X^\prime \rightarrow X$ to the grammar.

I'll have to think about your question on unambiguity.

---
Tags: formal-languages, context-free, formal-grammars, closure-properties
---


# Question
Title: Proving that directed graph diagnosis is NP-hard
I have a homework assignment that I've been bashing my head against for some time, and I'd appreciate any hints. It is about choosing a known problem, the NP-completeness of which is proven, and constructing a reduction from that problem to the following problem I'll call DGD (directed graph diagnosis).

### Problem

> An instance of DGD $(V,E,k)$ consist of vertices $V = I \overset{.}{\cup} O \overset{.}{\cup} B$, directed edges $E$ and a positive integer $k$. There are three types of vertices: vertices with only incoming edges $I$, vertices with only outgoing edges $O$ and vertices with both incoming and outgoing edges $B$. Let furthermore $D=O\times I$.
>
> Now, the problem is whether we can cover all nodes with at most $k$ elements of $D$, i.e.
>
> $\qquad \displaystyle \exists\\,S\subseteq D, |S|\leq k.\ \forall\\, v\in V.\ \exists\\,(v\_1,v\_2) \in S.\ v\_1 \to^\* v \to^\* v\_2 $
>
> where $a\to^\* b$ means that there is a directed path from $a$ to $b$.

---

I think that the Dominating Set problem is the one I should be reducing from, because this too is concerned about covering a subset of nodes with another subset. I tried creating a DGD instance by first creating two nodes for each element of the dominating set, copying all edges, and then setting the $k$ of the DGD instance equal to that of the DS instance.

Suppose a simple DS-instance with nodes $1$, $2$ and $3$ and edges $(1,2)$ and $(1,3)$. This is a yes-instance with $k = 1$; the dominating set in this case consists of only node $1$. Reducing with the method just described, this would lead to a DGD instance with two paths $(1 \to 2 \to 1')$ and $(1 \to 3 \to 1')$; to cover all nodes, just one pair $(1, 1')$ would be sufficient. This would have worked perfectly, were it not for the fact that the dominating set of the DS-instance cannot, of course, be determined in polynomial time, which is a requirement here.

I have found that there are many good-looking ways to transform the edges and vertices when reducing, but my problem is somehow expressing DGD's $k$ in terms of DS's $k$. Dominating Set seemed a fitting problem to reduce from, but because of this I think that maybe I should try to reduce from a problem that has no such $k$?

# Answer
Reduce from NP-complete SET-COVER instead.

Let $S\_1,\dots,S\_m \subseteq\\{1,\dots,n\\}$ with $k\in\mathbb{N}$ an instance of set cover. Define an instance $(V,E,k')$ of DGD like this:

* $V= \\{s\_1,\dots,s\_m,o\_1,\dots,o\_m,e\_1,\dots,e\_n,o\\}$
* $E= \\{(s\_i,o\_i) \mid i = 1,\dots,n \\} \cup \\{(s\_i,e\_j)\mid j \in S\_i\\} \cup\\{(e\_j,o)\mid j=1,\dots,n\\}$
* $k' = m + k$

It is easy to see that the constructed DGD instance has a positive answer if and only if the given set cover instance has a positive answer. In particular, all $m$ pairs $(s\_i,o\_i)$ have to be chosen no matter what in order to cover all $o\_i$; then $k$ of the $m$ pairs $(s\_i,o)$ have to cover all the $e\_j$, and the first components of those chosen are the solution of the SET-COVER instance. If no such choice is possible the SET-COVER instance has no solution as well.

As the construction is possible in polynomial time, this proves SET-COVER $\leq\_p$ DGD.

---

As an example,consider the example set cover instance given on Wikipedia, namely $\\{1,2,3,4,5\\}$ and sets $S=\\{\\{1,2,3\\},\\{2,4\\},\\{3,4\\},\\{4,5\\}\\}$. This translates to the following graph:

<sup>\[source\]</sup>
> 9 votes

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


# Question
Title: Are there other ways to describe formal languages other than grammars?
I'm looking for mathematical theories that deal with describing formal languages (set of strings) in general and not just grammar hierarchies.

# Answer
There are plenty of possibilities. Others have already mentioned automata which offer a rich selection. Consider the following frameworks, too:

1. Some languages can be defined directly by *(co)inductive definitions*. For instance, the smallest fixpoint of
$\qquad \begin{align\*} \phantom{a} \\ &\phantom{\Rightarrow}\ \varepsilon \in L \\ w \in L &\Rightarrow aw \in L \\ aw \in L &\Rightarrow baw \in L \\ \phantom{a} \end{align\*}$
is the same language as the one described by $(ba\mid a)^\*$, the largest fixpoint is $(ba\mid a)^\omega$. Note that such a definition can also be written in calculus or inference rule form:
$ \qquad \begin{align\*} \phantom{a}\\ \frac{}{\varepsilon}, \quad \frac{w}{aw}, \quad \frac{aw}{baw} \\ \phantom{a} \end{align\*}$
2. Words define *word structures* that can be used as models of *logical formula*. Essentially, every word defines the domain of its positions $D\_w = \\{1, \dots, n\\}$, predicates $P\_a : D \to \\{0,1\\}$ so that $P\_a(i) \Longleftrightarrow w\_i = a$ for all $a \in \Sigma$, a predicate $\<$ that is $\<$ from $\mathbb{N}$ restricted to $D\_w$ and a predicate $\operatorname{suc} : D\_w \times D\_w \to \\{0,1\\}$ that is true if and only if the second parameter is the direct successor of the fist.
So for instance, if $w = aababaab$ then
$ \qquad \begin{align\*} \phantom{a}\\ S\_w \models \forall\\, i. \forall\\, j.\ (P\_b(i)\ \land\ \operatorname{suc}(i,j)) \to \lnot P\_b(j); \\ \phantom{a} \end{align\*}$
in fact, this first-order formula defines---via the set of all word structures that fulfill it---the same language as $(ba\mid a)^\*$. The corresponding $\omega$-language $(ba\mid a)^\omega$ is described by the LTL formula
$ \qquad \begin{align\*} \phantom{a}\\ \square\\,(P\_b \to\bigcirc(\lnot P\_b)) \\ \phantom{a} \end{align\*}$
Several equivalences between classic language classes and certain logics are known. For example, FO corresponds to star-free languages, weak MSO to regular languages and MSO to $\omega$-regular languages. See here for references.
3. Something orthogonal to classic classes are *pattern languages*. Assume a terminal alphabet $\Sigma$ and a variable alphabet $X=\\{x\_1, x\_2,\dots\\}$. A string $p \in (\Sigma \cup X)^+$ is called a *pattern*. Let $\mathcal{H}= \\{\sigma \mid \sigma : X \to \Sigma^\*\\}$ the set of substitutions. We define the language of a pattern $p$ as
$ \qquad \begin{align\*} \phantom{a}\\ \mathcal{L}(p) = \\{\sigma(p) \mid \sigma \in \mathcal{H}\\}. \\ \phantom{a} \end{align\*}$
Note that $\sigma$ is extended to work on patterns; terminal symbols are left unchanged.
As an example, consider $\mathcal{L}(x\_1abbax\_1)= \\{wabbaw\mid w \in \\{a,b\\}^\*\\}$.
Note that we allow substitutions to delete variables; some properties of the class of pattern languages are hugely different for deleting vs. non-deleting substitutions. Pattern languages are of particular interest in Gold-style learning.
> 14 votes

# Answer
You should have a look at automata theory. There's plenty of material about it.

In example, you may define a regular language with a nondeterministic finite automaton with labelled edges: a string belongs to the language if the automaton can follow the transitions labelled by its characters and stops in a final state.

Also, a context-free grammar may be recognized by a pushdown automaton.

Another way to define languages is by means of Turing machines.
> 5 votes

# Answer
Further to the other answers, one can describe and classify languages in terms of "generators" and closure properties. For example, it makes sense to talk about the smallest AFL generated by some language. A good place to start learning about this type of description is this book, although it can be quite hard to find a hard copy of it.
> 5 votes

# Answer
From the Chomsky hierarchy there are four types of formal languages(each of them is a subset of the ones after it):

A **regular formal language** can be described by:

1. Regular Grammar
2. Finite Automaton (Deterministic/Nondeterministic)
3. Regular Expression

1., 2. and 3. are equivalent and from one of them you can construct the others.

A **context-free formal language** can be described by:

1. Context-free Grammar
2. Pushdown automaton

Also 1. and 2. are equivalent.

A **context-sensitive formal language** can be described by:

1. Linear bounded automaton (Turing machine with restricted tape)

A **recursively enumerable formal language** can be described by:

1. Total Turing machine
> 5 votes

---
Tags: formal-languages, formal-grammars
---


# Question
Title: Is the number of coin tosses of a probabilistic Turing machine a Blum complexity measure?
I read that the number of coin tosses of a probabilistic Turing machine (PTM) is not a Blum complexity measure. Why?

Clarification:

Note that since the execution of the machine is not deterministic, one should be careful about defining the number of coin tosses for a PTM $M$ on input $x$ in a way similar to the time complexity for NTMs and PTMs. One way is to define it as the maximum number of coin tosses over possible executions of $M$ on $x$.

We need the definition to satisfy the axiom about decidability of $m(M,x)=k$. We can define it as follows:

$$ m(M,x) = \begin{cases} k & \text{all executions of $M$ on $x$ halt, $k=\max$ #coin tosses} \\ \infty & o.w. \ \end{cases} $$

The number of random bits that an algorithm uses is a complexity measure that appears in papers, e.g. "algorithm $A$ uses only $\lg n$ random bits, whereas algorithm $B$ uses $n$ random bits".

# Answer
Probabilistic "functions" are not even functions in the classical sense of the term "function", that is, they do not assign to each member of the domain a specific member of the range. They are not even partial functions. So the requirement of the Blum axioms that the complexity functions be computable cannot be satisfied.

Specifically, for a TM $M$ with input $x$, the Blum axioms require an algorithm that for input $(M,x,n)$ decides if $\Phi(M,x)=n$, where $\Phi$ is the complexity measure. But if $\Phi(M,x)$ is a probabilistic function, then it cannot be computed by an algorithm, and there also can be no algorithm as required by the axioms.

We could, however, define a complexity measure differently on probabilistic models, allowing a random variable, which is after all, a kind of function. Then various properties of the r.v. -- mean, median, standard deviation, etc -- could well qualify as complexity measures, and you could develop the theory from there, in the probabilistic/statistical realm.

So, although Blum measures are somewhat out of favor, except for the classic space and time measures, there's no inherent reason the basic idea can't be extended in ways like this.
> 1 votes

# Answer
According to the definition on Wikipedia, $T = \\{(i,x,t) \mid \varphi\_i \text{ tosses } t \text{ coins on } x\\}$ has to be recursive if the measure you propose is to be a Blum complexity measure. As the number of coin tosses needed for $\varphi\_i(x)$ may very well be random as well, how can the set be decidable?

Probabilistic functions do not fit the classical paradigm of computable functions well; even non-deterministic machines are required to loop if they do not output the correct result.
> 0 votes

---
Tags: computability, complexity-theory, randomness, probabilistic-algorithms
---


# Question
Title: Proving a binary tree has at most $\lceil n/2 \rceil$ leaves
I'm trying to prove that a binary tree with $n$ nodes has at most $\left\lceil \frac{n}{2} \right\rceil$ leaves. How would I go about doing this with induction?

*For people who were following in the original question about heaps, it has been moved here.*

# Answer
> 8 votes
I assume now that the question is the following:

> Given a binary tree with $n$ nodes, prove that it contains at most $\left\lceil \frac{n}{2} \right\rceil$ leaves.

Let us work with the tree definition $\mathrm{Tree}= \mathrm{Empty}\mid \mathrm{Leaf} \mid \mathrm{Node}(\mathrm{Tree},\mathrm{Tree})$. For $T$ such a tree, let $n\_T$ the number of nodes in $T$ and $l\_T$ the number of leaves in $T$.

You are correct to do this by induction, but you will need *structural* induction that follows the tree structure. For trees, this is often done as complete induction over the *height* $h(T)$ of the trees.

The induction anchor has two parts. First, for $h(t)=0$ we have $T=\mathrm{Empty}$ with $l\_T=n\_T=0$; the claim clearly holds for the empty tree. For $h(t)=1$, i.e. $T = \mathrm{Leaf}$, we similarly have $l\_T=1=\left\lceil \frac{n\_T}{2} \right\rceil$, so the claim holds for leaves.

The induction hypothesis is: Assume that the claim holds for all (binary) trees $T$ with $h(T)\leq k$, $k\geq 1$ arbitrary but fixed.

For the inductive step, consider an arbitrary binary tree $T$ with $h(T)=k+1$. As $k\geq 1$, $T=\mathrm{Node}(L,R)$ and $n\_T = n\_L+ n\_R+1$. As $L$ and $R$ are also binary trees (otherwise $T$ would not be) and $h(L),h(R)\leq k$, the induction hypothesis applies and have

$\qquad \displaystyle l\_L \leq \left\lceil \frac{n\_L}{2} \right\rceil \text{ and } l\_R \leq \left\lceil \frac{n\_R}{2} \right\rceil.$

As all leaves of $T$ are either in $L$ or $R$, we have that

$\qquad \begin{align\*} l\_T &= l\_L + l\_R \\ &\leq \left\lceil \frac{n\_L}{2} \right\rceil + \left\lceil \frac{n\_R}{2} \right\rceil \\ &\leq \left\lceil \frac{n\_L + n\_R + 1}{2} \right\rceil \qquad (\*)\\ &= \left\lceil \frac{n\_T}{2} \right\rceil \end{align\*}$

The inequality marked with $(\*)$ can be checked by (four way) case distinction over whether $n\_L,n\_R\in 2\mathbb{N}$. By the power of induction, this concludes the proof.

---

As an exercise, you can use the same technique to prove the following statements:

* Every perfect binary tree of height $h$ has $2^h-1$ nodes.
* Every full binary tree has an odd number of nodes.

# Answer
> 2 votes
I am a little confused by the question. If you are interested in trees with degree at most $3$, which is what Wikipedia says you want, then we run into the problem that a single edge has $n=2$ nodes and $n=2$ leaves, but $n/2 = 1$. Anyway, here is something close that has an easy argument.

Let $T$ be such a tree with $n$ nodes and $L$ leaves. Since $T$ is a tree, there are $n-1$ edges, and double counting them, we see that $$2n - 2 \le L + 3(n - L)$$ which says that $$2L\le n + 2$$ and this is tight in the two-vertex example above. I guess that if you want to assume that there one root of degree two and $n\ge 3$, then you can refine this argument to give $$2L \le n + 1$$ which is what you are looking for, and this is tight when the tree is full.

---
Tags: data-structures, binary-trees, combinatorics, graphs, proof-techniques
---


# Question
Title: BigO, Running Time, Invariants - Learning Resources
What are some good online resources that will help me better understand BigO notation, running time & invariants?

I'm looking for lectures, interactive examples if possible.

# Answer
> 7 votes
1. MIT OCW Introduction to algorithms video lectures
2. Design and analysis of algorithms stanford class

# Answer
> 2 votes
Since @Pratik's answer covers good resources for algorithms, I just wanted to mention that since you asked about big-O notation, Peter Braß has written a book on the topic, which you can find here.

*Update:* In response to the comments, I recommend this book for beginning students who are having trouble wrapping their head around big-O. (Yes, every algorithms book ever covers it to some extent, but my experience is that one of the most common questions on math.SE is still basically "I am having trouble with big-O", so there must be a place for a more expansive treatment.)

---
Tags: algorithms, landau-notation, education, runtime-analysis
---


title: Types of Automated Theorem Provers

text:
# Question
Title: Types of Automated Theorem Provers
*I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.*

Which are the relevant automated theorem provers? I found A Review of Theorem Provers

Is this still current?

Which ones are still very active, i.e. which are currently used beyond the group that created it?

*Find the series' next question here.*

# Answer
> 16 votes
The categorization in that list is certainly still current.

Perhaps one new category has emerged, namely, *dependently-typed programming languages*. These are essentially automated theorem provers where the primary goal is not proving theorems, but programming. Due to the Curry-Howard correspondence, these two concepts are strongly intertwined. The ultimate goal of such programming languages is to write programs that have much stronger guarantees than regular typed programming languages. People also use these for theorem proving. Some new systems falling into this category include Agda and Epigram. One of the key characteristics of such languages is that they put a lot of effort into making it easier for programmers to define inductive families of datatypes. A simple example is a vector, which depends upon natural numbers (defined inductively).

Regarding which ones are still very active, I think they all are. Coq, Isabelle, Twelf, and PVS are used a lot in the programming languages community. Maude is used extensively in modelling systems. (Personally, I've used Coq and Maude.)

I'd never heard of a few of them. In the pdf you link to, there are links to the theorem provers. Some links are current, some are broken. Gandalf now seems to be some sort of bearded wizard.

The theorem provers mentioned in “A Review of Theorem Provers” are:

* ALF: subsumbed by ALFA, Coq, and Agda.
* ALFA: seems to no longer unsupported.
* COQ: actively supported.
* MetaPRL: seems to be no longer supported.
* NuPRL: actively supported.
* HOL: actively supported.
* PVS: actively supported.
* Isabelle: actively supported.
* TWELF: actively supported.
* ACL2: actively supported.
* INKA: seems to be no longer supported.
* GANDALF: seems to be no longer supported.
* TPS: may still be active, but has only a small following.
* OTTER: may no longer be supported.
* SETHEO: replaced by E-SETHEO, which seems to no longer be supported.
* SPASS: seems to be still active.
* EQP: seems to be no longer supported.
* MAUDE: very actively supported.
* OMEGA: seems to be no longer supported.
* Mizar: actively supported.

There are undoubtedly many new automated theorem provers that have not been mentioned in this list.

For completeness, as suggested by Raphael, there are site archiving proofs made using various tools. For example:

---
Tags: logic, automated-theorem-proving, proof-assistants
---


# Question
Title: Analyzing a modified version of the card-game "War"
A simple game usually played by children, the game of War is played by two people using a standard deck of 52 playing cards. Initially, the deck is shuffled and all cards are dealt two the two players, so that each have 26 random cards in a random order. We will assume that players are allowed to examine (but not change) both decks, so that each player knows the cards and orders of cards in both decks. This is typically note done in practice, but would not change anything about how the game is played, and helps keep this version of the question completely deterministic.

Then, players reveal the top-most cards from their respective decks. The player who reveals the larger card (according to the usual order: 2, 3, 4, 5, 6, 7, 8, 9, 10, Jack, Queen, King, Ace) wins the round, placing first his card (the high card) at the bottom of his deck, and then his opponent's card (the low card) at the bottom of the deck (typically, the order of this isn't enforced, but to keep the first version of this question deterministic, such an ordering will be enforced).

In the event of a tie, each player reveals four additional cards from the top of their decks. If the fourth card shown by one player is higher than the fourth card shown by another player, the player with the higher fourth card wins all cards played during the tie-breaker, in which case the winner's cards are first placed at the bottom of the winner's deck (in first-in, first-out order; in other words, older cards are placed at the bottom first), followed by the loser's cards (in the same order).

In the event of subsequent ties, the process is repeated until a winner of the tie is determined. If one player runs out of cards and cannot continue breaking the tie, the player who still has cards is declared the winner. If both players run out cards to play at the same time the game is declared a tie.

Rounds are played until one player runs out of cards (i.e., has no more cards in his deck), at which point the player who still has cards is declared the winner.

As the game has been described so far, neither skill nor luck is involved in determining the outcome. Since there are a finite number of permutations of 52 cards, there are a finite number of ways in which the decks may be initially dealt, and it follows that (since the only state information in the game is the current state of both players' decks) the outcome of each game configuration can be decided a priori. Certainly, it is possibly to win the game of War, and by the same token, to lose it. We also leave open the possibility that a game of War might result in a Tie or in an infinite loop; for the completely deterministic version described above, such may or may not be the case.

Several variations of the game which attempt to make it more interesting (and no, not all involve making it into a drinking game). One way which I have thought of to make the game more interesting is to allow players to declare automatic "trumps" at certain rounds. At each round, either player (or both players) may declare "trump". If one player declares "trump", that player wins the round regardless of the cards being played. If both players declare "trump", then the round is treated as a tie, and play continues accordingly.

One can imagine a variety of rules limiting players' ability to trump (unlimited trumping would always result in a Tie game, as players would trump every turn). I propose two versions (just off the top of my head; more interesting versions along these lines are probably possible) of War based on this idea but using different trump limiting mechanisms:

1. Frequency-War: Players may only trump if they have not trumped in the previous $k$ rounds.
2. Revenge-War: Players may only trump if they have not won a round in the previous $k$ rounds.

Now for the questions, which apply to each of the versions described above:

> 1. Is there a strategy such that, for some set of possible initial game configurations, the player using it always wins (strongly winning strategy)? If so, what is this strategy? If not, why not?
> 2. Is there a strategy such that, for some set of possible initial game configurations, the player using it can always win or force a tie (winning strategy)? If so, what is this strategy? If not, why not?
> 3. Are their initial game configurations such that there is no winning strategy (i.e., a player using any fixed strategy $S$ can always be defeated by a player using fixed strategy $S'$)? If so, what are they, and explain?

To be clear, I am thinking of a "strategy" as a fixed algorithm which determines at what rounds the player using the strategy should trump. For instance, the algorithm "trump whenever you can" is a strategy, and an algorithm (a heuristic algorithm). Another way of what I'm asking is this:

> Are there any good (or provably optimal) heuristics for playing these games?

References to analyses of such games are appreciated (I am unaware of any analysis of this version of War, or of essentially equivalent games). Results for any $k$ are interesting and appreciated (note that, in both cases, $k=0$ leads to unlimited trumping, which I have already discussed).

# Answer
> 7 votes
If I understand correctly, all information about the game is available to both players. That is, the starting configuration and all of the possible moves are known by both players (mainly because both players can look at the cards of the other player). This makes game is a zero-sum game of perfect information. Thus there exists is a perfect strategy available to both players that would achieve the best outcome in each game for that player. This was proven in 1912 by the German mathematician Ernst Zermelo.

I do not know what the strategy is, but one could imagine building a big game tree for it and getting a computer to find the strategy for me using the min-max algorithm.

The tree for each game would have as root the hands of the two players. The branches in the tree corresponds to the moves of the players. In the simplest case, these consist of simply laying down the requisite cards. In the more advanced cases, the 'trump' move can be made. Internal nodes of the tree record what the current configuration of cards is along with any information about the state wrt 'trumps'. The leaves of the tree correspond to the end game positions, which will be labelled with, say, +1 for a win to Player 1, 0 for a tie, and -1 for a win to Player 2. *Ignore looping games for now.*

Now the min-max algorithm will work as follows (from Player 1's perspective). Assume that it looks at a node where Player 1 makes a move and that the nodes below are annotated with a +1, 0, or -1 (the *payoff*) along with the choices the player needs to make to get the given result. Player 1 simply selects the node with the largest payoff, records that payoff and the choice required to get that. For the node where Player 2 is making the move, the node with the minimum payoff is chosen, and the choice is recorded. This reflects that Player 2 is aiming for the lowest score to win. This is propagated to the of the tree. The choices recorded at each node correspond correspond to the best strategy a player can make. The final payoff determines who wins. This is ultimately a function in terms of the payoff, though the exact choice of moves may vary.

*Potentially looping configurations* can be incorporated into the game tree by simply adding loops that return to an already seen configuration (when computing from the top). For such nodes you take the greatest fixed point if it is a node where Player 1 plays and the least fixed point when Player 2 plays.

Note that if you had not made the assumption that both players could examine both decks, then this approach would not apply. The game would then involve chance and the selected strategy would be game specific.

Whether or not there is a strong or weak winning strategy for one of the players depends on the outcome of the min-max algorithm applied to all trees. But there sure are a lot of them .... Computing the tree for one is probably fairly easy, since there are not very many choices made through the game.

---
Tags: algorithms, optimization
---


title: Polymorphism and Inductive datatypes

text:
# Question
Title: Polymorphism and Inductive datatypes
I'm curious. I've been working on this datatype in *OCaml*:

```
type 'a exptree =
  | Epsilon
  | Delta of 'a exptree * 'a exptree
  | Omicron of 'a
  | Iota of 'a exptree exptree

```

Which can be manipulated using explicitly typed recursive functions (a feature that has been added quite recently). Example:

```
let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
  fun f ->
    begin function
    | Epsilon -> Epsilon
    | Delta (t1, t2) -> Delta (map f t1, map f t2)
    | Omicron t -> Omicron (f t)
    | Iota tt -> Iota (map (map f) tt)
    end

```

But I've never been able to define it in *Coq*:

```
Inductive exptree a :=
  | epsilon : exptree a
  | delta : exptree a -> exptree a -> exptree a
  | omicron : a -> exptree a
  | iota : exptree (exptree a) -> exptree a
.

```

*Coq* is whining. It doesn't like the last constructor, and says something I don't completely understand or agree with:

```
Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".

```

What I can understand is that inductive types using a negation inside their definition like `type 'a term = Constructor ('a term -> …)` are rejected, because they would lead to ugly non well-founded beasts like (untyped) λ-terms. However this particular `exptree` datatype seems innocuous enough: looking at its *OCaml* definition, its argument `'a` is never used in negative positions.

It seems that *Coq* is overcautious here. So is there really a problem with this particular inductive datatype? Or could *Coq* be slightly more permissive here?

Also, what about other proof assistants, are they able to cope with such an inductive definition (in a natural way)?

# Answer
> 9 votes
This has come up on the Coq mailing list several times, but I never saw a conclusive answer. Coq isn't as general as it could be; the rules in (Coquand, 1990) and (Giménez, 1998) (and his PhD thesis) are more general and do not require strict positivity. Positivity enough is not enough, however, when you go outside `Set`; this example came up in several discussions:

```
Inductive Big : Type := B : ((B -> Prop) -> Prop) -> Big.

```

With plain data structures such as yours, the inductive type would not cause problems other than making the implementation more complex.

There is a general way to define types such as this defined as the fixpoint of a polynomial: $$F = \epsilon + \delta\\, (F \times F) + \omicron\\, \mathrm{id} + F \circ F$$

Instead of attempting to define the function $\mathrm{exptree} : a \mapsto \mathrm{exptree}(a)$, define the family of types $\mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree} \circ \mathrm{exptree}, \ldots$. This means adding an integer parameter to the type that encodes the number of self-compositions ($\mathrm{exptree}^0(a) = a$, $\mathrm{exptree}^1(a) = \mathrm{exptree}(a)$, $\mathrm{exptree}^2(a) = \mathrm{exptree}(\mathrm{exptree}(a))$, etc), and a supplementary injection constructor to turn $a$ into $\mathrm{exptree}^0(a) = a$.

```
Inductive et : nat -> Type -> Type :=
  | alpha : forall a, a -> et 0 a                      (*injection*)
  | omicron : forall n a, et n a -> et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -> et (S n) a -> et (S n) a
  | iota : forall n a, et (S (S n)) a -> et (S n) a
.

```

You can proceed to define values and work on them. Coq will often be able to infer the exponent. `Set Implicit Arguments` would make these definitions prettier.

```
Definition exptree := et 1.
Definition et1 : exptree nat :=
  delta _ _ (omicron _ _ (alpha _ 42)) (epsilon _ _).
Definition et2 : exptree nat := iota _ _ (omicron _ _ et1).

```

You may prefer to decrease the argument by 1, so that `exptree` is `et 0`. This removes a lot of `S n` in the definition, which may make some proofs easier, but it requires splitting the initial case from the recurrence case in every constructor that takes an $a$ in an argument (instead of adding a single injection constructor for $a$). In this example, there's only a single constructor to split, so this should be a good choice.

```
Inductive et : nat -> Type -> Type :=
  | omicron_0 : forall a, a -> et 0 a
  | omicron_S : forall n a, et n a -> et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -> et n a -> et n a
  | iota : forall n a, et (S n) a -> et n a
.
Definition exptree := et 0.
Definition et1 : exptree nat :=
  delta _ _ (omicron_0 _ 42) (epsilon _ _).
Definition et2 : exptree nat :=
  (iota _ _ (omicron_S _ _ et1)).

```

I think this is the same principle proposed in a more general form by Ralph Mattes.

### References

Thierry Coquand and Christine Paulin. *Inductively defined types*. In *Proceedings of COLOG'88*, LNCS 417, 1990. \[Springer\] \[Google\]

Eduardo Giménez. *Structural Recursive Definitions in Type Theory*. In *ICALP'98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1998.* \[PDF\]

# Answer
> 8 votes
Ralph Matthes describes how to simulate types like this in Coq in "A Datastructure for Iterated Powers" (code, paper).

# Answer
> 6 votes
One of the first things Coq does is building the induction principle associated with the inductive type you just defined and understanding the underlying induction principle is a good exercise.

For example `O : nat | S : nat -> nat` will generate the induction principle `P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n`.

What would be the induction principle corresponding to `iota`? It seems that there is no predicate `P` that would be able to talk about `P t` and `P (iota t)`, because it should talk about `exptree a`, `exptree (exptree a)`, `exptree (exptree (exptree a))` ...

Also the `Omicron` does the same thing but the type is smaller each time. You should feel that having a reference to both a smaller type and a bigger type would make things messy. (That said, `Omicron` is the right way)

That is not the exact criteria that says why the definition should not be accepted but this explains why it feels wrong to me.

`exptree` seems like you are building a grammar for expressions, thing that generally aren't *that* recursive. Do you want some help with that?

---
Tags: logic, programming-languages, coq, inductive-datatypes
---


# Question
Title: Reducing directed hamiltonian cycle to graph coloring
The 3-SAT problem can be reduced to both the graph coloring and the directed hamiltonian cycle problem, but is there any chain of reductions which reduce directed hamiltonian cycle to graph coloring in polynomial time?

# Answer
Let $Q \in \sf{NP}$ and $Q' \in \sf{NP\text{-}hard}$. Then, by definition, $Q$ is (many-one) reducible to $Q'$ in polynomial time.

The exact chain of the reductions will depend on the $\sf{NP\text{-}hard}$ness proof of $Q'$. Typically, it is proven by a chain of reductions starting from $\mathrm{SAT}$ and ending with $Q'$ and then using the Cook-Levin theorem. So the chain of reductions will be a reduction from $Q$ to $\mathrm{SAT}$ followed by the chain of reductions from $\mathrm{SAT}$ to $Q'$.

There is usually a more direct reduction for specific problems (without using Cook-Levin), since it is usually easy to find a propositional formula directly expressing the required property (with no reference to TMs). For example, in the case of Directed Hamiltionian Path ($\mathrm{DHP}$) and Graph Coloring ($\mathrm{GC}$), you can reduce:

* $\mathrm{DHP}$ to $\mathrm{SAT}$,
* $\mathrm{SAT}$ to $\mathrm{3SAT}$,
* $\mathrm{3SAT}$ to $\mathrm{GC}$.
> 4 votes

---
Tags: complexity-theory, np-complete, reductions
---


# Question
Title: Priority queue with both decrease-key and increase-key operations
A Fibonnaci Heap supports the following operations:

* `insert(key, data)` : adds a new element to the data structure
* `find-min()` : returns a pointer to the element with minimum key
* `delete-min()` : removes the element with minimum key
* `delete(node)` : deletes the element pointed to by `node`
* `decrease-key(node)` : decreases the key of the element pointed to by `node`

All non-delete operations are $O(1)$ (amortized) time, and the delete operations are $O(\log n)$ amortized time.

Are there any implementations of a priority queue which also support`increase-key(node)` in $O(1)$ (amortized) time?

# Answer
> 10 votes
Assume you have a priority queue that has $O(1)$ `find-min`, `increase-key`, and `insert`. Then the following is a sorting algorithm that takes $O(n)$ time:

```
vector<T>
fast_sort(const vector<T> & in) {
  vector<T> ans;
  pq<T> out;
  for (auto x : in) {
    out.insert(x);
  }
  for(auto x : in) {
    ans.push_back(*out.find_min());
    out.increase_key(out.find_min(), infinity);
  }
  return ans;
}

```

---
Tags: data-structures, priority-queues
---


# Question
Title: Why is unification so important to inference engines?
<sup>*I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.*</sup>

I keep reading about the Unification Algorithm.

* What is it and why is so important to Inference Engines?
* Why is it so important to Computer Science?

# Answer
> 12 votes
Unification is such a fundamental concept in computer science that perhaps at time we even take it for granted. Any time we have a rule or equation or pattern and want to apply it to some data, unification is used to specialize the rule to the data. Or if we want to combine two general but overlapping rules, unification provides us with the most general combined rule. Unification is at the core of

* Theorem provers and proof assistants, include some based on higher-order unification.
* Prolog implementations (as Resolution).
* Type inference algorithms.
* Computational linguistics/natural language processing.
* Term rewriting systems such as Maude, which can be used as the basis of programming language semantics.
* Deductive databases.
* Expert systems or more generally Artificial intelligence.
* Computer algebra systems.
* Pattern matching in functional languages (at least in part ... only matching).
* Some parsing approaches.
* Some query languages, especially involving the Semantic Web.

# Answer
> 9 votes
Proof assistants such as Isabelle/HOL work on a syntactical level on a logical calculus. Imagine you have the modus ponens rule (MP)

$\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$

and the proof goal

$\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$

We humans see immediately that this follows with modus ponens, but the machine has to match goal to rule *syntactically* (wether you do `apply rule mp` or `apply simp`), and this is what unification does. The algorithm finds $\varphi$ with $\varphi(P) = a\lor b$ and $\varphi(Q) = c \land d$, instantiates the rule and applies it.

The good thing about assistants' methods like `simp` now is that if your goal is

$\qquad \displaystyle (a \lor b) \to (c \land d), a \ \overset{!}{\Longrightarrow} d$

that they will find a suitable sequence of applications of rules MP, $P \land Q \Longrightarrow P$ and $P \Longrightarrow P \lor Q$ with compatible unifications for the respective steps and solve the goal.

---

*Notation:* With $\Gamma = \\{\varphi\_1, \dots, \varphi\_n\\}$ a set of logical formulae, the notation

$\qquad \Gamma \Longrightarrow \psi$

means the following:

> If I have derived/proven all formulae in $\Gamma$ (i.e. they are *valid*) then this rule asserts that $\psi$ is also valid.

In a sense, the rule $\Gamma \Longrightarrow \psi$ is the last step in a (long) proof for $\psi$. Proofs are nothing but chains of such rule applications.

Note that *rules* usually contain schematic variables ($P$ and $Q$ in the above) that can be replaced by *arbitrary* formulae as long as the same variable is replaced with the same formula in all instances; the result of that format is the concrete rule instance (or intuitively, a proof step). This replacement is above denoted by $\varphi$ which was found by unification.

Often people use $\models$ instead of $\Longrightarrow$.

# Answer
> 2 votes
I don't think it is important to *inference engines*. The unification algorithm is however very helpful for *type inference*. These are two very different kinds of inference.

Type inference is important to computer science because *types* are important in the theory of programming languages, which is a significant part of computer science. Types are also close to logic and are intensively used in automated theorem proving. There are implementations of unification algorithms in many, if not all, proof assistants and SMT solvers.

Inference engines are related to artificial intelligence, which is also important but very different. (I've seen links between learning and logic but this seems fetched.)

---
Tags: logic, proof-assistants, automated-theorem-proving, smt-solvers, unification
---


# Question
Title: Solving Recurrences via Characteristic Polynomial with Imaginary Roots
In algorithm analysis you often have to solve recurrences. In addition to Master Theorem, substitution and iteration methods, there is one using *characteristic polynomials*.

Say I have concluded that a characteristic polynomial $x^2 - 2x + 2$ has *imaginary* roots, namely $x\_1 = 1+i$ and $x\_2 =1-i$. Then I cannot use

$\qquad c\_1\cdot x\_1^n + c\_2\cdot x\_2^n$

to obtain the solution, right? How should I proceed in this case?

# Answer
Yes, the solution is in fact $T(n) = \alpha(1+i)^n + \beta(1-i)^n$ for some constants $\alpha$ and $\beta$ determined by the base cases. If the bases cases are real, then (by induction) all the complex terms in $T(n)$ will cancel, for all integer $n$.

For example, consider the recurrence $T(n) = 2T(n-1) - 2T(n-2)$, with base cases $T(0)=0$ and $T(1)=2$. The characteristic polynomial of this recurrence is $x^2-2x+2$, so the solution is $T(n) = \alpha(1+i)^n + \beta(1-i)^n$ for some constants $\alpha$ and $\beta$. Plugging in base cases gives us $$ T(0) = \alpha(1+i)^0 + \beta(1-i)^0 = \alpha+\beta = 0\\ T(1) = \alpha(1+i)^1 + \beta(1-i)^1 = (\alpha+\beta) + (\alpha-\beta)i = 2 $$ which implies $$ \alpha + \beta = 0 \\ \alpha - \beta = -2i $$ which implies $\alpha = -i$ and $\beta = i$. So the solution is $$ T(n) = i\cdot ((1-i)^n - (1+i)^n). $$

This function oscillates between $\sqrt{2}^n$ and $-\sqrt{2}^n$ with a "period" of 4. In particular, we have $T(4n) = 0$ for all $n$, because $(1-i)^4 = (1+i)^4 = -4$ (and because I chose the base case $T(0)$ carefully).
> 12 votes

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


# Question
Title: From the LR(1) parsing table, can we deduce that it is also an LALR and SLR table?
There is this question I read somewhere but could not answer myself.

Assume I have an LR(1) Parsing table. Is there any way that just by looking at it and its items, can I deduce that it is also a table for LALR and SLR?

# Answer
Trivially, yes: the grammar is extractible from the items.

Probably more in the spirit of the question. LALR(1) is easily extracted from LR(1): merge LR(1) items which correspond to the same LR(0) one and the grammar isn't LALR(1) if that process results in conflicts. (BTW this can be considered as a definition of LALR(1)).

SLR(1) is not so easy; you need to compute the follow sets to find out if there are conflicts. (SLR(1) is based on the LR(0) items like LALR(1), but it has "unneeded" conflicts due to the use of follow sets instead of the computation of look ahead one to choose which production to reduce.)
> 5 votes

---
Tags: compilers, parsers
---


# Question
Title: Optimization version of decision problems
It is known that each optimization/search problem has an equivalent decision problem. For example the shortest path problem

> * **optimization/search version:** Given an undirected unweighted graph $G = (V, E)$ and two vertices $v,u\in V$, find a shortest path between $v$ and $u$.
> * **decision version:** Given an undirected unweighted graph $G = (V, E)$, two vertices $v,u\in V$, and a non-negative integer $k$, is there a path in $G$ between $u$ and $v$ whose length is at most $k$?

In general, "Find $x^\*\in X$ s.t. $f(x^\*) = \min\\{f(x)\mid x\in X\\}$!" becomes "Is there $x\in X$ s.t. $f(x) \leq k$?".

But is the reverse also true, i.e. is there an equivalent optimization problem for every decision problem? If not, what is an example of a decision problem that has no equivalent optimization problem?

# Answer
As already stated in the comments, it depends on the definitions, as usual. My attempt to answer this needs quite a few definitions, so this will be another example of my inability to give concise answers.

---

**Definition:** An *optimization problem* is a tuple $(X,F,Z,\odot)$ with

* $X$ the set of suitably encoded (strings) *instances* or *inputs*.
* $F$ is a function that maps each instance $x\in X$ to a set $F(x)$ of *feasible solutions* of $x$.
* $Z$ is the objective function that maps each pair $(x, y)$, where $x \in X$ and $y\in F(x)$, to a real number $Z(x, y)$ called the *value* of $y$.
* $\odot$ is the *optimization direction*, either $\min$ or $\max$.

**Definition:** An *optimal solution* of an instance $x\in X$ of an optimization problem $P\_O$ is a feasible solution $y\in F(x)$ for which $Z(x, y)=\odot\\{Z(x, y')\mid y'\in F(x)\\}$. The value of an optimal solution is denoted with $Opt(x)$ and called the *optimum*.

**Definition:** The *evaluation problem*, denoted $P\_E$, corresponding to the optimization problem $P\_O$ is the following: Given an instance $x\in X$, compute $Opt(x)$ if $x$ has an optimal solution and output “no optimal solution” otherwise.

Note that this just asks for the *value* of the optimal solution not the whole solution itself with all its details.

**Definition:** The *decision problem*, denoted $P\_D$ corresponding to the optimization problem $P\_O$ is the following: Given a pair $(x, k)$, where $x\in X$ and $k\in\mathbb{Q}$, decide whether $x$ has a feasible solution $y$ such that $Z(x, y)\le k$ if $\odot=\min$ and such that $Z(x, y)\ge k$ if $\odot=\max$.

A first observation is now that $P\_O\in \mathrm{NPO} \Rightarrow P\_D\in \mathrm{NP}$. The proof is not difficult and omitted here.

Now intuitively $P\_E$ and $P\_D$ corresponding to $P\_O$ are not more difficult than $P\_O$ itself. To express this feeling formally (thereby defining what *equivalent* is supposed to mean) we will use reductions.

Recall that a language $L\_1$ is polynomial-time reducible to another language $L\_2$ if there is a function $f$, computable in polynomial time, such that for all words $x$, $x\in L\_1\Leftrightarrow f(x)\in L\_2$. This kind of reducibility is known as *Karp* or *many-to-one reducibility*, and if $L\_1$ is reducible to $L\_2$ in this manner, we express this by writing $L\_1\le\_m L\_2$. This is a central concept in the definition of NP-completness.

Unfortunately, many-to-one reductions go between languages and it is not clear how to employ them in the context of optimization problems. Therefore we need to consider a different kind of reducibility, *Turing reducibility*. First we need this:

**Definition:** An *oracle* for a problem $P$ is a (hypothetical) subroutine that can solve instances of $P$ in constant time.

**Definition:** A problem $P\_1$ is polynomial-time *Turing-reducible* to a problem $P\_2$, written $P\_1\le\_T P\_2$, if instances of $P\_1$ can be solved in polynomial time by an algorithm with access to an oracle for $P\_2$.

Informally, just as with $\le\_m$, the relation $P\_1\le\_T P\_2$ expresses, that $P\_1$ is no more difficult than $P\_2$. It is also easy to see that if $P\_2$ can be solved in polynomial time, so can $P\_1$. Again $\le\_T$ is a transitive relation. The following fact is obvious:

Let $P\_O\in \mathrm{NPO}$, then $P\_D\le\_T P\_E\le\_T P\_O$.

Because given the full solution, computing its value and deciding whether it meets the bound $k$ is simple.

**Definition:** If for two problems $P\_1$ and $P\_2$ both relations $P\_1\le\_T P\_2$, $P\_2\le P\_1$ hold, we write $P\_1\equiv\_T P\_2$; our notion of *equivalence*.

We are now ready to proof that $P\_D\equiv\_T P\_E$ given the corresponding optimization problem is $P\_O\in \mathrm{NPO}$ and $Z$ is integer valued. We have to show that $P\_E \le\_T P\_D$ holds. We can determine $\odot\\{Z(x,y)\mid y\in F(x)\\}$ with a binary search usign the orcale for $P\_D$. The definition of $\mathrm{NPO}$ ensures that $|Z(x, y)|\le 2^{q(|x|)}$ for some polynomial $q$, so the number of steps in the binary search is polynomial in $|x|$. $\Box$

For an optimization problem $P\_O$ the relation to $P\_E$ is less clear. In many concrete cases, one can show directly that $P\_D\equiv\_T P\_E \equiv\_T P\_O$. To prove that this holds generally within the framework given here we need an additional assumption.

First we need to extend $\le\_m$ from pairs of languages to pairs of the corresponding decision problems. Then it is easy to see that $\le\_T$ is more general than $\le\_m$.

Let $P$ and $P'$ be decision problems; then $P\le\_m P' \Rightarrow P\le\_T P'$. This holds because a many-to-one reduction can be interpreted as making use of an oracle in a very restricted way: The oracle is called once, at the very end, and its result is also returned as the overall result. $\Box$

Now we are ready for the finale:

Let $P\_O\in \mathrm{NPO}$ and suppose $Z$ is integer-valued and that $P\_D$ is NP-complete, then $$P\_D\equiv\_T P\_E \equiv\_T P\_O.$$ With the previous observations it remains to show $P\_O\le\_T P\_E$. To do this we will exhibit a problem $P\_O'\in \mathrm{NPO}$ such that $P\_O\le\_T P\_E'$. Then we have $$P\_O\le\_T P\_E' \le\_T P\_D'\le\_T P\_D\le\_T P\_E.$$ The second and third $\le\_T$ hold because of the equivalence of the decision and evaluation version proofed earlier. The third $\le\_T$ follows from the NP-completness of $P\_D$ and the two facts mentioned before, namely $P\_O\in \mathrm{NPO} \Rightarrow P\_D\in \mathrm{NP}$ and $P\le\_m P\_O' \Rightarrow P\le\_T P\_O'$.

Now the details: Assume that the feasible solutions of $P\_O$ are encoded using an alphabet $\Sigma$ equipped with a total order. Let $w\_0, w\_1, \ldots$ be the words from $\Sigma^\*$ listed in order of nondecreasing length and lexicographic order within the blocks of words with common length. (Thus $w\_0$ is the empty word.) For all $y\in\Sigma^\*$ let $\sigma(y)$ denote the unique integer $i$ such that $y=w\_i$. Both $\sigma$ and $\sigma^{-1}$ can be computed in polynomial time. Let $q$ be a polynomial such that for all $x\in X$ and all $y\in F(x)$ we have $\sigma(y)\<2^{q(|x|)}$.

Now the problem $P\_O'$ is identical to $P\_O$ except for a modified objective function $Z'$. For $x\in X$ and $y\in F(x)$ we take $Z'(x, y)=2^{q(|x|)}\cdot Z(x,y)+\sigma(y)$. $Z'$ is computable in polynomial time thus $P\_O'\in \mathrm{NPO}$.

To show that $P\_O\le\_T P\_E'$ we observe that $x$ is feasible for $P\_O$ if and only if it is feasible for $P\_E'$. We can assume that this is the case, since the opposite case is trivial to handle.

The substituion of $Z'$ for $Z$ is monotonic in the sense that for all $y\_1, y\_2\in F(x)$, if $Z(x, y\_1)\<Z(x, y\_2)$ then $Z'(x, y\_1)\<Z'(x, y\_2)$. This implies that every optimal solution for $x$ in $P\_O'$ is an optimal solution of $x$ in $P\_O$. Thus our task reduces to the computation of an optimal solution $y$ of $x$ in $P\_O'$.

Querying the oracle for $P\_E'$ we can get the value of $Z'(x,y)=2^{q(|x|)}\cdot Z(x,y)+\sigma(y)$. Forming the remainder of this number modulo $2^{q(|x|)}$ yields $\sigma(y)$ from which $y$ can be computed in polynomial time.
> 33 votes

# Answer
As the comments say, the answer depends on the exact definitions. Let me interpret the question in a very basic (even naïve) way.

Let $S$ be some relation, that is $S \subseteq \\{ (a,b) \mid a,b \in \Sigma^\*\\}$.

Now we define a **search problem** for $S$:

> Given $a$, find a $b$ such that $(a,b) \in S$.

and a **decision problem** for $S$:

> Given $(a,b)$ answer whether or not $(a,b) \in S$.

<sub>(for instance, in the example given in the question, $S$ will hold all the pairs $(u,v,k)$ such that there exists a path between $u$ and $v$ which is shorter than $k$.)</sub>

Note that these two problems are **well defined**. *For this definition*, we can ask whether the two problems are "equivalent" for any $S$. In "equivalent" I mean that if one of them is computable (i.e., there exists an algorithm that solves it) than the other one is computable as well. In general, they are not.

**Claim 1**: *Decision* implies *Search*.

Proof: Let $D\_S$ be the algorithm that solves the decision problem of $S$. Given an input $a$, We can run $D\_S(a,x)$ for any $x\in \Sigma^\*$, one after the other, or in parallel. If there exists $b$ such that $(a,b)\in S$, we will eventually find it. If not, the algorithm might not stop$^\dagger$.

**Claim 2**: *Search* does **not** imply *Decision*.

The reason is that the search algorithm might return a different $b$ than the one we need. That is, for every $a$ there is some $b$ that is very easy to find, but other $b'$ that is not. For instance, let $L$ be some undecidable language, then define $$S = \\{ (x,0) \mid x\in \Sigma^\*\\} \cup \\{ (x,1) \mid x \in L\\}.$$ For every $x$ the search algorithm can return $0$. But no decision algorithm can answer correctly whether $(x,1) \in S$, for *all* the pairs $(x,1)$. If it could, it would have decided an undecidable problem, which is impossible.

$^\dagger$ This depends on $S$. If, for instance, $S$ is bounded, there might exists an algorithm that does stop.
> 5 votes

---
Tags: complexity-theory, optimization, search-problem, decision-problem
---


# Question
Title: How to prove that  $n(\log_3(n))^5 = O(n^{1.2})$?
This a homework question from Udi Manber's book. Any hint would be nice :)

I must show that:

> $n(\log\_3(n))^5 = O(n^{1.2})$

I tried using Theorem 3.1 of book:

> $f(n)^c = O(a^{f(n)})$ (for $c \> 0$, $a \> 1$)

Substituing:

$(\log\_3(n))^5 = O(3^{\log\_3(n)}) = O(n) $

but $n(\log\_3(n))^5 = O(n\cdot n) = O(n^2) \ne O(n^{1.2})$

Thank you for any help.

# Answer
Do what you did, but let $a = (3^{0.2})$... that should do it, right?

The reason that what you did didn't work is as follows. The big-oh bound is not tight; while the logarithm to the fifth is indeed big-oh of linear functions, it is also big oh of the fifth root function. You need this stronger result (which you can also get from the theorem) to do what you're doing.
> 14 votes

# Answer
Another way to think about it more intuitively, is to see that the main thing you have to show is that $(\log\_3(n))^5$ is $O(n^{0.2})$, or equivalently that $\log\_3(n)$ is $O(n^{0.04})$. Logs always grow slower than any constant power of n, no matter how small.

If you want to formalize the last sentence, then you can use theorem 3 with a sufficiently small $\alpha$ as @RanG mentions in the comment on @Patrick87's answer.
> 5 votes

---
Tags: asymptotics, landau-notation, mathematical-analysis
---


# Question
Title: Examples of sophisticated recursive algorithms
I was explaining the famous deterministic linear-time selection algorithm (median of medians algorithm) to a friend.

The recursion in this algorithm (while being very simple) is quite sophisticated. There are two recursive calls, each with different parameters.

I was trying to find other examples of such interesting recursive algorithms, but could not find any. All of the recursive algorithms I could come up with are either simple tail-recursions or simple divide and conquer (where the two calls are "the same").

Can you give some examples of sophisticated recursion?

# Answer
My favorite recurrence shows up in output-sensitive algorithms for computing convex hulls, first by Kirkpatrick and Seidel, but later repeated by others. Let $T(n,h)$ denote the time to compute the convex hull of $n$ points in the plane, when the convex hull has $h$ vertices. (The value of $h$ is not known in advance, aside from the trivial bound $h\le n$.) Kirkpatrick and Seidel's algorithm yields the recurrence $$ T(n,h) = \begin{cases} O(n) & \text{if }n \le 3 \text{ or } h \le 3 \\ T(n\_1, h\_1) + T(n\_2, h\_2) + O(n) & \text{otherwise} \end{cases} $$ where $n\_1, n\_2 \le 3n/4$ and $n\_1 + n\_2 = n$ and $h\_1 + h\_2 = h$.

The solution is $T(n,h) = O(n\log h)$. This is a little surprising, since $h$ is not the parameter being split evenly. But in fact, the *worst* case of the recurrence happens when $h\_1$ and $h\_2$ are both about $h/2$; if somehow magically $h\_1$ is always constant, the solution would be $T(n,h) = O(n)$.

I used a variant of this recurrence in one of my first computational topology papers: $$ T(n,g) = \begin{cases} O(n) & \text{if }n \le 3 \text{ or } g = 0\\ T(n\_1, g\_1) + T(n\_2, g\_2) + O(\min\\{n\_1, n\_2\\}) & \text{otherwise} \end{cases} $$ where $n\_1 + n\_2 = n$ and $g\_1 + g\_2 = g$. Again, the solution is $O(n\log g)$, and the *worst* case occurs when both $n$ and $g$ are always split evenly.
> 15 votes

# Answer
The recursion that I used in my paper "A linear-time algorithm for computing the Voronoi diagram of a convex polygon" by Aggarwal *et al* is also quite complicated.

Here is a description of the algorithm from our paper. In case it's not clear from the description, in step 3 the red points are partitioned into crimson and garnet points. Steps 1, 3, and 6 are all linear time. We also know that if $n$ is the total number of points, $|\mathrm{B}| \geq \alpha n$, $|\mathrm{R}| \geq \beta n$, and $|\mathrm{C}| \geq \gamma n$ for some $\alpha, \beta, \gamma \> 0$.

I'll let you figure out why the entire algorithm takes linear time.

> 1. Partition the original points into the blue and red sets B and R.
> 2. Recursively compute the convex hull of the blue points.
> 3. Using the structure of the blue hull, select the crimson points C.
> 4. Add the crimson points to the blue hull one at a time.
> 5. Recursively compute the convex hull of the garnet points G.
> 6. Merge this garnet hull with the expanded blue hull of step 4.
>
> What makes the algorithm linear is the ability to add a fixed fraction of the red points to the blue hull at constant cost per point. The points added are the crimson points.

The recursion is thus $$ T(n) = T(|B|) + T(|G|) + O(n) $$ where you don't know $|B|$ and $|G|$ but are guaranteed that $|B| + |G| \leq (1-\gamma) n$.
> 13 votes

# Answer
There is a variation on the median finding recurrence that comes from range searching with halfplanes. The recurrence itself is of the form

\\\[ T(n) = T(n/2) + T(n/4) + cn \\\] which is similar to the median-finding recurrence. For more on this, look at Jeff Erickson's lecture notes and in particular Section 4.
> 6 votes

# Answer
There are a bunch of cool recursive algorithms \[1\], \[2\] used in RNA secondary structure prediction. Left to its own devices, a strand of RNA will form base pairs with itself; one relatively simple example from \[3\] computes the maximum number of nested, paired bases an RNA string will form with itself:

$M(i,j)=\underset{i\leq k \< j - L\_{min}}{max} \begin{cases} M(i,k-1)+ M(k+1, j-1)+1 \\M(i, j-1) \end{cases}$

---

1. Optimal computer folding of large RNA sequences using thermodynamics and auxiliary information by M. Zuker, P. Stiegler (1981)
2. A Dynamic Programming Algorithm for RNA Structure Prediction Including Pseudoknots by E. Rivas, S. R. Eddy (1999)
3. Fast algorithm for predicting the secondary structure of single-stranded RNA by R. Nussinov, A. B. Jacobson (1980)
> 6 votes

# Answer
I still don't really understand what you mean by "sophisticated recursion". For example, the recursion step in the FFT algorithm is sophisticated!

But if you want to look for more *complicated* recursion, then mutual recursion might be one possible answer. Mutual recursion is useful when working with fuctional programming languages. Mutual recursion is the key feature of recursive descent parsers.
> 4 votes

# Answer
Off the top of my head, the McCarthy 91 function

```
F(N) =
    n - 100    if n > 100
    F(F(n+11)) if n <= 100

```

and the Ackermann function

```
A(m, n) =
    n + 1             if m = 0
    A(m-1, 1)         if m > 0 and n = 0
    A(m-1, A(m, n-1)) if m > 0 and n > 0

```

might count as offbeat, albeit toy-ish, recursive functions.
> 4 votes

---
Tags: algorithms, recursion
---