title: functional vs state-based

text:
# Question
Title: functional vs state-based
As mentioned in Lambda Calculus - Computerphile,

> Alonzo Church's method is functional where a function as a blackbox, takes an input, processes, and produces an output, and Turing machines have internal state.

* First, I would like to know what does it exactly mean by `functional` and `state-based`?
* Are they the same as the terms `stateful` and `stateless`?
* And how are they related, similar and different from one another?

Not quite sure if this question is to be asked here or in Stackoverflow.

Ref: https://www.revolvy.com/main/index.php?s=State+(computer+science) Ref: Learning fundamental differences between functional programming and Object Oriented Programming

# Answer
The terminology isn't absolute when applied to actual languages. Usually "stateful" refers to holding the "state of the computation" largely in variables of some sort (variables = changeable references to values). These can be ordinary variables (C) or fields of objects (C++, Java). It is possible in many such languages, however, to minimize such state and to program largely with constants only and with parameters of functions and methods. The latter can be variables or constants, depending on the language.

The reason that stateful languages can be programmed this way is that they also employ a run time stack in which values can be maintained.

Stateless programming in most commonly done in functional languages that minimize the use of variables, depending on constants and constant function arguments. The computation "state" is the stack itself. However, most functional languages do have some mechanism for declaring variables (things which vary), though they also tend to call names that refer to constants as "variables" confusing the issue somewhat.

In "pure functional programming" you utilize only constants and immutable function arguments to move values around the computation. The "State of the Computation" is the state of the run time stack. This is true Stateless programming.

Most imperative and OO programming, on the other hand is stateful. The "State of the Computation" is comprised of both the state of the run time stack and the currently referenced values of the variables.

Another way to think of it is that in stateless programming, the state is "implicit" in the stack and the current program pointer. In stateful programming, the state is explicit in the variables and fields (to a large part - there is also the stack).
> 3 votes

# Answer
* Statefull = full of state.
* Stateless = has no (changing) state.

Therefore they are opposite, not the same.

Functional programming is stateless.
> 0 votes

---
Tags: functional-programming, turing-machines
---


# Question
Title: How to Specify the Behavior of Automata for Verification
I am wondering what it takes to "verify" or "prove" that an automaton is correct. What the components are that are required. It seems that an automaton would be an easier thing to formally verify as sound than say an arbitrary function. Not sure though what needs to be verified in an automaton, which is what brings up the question.

Thank you!

# Answer
> 3 votes
It feels to me like this has already been explained before (, ). To prove that an automaton is correct, you first must define what correctness means to you. Usually that is done by writing a specification of what it means to be correct. Then, you prove that an automaton meets the specification.

If you're interested in knowing how to do that, that's a broad subject that people have written entire books about. I suggest reading a textbook on model checking (particularly of finite-state systems).

How do you know what the specification should be? Well, you have to figure out what correctness means, or the requirements are. That's not really a question about computer science but rather a question about your application or your business domain and what problem you are trying to solve or what you're trying to do with the automaton.

If you're asking "what to verify", we can't answer that, because that's something you have to decide: you have to decide what properties you want to prove. It's like asking 'how do I prove the natural numbers?' You can't. You have to decide what theorem you want to prove, before you can ask how to prove it. If you ask a mathematician how to know what theorems to prove, the answer will probably be something like "well, you have to figure out what you want to know or what is interesting to know".

---
Tags: automata, proof-techniques, software-verification
---


title: How can segment be 60KB

text:
# Question
Title: How can segment be 60KB
I read that each segment is 64KB,but how? If you have address ABCD:EFGH , then 1 segment is 16B if it is addreses by bytes. How do they don't overlap? Example: 0000:0010 = 00010 0001:0000 = 00010 , is is same address.

# Answer
> 2 votes
In "real mode" on the x86, an address is 32 bits long. The higher 16 bits can be considered the segment address, while the lower 16 bits are the address within the segment. But it's a bit more complicated than having $2^{16}$ segments of $2^{16}$ addresses each.

If you have a 16-bit address, then you're able to address $2^{16} = 65,536$ different locations. If each of those is a byte, you have 65,536 bytes, or 64KB, of addressable memory. So a segment is *at most* 64KB long.

To get the actual address, the segment address is effectively shifted left by four bits, then added to the address within the segment. This does, as you've noted, mean that the addresses are not unique! The address 0x0000.00FF is the same as the address 0x000F.000F in this system. Segments can, and frequently do, overlap. And this isn't considered a problem, because in "real mode", there's no protection whatsoever. Segments are just a convenience; the CPU doesn't care if you want to write to opposite ends of memory in completely different segments.

This also limits the total amount of addressable memory to $2^{20}$ bytes, rather than the $2^{32}$ you would expect with an address of that length. But this is also by design: the 8086 has only 20 address pins. So despite the apparent clumsiness of this system, it ended up working out well.

---
Tags: operating-systems
---


# Question
Title: A fuzzy string matching algorithm for finding all occurrences from a set of strings in a large string
I have thousands of documents, and a term list with thousands of entries. The entries in the term list range in length from an acronym of two characters to a 14-word phrase with 96 characters. I would like to find every occurrence of any term in the term list in each document in the order that they appear.

I have created two test implementations so far: one using the Aho-Corasick algorithm and the other using n-gram matching. I tested them both on a medium-sized document (8 MB). The Aho-Corasick algorithm came up with over 8700 matches in 24 seconds. This would be great, except that I would like to use a fuzzy matching algorithm, and Aho-Corasick only finds exact matches. N-gram matching found 9600 matches, since some of them are approximate, but it took 885 seconds!

As such, I would like suggestions on an efficient fuzzy matching algorithm for finding matches from a set of strings. Is there any way to modify the current code I have for the Aho-Corasick algorithm so that it can take into account Levenshtein distance? I have found some other questions on this site that are related, but I didn't feel like they solved my problem. Thanks.

# Answer
One approach: Build a BK tree containing the terms in your term list. Given any word $w$, this lets you efficiently find the term that is closest to $w$ in Levenshtein edit distance.

Now the problem becomes easy. Do a linear scan over the document. For each word, look it up in the BK tree to find the closest match in your term list, and if it is close enough, output it.

Alternatively, you could read Peter Norvig's tutorial on spell checking, and the references he lists there, and try using that. They might be especially effective if your fuzzy matching only considers very small Levenshtein edit distance (e.g., distance 1 or 2).
> 1 votes

---
Tags: algorithms, string-matching
---


# Question
Title: Naive Bayes' Classification and Using the Entire Vocabulary in the Denominator
I am working through the NLP notes for Naive Bayes' classification here: https://web.stanford.edu/~jurafsky/slp3/6.pdf

Below $c$ is the class of the observation and $w\_i$ is the $i$th word of a text document.

In developing the maximum likelihood estimate for the conditional probability of the feature (word) $w\_i$ given class $c$ the following expression is given for the conditional probability:

$$\hat{P}(w\_i \mid c) = \frac{count(w\_i,c)}{\sum\_{w\in V} count(w,c)}$$

It is mentioned that $V$ consists of the union of all the word types in all classes, not just the words in one class $c$. The importance of this fact is stressed later on when add-one (Laplace) smoothing is used to avoid probability estimates that equal 0.

It is mentioned that:

**It is crucial that the vocabulary $V$ consists of the union of all the word types in all of the classes, not just the words in one class $c$ (try to convince yourself that this is true).**

I have thought for awhile on this aside given in the text, but it does not seem to make much sense. To me, wouldn't $count(w,c)$ always equal $0$ for any $w$ which is not contained in a document of class $c$? Why sum over all words in the vocabulary if they will just equal $0$?

# Answer
> 1 votes
If you're using Laplace smoothing, you'll replace the count with a "pseudocount", and that won't be zero. So, it *does* make a difference.

---
Tags: machine-learning, natural-language-processing
---


# Question
Title: How can I generate Rubik's cube algorithms equivalent to a given algorithm?
I am developing a computer program that solves the Rubik's cube. It is not anything advanced nor fast. It solves the cube by the Friedrich method, using algorithms that I use in real life to solve the cube. Because of that, the output solving algorithm is quite a long one and I was wondering is there is a way to transform the output to an equivalent algorithm, but shorter. This might actually be impossible, but I think this is a question worth asking. For example here is a list of equivalent algorithms that orient the corners of the last layer of that cube state shown in the image.

L.E.: Friedrich splits the solve in 4 steps(cross, inserting corners and their corresponding edges(F2L), orienting the last layer(OLL) and permuting the last layer(PLL)). So far my program only solves the cross, and I am now beginning to code the algorithms for the second step(F2L). All the algorithms I find online for F2L, OLL and PLL are designed to be remembered and/or executed as easily and naturally as possible, so they are not necessarily the shortest ones. Using Kociemba's program I can find shorter algorithms equivalent to those used by humans only for PLL, where the entire cube stays the same except for the edges and corners of the last layer. This is because Kociemba only gives the algorithms that leads to complete solve of the cube(and only for PLL we need this solution). For F2L for example I don't know what configurations I should put the cube in in order to output the algorithm that only inserts the desired pair(corner and edge) in the correct place and doesn't care about the cubies in the last layer, or the cubies in the other corners(that are not solved yet). I hope that makes sense. I make this program for a project for my Algorithms course, first year in CS and the requirements are that it must solve any given state of the 3x3x3 cube and output the shortest solution. I know group theory can be used, but it is much more complex and requires more time than I was given to finish the project, so I thought that Friedrich would be easier to achieve.

So far my outputs an algorithm for solving the cross that averages at 10 moves with a maximum of 19 in half turn metric. The execution time varies from 0.02 to 0.03 seconds per cube. This data was obtained from running the program on 1500 randomly generated cube states.

# Answer
### Solutions

Finding solutions of a Rubik's cube is infeasible by enumeration (BFS - too much space required), DFS takes too much time and does not guarantee the optimal solution, I highly doubt that optimal solution would be required.

There are at least three algorithms worth noting: Kociemba's algorithm, Thistlewaite's algorithm and Iterative deepening $A^\*$ (Korf's). Here is a methods comparison. Iterative deepening needs admissible heuristic, which for Rubik's cube is the sum of 3D Manhattan distances calculated separately for corners and cubies. Due to Korf, it also needs pattern database to achieve optimal solution in reasonable time.

### Algorithm Optimization

For optimizing any given algorithm all above will work in reasonable time, including BFS for short algorithms. To make small number of turns in overall solution the structured system should yield low number of turns in average, Friedrich method is mainly used for manual solving with medium number of algorithms (more than 100 is huge number to learn at once, not that challenging to program), so instead of optimizing single steps it would be better to find system that scores better. For example ZBLL method with 493 algorithms (including mirrors) with average about 40 turns, Friedrich scores about 56.

### Solving Between States

This step is inevitable: the modification of the stop condition in the search tree - at some point while processing partial algorithm the stop condition should be changed to check only target pieces and already solved ones. There is no good way to mitigate this effect, at initial phases enumerating all possible permutations of the cube is too memory and time consuming. Searching for shorter algorithm without changed condition (via ready to use solver or own algorithm) will yield very long solution, because all pieces will be preserved e.g. the last layer while solving the middle layer. To really improve the overall score instead of shortening given moves it is far more valuable to implement look ahead (e.g. better last layer orientation while solving the second one, or increasing number of algorithms possibly merging phases together).

There is also Hamilton circuit for Rubik's cube with included graph for cosets - this is not a full solution, but still worth reading.
> 5 votes

# Answer
I'm aware that you said that you don't want to use group theory in your algorithm, but here's one option that can act as a *postprocessing* step, i.e. you can apply it to your output sequence without having to modify your algorithm:

Given a group presentation for the moves on the Rubix cube (i.e. a collection of elementary moves and the equations that hold between them), then you can use the utilities provided with the automatic groups software MAF to convert any sequence of moves into its unique minimal equivalent.

MAF even has an examples directory entitled rubik, which AFAIK might contain the move descriptions you need.

Don't be too discouraged by the apparent complexity of automatic groups. In outline, what you need to do is:

1. Find a group presentation corresponding to your elementary moves.
2. Use the MAF utilities to obtain a confluent rewriting system for your group.
3. Use this rewriting system to reduce your lengthy move sequence.
> 1 votes

# Answer
There are many ways to achieve the 3x3x3 solution other than just an alg list and pre-search databases. While Korf, Kociemba, et al have worked on the 3x3x3, our discussion board group has a 5x5x5 author whose software can solve a randomly scrambled 5x5x5 cube in 5 seconds or less and solve cubes of any size. We have another author whose solver produces solutions to random 5x5x5 scrambles in the 70-75 move range. And a third program can bruce force search into the quintillions of nodes using 100 GB+ hash tables for the 5x5x5. Many of the algorithms and techniques are discussed, with screen shots and example solves linked to a 3D cube replay. Visit http://cubesolvingprograms.freeforums.net/ for more information.
> 0 votes

---
Tags: algorithms, optimization
---


title: DRAM write operation

text:
# Question
Title: DRAM write operation
In a typical read operation from a dram chip, all the banks are equipped with sense amplifiers which select one bit from each bank using column multiplexer. But how does write operation takes place? How does only one column in a bank is written in a particular row?

# Answer
> 1 votes
When reading the row then bits are amplified and sent back on the line as part of the feedback circuit. The bits are also stored in a small chunk of SRAM where they are cached for reads and writes.

writes to the rows don't happen immediately, only when unloading the data from the cache.

When unloading the cache the feedback circuit normally used to refresh the data is overridden with the new values in the row. All bits of the row are written.

---
Tags: computer-architecture, memory-hardware
---


# Question
Title: Will hardware/implementation affect the time/space complexity of algorithms?
I’m not even a CS student, so this might be a stupid question, but please bear with me...

In the pre-computer era, we can only implement an array data structure with something like an array of drawers. Since one have to locate the drawer with corresponding index before extracting the value from it, the time complexity of array lookup is $O(log(n))$, assuming binary search.

However, the invention of computers made a big difference. Modern computers can read from their RAM so fast that we now consider the time complexity of array lookup to be $O(1)$ (even it’s technically not the case, because it takes more time to move the register over a greater distance, etc)

Another example is Python dictionaries. While one might get a dictionary access complexity of $O(n)$ with an ill-written overloaded `__hash__` magic method (or ridiculously bad luck, i.e. keys having lots of hash collisions), it’s usually presumed to be $O(1)$. In this case, time complexity depends on both the hash table implementation of Python dictionaries, and the keys’ implementation of the hash functions.

Does this imply that hardware/implementation can affect the time complexity of algorithms? (While both examples are about data structures instead of algorithms, the latter are built on the former, and I've never heard of time complexity of data structures, so I'm using the term "algorithms" here)

To me, algorithms are abstract and conceptual, whose properties like time/space complexity shouldn’t be affected by whether they’re implemented in a specific way, but are they?

# Answer
> 44 votes
Sure. Certainly. Here's how to reconcile your discomfort.

When we analyze the running time of algorithms, we do it with respect to a particular model of computation. The model of computation specifies things like the time it takes to perform each basic operation (is an array lookup $O(\log n)$ time or $O(1)$ time?). The running time of the algorithm might depend on the model of computation.

Once you've picked a model of computation, the analysis of the algorithm is a purely abstract, conceptual, mathematical exercise that no longer depends on hardware.

However, in practice we usually want to pick a model of computation that reflects the reality of our hardware -- at least to a reasonable degree. So, if hardware changes, we might decide to analyze our algorithms under a different model of computation that is more appropriate to the new hardware. That is how the hardware can affect the running time.

The reason this is non-obvious is because, in introductory classes, we often don't talk about the model of computation. We just implicitly make some assumptions, without ever making them explicit. That's reasonable, for pedagogical purposes, but it has a cost -- it hides away this aspect of the analysis. Now you know.

# Answer
> 5 votes
I think there's a fundamental misunderstanding in the question. You compare a person finding an object in a sorted list (e.g., a specific page in a book, given its number) with a computer looking up an item from an array.

The reason that the former takes time $O(\log n)$ and the latter takes time $O(1)$ is *not* that the computer is so fast that it can do the binary search in the blink of an eye. Rather, it's because the computer doesn't use binary search at all. The computer has a mechanism to directly retrieve items from the array without searching. To retrieve the contents of an array cell, the computer just tells the memory controller the analog of "Give me page seventeen", the memory controller sets the voltages on the address wires to the binary representation of seventeen and the data comes back.

So, yes, the hardware (i.e., the model of computation) does affect the running time of algorithms, as D.W. explains, but that's not what your array access example seems to be based on.

# Answer
> 2 votes
No, the hardware doesn't affect the complexity of algorithms.

**But**, it does affect the choice of algorithm, and it can affect the usefulness of complexity analysis to a point where the analysis becomes pretty much meaningless (or merely of academic interest).

Finding the right drawer (as accessing an array element) uses the "open Nth element directly by index" algorithm, not the "search linearly" or "do binary search" algorithm. The algorithms are not changed, but the choice.

On the other hand side, complexity analysis itself, or rather its meaningfulness, *is affected* greatly by hardware.

Many algorithms that are stellar by their complexity analysis are poor performers or even useless in practice because the insignificant constant factor is not at all insignificant, but *dominating*.

Or, because assumptions that were once true (or mostly true) no longer hold. Such as, for example, every operation is mostly the same (only small constant differences that don't matter), or it doesn't make a difference which memory locations you access in which order. By complexity analysis, you may conclude that some algorithm is vastly superior because it only needs so and so many operations. In practice, you may find that each operation causes a guaranteed cache miss (or worse yet, page fault), which introduces a *k* that's so huge that it is no longer insignificant, but dominating everything.
If algorithm A takes 500 operations for processing a dataset of a given size and algorithm B takes only 5, but B causes 5 faults which burn twenty million cycles each, then despite what anaylsis or common sense may tell you, A is better.

This has lead to funny surprises such as e.g. in Cuckoo Hashing a few years ago. Which was vastly superior because \[long list of benefits\]. After the hype cooled, it turned out that it was vastly *inferior* because it *guaranteed* two cache misses (faults, for larger data sets) on every access.

Similar has happened to identifying and processing subsets of data. Often, the correct solution nowadays is: *"just do it all"*, i.e. instead of figuring out what you need to proess and do that, process the complete dataset linearly even if you maybe only need half of it. Because, believe it or not, that's faster due to no branch mispredictions, no cache misses, no page faults.
Need to read the first 8kB and the last 3kB of a 3MB file? Well, read the complete file, and throw away what you don't want, because seeking in between will be ten times slower than just reading the complete thing.

Use a map because it has logarithmic complexity? Or a hash table, which has constant access time? Constant sounds awesome. Well, for anything with fewer than a thousand or so things (depending on hardware, data size, and access pattern), a linear search may be just as good or better. Surprise.

So, it's not the *algorithms* per se that are affected, but their usefulness, and choice.

---
Tags: algorithms, algorithm-analysis, data-structures, runtime-analysis
---


# Question
Title: Bounds on probe lengths and number of rehashes with universal hashing
Say I have a family of hash functions that are weakly universal, i.e. the probability of two non-identical keys $x\neq y$ are mapped to the same hash-value is bounded by $k/m$ when I have $m$ bins and $k$ is some constant (I am mainly interested in $k=1$ and $k=2$):

$$\Pr\_h\left\[h(x)=h(y)\right\] \leq \frac{k}{m} $$

I have $n$ keys mapped to $m$ bin and I keep a constant bound on the load factor $n/m\leq \alpha$.

With this setup, I am interested in putting a bound on how many collisions I allow in any bin, $K$, and rehashing whenever I have to insert a key in a bin that already holds $K$ elements. For a given bound on the load factor, $\alpha$, and a given bound on the maximum elements in any bin, $K$, I am interested in knowing the probability of picking a hash function that puts less than $K$ elements in each bin.

This is a setup I am interested in for teaching purposes, and I am aware that there are smarter solutions to hash tables, but I would like to handle this setup before moving on to them. In my lecture notes, I have already described rehashing and just want to take this to a probabilistic analysis place, so I want to know the expected number of rehashes needed in this setup.

I would actually also love to know if I could put a bound on the probe length in open addressing hashing and rehash when I reach that, but I guess this is a much harder question.

I guess that if I can fix the probability of hitting any given bin more than $K$ times at a constant $p$, I have a strategy for sampling my way out of the problem, where I expect to rehash $1/p$ times if the number of keys, $n$, and the number of bins, $m$, are fixed. But if I add keys one at a time, resize when $n/m\>\alpha$, and rehash when I exceed the bound $K$ in any bin, do I have any guarantee that I will not have to rehash for every new element added after number $K+1$? I mean, my rehash could put $K$ elements in the largest bin and the next key could then trigger a rehash. An advisory, of course, cannot pick the keys so this happens, if I sample random functions, but do I have any probabilistic bounds that guarantee that I can rehash to keep probe-lengths bounded by a constant and still not rehash so often that I break the amortised constant running time on the table operations?

# Answer
This does not seem like a good example for teaching purposes, as there's no clean analysis or useful conclusions you can draw.

In particular, from only the assumption that you have a weakly universal hash function, you can't draw any useful conclusions about the probability of a having less than K items in the bucket. That would require some notion of K-wise independence. Weak universality is a weakened form of 2-wise independence, and if $K\>2$, it gives you no information about K-wise independence. In particular, the hash function could be arbitrarily bad, and the probability could be arbitrarily high. You need stronger assumptions about the hash function to do any useful analysis.

Instead of assuming weak universality, if you want to get a clean analysis, I suggest you assume that the hash function is (or behaves like) a random function, chosen uniformly at random from the set of all possible functions with that signature. Then the calculations get easy, since each output of the hash function is uniformly random and independent of all other outputs.
> 1 votes

---
Tags: hash, hash-tables
---


# Question
Title: No common terms between polynomials: an efficient check?
The "common term" would be in standard form, but the two input multivariate polynomials needn't be, e.g $x(1+y)+y$ and $y(x+a+b)$ have one common term, $xy$.

A brute force solution would be to expand both polynomials to standard form, then check for common terms. e.g. $x+xy+y$, $xy+ay+ab$.

Is there a better way?

**EDIT** if it makes it easier, we can loosen "same term" to allow different coefficients, so that e.g. $2xy$ and $3xy$ count as the "same term". (there must be a more mathy way to say that)... so, perhaps it becomes like a single component in Fourier analysis?

Maybe, a *specific* term could be identified by differentiating its factors by their power number of times to eliminate it (e.g. $x^2y^3$, differentiate by $x$ twice and by $y$ three times). Though, seems inefficient, and unclear how to extend that to checking *all* terms apart from brute force.

---

BTW "no common terms" is the opposite of "all terms in common" (in a sense), i.e checking for identical polynomials. This *does* have an efficient algorithm, using the *Schwartz-Zippel lemma* (see Is there an efficient algorithm for expression equivalence?).

# Answer
> 2 votes
Here is an approach that might occasionally be a bit better in practice, but is still exponential-time in the worst case, so it is not a satisfying answer to your question. Suppose we want to determine whether the polynomials $f(x,y,\dots),g(x,y,\dots)$ have a common term. First write

$$\begin{align\*} f(x,y,\dots) &= f\_0(y,\dots) + x f\_1(y,\dots)\\ g(x,y,\dots) &= g\_0(y,\dots) + x g\_1(y,\dots). \end{align\*}$$

Then recursively check whether $f\_0,g\_0$ have a common term; and check whether $f\_1,g\_1$ have a common term.

To express $f$ in that format, note that

$$f\_0(y,\dots) = f(0,y,\dots)$$

so it suffices to plug in $x=0$ into the expression for $f$ to get an expression for $f\_0$. Try to simplify that expression as much as possible using standard rules for simplifying polynomials. Then, you can write

$$f\_1(y,\dots) = (f(x,y,\dots) - f\_0(y,\dots))/x.$$

Simplify that expression as much as possible.

If no simplification is done, the running time is exponential in $n$, the number of variables. We obtain a recurrence of the form $T(n) = 2 T(n-1) + O(1)$, so the worst-case running time is exponential. The room for hope is that if simplification is done at each stage, it's possible that for some inputs this might be faster than that. In general it will still be exponential-time in the worst case, though, so I don't know whether this will actually be any better in practice.

---
Tags: complexity-theory, time-complexity, decision-problem, polynomials
---


# Question
Title: Capsule networks for classification with limited data
Capsule networks seem to match performance of convolutional neural networks on image classification tasks (more specifically on classification of handwritten digits in the MNIST dataset) .

I have also read in various articles that capsule networks require less training data than convolutional neural networks. Does this mean that a capsule network could reach the same accuracy as convolutional neural networks with less data? Eg. could a capsule network achieve the same accuracy as convolutional neural networks on the MNIST while only training on a fraction of the dataset?

# Answer
Actually, the literature so far suggests that convolutional networks have better accuracy than capsule networks on many tasks, so it's by no means clear that capsule networks are superior across the board to CNNs. This is perhaps not surprising; we have many years of experience working out how to engineer convolutional networks so we get the best possible performance out of them, whereas capsule networks are still new and haven't yet benefitted from that degree of engineering. So, we might see further improvements in the performance of capsule networks in the coming years, now that they are getting more attention.

There are some specific areas where capsule networks have significantly outperformed convolutional networks. Those seem to be primarily those where viewpoint invariance is especially critical. There are others where so far they are worse. For instance, capsule networks so far have done significantly worse than convolutional networks on CIFAR10. There is active research and an active debate in the machine learning community about how well capsule networks will perform. I think it's too early to say how that will pan out.

As far as amount of training data, it is likely that this will depend on the task as well, and is probably an open problem at this point. I would imagine that capsule networks might need significantly less training data for tasks where viewpoint invariance is especially central, but that might not be true across all tasks.

In general, not a lot is known yet about the performance of capsule networks, and the answer to most questions of the form "how well will capsule networks perform on X?" is "you'll have to try it and see".
> 1 votes

---
Tags: machine-learning, neural-networks, computer-vision
---


# Question
Title: Find the fastest duration for a certain distance in a walk
I apologize in advance if the wording of my problem is inappropriate for this forum. Or if another platform i more suitable for it. I'm new here and typically do not have to solve complex algorithmic problems.

I'm looking for an algorithm that is able to find a answer to the following question:

If I ran 10 km this morning, how can I find out how fast my fastest kilometer was? (=searching for duration of fastest km)

My "run" datastructure consists of a list of data records, where each entry contains the following information:

* timestamp in milliseconds
* distance since start in meter

The data structure is arranged chronologically.

I already got a pretty straight forward solution to the problem, but I guess I would end up with a poor performance on this one:

1. start with the last entry of the list (i=size) and stop if available / remaining distance data\[i\] is smaller than 1km
2. search backwards in the list and calculate the distance delta for each entry until the delta for the distance is \>= 1km OR (if we got a duration candidate from a previous iteration) the current calculated duration is already exceeding out current best.
3. if duration is too high start all over with i=i-1 until end condition is met
4. if a duration candidate is found remember this candidate decrease "i" and proceed with 1)

I really believe there must be an algorithm or better approach out there that can be applied to this question. Does anyone have an idea or can steer me in the right direction?

# Answer
I suggest you use exactly your algorithm, except use binary search during your binary search. You will want to store the events in an array rather than a linked list, to allow efficient random access into it. The total running time will be $O(n \log n)$, where $n$ is the number of events in your data structure. That seems quite reasonable, and this should be quite efficient in practice.
> 1 votes

# Answer
I'm not certain I understand your algorithm, but the "start all over" part makes it sound like it will take $O(n^2)$ time for $n$ data points, which starts to take a while once you have more than 10000 or so. You can solve this problem in linear time by "walking two pointers forward" (or backward):

1. Set bestTime to a huge time.
2. Set s to 1. s will be the index of the start of our "current interval".
3. Set e to 1. e will be the index of the end of our "current interval".
4. While dist\[e\] - dist\[s\] \< 1km:
    * Increment e.
5. At this point, we know that the index range s..e identifies a range of 1km. (Or possibly just over, but by the smallest possible amount -- we know that s..(e-1) is *shorter* than 1km.)
6. Is time\[e\] - time\[s\] \< bestTime?
    * If yes: We have a new fastest 1km interval. Set bestTime to time\[e\] - time\[s\], and set bestStart to s.
7. Increment s.
8. Go to 4.

The key idea is that, after we have finished dealing with the 1km interval starting at some index s (that is, at time time\[s\]), to find the endpoint of 1km interval starting at index s+1, we don't need to "start from scratch": We know it must end at or after the end of the interval that began at position s. Although any particular starting point s might require many iterations of step 4 to find its corresponding endpoint e, this actually isn't a problem, since *we never move e backwards*: this means that across the entire algorithm's execution, e is only ever incremented in step 4 at most $n$ times.
> 1 votes

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


# Question
Title: Removing conflicts of LR(1) parsing tables
```
S' -> S $

S -> I ; S
S -> return E ; S
S -> return I ; S
S -> ''

I -> id
I -> id = E
I -> id = I

E -> C && C
E -> C || C
E -> ! C
E -> C

C -> A > A
C -> A < A
C -> A >= A
C -> A <= A
C -> A == A
C -> A

A -> T A'
A'-> + T A'
A'-> - T A'
A'->''

T -> F T'
T'-> * F T'
T'-> / F T'
T'->''

F -> id
F -> const
F -> ( A )

```

This is supposed to be a LR(1) grammar, but its LR(1) parsing table have a conflict on the `;` symbol column: it has both a shift and a reduction transition. How this conflict can be removed?

# Answer
The ambiguity comes from

```
I -> id

```

because that rule means that both `I` ans `E` derive `id`, which in turn means that `return id` could be a derivation of either:

```
S -> return E ; S

```

or

```
S -> return I ; S

```

Also, `id1 = id2` could be derived from:

```
I -> id = E

```

or

```
I -> id = I

```

It doesn't make sense for `id` to be a statement if `id + 3` is not; I'd just drop the `I -> id` production.
> 0 votes

---
Tags: parsers, lr-k
---


# Question
Title: How to define the Atomic Propositions in Model Checking
The atomic propositions in Symbolic Model Checking form the state in the state-transition graph (the model $\mathcal{M}$ in Model Checking). The other part of Model Checking is the *specification*, which is usually some sort of temporal logic formula over the atomic propositions in the model.

My question is about the atomic propositions themselves. I have only seen a few rudimentary examples of them, such as $x = 20$ or $printer is busy$. These atomic propositions (I think) are stating a **fact** about the state of the program at that point in the system. You then use a temporal logic formula to see if the model holds under it. I am confused by how the atomic propositions are both *defined* and *used*.

First, how they are defined. I haven't seen anywhere a description on how you define these atomic propositions. That is my first question. I don't understand how stating $x \> 100$ in a state in the model $\mathcal{M}$ means anything. I didn't have to prove it or anything. It was just stated as fact. Then the temporal logic formula comes along and is checked against it, but there's some disconnect there for me. The value was never proven correct in the first place. It's as if, in my program, I make an HTTP request and during the waiting period before a response, my atomic proposition is that $\mathtt{the\ sky\ is\ blue}$. Wondering why was it put there, how do I know that it is true. A better atomic proposition would be $\mathtt{the\ request\ was\ sent}$. But again, I don't see how the program/model/checker "knows" this. I don't see what is doing the verification that that statement is true.

So my question is basically, how you define atomic propositions in Symbolic Model Checking. What goes into them. How you are allowed to make such statements that seemingly aren't verified. I don't see how I can say anything about the state of the program without something else "checking" that yes $\mathtt{the\ request\ was\ actually\ sent}$. I understand that *after* we define this model, we have our specification formulas and check them against the model. But we never checked the model itself for accuracy, is what I'm trying to get at.

I feel like, after writing down, in a specific state, an atomic proposition, I would then need to write a *unit test* to verify that it was true for some input. Not sure what I'm missing.

# Answer
Formal verification often involves at least three steps:

1. Make a formal model of the real-world system. (The formal model might be a state-transition graph or automaton, for example.)
2. Write down a specification that hopefully captures the real-world requirements.
3. Verify that the formal model of the system meets the specification.

Formal methods provides guarantees about step 3; if step 3 succeeds, then we know that the formal model meets the spec. It doesn't provide any guarantees about steps 1 or 2. If there is a bug in the model, that causes it to fail to accurately capture the behavior of the real-world system, then the result of the verification process becomes meaningless and all guarantees are off. So, you need some separate way to gain assurance in those steps.

The atomic propositions are part of that modelling process. Usually, there are some parts of the real-world system that we model in the state-transition graph and others that we don't. For instance, consider a traffic light. It has some sensors to sense presence of cars and pedestrians; some logic to determine what color light to show in each direction; and some actuators (light bulbs) to actually display those chosen colors. We might choose to model the logic in a formal model, and verify that the logic works properly. This verification process might not verify anything about the sensors or the actuators; it might just assume they are correct. That might be justified if, for instance, we think the logic is the part that is most likely to have subtle errors. Then you might have an atomic proposition for "sensor #1 detected a pedestrian at such-and-such cross-walk" ($p\_1$) and an atomic proposition for "turn on the green light facing in the N direction" ($q\_N$). Those atomic propositions represent the inputs or outputs to the logic, or facts about the state of the system. The spec then has to be stated in terms of the atomic propositions, e.g., "it should be impossible to have the green light turned on in the N direction and in the E direction" ($G (\neg q\_N \lor \neg q\_E)$).
> 3 votes

---
Tags: propositional-logic, model-checking, software-verification
---


# Question
Title: What is the difference (if any) between transition systems and finite automata?
is there any difference between transition systems and finite automata? Is it that transition systems consist of both NFA (nondeterministic finite automata) and DFA (deterministic finite automata)?

# Answer
Yes, did you try wikipedia?

To quote the second paragraph \[in transition systems\]:

> * The set of states is not necessarily finite, or even countable.
> * The set of transitions is not necessarily finite, or even countable.
> * No "start" state or "final" states are given.
> 5 votes

# Answer
The difference is mainly that automata are a model of *machines/programs/..* while transition systems are a model of machine/program/..'s *behaviour*. So one does not have the same questions and requirements for them.

You are right in thinking that they look the same: some version of directed graphs decorated in some way. However, what is important in mathematics (as in object-oriented programming) is not the objects themselves but the operations they support.

Imagine asking what is the difference between points in $\mathbb{R}^3$ and vectors in $\mathbb{R}^3$? They both are triples of numbers, no? Well, yes but this is not the point. Vectors are displacements so it is meaningful to add them, scale them. Points cannot be added meaningfully. They can be subtracted, as in $B - A$. BTW, this gives you a vector, hence $B-A$ is usually denoted $\vec{AB}$.
> 2 votes

# Answer
What you probably mean by transition system is a Kripke structure Basically you can call any directed graph with labeled vertices a transition system.
But finite automaton is a concept and includes any language deciding machine with finite memory. DFA and NFA are specified kinds of finite automaton and they can decide all the languages decidable by any other kind of finite automaton.
DFA and NFA are like transition systems with additional constraints:
In both cases:
\- Edges should be labeled by the members of the alphabet
\- A start state should be specified
\- A set of final states should be picked
In DFA only
\- Each state should have exactly one outward transition for every member of the alphabet
> 2 votes

# Answer
Another note, in transition systems the state is often a *set of variables* (atomic propositions, boolean vectors, etc.). Whereas in automata the state is almost always a *label* (a simple identifier such as a name or an integer or an id type of thing). The state doesn't *contain* anything in automata, whereas it does in transition systems.
> 0 votes

---
Tags: terminology, automata, finite-automata, transition-systems
---


title: Character in Huffman encoding

text:
# Question
Title: Character in Huffman encoding
Is a full stop regarded as a character along or must it be with a space in huffman encoding. I know of taking a comma with a space to a character.

# Answer
Huffman coding works with any character set.
> 1 votes

---
Tags: data-compression
---


# Question
Title: What exactly is Symbolic Model Checking?
I know that Symbolic Model Checking is state space traversal based on representations of states sets and transition relations as formulas like in CTL using models like Kripke Model. I know the theory. But I'm finding it hard to understand the actual application. Where exactly is it used? What exactly does it do and how does it work?

Can someone explain with a real example and relate theory to practice?

# Answer
Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs).

The question is what do they do and how do they work.

You first have your source code for some application. You then transform your source code into some state-transition graph like a Kripke Structure. The states are filled with atomic propositions which describe what is true in that particular state. In Symbolic Model Checking the atomic propositions are encoded as OBDDs to save on space and improve performance.

The Model Checker then starts at some initial state, and explores the states, looking for errors in the state-transition graph. If it finds an error it will often generate a test case demonstrating the error. It uses the symbolic OBDDs to somewhat optimally navigate the state space. Wish I could explain more there but still learning.

But that's basically it. You have a program converted into a formal model (state-transition graph), and then you use symbolic optimizations to navigate the state space to look for errors (by comparing it against an LTL/CTL specification). And if an error is found, the Model Checker gives you some stuff to help document and solve it.
> 5 votes

# Answer
Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example:

* A symbolic model of an OAUTH2 implementation could help check for unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process.
* A symbolic model of a cryptographic protocol, such as a TLS handshake, could help verify that the cryptographic design doesn't have any unintended consequences.

This works by writing a symbolic description of all the primitive functions and protocol algorithms, and then having a symbolic model checker, such as ProVerif, traverse the state space and attempt to detect state combinations that produce unfavorable results. In the case of ProVerif, symbolic models are described using the applied Pi calculus as the modeling language. This allows the description of protocols in a functional, ML-like syntax.
> 6 votes

---
Tags: formal-methods, model-checking, software-verification
---


# Question
Title: Does the undecidability of the halting problem require Turing Machines to be enumerable?
I (think I) understand the enumeration and then diagonalization proof of the undecidability of the halting problem, but I came cross this proof in SICP below, which does not seem to require the enumeration. Did I miss anything?

```
(define (run-forever) (run-forever))

(define (try p)
  (if (halts? p p)
      (run-forever)
      'halted))

```

I suspect this has to do with how a TM is encoded, i.e. the parameter for `try`. Being able to encode a TM might require enumeration? But I'm still very confused.

# Answer
**No, being able to enumerate Turing machines is not directly relevant.**

Let us consider some abstract notion of *algorithm.* The ingredients for the undecidability are as follows:

1. The Halting problem makes sense. This means that

a) Algorithms can "halt" on some inputs, and fail to "halt" on others. Halting allows the algorithm to output something, eg "Yes" and "No".

b) Algorithms can take algorithms as input.
2. Algorithms allow if-then-else branching
3. There is an algorithm that takes an algorithm as input, and simulates how the input-algorithm would act.

The code snippet in the question is essentially how you do it, and the criteria above are essentially saying "this code snippet is valid pseudoc-code for our abstract notion of algorithm".

To see that the fact that TMs can be enumerated really does not factor in, one can look at models of computation such as the BSS-machines. These can have arbitary real numbers as parameters in the code, so there are uncountably many machines. However, they still meet all criteria above, and thus the standard argument shows that BSS-machines cannot decide the BSS-Halting problem.
> 1 votes

# Answer
## Yes, but it's been proven that Turing machines are enumerable.

All proofs of the Halting Problem depend on the ability for one Turing machine to simulate another. This requires the ability to encode a Turing machine into a string in the tape language of another Turing machine. And since strings are proven to be enumerable, if Turing machines *aren't* enumerable, then they can't be losslessly converted into strings in this way (since it would provide an enumeration).

However, formally speaking, a Turing machine is simply a 7-tuple of sets, symbols, and functions. All of these are enumerable, and tuples of enumerable types are enumerable. Therefore Turing machines are enumerable.

This is generally considered a good thing, because it means that the encoding into strings is possible, which means we can have universal Turing machines, which means we can have Turing completeness.
> 0 votes

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


# Question
Title: How often is Prolog/ASP used in non-research areas?
I've just recently found out about KRR (Knowledge representation and Reasoning) and ASP, not hearing a thing about them before (except a bit about prolog). I've read a bit about them and one of their primary usage seems to be AIs.

My question would be how widely used ASP or other declarative languages are, is there some frequently used program using them (like search engines?) or is it mostly for research purposes? What may be the reason they are not so well known? Is it because AI-development belongs to a more "advanced level" of programming?

# Answer
> 4 votes
> how widely used ASP or other declarative languages are

You can see the activity of Prolog which I think is the most common ASP programming language:

Just based on that, Prolog's top package is (483 / 139,326) x 100 = **0.35%** as popular as one of Node.js's large packages. Or **0.07%** as many packages.

> is it mostly for research purposes

IMO yes, it is mostly for research purposes. But it is similar to Ocaml, which from my experience was mostly for research purposes until corporate users like Facebook published Flow (typed JavaScript programming), and others published Coq (automated theorem proving), which helped bring Ocaml to the mainstream.

> What may be the reason they are not so well known?

IMO Prolog is not used because it is (a) a different paradigm, (b) the package manager isn't up to par (this is a big deal these days), and (c) there is no *evangelized* web framework. If there was a good package manager like NPM for Node.js, and there was a web framework that was marketed, as well as a small group of evangelists, that would help bring it to the mainstream. Ruby had 37signals and Rails, Python had Google, etc.

> Is it because AI-development belongs to a more "advanced level" of programming?

No not really. Some AI research uses prolog for modeling stuff, but it is not a requirement for AI. AI could be divided into two parts: (1) Machine learning / probabilistic-based models where the relations are learned and not well-defined, and then (2) manually defined models. Most AI is a mixture of both, but the manually defined models are valuable and kept private for the most part. The manually defined models could be defined using Prolog, and there are a few papers out there for doing that, but it is not necessary. To summarize, all AI work can be done in regular programming languages, just that Prolog might make it slightly more compact to write in some cases.

# Answer
> 3 votes
Read about AI winters and more on the history of AI.

In the 1980s, symbolic AI was dominant. In that time, expert systems proliferated. Many of them have been coded in Prolog.

Today, we still have (in some areas) business rules systems and business rules engines, and the business rules approach used in business rule management systems, which IMHO are the direct successors of expert systems from the 1980s. AFAIK, a lot of business oriented software is built on similar principles. I believe that many credit (or insurance) decisions are made today automatically (and daily) in banks with such systems. Rewriting systems like XSLT are also in daily use, and are descendants of 1980's expert systems ideas. Declarative programming (including CLIPS or even make or other rule-based systems) can be viewed as the dissolution of symbolic AI ideas in the general programming and software industry (as soon as something becomes "easy" and "widespread" it cannot be called AI anymore).

Today, AI is reduced to machine learning approaches (including neural computing). What (broadly) was called AI before the 1980s is currently called AGI.

The next AI winter might be some abstract interpretation winter. Abstract Interpretation is a theory and mindset about static program analysis. Today, that AI has become a buzzword, and is sometimes presented as the solution to most software safety concerns (which IMHO it is not).

Some persons (including me) believes that symbolic AI is not entirely dead (at least when combined with other paradigms). An interesting view is that of Jacques Pitrat (a retired researcher and French AI pioneer) in his blog.

But AI (both as "artificial intelligence" as defined in Dartmouth 1956 and as "advanced informatics") systems are hard to build. Many years of effort are needed to develop them. Remember Brook's insight: "while it takes one woman nine months to make one baby, nine women can't make a baby in one month". This is true for complex and challenging software systems (which might need nine years to be completed, but we live in a world which cannot afford paying a small team of talented software researchers for nine years). For social and economical reasons that I don't fully understand (but that I do deeply regret), software has no equivalent of large long term projects like ITER (and has not even small long-term research projects lasting more than 4 or 5 years with a dozen of researchers). See also the softwareheritage project, and notice that the software domain is today less creative, as a whole, than the many ideas that flourished in the 1980s. See Liam Proven's FOSDEM 2018 talk *The Circuit Less Traveled*

What was mostly called in the previous century (XXth century) AI is today called AGI. The *terminology* has changed, and the ambition is today nearly gone. These days, in the early 2020s, AI is mostly about neural networks and machine learning. My feeling in 2019 is that AI became a useless buzzword today (it is *no more* about ***A****rtificial* ***I****ntelligence*).

# Answer
> 2 votes
I just walked 354 students, mostly SE's, through installing SWI-Prolog. Had about a dozen install issues. Most found the process fairly easy.

I'll admit, if SWI-Prolog had 100x as many users the install would get more polished. But nobody is shying away because the install is too hard.

As for packs, to install a pack you query pack\_install(my\_pack).

That's *easier* than installing ruby gems.

Now, as to how often it's used in non-research areas - the d/l stats mean nothing a) because http://swi-prolog.org is served through a CDN (that we have to use multiple servers and a CDN says something), and b) we know the majority of users are undergrads taking a PL theory/survey course.

Commercial use is becoming more common. I've been writing just Prolog for a few years now, and I'm not an academic (sometimes I was working as a contractor for a university, but not as an academic, as an engineer).

Most of the applications are in AI or machine learning environments. Hard ML problems often benefit from an admixture of symbolic AI.

---
Tags: prolog
---


title: Context Free Grammar Exercise

text:
# Question
Title: Context Free Grammar Exercise
I'm studying Context free Grammar and I have a question to a specific Exercise:

Why is **i.** True? How is this possible?

# Answer
For every nonterminal $A$ it *always* holds that $A \Rightarrow^\* A$. This is because $\Rightarrow^\*$ is the *reflexive* transitive closure of $\Rightarrow$. In words, $A \Rightarrow^\* \alpha$ is $\alpha$ can be obtained from $A$ by applying *zero* or more productions.

The similar notation $\Rightarrow^+$ is the transitive closure of $\Rightarrow$, and corresponds to *one* or more productions. In your grammar, it isn't the case that $T \Rightarrow^+ T$.
> 2 votes

---
Tags: context-free
---


# Question
Title: An example of something you can formally verify with proofs in Software Development
I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques for formal verification include using type systems, model checking, automated theorem proving, proofs, and doing program derivation. Finally, there is testing, but I wont go into that here.

I have asked several questions regarding these topics:

The gist of the answers is essentially, **you can't apply formal proofs to realistic software applications**. This is a bit disappointing to hear, especially when there are projects such as CompCert, the "formally verified" C compiler. My first question is, what exactly they mean (in CompCert) by "formally verified". Wondering which of the following (or something different) this includes:

* Model Checking
* Formal Proofs (e.g. Hoare Logic)
* Type Theory
* Transition Systems
* Operational Semantics / Denotational Semantics

My second question is, what is a *realistic application* of proofs to formally verify software (i.e. a web application example, not a textbook example). After asking these questions, **I am discouraged that there are no applications of formal proofs to practical software development.**

At first I thought that using Coq I could somehow write "formal proofs" for my code, and walk away with a sense of confidence that my code was "formally verified". But now I don't know if that has any practical or realistic meaning. That was what I was getting at in How to prove a function returns a value, High-level requirements for a Proof of “Saving to the Database”, and How proofs can be applied to a simple logging function.

Then I imagined that perhaps Operational Semantics or Hoare Logic could help in "formally proving" the behavior of functions. But the gist of the answers was "it's too hard" or "it's impractical". Nevertheless, it seems that CompCert accomplished it (but not sure if they used Hoare Logic, Operational Semantics, or others), or maybe I am missing something. So what my sense is is **there is no use in Hoare Logic or Operational Semantics in practical software development**. I would like to be proven wrong on that.

I realize that Model Checking is a good candidate for matching a program model with a specification. But the question still remains, how you know that your model is correct in the first place. That is where it seems formal proofs or some other formal verification technique could shine somehow (which is what this question is about). Wondering how in practice you can apply *formal proofs* to software development. How to verify that your Model Checking model is correct. It seems the only answer is "formal proofs". But then the question is *how*. How to apply formal proofs to your model to verify it is correct. I've tried asking questions about it but have had no luck.

# Answer
> 7 votes
Look into tools like Frama-C, SPARK, Astrée, etc...

They have their use in very specific cases, notably software verification of small to medium sized embedded safety critical software (e.g. inside aircrafts, per DO-178C, or nuclear power plants, etc...). Such software have a few dozen thousands lines (or perhaps two hundred thousands at most of C or Ada code), but a bug inside them could crash a plane. So the industry is ready (and required by external regulations) to spend a lot of money and efforts on such small critical software. There are also many severe coding rules (e.g. dynamic allocation, recursive functions, dead code are forbidden).

**Proving software**, even with these tools, **is *very* costly**. A typical safety-critical software costs about a hundred or a thousand times more to develop than a usual software (like your phone applet or some Unix command line tool) of equivalent size, because formal methods (but not only them) are involved. The teams developing them should have formal methods experts working together with aircraft software experts. Sometimes, a small routine has to be rewritten and annotated to be processable by code provers.

There are several research projects around such tools and their use. For a recent example look into VESSEDIA (but you could find many others). One of its results might include a simple proof of a small subpart of the Contiki OS. From an outside view, the results are related to simple subsystems of it (e.g. some simply-linked-list module). In practice the proof requires a lot of formal annotations (so the developer has to provide annotations in ACSL about half as long as the *simple* C code that is specified by these annotations).

The L4 microkernel has also a variant, called seL4, which uses formal methods (the code size which is formally proved is a few dozen thousands of C code). AFAIU that variant (with its proof) is open-source.

But **formal methods don't scale well**. It is very unlikely that they would scale -in the next 20 or 30 years- (for present-day programming languages and code) to software as big as the Qt toolkit or the Linux kernel (because formally specifying the intended behavior of Qt or of Linux kernel is practically impossible). For example, C heap allocation is easy to code (that is, a lot of C code uses `malloc` & `free`), but difficult to formalize and prove (because current shape analysis techniques don't scale well to large programs). That internal complexity and difficult of formal methods hinders its uses in real-world programs (whose size is growing a lot: a source code editor today is much more complex and bigger than what `vi` was in the 1980s).

I was part of several research grant submissions mixing more or less formal methods and other approaches (e.g. machine learning techniques on large amount of code, natural language processing techniques), but such funding is hard to get (e.g. there is probably no more any H2020 or FP9 calls dedicated to software engineering before my retirement; the last one was ICT-16 to which I was part of a submission -and waiting (in june 2018) for its evaluation; but only a few percents of submitted proposals get funding). See also this answer to another (but indirectly related) question. BTW, I might be interested in joining some European consortia in 2019 for HPC software tooling using such ideas.

To summarize: **There is *No silver bullet***, so I agree with you:

> there is no use in Hoare Logic or Operational Semantics in practical software development

(because even if you have proven your code w.r.t. some explicit formal specifications, there could be - and there still is some - "bugs" or incompleteness in the formal specifications; specifying "correctly" what a real-life software such as a word processor or some web application should do is practically impossible, since you want that specification to be "complete" and cover all the practical cases).

However, notice that recent practical programming languages (e.g. Rust, Ocaml, and also monsters like C++20 or C++17 which became so complex that only a dozen of people understands them fully) have been inspired by formal proof techniques. And academic curiosities like Agda uses even more them. Also, static source code analyzers like clang-analyzer (and even some optimization passes of GCC) use techniques related to formal proofs.

Regarding CompCert, you could download its source code (and proof) and study its code, but you are not allowed to use that source code for non-academic purposes (so CompCert is not free software but its source code is downloadable and you are allowed to study and experiment it. However the resulting binary has license restrictions).

See also this draft report (and the references there).

NB. Seeking partners interested by RefPerSys

# Answer
> 6 votes
Quite a lot of things can and have been formally verified with formal methods.

1. Compilers. We want to prove that a compiler preserves the semantics of its source program. For example, if we write a `int x = 3; x++;` in C, we mean that. But the compiler might not produce correct assembly and machine code.

It is known to be difficult to debug compilers, so a bunch of people at INRIA, the French national lab for computer science, led by Xavier Leroy, decided to start from scratch and write a C compiler that is provably correct. Eventually, they produced CompCert, which has since been used commercially by companies like Airbus to compile important software.

There have also been certified compilers for other languages. One of such exists for ML (CakeML). I would not surprised to find more.

**Note**: According to @BasileStarynkevitch, CompCert has been used for purposes related to aviation, but it is not sure if Airbus is using it to compile on-plane software as of June 2018. According to Xavier Leroy (via personal communication to Basile), last year Airbus was still considering this as a possibility. But at least it has been used for *something*.
2. Operating system kernels. Operating system kernels are also hard to debug, and can be pretty nasty if there's a bug (it stops the entire machine!). If you run into a OS kernel bug on a satellite, it wouldn't be a very good day for you. So, a bunch of researchers in Australia wrote an operational specification for an OS kernel. Then, they developed a kernel according to that specification and proved it free of bugs (e.g., deadlocks, livelocks, overflows...). Of course, the spec is assumed to be correct. That became the seL4 kernel.

For follow-up on this work, see HACMS (a project which developed a verified drone based on seL4) and CertiKOS (a project which developed a layered, POSIX, concurrent OS kernel).
3. An example closer to us. Part of the control software running on the Paris Metro Line 14 is formally verified using the B-Method. Later, the B-Method was also used on Line 1 when it was automated. The French people really like formal methods!

Of course, most software would be too costly to verify. I doubt anyone would want to fully verify a browser or a word processor, as they don't matter all that much (if they crash, just restart!). But if your software is running on an airplane or a train carrying a hundreds of people and tasked with operating the vehicle, it would be reasonable to want to verify that.

Hoare logic and/or operational semantics *per se* might not be that useful in software development, but they are important theoretical and/or intellectual foundations of useful verification methods. Therefore, they're still important to have a sound grasp and understanding of those tools. I believe it wouldn't be an exaggeration to state that every software verification expert (or quasi-expert) has a good understanding of Hoare logic and operational semantics!

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


# Question
Title: Why does the Pumping-lemma for context-free languages use uvwxy, but the one for regular ones uvw?
Basically what the title says. Why can you "ignore" the "xy" part if you want to prove whether a language is regular?

# Answer
> 13 votes
Both pumping lemmas have an intuitive explanation in terms of an automaton that can recognize a language.

A regular language can be recognized by a finite automaton. All words are recognized through:

* either a finite path through the automaton: words that are shorter than the pumping length;
* or a path that goes through a node at which there is a loop, in which case it is possible to go through the loop any number of times: that's the $y^n$ part, where $y$ is the path through one round of the loop and $n$ is the number of lops.

A context-free language can be recognized by a pushdown automaton. All words are recognized through:

* either a finite path through the automaton: words that are shorter than the pumping length;
* or a path that includes both a loop with pushes to the stack, and another loop with corresponding pops. Pushes and pops have to balance in order to get an empty stack at the end. Then the word contains a loop with pushes $v$, some further path $w$, and a loop with pops $x$. The number of runs through the two loops has to be the same, but it can be any number, hence the middle bit $v^n w x^n$.

You can also get a similar intuition from the ways regular and context-free languages can be specified by a regular expression and a context-free grammar respectively.

If a word is recognized by a regular expression, then:

* either the word does use a part of the expression under the $^\*$ (Kleene star) operator, and that part $y$ can be repeated any number of times;
* or the word doesn't use any part of the expression under a star, and it can't be longer than the expression itself.

If a word is recognized by a context-free grammar, then:

* It may be that the word is recognized by a parse tree where there is a subtree $\mathcal{T}\_1$ which is recognized by the nonterminal $A$, and a subtree $\mathcal{T}\_0$ of that subtree is recognized by the same nonterminal $A$. In that case, let $w$ be the part of the word that is recognized by $\mathcal{T}\_0$ and $vwx$ be the part that is recognized by $\mathcal{T}\_1$. You also get a valid parse tree if you replace $\mathcal{T}\_1$ by $\mathcal{T}\_0$ or vice versa. Furthermore, since $\mathcal{T}\_1$ contains $\mathcal{T}\_0$, after replacing $\mathcal{T}\_0$ by $\mathcal{T}\_1$, you can replace the copy of $\mathcal{T}\_0$ inside $\mathcal{T}\_1$ by $\mathcal{T}\_1$, and so on. This means that you can replace $vwx$ by $w$, $v^2wx^2$, $v^3wx^3$, etc. and still get a word with a valid parse tree.
* Otherwise, there is no subtree of the parse tree which reuses the same nonterminal, and in that case the length of the word is bounded because the depth of the parse tree is bounded by the number of nonterminals in the grammar.

# Answer
> 6 votes
That is because of the "structure" of the languages that is observed by the respective pumping lemma's. Have a look at the proofs of the respective pumping results.

For regular languages the structure is linear, and for every long word there is a state that is repeated twice in the accepting computation of a finite state automaton. The string read between these states can be repeated.

The structure of context-free languages is nested, tree-like. Again a long word will have a derivation tree that repeats a nonterminal on one of the paths in the tree. This structure also can be repeated, but will generate two strings, both to the left and right.

# Answer
> 4 votes
The pumping lemma for context-free languages is, at heart, an application of the pigeonhole principle. If we take any long enough word in the language and consider one of its parse trees, there will be a path in which one of the nonterminals repeats. This will allow us to "pump" part of the word, by a cut and paste process.

As an example, consider the following parse tree:

The repeating nonterminal is $A$. We can eliminate the repetition to obtain the parse tree:

We can also "pump" the repetition to obtain the parse tree:

In terms of the words themselves, we started with the word $sabacabas$, and obtained first the word $sacas$ and then the word $sababacababas$.

Pumping corresponds to varying the number of applications of the derivation $A \Rightarrow^\* abAba$. You can see that two different parts are being pumped at the same time. This is necessary for languages like $\\{a^n b^n : n \geq 0\\}$: the $a$ and $b$ parts need to be pumped separately.

Consider now what happens when we apply the same arguments to a *left regular* grammar:

Since the grammar is left regular, the pumped derivation $A \Rightarrow^\* abA$ only contains one pumped part. This will always be the case for left regular grammars, due to the form of the parse trees.

In terms of the decomposition $uvwxy$, this implies that $x = \epsilon$, and so $uv^iwx^iy = uv^iwy$, which is exactly the form of the pumping lemma for regular languages (considering $wy$ as a single word). The particular shape of the parse trees in left regular grammars enables us to obtain a stronger pumping lemma.

*Credit: all parse trees drawn using Syntax Tree Generator.*

---
Tags: regular-languages, pumping-lemma, chomsky-hierarchy
---


# Question
Title: Improvement Heuristics for Asymmetric TSP
i have been solving the Time-Dependent Traveling Salesman Problem using an Ant Colony Optimization. Upon reading the ACO papers, there are several reminders which state that ACO performs best with daemon actions - improvement heuristics.

In the classical TSP, the most common improvement heuristic used is the k-opt exchange, which works particularly well because one does not need to calculate the whole solution cost, but only differentials on the updated solution.

When the problem is assymetric (which is the case for the time-dependent variation), this is not the case.

I wonder if there are usefull improvement heuristics which can be used as daemon actions to the Assymetric/time-dependent TSP.

I already did some research on this subject, but found no interesting material.

# Answer
> 1 votes
I have the exact same doubt now, so, I found your question because I did a heavy research about this theme and didn't find any good direction yet. As you, I'm currently working on TSP and VRP variations and solving it by the Ant's Colony Optimization Method.

I have an instance of 16 cities to be visited, one origin and one destination, I optimized it using pure ant's algorithms and the best result I got was 557 km, by comparation the nearest neighboor algorithm found 586 km as a result, however, I notice that the ant's algorithms aren't precise, sometimes it returns a very bad result, better than the nearest neighboor though. But I wasn't satified with this drawback, and I started to read about heuristics (daemons actions) to be coupled with the ant's algorithms, then It is very interesting that all of them assume that we are working with a symmetric matrix, but real problems are hardly symmetric.

I first tried to apply the 2-opt heuristic, because I read that it is fast and give a good result, so it suits for a real application that an user waits to get the answer as fast as possible and as good as possible. But latter I saw that the step of 2-opt which reverses a path when exchange edges is guaranteed only when working with symmetric matrices...

Well, After all, I applied a very simple heuristic, that I don't know the name yet, but I saw some comments that it is not a good solution (because doesn't solve the crossed arcs problem and may create more of them), even though, it helps me to provide better solutions and also more precise, as an example, the instance I told about above, it gives the result of 554 km almost all the time.

The heuristic I applied does this job: After the ACO build a solution, I refine it by exchange cities (in other words, exchange vertex or nodes), if it improves the solution, I save this new solution and continue the process of exchanging cities, using the new solution constructed until I reach the solution's vector length.

For example, if I have the following path as a solution given by the ACO:

A -\> B -\> C -\> D -\> E -\> F

the heuristic moves B ahead in the path, for example:

A - \> C -\> B...

then:

A -\> D -\> C -\> B -\> E -\> F

if it finds a better solution, for example, let's suppose the above solution is an improvement, then it continues moving the city in the second position in the solution vector:

A - \> E -\> C -\> B-\> D-\> F

Then, it starts the same procedure to the third position city...

I'd like to add that the solution which updates the pheromone matrix is the solution built by the ACO and improved by this heuristic.

As I experienced, the ACO does a pretty good job creating solutions with very few crossed arcs, because this the heuristic applied is working fine, and as we are working with asymmetric matrix I think that it is possible to crossed arcs being better paths than paths without any crossed arc... But It is just my feeling, actually, I analyzed the solutions above only by the value of route's length in kilometer, but I did not plot them yet to see how they look like.

Well, I hope to help you with these informations, and if you have find any nice heuristic to couple with the ACO as a daemon action, keep me posted!

---
Tags: np-hard, heuristics, traveling-salesman
---


# Question
Title: Why is my own implementation of Bubble Sort so much slower than another one I found online?
I wrote my implementation of Bubble Sort according to my understanding of the general principle of how the algorithm works, and then compared it against another implementation I found online.

```
def my_bubble_sort(n):
    switched = True
    while switched:
        switched = False
        for i in range(1, len(n)):
            if n[i] < n[i - 1]:
                switched = True
                n[i - 1], n[i] = n[i], n[i - 1]
    return n

def some_other_bubble_sort(n):
    for i in range(len(n) - 1):
        for j in range(len(n) - 1 - i):
            if n[j] > n[j + 1]:
                n[j], n[j + 1] = n[j + 1], n[j]
    return n

```

While `my_bubble_sort()` is **much** faster on processing lists that are already sorted, `some_other_bubble_sort()` is almost three times faster (= takes 35% of the time) compared to `my_bubble_sort()` on actually random, unsorted lists.

I'm not sure why that is. Can anyone help me understand?

It can't be the additional checks against `switched` that make my implementation that much slower, can it?

**Pastebin link**

I also found that my version seems to be fairly close to **the one taught at this MIT lecture**.

Which one is generally preferable? Are they both valid implementations of `bubble sort`? Or is either of the two technically another sorting algorithm?

And which one would be preferable, generally speaking?

# Answer
From your pastebin, here is the first place you go wrong:

```
unsorted1 = unsorted2 = [randint(1, 99) for _ in range(count)][:]

```

Here you assign `unsorted1` and `unsorted2` to point to the same list. So when you call `some_other_bubble_sort` on `unsorted2`, it is in fact no longer shuffled! It is sorted.

The solution is to first assign `unsorted1` and then `unsorted2` to a copy:

```
unsorted1 = [randint(1, 99) for _ in range(count)]
unsorted2 = unsorted1[:]

```

That makes your algorithm only slightly less than twice as slow. That can be explained simply by the fact your implementation does a lot more stuff. In Python the little things add up, like setting `switched` to `True` every iteration.
> 3 votes

---
Tags: complexity-theory, algorithm-analysis, sorting
---


# Question
Title: Finding the smallest positive missing number in array of integers contains negative and duplicates number
I found this solution but I don't understand it. Can anyone explain the idea behind it ?

the solution:

> **A O(n) time and O(1) extra space solution:**
> The idea is similar to this post. We use array elements as index. To mark presence of an element x, we change the value at the index x to negative. But this approach doesn’t work if there are non-positive (-ve and 0) numbers. So we segregate positive from negative numbers as first step and then apply the approach.
>
> Following is the two step algorithm.
>
> 1. Segregate positive numbers from others i.e., move all non-positive numbers to left side. In the following code, segregate() function does this part.
> 2. Now we can ignore non-positive elements and consider only the part of array which contains all positive elements. We traverse the array containing all positive numbers and to mark presence of an element x, we change the sign of value at index x to negative. We traverse the array again and print the first index which has positive value.

# Answer
The solution has two parts. The first part filters out all non-positive numbers - this can be done in-place using the *partition* subroutine of quicksort.

After the first part, we have an array $A\[1\],\ldots,A\[n\]$ of positive numbers, and we want to find the smallest positive integer which is not present. We create a new Boolean array $B\[1\],\ldots,B\[n\]$ initialized to *false*. We go over all elements in $A$, and whenever we find an element $i \leq n$, we set $B\[i\]$ to *true*. We then find the smallest index $i$ such that $B\[i\]$ is *false* \- this is the smallest positive integer which is not present. If all elements of $B$ are true, then $n+1$ is the smallest positive integer not present (why?).

As an optimization, we store the array $B$ by modulating the *sign* of elements in $A$: to represent $B\[i\]$ being *false* we use a positive sign for $A\[i\]$, and to represent $B\[i\]$ being *true* we use a negative sign for $A\[i\]$.
> 1 votes

---
Tags: algorithms, arrays
---


# Question
Title: Does O(f(n)) + O(g(n)) = O(max{f(n), g(n)})?
A question from a lecture of mine. The way I see it, while summing sets is meaningless, O(f(n)) + O(g(n)) is obviously limited from above by the greatest function in either, which means that I practically take the maximum of O(f(n)) and the maximum O(g(n)), and claim that either is the maximal one, or they are equal.

Would this be a legitimate claim in an exam?

# Answer
> 1 votes
One way to read this "identity" is as follows:

> If $a = O(f(n))$ and $b = O(g(n))$ then $a+b = O(\max\\{f(n),g(n)\\})$.

This indeed holds, as you can prove using the definition of big O.

There is another possible interpretation:

> $\\{ a + b : a = O(f(n)), \\; b = O(g(n)) \\} = \\{ c : c = O(\max\\{f(n),g(n)\\})\\}$.

This also holds, as you van prove using the definition.

Whether it is a *legitimate claim in an exam* is up to your professor. It is definitely a legitimate claim in a paper.

---
Tags: asymptotics
---


# Question
Title: Potential General Model of Computation with Physics?
I posted a question about a month back regarding the significance of Turing machines (relative to other models of computation). In that post, I mentioned vaguely some conversion between an input string and a physical system as a model of computation. (I just got my BS in CS, so it's likely I have no idea what I'm talking about.)

Would the following be a valid, or at least meaningful, general model of computation:

Let $ f: Z \mapsto Z$ be a function. Then, $f$ is computable iff for all integers $a$, there exists a bijection $P$ from the integers to formal physical systems (Classical mechanics?), such that when $P(a)$ is "set into motion", it reaches and equilibrium or static state $s$ where $P^{-1}(s) = f(a)$.

If this makes sense, please let me know.

# Answer
> 2 votes
It would be meaningful, if you properly defined "formal physical system", "set in motion", and so on, in a mathematical way. Pretty much anything can be made meaningful in mathematics (which is what this sort of theoretical computer science really is).

The question is, *is it useful*?

It would seem that the functions computable by Turing machines are a subset of this new class, since you can make a Turing-complete physical computer with enough rolling marbles. (Or, if you allow transistors in your "formal physical systems", I could just use "my laptop at the moment when I run this Python code" as the system.)

Then, are there things your physical systems can do that Turing machines can't? Given that a Turing machine can simulate classical mechanics to arbitrary precision, given enough time and memory, I'm inclined to say no.

Finally, are your physical systems easier to work with mathematically? The answer seems like a pretty solid "no", given how much calculus is involved in classical mechanics, compared to the simple state-machine-plus-memory of a Turing machine.

So while you could in theory use physical systems to define computability, there doesn't seem to be an advantage to doing it this way.

---
Tags: turing-machines, computation-models, physics
---


# Question
Title: What are the general applications of Computer Science in the field of Psychology?
I am keenly interested to do a project in Computer Science that can aid to address the problems in the field of Psychology. Now I want to know what are the most general and research-oriented issues or problems areas in Psychology that can be solved through computation or at least aid to be solved via Computer Science. Looking for authentic answers. Thank you

# Answer
Here are some of the areas that intuitively come into my mind where Computer Science and Psychology can go along together. As a student of Computer Science, one has to study the following core subjects at the undergrad level that are either directly or indirectly related to Psychology:

***1. Data Structures and Algorithms:*** All the data structures do exist in the real world and the human mind perceives them to store, arrange, sort and search the required data as per their strength and limitation. Now the question arises, could there be a data structure or algorithm that is beyond the perception and capacity of human mind? Perhaps certainly or maybe.

***2. Design and Analysis of Algorithms:*** Could there be a general algorithm for curing a mental disease, achieving happiness, finding love or the best match, finding career, overcome stress or depression, defeating a rival, rehabilitating a heroine addict or leading a "perfect life"? All of such aspects of human life can be addressed computationally. And yes the answers to these questions are indeed subjective and debatable as well.

***3. Artificial Intelligence:*** Can we ever have machines more intelligent than humans? Oh yes, we certainly have such intelligent machines. But do such machines recognize vision and pattern as we humans do? That is an area of continuous research in Computer Science.

***4. Human Computer Interaction:*** In the modern world, humans do interact with computers almost on a daily basis. Commercial hardware, software applications and games, all of them are designed with the "interface" keeping in view the human user's perception, expectation and limitation in consideration. Now the question arises: Can we have Computers as our personal psychiatrists? Can we treat mental or psychological patients with Computer-Aided Psychotherapy? I really want to explore!!!!

***5. Professional/Ethical Issues in Computing:*** Can we ever be able to fully secure personal or professional data via Computers? Can we get rid of pornography from the internet? Can we develop a game that counters games leading to suicide like "Blue Whale"? Can we rid the world from religious fanaticism, terrorism, racism and hate crimes via Computer Science? All of such questions and problem areas are pending to be addressed.
> -1 votes

---
Tags: computation-models
---


# Question
Title: Is finding all primes less than n, doable in polynomial time?
Bear in mind I'm almost a complete noob at complexity theory.

I was reading about how AKS Primality shows that numbers of size n can be shown to be prime or composite in polynomial time. Given that, does that imply finding all prime numbers less than a number n is also doable in polynomial time and thus the algorithm runs in FP. Additionally, does this imply that counting all primes less than n is not in #P?

Any ideas, or comments are appreciated Thanks!

# Answer
> 4 votes
No, it doesn't. There are exponentially many primes less than $n$, so you can't enumerate them in polynomial time.

# Answer
> 1 votes
The answer by D.W. already points out that listing all primes up to $n$ cannot be done in time polynomial in the representation of $n$.

It can be done in time polynomial in $n$, though. Using the sieve of Eratosthenes, the running time is $n\log n$.

You had one other question: Whether counting primes can be done in #P. Yes, it can. This is a direct consequence of having a PTIME primality test. (And it would not have been contradicted by (listing or) counting being in FP, as FP is a subclass of #P.)

---
Tags: complexity-theory, np, primes
---


# Question
Title: Given all maximal independent sets of a graph, find the maximum indepdent set
I am new to this independent set problem in graph theory. As per my understanding so far an independent set is a set of vertices in which no two vertices are adjacent. And the maximal independent set is a set of vertices in which if some vertex is added it will construct an edge.

I understand this now my question is if given all maximal independent set for a graph then the maximum independent set of that graph will be maximal independent set with maximum cardinality right?

Note: As per my understanding there can be more than one maximum independent set but their cardinality will be same.

# Answer
If an independent set is *maximal*, it means you cannot add any more vertices into the set. As you correctly suggest, this does *not* mean that the set is necessarily a maximum independent set in the graph.

You are also correct in saying that every maximum independent set is maximal, and that a graph can have several maximum independent sets.
> 2 votes

---
Tags: graphs
---


title: Show that NP is not equal to SPACE(n)

text:
# Question
Title: Show that NP is not equal to SPACE(n)
I want to show that $\text{NP} \neq \text{SPACE}(n)$ and tried it like this:

Let $L$ be in $\text{SPACE}(n)$ so there is a deterministic $k$-tape TM which decides $L$ in polynomial time. Let's consider a binary alphabet. There are $2^{kn}$ possible strings on the working tapes so for an input of length $n$ the TM can be in $2^{kn} \cdot k \cdot n \cdot |Q|$ different configurations where $Q$ is the finite state set.

Since the TM is deterministic and decides $L$ no configuration can be visited twice (otherwise we would be in an infinite loop). So $2^{kn} \cdot k \cdot n \cdot |Q|$ is also an upper bound for the runtime of the TM which is exponential and therefore not in $NP$.

Is this argumentation enough? I found this answer on the internet and now I'm confused because it looks so much more complexive but also comprehensibly...

# Answer
> 7 votes
In order to prove that $\mathsf{SPACE}(n) \not\subseteq \mathsf{NP}$, you need to identify a language in $\mathsf{SPACE}(n)$ which is not in $\mathsf{NP}$. Not every language in $\mathsf{SPACE}(n)$ would work — for example, every regular language is in $\mathsf{SPACE}(n)$, and all of these are also in $\mathsf{NP}$.

Your argument, as I understand it, is roughly as follows:

1. Every machine in $\mathsf{SPACE}(n)$ runs in at most exponential time.
2. Hence every such machine is not in $\mathsf{NP}$.

The second conclusion is not correct, since exponential time is only an *upper bound*. For example, a DFA uses constant space and does run in polynomial time.

Worse, even if some machine in $\mathsf{SPACE}(n)$ does run in exponential time, it could be that there exists another machine accepting the same language that runs in polynomial time — especially if we are allowed to use nondeterminism. As an example, it is suspected that $\mathsf{SAT}$ (which is in $\mathsf{SPACE}(n)$) requires exponential time, but it does belong to $\mathsf{NP}$.

The proof outlined in your link is not too hard, given the space hierarchy theorem. This theorem gives you a language $L$ which is in $\mathsf{SPACE}(n^2)$ but not in $\mathsf{SPACE}(n)$. The padded language $L' = \\{ 1^{|x|^2}0x : x \in L \\}$ does lie in $\mathsf{SPACE}(n)$ (why?), and so if the latter is equal to $\mathsf{NP}$, it follows that $L' \in \mathsf{NP}$. However, $L$ polytime reduces to $L'$, and so it would follow that $L \in \mathsf{NP}$ as well, contradicting $L \notin \mathsf{SPACE}(n)$.

# Answer
> 1 votes
* Problems in $\mathrm{NP}$ use a non-deterministic TM for running in polynomial time. So it's not a proof of not being in $\mathrm{NP}$ that a TM runs in exponential time on a deterministic TM.
* There is no proof for the existence of a TM which satisfies the upper bound.

---
Tags: complexity-theory, time-complexity, space-complexity
---


title: Simple path in a Finite Acceptor

text:
# Question
Title: Simple path in a Finite Acceptor
What is the definition of a 'simple path' in a finite acceptor? My concern is whether self loops can be considered as a part of simple path from initial to final state?

# Answer
The only reasonable definition for a simple path in a finite acceptor would be a finite path in its transition graph, i.e. no vertices (states) may appear twice in that path. This especially excludes paths that use self loops.
> 2 votes

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


# Question
Title: Rice's theorem application on a language that resembles ETM
I'm working on an exercise that involves checking if the Rice's theorem can be applied on a two languages.

The first language is $E\_{TM} = \\{ \langle M \rangle \text{ | M is a Turing Machine and } L(M) = \emptyset \\} $.

I already know it's undecidable, thus Rice's theorem should apply without any problem and in fact it checks the three theorem's requisite just fine.

The second language is $X = \\{\langle M \rangle \text{ | M is a Turing Machine that does not halts on any input string \\}}$.

To me, the fact that the TM does not halts on any string means that the language is empty, which means that X is similar if not equal to $E\_{TM}$.

But the property stated in X is not on the language of the TM, but rather describes what it does on all possible strings.

Is this reasoning correct?

Thanks for your help.

# Answer
First of all, note that there are undecidable languages where Rice's theorem cannot be applied. In your third paragraph one may suggest that it would work that way. But in fact, for $E\_{TM}$ you can apply the theorem.

$X$ is not the same language as $E\_{TM}$ but it is a proper subset of $E\_{TM}$. E.g. the TM $M\_0$ that prints $0$ (reject) immediately after the start for any input and halts after that is in $E\_{TM}$ but not in $X$. However, Rice's theorem is applicable for $X$. You have to find a proper, non-empty subset of all computable functions $\mathcal{R}$ that contains precisely the function computed by the TM in $X$. Let $$\mathcal{S} = \\{f\_M \mid f\_M(x) = \bot \text{ for all } x \in \\{0, 1\\}^\ast\\},$$ where $\bot$ means "never halt". Then

* $\mathcal{S} \neq \varnothing$ as the function of the Turing machine that immediately goes in an infinite loop is in $\mathcal{S}$,
* $\mathcal{S} \neq \mathcal{R}$ as $M\_0$'s function (see above) is not in $\mathcal{S}$.

Obviously, the set of all Turing machines that compute a function from $\mathcal{S}$ coincide with $X$. Thus, $X$ is undecidable following Rice's theorem.

Note that Rice's theorem can be stated in different ways but it should look like this when speaking about TMs.
> 0 votes

---
Tags: turing-machines, undecidability, rice-theorem
---


title: Turing decider Halting Problem

text:
# Question
Title: Turing decider Halting Problem
Wiki and my classes Textbook defines a decider as:

> In computability theory, a machine that always halts—also called a decider (Sipser, 1996) or a total Turing machine (Kozen, 1997)—is a Turing machine that halts for every input.

So shouldn't this decider be able to decide the Halting Problem? Because it halts always? I am a bit confused.

# Answer
> 1 votes
Here is an example of a decider:

> On input $w$, accept if $|w|$ is even, and reject if $|w|$ is odd.

Does it solve the halting problem?

---
Tags: turing-machines, halting-problem
---


# Question
Title: What does "terms evaluated in related environments yield related values" means in the context of typing judgements?
I am reading Theorems for free! by Philip Wadler which is a paper about how to derive theorems from the type signature of a function.

> Parametricity is just a reformulation of Reynolds’ abstraction theorem: **terms evaluated in related environments yield related values**.

What is an *environment* in this case ? More generally, how do I interpret the statement in bold ?

I think I understand the parametricity thing correctly but somehow I cannot map this sentence to something more intuitive.

# Answer
The environments are *related* not identical. The context of this statement is logical relations, as described e.g. here. A logical relation is a type-indexed family of relations which follows the structure of the types (in a way I won't elaborate on). If for each type $\tau$, we assign a (binary) relation $R\[\tau\]$, then given $f:\tau\_1\to\tau\_2,x:\tau\_1\vdash f\\, x : \tau\_2$ when $R\[\tau\_1\to\tau\_2\](f,f')$ and $R\[\tau\_1\](x,x')$ we can ask if it is the case that $R\[\tau\_2\](f\\, x,f'\\, x')$. This is what it is referring to in "terms evaluated in related environments yield related result".
> 3 votes

---
Tags: type-theory
---