# Question
Title: Why is Rule 110 considered "weakly" universal?
My supposition is that this is was more or less an automatic designation based on the fact that Rule 110 requires an infinite "background tiling" of the 14-bit sequence `00010011011111`, and since by convention a proper Turing-complete system is supposed to begin with a blank tape or its equivalent, this doesn't count.

I would understand the argument for "weakly" universal if the tiling sequence was dependent on the program in some way, but that's not the case here. In fact, as near as I can tell, within the mathematical universe of Rule 110, that sequence **is** the blank tape.

*(The staggered small triangle tiling is what this sequence looks like on a typical plot.)*

If you start with virtually any aperiodic seed row (e.g. a few random bits on top of a `0` tiling), the system invariably settles into a state where the obvious background is that sequence. It's the sequence of least resistance, sort of the lowest-energy vacuum state of the Rule 110 universe. On top of that, it's a constant finite overhead, which already to me seems like suspect grounds for the "weakly" qualifier.

Is there a good reason for this designation that I've missed or something I've misunderstood?

# Answer
Universality of Turing machines and Turing completeness of arbitrary computational systems are two different things. There is a concept of a weakly universal Turing machine, but no analogous concept of weak Turing completeness.

The question that you linked in your answer is about a Turing machine that simulates a rule-110 cellular automaton. That Turing machine is weakly universal. The rule-110 system that it simulates is Turing complete, but it is not weakly universal, since it isn't a Turing machine.
> 1 votes

# Answer
Thanks to D.W., I searched for sources, and started to find plenty of references (many on comments on stackexchange, some papers), but eventually came to

https://math.stackexchange.com/questions/1609858/how-are-weakly-universal-turing-machines-actually-defined

This answers my question inasmuch as it directly discusses all this nonsense, and seems to reaffirm my understanding that R110 *is* universal in every reasonable sense of the word, no qualifiers needed.
> 0 votes

---
Tags: computation-models, turing-completeness, cellular-automata
---


# Question
Title: What is the minimal number of nodes with the right subtree in a height-balanced BST?
I have a binary search tree of size $N$.
The tree is height balanced: difference of heights of a node's subtrees is no more than 1 (true for RB or AVL trees).
$K$ is the number of nodes that have a non-empty right subtree.

If the tree is intentionally created to minimize $K$, then what is $\min(K)$?

# Answer
> 2 votes
Given your requirement to minimize $K$, the number nodes with right subtree, while maintaining subtree height difference of at most 1,you should start with the AVL tree $T\_h$ of height $h$, with minimum number of nodes. It is known that such tree has $F\_{h+2} - 1$ nodes, where $F\_i$ is the $i$th Fibonacci number (here I am using the version where $F\_0=F\_1=1$). Note that $T\_h$ can be recursively constructed from a root $r$ with left subtree $T\_{h-1}$ and right subtree $T\_{h-2}$. We force the right subtrees of all nodes in the tree to have lesser nodes for the purpose of minimizing $K$.

Notice that since $T\_h$ already has minimal number of nodes and must be balanced, all nodes whose subtree has height $\ge 2$ must have left and right subtrees. The number of such nodes should give you the minimum value for $K$.

To count these nodes, you can remove from $T\_h$ nodes with height 0 (these are the leaves) and nodes with height 1 (since this nodes have no right subtree from the way $T\_h$ is constructed). I claim that after removal you'll get the AVL tree $T\_{h-2} $, that has $K =F\_h - 1$ nodes.

---
Tags: binary-search-trees
---


# Question
Title: Thought experiment about two AIs involved in an infinite game
I came up with a thought experiment on the limits of artificial intelligence that I was hoping to get advice on how to solve as well as any recommendations for further reading that explain relevant concepts for solving/dissolving the thought experiment.

Suppose some superpowerful artificial intelligence A1 attempts to simulate in advance the behavior of another superpowerful artificial intelligence A2; that A2 can watch the simulation A1 makes of it; and that A1 wants to simulate A2 while A2 does not want to be simulated by A1. Let some arbitrary event A2 would do in the future be called event 1, and then suppose A2 watches A1's simulation of it. Couldn’t A2 be built to do something other than what it would see itself do in the simulation of event 1? Call the event of it watching itself do event 1 and then doing something else, event 2. But since A2 wants to make the simulation perfect it would anticipate and simulate A2 doing event 2. But in that case A2 would just be watching itself do event 2 in the simulation and then couldn't it just do something other than what it would see itself do in the simulation of event 2? Call the event of it watching itself do event 2 and then doing something else, event 3. Then in order for A1 to make its simulation perfect it must anticipate and simulate A2 doing event 3, and so on, creating an infinite chain of events done by each AI.

My thoughts are, one AI wins if it goes up to/simulates an event k and the other AI cannot go up to/simulate event k. But I have no idea how to prove that such an event does or does not exist (and honestly I'm not even positive the thought experiment is well-formed). Where should I begin? Moreover, is such a situation physically realizable?

# Answer
> 1 votes
The premise that A2 can watch A1's simulation seems poorly motivated. As we all know, if we want to predict someone's actions, we shouldn't tell them our prediction, otherwise they might behave contrarily just to spite us. In practice, most settings that I can imagine where I would want to simulate another agent, nothing forces me to allow the other agent to watch/observe my simulation and my simulation's predictions. So, the problem setup seems artificial and designed in a way that will lead you to draw conclusions of dubious relevance.

From your problem statement I suspect you would be interested in Newcomb's paradox.

This doesn't seem to be a matter of computer science.

---
Tags: reference-request, artificial-intelligence
---


# Question
Title: Maximum, delete and insert fastest data structure
The runtime to find a max element in max heap is $O(1)$. It takes $O(\log n)$ time to delete an element and $O(\log n)$ time to insert a new element in the heap.

Does there exists a data structure in which max element can be found in $o(\log n)$ and still the time to delete is $o(\log n)$ and $o(\log n)$ time to insert a new element?

$n$ denotes the number of elements.

# Answer
> 4 votes
You cannot create a data structure that guarantee $o(\log n)$ time for insertion AND $o(\log n)$ for maximum extraction, be it worst, amortized or average case.

The reason is that such a data structure would allow comparison sorting in $o(n \log n)$, which is theoretically not possible.

# Answer
> 2 votes
Just to add to the previous answer, you can get $O(1)$ amortized bound for find, insert, and delete with some limitations with soft-heap \[wiki, original paper, simplified implementation\]. This heap can break the lower-bound for sorting by allowing some kind of *corruptions* to the keys.

Corruption means the soft-heap will make changes to keys of certain items in the heap so that multiple items will *share* a common key, without any means of retrieving the original keys. The number of corrupted keys can be controlled by a paremeter $\varepsilon$ such that it is guaranteed that at most $\varepsilon n$ are corrupted. Despite this seemingly unusual implementation it has applications for MST and linear-time selection.

# Answer
> -2 votes
Data structure that can be used for the aforementioned situation :

**AVL tree :** The self-balancing feature of AVL tree guarantees the performance of O(logN) in the worst case for all operations, including insertion, deletion, and searching.

**Disadvantage of AVL tree :** It's a complex data structure. if the program involves frequent insertion and deletion of elements then one should rather use red-black tree to avoid multiple rotations.

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


# Question
Title: 7 segment decoder Combinational Logic Circuits using Logic Gates
How can a 7 segment decoder operation be implemented using boolean NOR gate ONLY?

Question:

Here's my truth table and k-map:

Normal circuit diagram:

# Answer
> 1 votes
You can use the following systematic transformation

$$\bigvee\_{i=1}^{m}\left(\bigwedge\_{j=1}^{n\_i} v\_{i,j}\right) =\overline{\left(\overline{\bigvee\_{i=1}^{m}\left(\bigwedge\_{j=1}^{n\_i} v\_{i,j}\right)}\right)} =\overline{\left(\overline{\bigvee\_{i=1}^{m}\left(\overline{\bigvee\_{j=1}^{n\_i}\overline{v\_{i,j}}}\right)}\right)}$$

though the expression is not minimized.

---
Tags: boolean-algebra
---


# Question
Title: Proving monad laws for flatMap and unit, given laws for compose and unit
I'll use scala notation but hopefully things will make sense in general (I'm trying to prove that you can define a monad using either \[flatMap (aka bind) and unit\] or \[compose and unit\])

The book Functional Programming in Scala (github at https://github.com/fpinscala/fpinscala) makes the claim that if we have a type constructor `M` and functions compose and unit

```
compose(f: A => M[B], g: B => M[C]): A => M[C]
unit(a: A): M[A]

```

satisfying

```
compose(compose(f, g), h) == compose(f, compose(g, h))
compose(f, unit) == f
compose(unit, f) == f

```

then defining a function flatMap

```
flatMap(x: M[A])(f: A => M[B]) = compose(_: Unit => x, f)(())

```

will satisfy

```
flatMap(flatMap(x)(f))(g) == flatMap(x)(a => flatMap(f(a))(g)
flatMap(x)(unit) == x
flatMap(unit(y))(f) == f(y)

```

I can't prove this. The easiest place to see my confusion is trying to show the last identity. We have

```
flatMap(unit(y))(f) = compose(_: Unit => unit(y), f)(())

```

If there was some rule like

```
compose(_: Unit => unit(y), f)(()) = compose(unit, f)(y)

```

or more generally

```
compose(f∘g, h)(a) = compose(f, h)(g(a))

```

then we could conclude that the identity is true, but as is, I don't see any move I'm allowed to make. Any ideas?

The solutions for this question https://github.com/fpinscala/fpinscala/blob/master/answerkey/monads/10.answer.scala only do the case where compose is defined in terms of flatMap but the questions asks "Prove that these two statements of the identity laws are equivalent" so I think the solutions should include both implications.

# Answer
That rule you are asking for is (with slight tweaking) a naturality condition mathematically. It would be more naturally written as: $$\mathtt{compose}(f\circ g,h)=\mathtt{compose}(f,h)\circ g$$ If `compose` used the typical order for composition, you could write it more prettily as: $$(h\odot f)\circ g = h\odot(f\circ g)$$ where $h\odot f = \mathtt{compose}(f,h)$.

The type `A => M[B]` corresponds to the hom-functor for the Kleisli category of $M$, $\mathcal{C}\_M(A,B)\equiv\mathcal{C}(A,MB)$. Given a Kleisli arrow $h : B \to MC$, we have the function $h\odot- : \mathcal{C}(A,MB)\to\mathcal{C}(A,MC)$, and this is natural in $A$. The naturality diagram is: $$\require{AMScd} \begin{CD} \mathcal{C}(A,MB)@\>h\odot -\>\>\mathcal{C}(A,MC) \\ @V-\circ gVV @VV-\circ gV \\ \mathcal{C}(X,MB) @\>\>h\odot -\> \mathcal{C}(X,MC) \end{CD}$$ where $g : X \to A$. (In fact, this can also be read as a naturality diagram for $-\circ g : \mathcal{C}\_M(A,-)\to\mathcal{C}\_M(X,-)$.) That $h\odot -$ is natural can be easily derived from its definition as $f\mapsto \mu\circ Mh \circ f$ where $\mu$ is the multiplication of the monad $M$, i.e. `flatten`, and $Mf$ is the functorial action of $M$, i.e. `map`.

At any rate, the equation you want would be a free theorem if Scala was a suitably nicely behaved language. Indeed, that Scala isn't "suitably nicely behaved" is an omnipresent problem and leads to many of these laws not actually holding. (This problem occurs with Haskell too, but not nearly so catastrophically.) I assume Paul and Runar discuss this and free theorems somewhere in the book. They're certainly aware of it.
> 5 votes

# Answer
The interesting question is how to prove the equivalence (and what that equivalence actually means) under some required restrictions.

The required restrictions are that your function's code must be "fully parametric": use only type parameters and never any specific types; no run-time identification of type parameters; no reflection; and of course no side effects. Of course you can make an example in Scala (and in Haskell, etc.) where the functions do not satisfy the law because they identify types at run time. But it's a case that almost never comes up in practice.

What you are missing for your proof is a naturality law of `compose`. Without assuming that law, it is **not true** that `flatMap(unit(y))(f) == f(y)`.

Naturality laws will hold automatically whenever the code is "fully parametric", i.e., restricted in the way I just described. But this is a complicated subject that currently has no good tutorials available. For instance, the "Theorems for free" paper is certainly not suitable as a tutorial for a practicing Scala or Haskell programmer trying to understand how to prove - or even how to write - a naturality law for `compose`.

So, let us just assume that the following additional "left naturality" law holds for `compose`:

```
 for all f : A => B, g: B => M[C], h: C => M[D]:
 compose(f andThen g, h) = f andThen compose(g, h)

```

Now we have:

```
 flatMap(unit(y))(f)
   ==  compose(_: Unit => unit(y), f)(())
   == compose( (_ => y) andThen unit, f)(())  // Now use the left naturality law of `compose`.
   == ((_ => y) andThen compose(unit, f))(())
   == ((_ => y) andThen f)(())
   == ((_ => f(y))(())
   == f(y)

```

The other laws of `flatMap` can be also derived from the laws of `compose` only by assuming a naturality law of `compose`.

The book "Functional programming in Scala" never mentions this additional assumption - neither in the chapter on monads nor in the chapter on applicatives, where a similar equivalence holds between "ap" and "zip" but only when certain naturality laws are assumed.

For the `flatMap` and `compose`, the authors of "FPiS" show you the proof of laws only in the direction where no additional assumptions are needed: namely, when `compose` is defined via `flatMap`. So, I guess, the authors never tried themselves proving those laws in the other direction.

The equivalence between `compose` and `flatMap` is explained in detail (but using a special, better adapted notation) in Section 10.2.6 of my book "The Science of Functional Programming". LyX/LaTeX source: https://github.com/winitzki/sofp pdf: https://leanpub.com/sofp

In my book, I go through a large number of derivations where one function type is equivalent to another. In each case, I find that there are extra naturality laws that one has to assume. Intuitively, this makes sense, because how else can a function `flatMap` with two type parameters be equivalent to a function `compose` with three type parameters? Only when `compose` is additionally constrained by a law that can arbitrarily modify one of its type parameters and so cancels the additional freedom of having one more type parameter.

The easiest example of "equivalence under naturality" is the equivalence of `pure[A]: A => M[A]` and `u: M[Unit]`. You can define `pure(x) = u.map(_: Unit => x)` and `u = pure(())` but this does not already prove an equivalence between the types of these functions.

Indeed, they cannot be simply equivalent: `pure[A]` has a type parameter `A` but `u` has no type parameters.

So, in fact, they are equivalent only we assume a naturality law for `pure`:

```
  for all x: A, f: A => B:
  pure(x).map(f) = pure(f(x))

```

Only with this additional law, one can prove that defining `pure` via `u` and back gives indeed an isomorphism in both directions.
> 2 votes

# Answer
Thank you Derek Elkins for your helpful answer. One thing I took away from your answer is that the equation I want might not be true in Scala, because it has "too many escape hatches for parametricity", as described in http://data.tmorris.net/talks/parametricity/b8e0cb9d7f5dcdf48ef18eb49fc84905ece6b8ec/parametricity.pdf

So I tried to find a counterexample, here is my (I hope successful) attempt. First we define Mon (short for Monad) as requiring `compose` and `unit` to be defined and then defining `flatMap` in terms of compose. The typeTags are needed for later (also I'd never really played with typeTags and implicits before so there are probably better ways to do it).

```
import scala.reflect.runtime.universe._
import language.higherKinds

trait Mon[M[_]] {
    def compose[A, B, C](f: A => M[B], g: B => M[C])
        (implicit tA: TypeTag[A], tB: TypeTag[B], tC: TypeTag[C]): A => M[C]

    def unit[A](a: A): M[A]

    def flatMap[A, B](ma: M[A])(f: A => M[B])
        (implicit tA: TypeTag[A], tB: TypeTag[B]): M[B] =
            compose((_: Unit) => ma, f)(typeTag[Unit], tA, tB)(())
}

```

Then we define `Option` to be a `Mon` as follows

```
val optMon: Mon[Option] = new Mon[Option] {
     def unit[A](a: A): Option[A] = Some(a)

    override def compose[A, B, C](f: A => Option[B], g: B => Option[C])
        (implicit tA: TypeTag[A], tB: TypeTag[B], tC: TypeTag[C]): A => Option[C] =
        (a: A) => if (tA.tpe == tB.tpe || tB.tpe == tC.tpe)
            f(a).flatMap(g)
        else
            None
}

```

This defines `unit` in the normal way. The definition of `compose` in the 'natural' way would just be `f(a).flatMap(g)`, but we use the ability of Scala to inspect the types, and define it to be the natural formula if `A == B` or `B == C`, otherwise just `None`.

We now show that `optMon` satisfies the three monad laws in terms of compose and unit:

```
compose(f: A => M[B], unit: B => M[B])
= (a: A) => f(a).flatMap(unit)
= (a: A) => f(a)
= f

compose(unit: A => M[A], f: A => M[B])
= (a: A) => Some(a).flatMap(f)
= (a: A) => f(a)
= f

```

For

```
compose(f: A => M[B], compose(g: B => M[C], h: C => M[D]))
= compose(compose(f, g), h)

```

note that the LHS is made to be `None` by our compose formula if (A != B and B != D) or (B != C and C != D). The RHS is made to be `None` if (A != B and B != C) or (A != C and C != D). One way the LHS can be forced to be None is if A != B and B != D. Then if B != C the RHS is forced to be None, otherwise B = C but then A != C and C != D so the RHS is forced to be None. Similar arguments show that if (A != C and C != D) is true then the RHS is forced to be None. Symmetrical arguments show that if the RHS is forced to be None then the LHS is forced to be None. When neither side is forced to be None then the equation is just the associativity law for a monad defined in terms of flatMap which is true.

Finally we show that flatMap (defined in terms of this compose) does not satisfy one of the identity laws.

```
flatMap(unit(""), (s: String) => Some(s.length))
= compose((_: Unit) => unit(""), (s: String) => Some(s.length))(())
= None // because A != B and B != C
!= ((s: String) => Some(s.length))("")
= Some(0)

```
> 1 votes

---
Tags: functional-programming
---


# Question
Title: What are the 175 billion parameters used in the GPT-3 language model?
I am currently working my way through *Language Models are Few-Shot Learners*, the initial 75-page paper about GPT-3, the language learning model spawning off into ChatGTP.

In it, they mention several times that they are using **175 billion parameters**, orders of magnitudes more than previous experiments by others. They show this table, for 8 models ranging from 125 million params to 175 billion params.

Then they say:

> Table 2.1 shows the sizes and architectures of our 8 models. Here nparams is the total number of trainable parameters, nlayers is the total number of layers, dmodel is the number of units in each bottleneck layer (we always have the feedforward layer four times the size of the bottleneck layer, dff = 4 ∗ dmodel), and dhead is the dimension of each attention head. All models use a context window of nctx = 2048 tokens. We partition the model across GPUs along both the depth and width dimension in order to minimize data-transfer between nodes. The precise architectural parameters for each model are chosen based on computational efficiency and load-balancing in the layout of models across GPU’s. Previous work \[KMH+20\] suggests that validation loss is not strongly sensitive to these parameters within a reasonably broad range.

I am not an expert in machine learning, I just know basic RNNs and how they work with just a few parameters and a few layers (I don't know, like 5 parameters and 5 layers max, it's been a while)? What are the things counted as **parameters** in this 175 billion parameter network? How does the network look with its 96 layers? How many nodes are there per layer sort of thing?

I am trying to understand this paper and eventually how ChatGPT works, and getting to section 2 so far, I haven't seen what you would use as inputs/parameters to such a large model. The ones you learn in school are tiny compared to this. Hoping for a little illumination on what could be going on.

# Answer
The 175 billion parameters in the GPT-3 language model are values that are used by the model to make predictions about the next word or words in a sentence or piece of text. These parameters are essentially the weights that are applied to the input data in order to make the model's predictions. In a neural network, the parameters are the values that are learned and adjusted during the training process in order to minimize the difference between the predicted output and the desired output.

The GPT-3 model has 96 layers, which means that it is composed of multiple layers of neural networks. Each layer of the network is made up of a number of nodes, which are the individual processing units of the network. The number of nodes per layer can vary.

To use the GPT-3 model, you would need to provide it with some input data, such as a sentence or a paragraph of text. The model would then process this input using its 175 billion parameters and its 96 layers, in order to make a prediction about the next word or words that should come next in the text. The model's predictions would be based on the input data and its learned parameters, and it would be able to generate human-like text as a result.
> 2 votes

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


# Question
Title: Vertex deletion algorithm with connected constraint
While working on a job distribution problem, I ended up hitting a graph problem that I can't seem to get a foothold on.

Consider a not-necessarily connected graph, like one shown below. Each step, we can delete up to N vertices from the graph, but can't delete two nodes if they are connected, only one or neither of the pair. Goal is to minimize the number of steps required to delete all vertices.

Example graph:

For example, for N=2, at step 1, we cannot delete 1 **and** 2 (as they are connected), but we can delete 1 **and** 5, since they are not connected. An example sequence of steps:

Step 1: delete nodes 0 and 2

Step 2: delete nodes 4 and 5

Step 3: delete nodes 1 and 6

And so on. There are "bad" sequences of steps, for example deleting all size 1 components before anything else. Any suggestions on where to learn more about this, or ways to generally solve this problem?

# Answer
This problem is known as *mutual exclusion scheduling*. This problem is NP-hard for all $N \geq 3$ \[1\].

When $N = 2$, this is equivalent to the minimum edge cover problem on the complement graph. It is solvable in polynomial time by a graph matching algorithm.

This problem can also be viewed as a graph coloring problem, called *$\ell$-bounded $k$-coloring*. Bodleander and Fomin \[2\] showed this problem is polynomial-time solvable for bounded treewidth graphs.
> 6 votes

# Answer
If a graph has $n$ vertices then there is the obvious upper bound of $n$ steps where one vertex is removed in each step.

If a disconnected graph $G$ is composed of several connected components, the total number of steps required to remove all the vertices from $G$ is equal to the number of steps required to remove the connected component that requires the most steps to remove all its vertices as each connected component can be considered independently and the vertex removals from each connected component can be completed in one step.

Now consider the case of a connected graph. If there is a cut vertex, then it will be optimal to remove one of the cut vertices. The number of vertices in the largest connected component will be at most $n-2$. So if a graph has a cut vertex, it can be removed in $n-1$ steps.

Other than this, there isn't a better upper bound for graphs in general. Consider the complete graph, $K\_t$. Removing any vertex results in the graph $K\_{t-1}$ and only one vertex can be removed as every vertex is connected to every other vertex. So for $n$ vertices, there is always a graph that requires $n$ steps to remove.
> 3 votes

---
Tags: graphs
---


# Question
Title: Finding $k^{th}$ smallest in row and column-wise sorted matrix $m\times n$
Let $M$ be a $m\times n$, in which rows and columns of $M$ are sorted in increasing.

**Problem.**

Find $k^{th}$ smallest number in $O(m\log(mn))$.

**My attempts.**

I merge all rows in a single sorted array in time $O(mn\log(mn))$ but this idea isn't efficient and I think there is a solution with running time $O(m\log(mn))$. After many hours thinking about this problem, I found a solution with running time like $O(k\log(mn))$, so $k$ can be $O(mn)$, eventually, this gives us the bound $O(mn\log(mn))$.Anyone can give me some hints about how I can achieve my desired time complexity?

# Answer
There is a $O(n)$ time solution. See discussion here.

\[1\]: Selection in X+Y and Matrices with Sorted Rows and Columns. A. Mirzaian, E. Arjomandi, Information Processing Letters 20:13-17, 2 January 1985.

\[2\]: https://softwareengineering.stackexchange.com/questions/233031/given-two-sorted-array-in-ascending-order-with-same-length-n-calculate-the-kth
> 1 votes

# Answer
This problem can be solved in $O(n\log n)$ time.

As an example, consider the square matrix $M = \begin{bmatrix}a & b & c \\ d & e & f \\ g & h & i\end{bmatrix}$ where $M\_{i,j} \leq M\_{i+1,j}$ and $M\_{i,j} \leq M\_{i,j+1}$.

To visualise the solution, organise the matrix into a lattice.

There is an edge $v\_1v\_2$ in the graph if it is known that $v\_1 \leq v\_2$. Labelling the bottom row of the lattice as the first, if $r \leq n$ then the $r^{\text{th}}$ row of the lattice contains the elements that sit between the $\frac{r(r-1)}{2}+1$ smallest element and the $\frac{r(r+1)}{2}$ smallest element.

Notice that if row $r$ of the lattice contains the $k^{\text{th}}$ smallest element and $r \leq n$ then

\begin{align\*} \frac{r(r-1)}{2}+1 &\< k \leq \frac{r(r+1)}{2} \\ r-1 &\< \frac{-1 + \sqrt{8 k + 1}}{2} \leq r \end{align\*}

If $r \> n$ then notice that the $k^{\text{th}}$ smallest element is the $mn - k + 1^{\text{th}}$ largest element and use a similar formula for finding the row in the lattice.

So compare elements in row $\left\lceil \frac{-1 + \sqrt{8 k + 1}}{2} \right\rceil$ of the lattice and notice that a row in the lattice represents a diagonal in the original matrix.

A row in the lattice has at most $\min\\{m,n\\}$ squares. Assume WLOG that $m \leq n$. The $k^{\text{th}}$ smallest item can be found in $O(m\log m)$ time.

For non-square matrices, use a similar procedure but find a piece-wise expression to find the relevant row.To do this, make use of the fact that a diagonal of an $m\times n$ grid has at most $\min\\{m, n\\}$ elements.
> 1 votes

---
Tags: algorithms
---


# Question
Title: What is the best way to solve the coin change problem using dynamic programming?
I have found two ways of applying dynamic programming to the coin change problem of finding the minimum number of coins from a given set of denominations to make a given sum. I wanted to know if one is better than the other:

```
def money_dyn1(m, coins):
    a = [[float("+inf") for j in range(m + 1)] for i in range(len(coins) + 1)]
    for i in range(len(a)):
        a[i][0] = 0

    for i in range(1, len(a)):
        for j in range(1, len(a[0])):
            if coins[i - 1] > j:  # if the coin is bigger than the sum to reach
                a[i][j] = a[i - 1][j]
            else:
                a[i][j] = min(a[i - 1][j], a[i][j - coins[i - 1]] + 1)

    print(a[-1][m])

```

and

```
def money_dyn2(m, coins):
    a = [None for j in range(m + 1)]
    a[0] = 0

    for i in range(0, len(a)):
        for c in coins:
            if i + c < len(a) and a[i] != None:
                if a[i + c] == None or a[i + c] > a[i]:
                    a[i + c] = a[i] + 1
    return a[m]

```

I find the later much simpler to understand, but when I lookup examples on the internet about DP applied to this problem, it seems that most of the solutions implement the first implementation (using the 2D array).

Is one of those implementation better than the other ? What are the differences between those ? (both mathematically and algorithmically)

# Answer
Nice question!

##### We are computing entries in a matrix.

We are computing the minimum number $a\[i\]\[m\]$ of coins to yield value $m$ using the first $i$ coins for all valid $i$'s and $m$'s using the recurrence relation $$a\[i\]\[m\]=\begin{cases}a\[i-1\]\[m\]&\text{if }m\<coins\[i\]\\\min(a\[i-1\]\[m\], a\[i-1\]\[m-coins\[i\]+1)&\text{otherwise}\end{cases}$$ starting from the initial numbers for $i=0$ or $m=0$.

##### Two ways to computing them: by rows and by columns

All $a\[i\]\[m\]$'s form a two-dimensional matrix, with each row corresponding to fixed set of available coins and each column corresponding to a fixed amount of money. As you noted, there are two routes to compute all entries of that matrix.

* Row by row starting from the row of no coins. This is `money_dyn1`.
* Column by column starting from the column of zero money. This `money_dyn2`.

#### There are not much difference between the two ways

If the route by rows as implemented by `money_dyn1` is more popular, I would assume that is because the immediate reaction of people is more like "if I have this set of coins, how do I select/adjust coins to give various amount of change?" instead of "if the amount of change is this, how do I select/adjust coins for my various coin sets?" The amount of change to give to others is naturally the changing part of a setup while the coins I have sounds like real estate that changes infrequently. OK, I am analyzing psychology and social practices, which is somewhat beyond the realm of computer science.

The point is there is not much difference between the two ways, both mathematically and algorithmically.

For example, here is an implementation of the first way, `money-dyn1` using 1D-array just as `money-dyn2`.

```
def money_dyn1_Apass(m, coins):
    """ A version of money_dyn1 using 1D array"""
    a = [None for _ in range(m + 1)]
    a[0] = 0

    for c in coins:
        for i in range(m - c + 1):
            if a[i] is not None and (a[i + c] is None or a[i + c] > a[i] + 1):
                a[i + c] = a[i] + 1

    return a[m]

```

Personally, I find both approaches are natural and easy to understand. Most of times, I would assume my students are more comfortable with the first method, but not by a large margin.
> 1 votes

---
Tags: algorithms, dynamic-programming, coin-change
---


# Question
Title: How to solve this recurrence relation: T(n) = R(n-1) + n log n R(n) = T(n-1) + n^2
How to solve this recurrence relation:

T(n) = R(n-1) + n log n

R(n) = T(n-1) + n^2

# Answer
> 2 votes
How to solve:

* eliminate one of $T$ or $R$.
* write the homogeneous part of the recurrence and plug $T/R(n)=r^n$.
* after simplification, find the roots of the characteristic equation.
* express the solution as a linear combination of terms $r^n$.
* now you have to find particular solutions of the full equation.
* due to the particular values of the roots, you will see that they can be found by summation of the non-homogeneous parts. There are two terms.
* the first term can be summed using the Faulhaber formula.
* the second yields no easy analytical form and you need to fall back on an approximation.
* finally, plug the initial conditions and solve for the unknowns coefficients.
* from $T(n)$ you can easily draw $R(n)$ and conversely.

---

If you can satisfy yourself with a $\Theta$ representation, just perform steps 1 and 6.

---
Tags: time-complexity, asymptotics, recurrence-relation, mathematical-analysis
---


# Question
Title: What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?
I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a definition:

> * Monomorphic Types ($\tau$):
>     + Basic Types: $int,bool,float,string,unit, \dots$
>     + Type types: $\alpha, \beta, \gamma, \delta, \epsilon$.
>     + Compund Types: $\alpha \to \beta, int * string, bool list, \dots$
> * Polymorphic Types:
>     + Monomorphic types $\tau $
>     + Universally quantified monomorphic types
>     + $\forall \alpha\_1, \dots, \alpha\_n . \tau $ (Question: is this not just universally quantified monomophism? If not what's the difference?)
>     + Can think of $\tau$ (I assume they mean monomorphic types) the same as $\forall . \tau$

I guess I find MANY things in this definition rather confusing. But was seems to be the core about my confusion is the difference between:

$$ expr: \alpha \to \beta$$

vs

$$ expr : \forall \alpha, \beta . \alpha \to \beta$$

I don't understand why they are not the same. What is the difference?

After writing this question I have some ideas of what might be going on and want to double check. Is what is going on that $\alpha \to \beta $ (the first one) saying that the expression $expr$ has a monomorphic type as its type (so it just has a real "fixed" type as a type)... Perhaps what's confusing me are type variables. Because nothing can be of a type "type variable". Type variables are just (meta) variables that can later be filled in with a real "basic type", right? So $\alpha \to \beta$ in my first example just stands for "some function type from one type to another but we have not decided which type to choose later, but the expression really just has a fixed basic type as a type once used in a real programming context". Is that right? So saying $fun x \to x$ has type $\alpha \to \alpha$ when reasoning in the meta-theory just means that the function really just has a fixed basic type except we have not specified it. While saying (in a more expressive type system) that $fun x \to x$ has type $\forall \alpha . \alpha \to \alpha$ means that that expression actually has the capability of encompassing all the monomorphic types at once. i.e. in the monomorphic version we actually have to define each identity function separately for each type (for the sake or argument) while in the polymorphic version we have only have 1 single programming construct for all of them...so the type variable basically just stands for a real monomorphic type (at least in the context of this definition).

I guess if we allowed type variables to be anything, then I'd be confused...I think my main worry is about type variables.

---

More rambling cuz I'm confused:

Lets look at this from FOL or as if we were trying to construct or define what an L-term is with an L-structure (see mathematical logic MATH 570). I think right now what confuses me is that this mapping between this vague definition of types (that seems to attempt to define an L-term) is not clear to me. Where is the recursion? What is the L-structure? This type definition is vague for me to really believe it. Something like this would be much better:

---

Related question: What does $ \forall \alpha\_1, \dots , \alpha\_n . \tau $ mean formally as a type?

# Answer
$$\newcommand{\expr}{\mathsf{expr}} \newcommand{\int}{\mathbf{Int}} \newcommand{\List}{\mathbf{List}} \newcommand{\let}{\mathbf{let}} \newcommand{\id}{\mathsf{id}} \newcommand{\in}{\mathbf{in}} \newcommand{\map}{\mathsf{map}} \newcommand{\string}{\mathbf{String}} $$

It's not really possible to answer this without being a little more precise about the status of some things. To this end, let's be clear about distinguishing 'meta' variables from variables that may be part of the syntax of the language. I'll use Greek letters for meta variables and English letters for object variables. Term names will be sans-serif, like $\expr$, keywords/constants will be bold, like $\int$.

So, the two things you ask about actually become at least three things: $$ \begin{align} \expr &: α → β \\ \expr &: a → b \\ \expr &: ∀ a\ b. a → b \end{align} $$

The first is something you might see when discussing the simply typed lambda calculus. It does not have type variables in its object language at all, but it would be inconvenient to talk about particular concrete types all the time. So instead, people tend to talk about things in a schematic way, where meta variables stand in for arbitrary particular simple types. So, something like:

$$\frac{}{λx. x : α → α}$$

is actually a schematic statement, saying that $λx.x$ could be shown to have any type of the form $α → α$. But in a concrete derivation, each occurrence of $λx.x$ can only have a particular concrete type, like $\int → \int$. There is no universal identity function in the language, each occurrence of $λx.x$ stands for an identity function that only works on one type. Perhaps it might help to require annotating the lambda bound variable in this scenario, like so:

$$λ(x : \int). x$$

since now the notations for different identity functions are actually syntactically distinct.

Now, the obvious problem with this is that the concrete system is awful to work in. You can tell, because people are routinely writing *schemas* rather than concrete stuff. It is basically the type system of C, and schemas are like macros that automatically copy and paste your code, which is one way that people work around this awfulness in actual C (the other way being unsafe casting, which prevents the types from guaranteeing that your code actually makes sense).

To remedy this, we can move to #2, which is to make type schemas a well-defined part of the language. This is the approach of things like Hindley-Milner (HM), and the many languages based on it (ML, Haskell, ...). One way of looking at HM is that you add named definitions to the language itself, and these definitions are allowed to have internalized type schemas, rather than particular simple types. Then, when those named definitions are referenced, the schema can be instantiated to any concrete type necessary, and the fact that the schematic definitions are uniform in the choice of type ensures that they will work. So for instance:

$$ \begin{align} \let\ &\id : a → a \\ &\id = λ x. x \\ \in\ &(\id\ 5, \id\ \texttt{"hello"}) \end{align} $$

This sort of system is a pretty strong sweet spot, because it is easy to implement and these sort of named schematic definitions cover a wide range of things that people want to write.

However, one deficiency is that these schematic objects are not first class. Expressions cannot be given a schematic type, only named definitions can, even though we somehow figure out that expressions are valid ways of implementing them. And we cannot take something with a schematic type as an argument to a function to be used at multiple instantiations. Even though:

$$λi. (i\ 5, i\ \texttt{"hello"})$$

seems similar to our term with $\let$ above, it is invalid, because $i$ is a lambda-bound variable, not a definition name.

So, the step to eliminating this discrepancy is to pass from type schemas: $$a → b$$ to quantified types: $$∀ a\ b. a → b$$.

The idea is that the quantifier can bind variables and produce something that is a type in its own right. Then we can ascribe these types to expressions (and variables), rather than only to named definitions. If we do keep named definitions around (which really we probably should, although many type theories aren't presented that way), they no longer have a special status with respect to typing.

All our previous schematic definitions can be translated to this new system by putting all the quantifiers at the beginning of the schema:

$$ \begin{align} \let\ &\id : ∀ a. a → a \\ &\id = λ x. x \\ \in\ &(\id\ 5, \id\ \texttt{"hello"}) \end{align} $$

But now we can write a corresponding lambda expressions and make sense of their types:

$$ \begin{align} (λi. (i\ 5, i\ \texttt{"hello"})) &: (∀ a. a → a) → (\int, \string) \\ λx. x &: ∀ a. a → a \\ (λi. (i\ 5, i\ \texttt{"hello"}))\ (λx.x) &: (\int, \string) \end{align} $$

There are subtleties/consequences to these steps that I haven't mentioned, but this is sort of the core idea. You might also make slightly different choices for notation. For instance, you might require writing the prefix $∀$ syntax for the schemas because it is clearer that it means the named definition works for *every* choice of instantiation of the variables, not for some unknown choice.
> 5 votes

# Answer
From a programmer's perspective, the real difference between $f : \forall \alpha. \alpha\to\alpha$ and $g : \beta\to\beta$ is that the function $f$ can be applied to an argument of an arbitrary type, because we can substitute $\alpha$ to any other type. But the function $g$ has a specific type $\beta\to\beta$, and can only be applied to an argument of type $\beta$. In a program, perhaps the type $\beta$ is defined somewhere in an outer scope, or perhaps it is a type parameter in some outer scope. But at the place where we are writing our code, we can't change what $\beta$ is.

In the language of computer science researchers, $\beta$ is a free type variable while $\alpha$ is a bound type variable. This is a confusing language, but we just need to remember that $\beta$ being a "free variable" means that it has no visible definition in the scope where we have written $g : \beta\to\beta$.
> 0 votes

---
Tags: programming-languages, type-theory, type-checking, type-inference, polymorphisms
---


# Question
Title: Why are the laws of an applicative functor defined the way they are?
Let's recall the definition of an applicative functor. Throughout this question, I write $x: T$ to denote that the value $x$ has type $T$.

> **Definition:** An *applicative functor* consists of a type constructor $F: * \to \*$ together with two operations:
>
> * a function $\mathsf{pure}: A \to F(A)$ that transforms a base value $x: A$ into a "wrapped" value $\mathsf{pure}(x): F(A)$.
> * a binary operation $\circledast: F(A \to B) \to F(A) \to F(B)$ that applies a wrapped function $f: F(A \to B)$ to a wrapped value $x: F(A)$ and produces a wrapped result $f \circledast x: F(B)$.
>
> We require these operations to satisfy the following conditions:
>
> * *Wrapped identities apply as identities.* $$ \mathsf{pure}(\operatorname{id}) \circledast x = x $$
> * *Wrapped composition applies as composition.* $$ \mathsf{pure}(\circ) \circledast f \circledast g \circledast x = f \circledast g \circledast x $$ Here, $\circ$ denotes the function composition operator.
> * *Wrapping distributes across function application.* $$ \mathsf{pure}(f(x)) = \mathsf{pure}(f) \circledast \mathsf{pure}(x) $$
> * *Wrapping exchanges across application.* $$ f \circledast \mathsf{pure}(x) = \mathsf{pure}(g \mapsto g(x)) \circledast f $$

**Question:** Why are these the "correct" laws for an applicative functor? To be more precise,

1. Are these laws known to be logically independent, in the sense that none of these four laws can be derived from the other three?
2. Assuming the answer to question 1 is "yes," what essential characteristic of applicative functors would be lost if we dropped each law, in turn, from the definition? In other words, for each law $L$, there should exist structures $(F, \mathsf{pure}, \circledast)$ satisfying all laws except $L$; why do we not want to call these applicative functors?

# Answer
As described in the original idioms paper, `Applicative` (called `Idiom` there) corresponds to a strong lax monoidal functor. This can be formulated as:

```
class (Functor f) => MFunctor f where
    unit :: () -> f ()
    pair :: (f a, f b) -> f (a, b)

```

The applicative functor laws are then equivalent to the above operations being "monoidal" in the following sense (plus the functor laws):

```
fmap snd (pair (unit (), u)) = u
fmap fst (pair (u, unit ())) = u
fmap (\(a, (b, c)) -> ((a, b), c)) (pair (u, pair (v, w))) = pair (pair (u, v), w)

```

The "strength" aspect comes from the fact that these operations (and the functor ones) are "first-class". In a language without higher-order functions, the lax monoidal functor would not be strong. (The usual presentation of `Applicative` doesn't even make sense in a language without higher-order functions whereas the `MFunctor` presentation does.)

So, dropping any of the laws means you don't have a lax monoidal functor.

Yet another way of looking at it is to note that the applicative functor operations and laws give rise to a family of operations: `liftN :: ((a1, ..., aN) -> b) -> (f a1, ..., f aN) -> f b` with `unit = lift0 id` and `pair = lift2 id`. Using Agda, we could present this more formally as:

```
open import Level

data List {i : Level}(A : Set i) : Set i where
    Nil : List A
    Cons : A → List A → List A

record ⊤ : Set where
    constructor tt

record _×_ (A B : Set) : Set where
    constructor _,_
    field
        fst : A
        snd : B

All : (Set → Set) → List Set → Set
All P Nil = ⊤
All P (Cons x xs) = P x × All P xs

module _ {F : Set → Set}
    (map : {A B : Set} → (A → B) → F A → F B)
    (unit : ⊤ → F ⊤)
    (pair : {A B : Set} → F A × F B → F (A × B))
 where
    pull : {As : List Set} → All F As → F (All (λ A → A) As)
    pull {Nil} tt = unit tt
    pull {Cons A As} (x , xs) = pair (x , pull {As} xs)

    liftN : {B : Set}{As : List Set} → (All (λ A → A) As → B) → All F As → F B
    liftN f xs = map f (pull xs)

```

This perspective arises due to the connection between monoidal categories and multicategories. A lax monoidal functor corresponds to a map of multicategories, `liftN` being the action on multiarrows. If Haskell had multi-ary functions, it would be natural to model it with a multicategory. The appropriate analogue of "functor" would be a map of multicategories, i.e. an applicative functor. From the multicategory perspective, the applicative functor laws are what make the action on multicomposition coherent. Roughly speaking, if we dropped, say, the associative law for `pair`, this would be akin to having functions with a binary tree of parameters instead of a list of parameters. One could explore generalized multicategories for this.
> 9 votes

# Answer
There is an answer to your question from the viewpoint of practical functional programming. Applicative functors are then defined via the `zip` method, not via `ap`. The `zip` method is clearly a useful method in practice, and a programmer with some practical experience expects `zip` to have certain properties. One of these properties is the associativity law:

```
  fa `zip` (fb `zip` fc) should return a value of type F (A, (B, C))
  (fa `zip` fb) `zip` fc should return a value of type F ((A, B), C)
  These two values should be equal after flattening the tuples via F's fmap

```

Similarly one can formulate other properties of `zip` and `pure` from the programmer's perspective. If those properties don't hold, programs using `zip` will be much harder to write correctly, because the order of zipping will affect the results, etc.

After that, you can show that `zip` and `pure` is equivalent to `ap`. It is not easy to just derive the laws of `ap` from the laws of `zip`, the types get quite complicated. So, instead, we can motivate the laws of `ap` directly from formal considerations of category theory. We consider `ap`'s type signature:

```
 ap :: F (a -> b) -> F a -> F b

```

This looks like a lifting from one sort of functions (of type `F(a -> b)`) into another sort of functions (of type `F a -> F b`). It is natural to require that this kind of lifting should satisfy identity and associativity laws. Then you just need to write those laws and complete the proofs.

This is the approach I am using in Chapter 9 of my book "The Science of Functional Programming". LyX/LaTeX source: https://github.com/winitzki/sofp pdf: https://leanpub.com/sofp That book is written with programming examples in Scala but the material is largely independent of Scala. I show the motivations and full step-by-step proofs of all laws.
> 0 votes

---
Tags: terminology, functional-programming, category-theory
---


# Question
Title: Can we somehow get functoriality from purely type-theoretic reasoning?
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the functoriality conditions.

Is there a "free theorem" result for functoriality? i.e. is it sometimes possible to see from the type of a "functor" that it is indeed a functor?

# Answer
There are two senses in which type formation operations are 'functorial,' but neither matches functoriality on the *category* of types.

First, you can interpret the collection of types as a groupoid, and consider isomorphisms between types to be 'arrows.' These compose, but also always have inverses, so are in some sense undirected. However, this is also *why* all constructions are able to be functorial, because type formation operations have both covariant and contravariant positions, and thus may not preserve the direction of arrows.

Anyhow, functoriality here says that if you have $P : A \cong B$ then there is always $F P : F A \cong F B$, and: $$F\ \mathsf{Refl}\_A = \mathsf{Refl}\_{F A} \\ F (P \cdot Q) = F P \cdot F Q$$ This is essentially the direction of homotopy type theory, where these properties are internalized (and the 'dimension' is not limited to just groupoids).

The second functoriality property is already in the other answer. The "identity extension lemma" is a functoriality property where categories are relaxed to reflextive graphs (rather than tightened to groupoids). Again, type formation operations are able to be functorial because reflexive graphs do not have operations where 'direction' matters. However, this time it is because edges are not assumed to be composible.

So, the identity extension lemma says that every relation $R : A \Leftrightarrow B$ induces a relation $FR : FA \Leftrightarrow FB$ where:

$$F\ \mathsf{Refl}\_A = \mathsf{Refl}\_{F A}$$

And that's all there is to being a "relator" of reflexive graphs. There are also type systems that can talk about this sort of thing internally, possibly even with homotopy type theory features, like here.

Now, The first approach doesn't give you 'normal' functoriality for all type formations because not every map $f : A → B$ is an isomorphism. And of course, if we do $F A = A → A$, that's not going to extend to $(A → A) → (B → B)$ nor the other direction, without also having some map in the other direction. However, given an isomorphism, it induces $(A → A) \cong (B → B)$

In the second approach, a map $f : A → B$ induces a relation $\mathsf{gr} f : A \Leftrightarrow B$ given by $(x, f\ x)$. However, although we could compose the maps, there is no notion of composition of relations to talk about, and relate back to the composed functions. Considering the same type construction:

$$FR(m,n)\quad \Longleftrightarrow \quad R(x,y) ⇒ R(m\ x, n\ y)$$

So:

$$F(\mathsf{gr}\ f)(m,n)\quad \Longleftrightarrow\quad f \circ m = n \circ f$$

If you try to apply this to composed maps, then you know:

$$f \circ m = n \circ f \\ g \circ m = n \circ g$$

so $$f \circ g \circ m = f \circ n \circ g$$

but then there's nothing to do further.

You can read more about this angle in this paper, which tries to apply parametricity to a wider mathematical scope. A counter-question that the paper kind of motivates is: why do you care specifically about *category* functoriality? The original intuitive specification of "naturality" sounds very much like the intuitive specification of "parametricity," but the former was eventually formalized in terms of directed maps, rather than undirected relations. However, there is nothing inherently more legitimate about directed maps vs. relations or isomorphisms, and some things work out more appropriately for the latter than the former. Sometimes even in category theory it it necessary to shift into the 'undirected' perspective to make easier sense of something. See for instance here.

On a final note, you *can* have a type theory that keeps track of category theoretic functoriality of things. Here is early work, and here is something closer to homotopy type theory. The former tracks functoriality of everything explicitly, and is of course significantly more complicated for it. The latter allows functoriality to be an internally definable property, similar to the 'dimension' in homotopy type theory. But in neither would every type expression be necessarily functorial with respect to directed maps, because that would require limiting what one is able to write.
> 1 votes

# Answer
In a specific lambda-calculus, e.g., in System F, you can just write the type and see whether it is covariant in its free type parameters. Each function arrow creates a contravariant position to the left of it and a covariant position to the right of it. So, for example, `F a b = (a -> a -> b) -> a` is covariant in `a` and contravariant in `b`.

The morphism parts of the functor follow automatically from the type.

There is a parametricity result that a covariant type constructor has a unique `fmap` method that satisfies the parametricity law. It will then follow that the `fmap` method also satisfies the functor laws.
> 0 votes

---
Tags: type-theory, category-theory, haskell, polymorphisms
---


title: Halting problem disproof

text:
# Question
Title: Halting problem disproof
## Introduction

This is a heavily updated question I have asked on this forum previously. I have understood and corrected the earlier errors and mistakes I made, and after doing that it still seems I have a problem. I would also like to state that I am not looking for a different proof of the halting problem, and I am not looking to disprove it, just to determine why *my counter* falls apart.

## The original proof

let $f(x)$ be an arbitrary piece of code run on the input $x$. The program $f$ has an encoded representation, e.g in binary, which we denote as $\[f\]$.
Assume there exists a function $h(f,x)$, which returns $True$ iff $f(x)$ halts. We *must* then be able to create the composite function $ h'(f)$ which just runs $h(f,\[f\])$.
We can then create the final function $H(f)$, which can be represented in pseudocode as:

```
if h'(f):
 Loop
else:
 return

```

To summarise, $H(f)$ will loop if $f(\[f\])$ doesn't, and will not loop if $f(\[f\])$ does.
From the function $H(f)$, we can create a paradox by running $H(H)$. This is as if $H(H)$ loops, then $h'(H)$ must have shown that $H(H)$ did not loop, which is the opposite of out assumption. Likewise if $H(H)$ does not loop, then $h'(H)$ must have shown that $H(H)$ did loop, and paradox. Hence, the function $h(f,x)$ cannot exist.

## The counter

The key idea of my counter argument, is that the original disproof seems not to care what the function $h(f,x)$ or the condition it evaluates to (Halt or no) actually is. Taking advantage of that fact, we can recreate the argument except instead of using the function $h$ we create are own function which we know we know exists. This means if we observe a paradox with our new function which we know can be created, the paradox with $h$ does not mean $h$ can't be created.

## Setup

Let the function $r(f,x)$ return $-f(x)$, where $f(x)$ is a function which returns a value . We can then create the function $R(f)$ which is equal to $r(f,\[f\])$. If a function can be expanded into a infinite tower of functions we call it telescopic, e.g if $H(H) = H(H,H) = (H(H(H)) = H(H(H(H(...))))$ then $H(H)$ is telescopic (I have expanded $H$ slightly here for convenience. with the expansion, $H(f)$ is just shown as $H(f(\[f\]))$).
We then have 3 possibilities:

1. $H(H)$ is not telescopic
2. $H(H)$ is telescopic, but has a time complexity \> $O(1)$#
3. $H(H)$ is telescopic, and has constant time complexity.

### Case 1

If case 1 is true, then the function $R(R)$ is also logically not telescopic. That means we have the same paradox for a function, $r$, which is real. This is as if $R(R)$ is positive, $R(R)$ should be negative and vice versa. The condition that $r$ runs only on algorithms that do not halt is not violated. This is because if an algorithm returns a value (so does not halt), the output can be multiplied by -1, which is what $r$ does. This means that for all inputs of $r$, which by definition do not halt, $r$ does not halt. This is the same for $R$. Because of this, $R(R)$ must not violate the condition as $R$ does not halt, and the input size is not infinite as we assume in case 1 that $R(R) != R(R(R(R(R(...)))))$. In case 1, $h$ is not proved as being impossible as the same paradox can be created with a real function.

### Case 2

If case 2 is true, then the function $H(H)$ telescopes. This means that the function $H(H)$ has an infinite sized input. Because the pseudocode of $H$ just checks if $h'$ returns false to decide if it loops or not, if $h'$ takes infinite time to compute then we get that $H(H)$ does not halt, but this is not because $h'(H)$ has evaluated to true, but because $h'$ does not evaluate at all because it has a telescoping, so infinite sized, input. This is the same paradox as when we run $R(R)$. $R(R)$ telescopes, so although $R$ will return on all non halting inputs, and so $R$ does always halt, $R$ when run on an infinite chain of inputs will halt, even though the chain is made up of halting functions; an infinite chain of halting functions does not necessarily halt. Because we can create a paradox in the possible function $r$ the same as the function $H$, the paradox for $H$ does not prove that $H$ does not exist - non-termination is not the same as a paradox.

### Case 3

If case 3 is true, then because $H(H)$ has an infinite input does not matter; $H$ will still evaluate at some point. In this case, the paradox holds. The reason that even though in case 2 a function which can compute for any input is unable to compute a given input, is as the given input is essentially infinity, which is seen by analogy through $r$. The input being infinity does not matter in case 3, as $h$ takes constant time. The only problem is that for $h$ to compute at always the same pace, $h$ cannot actually read or use the program. A given program which prints "Hello world" 1 time, and then has a while true loop would be evaluated as fast as the same program which prints "Hello world" 3 times. If $h$ knows if a program will halt, it should also know where it halts, or what causes it to halt, so $h$ should identify that the while loop causes it to not halt. The program of "Hello world" and a while loop could be represented as an array, where 1 is the while loop and 0 is a print, the first example could be represented as `[0,1]`. The second example would be `[0,0,0,1]`. Any binary array could be represented as a sequence of hello worlds and while loops, but $h$ would be able to determine the existence of a 1 in any of the arrays with constant time, which I do not believe is possible.

### Conclusion

First of all, thank you for reading my convoluted essay, I appreciate you taking the time to read this and if you see a mistake please let me know. What I hope I have shown is the following: best case scenario, where my argument in case 3 is incorrect, the halting problem proof seems to only disprove the existence of a function $h$ which acts like case 3. A function $h$ which determines if the input function halts in $O(n)$ or $O(logn)$ or any other time complexity is, on the other hand, valid. On the other hand, even if my argument in case 3 is correct, the exact same conclusion exists where $h$ cannot exist. Have I made a mistake in my logic somewhere? Its possible my case 2 and 3 arguments are incorrect but I cannot work out where I have gone wrong.

# Answer
> 6 votes
> the original disproof seems not to care what the function $h(f,x)$ or the condition it evaluates to (Halt or no) actually is

This statement looks to me like a misunderstanding. The original proof does "care": see the statement "Assume there exists a function $h(f,x)$, which returns $True$ iff $f(x)$ halts.".

> Let the function $r(f,x)$ return $-f(x)$, where $f(x)$ is a function which returns a value.

This is not yet a well-defined definition of $r$. If the intent is to define a mathematical function, you must specify the result of $r$ on all possible inputs; you haven't specified what the value of $r(f,x)$ is when $f(x)$ doesn't return a value. If the intent is to define an algorithm (i.e., a function in some programming language), you must specify the steps the computer takes to compute it. There is no (always-terminating) way for a computer algorithm to check whether $f(x)$ will return or not.

Perhaps you mean that the algorithm $r(f,x)$ is defined by the code "return -$f(x)$". In that case, there is no "where..." clause.

In that case, it appears that $R(f)$ can be defined as the algorithm that executes the code "return -$f(\[f\])$".

I find the definition of "telescopic" unclear. For instance, if I define the function $g$ by $g(x)=7$ for all $x$, is $g(g)$ considered telescopic? Well, $g(g)=7$ and $g(g(g))=7$ and so on, so $g(g)=g(g(g))=\cdots$, so it appears it satisfies the conditions of the definition and can be considered telescopic. Yet I'm unsure whether that is your intent.

I don't understand what is the definition of $H$ in this proof.

I don't understand why it follows that if $H(H)$ is telescopic then $R(R)$ is not telescopic.

I don't understand what you mean by the time complexity of $H(H)$ being $O(1)$. $H(H)$ is a single expression. To use asymptotic notation, normally we have to have a family of problems, with running time a function of the length of the problem input. That doesn't seem relevant here as we don't have a family of problems, we don't have a function, we just have a single expression $H(H)$. The running time to evaluate $H(H)$ is what it is: it is either a fixed constant (if $H(H)$ terminates) or it is infinite (if $H(H)$ doesn't terminate). Asymptotic notation is not applicable here.

---

I haven't tried to check the rest of the argument for errors. One error is enough to invalidate a proof.

In general, if you're not convinced by a proof, rather than trying to construct some other complicated proof that seems analogous to you, it might be a more effective strategy to identify the first statement in the proof that you don't find convincing. If do you find all statements convincing, then presumably you should be convinced by the proof. When you construct a long complicated proof, there is a good chance there is an error in it somewhere, but checking the correctness of proofs is not really the purpose of this site. Our mission is to build up a high-quality archive of knowledge, in the format of questions and answers that will hopefully be helpful to others in the future. If you're the only one to come up with that long complicated proof, then it's not clear how checking that proof in detail would contribute to the mission.

# Answer
> 1 votes
I don't understand your points about telescoping and time complexity, but I don't think I need to.

I see you have defined this program $r(f,x)$ and you have found a case where the program does not halt and there's no way to fix it to make it halt. What I think you have proven is: there is no such program $r(f,x)$ that always halts and returns the negative of whatever $f(x)$ returns.

You could make one that did always halt, but it wouldn't always give the correct answer. Every possible $r$ *either* gives wrong answers *or* sometimes doesn't halt.

To connect this to the halting problem, notice that *a halting decider **always** halts.* If a program sometimes doesn't halt, then it's not a halting decider. You proved that every possible program-negative-number-maker gives wrong answers or sometimes doesn't halt, and therefore it isn't really a program-negative-number-maker. The same logic shows that every possible halting decider gives wrong answers or sometimes doesn't halt, and therefore it isn't really a halting decider.

See also Rice's theorem which says: "all non-trivial semantic properties of programs are undecidable." Yup, that's right - ***all** of them*. There's no way to tell whether a program always returns 42. There's no way to tell whether a program always returns a positive number. Your version isn't quite the same but I think it's the same basic idea.

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


title: Counting independent sets

text:
# Question
Title: Counting independent sets
I know the Independent set problem is NP-complete. But could there be a more efficient way to count the exact number of different independent sets in an arbitrary, given graph?

# Answer
> 4 votes
No, this problem is well-known to be #P-complete. For more, you can see this question on CSTheory.

---
Tags: algorithms, graphs, combinatorics, counting
---


# Question
Title: Is $L = \{a^{p^2}\mid p\text{ is a prime}\}$ regular?
By pumping lemma, we choose the word $w=a^{p^2}$ that the decomposing is $\[a^sa^ta^{p-s-t}\]^p$ such that $u=a^s,v^i=a^t,x=a^{p-s-t}$

$\[a^sa^{it}a^{p-s-t}\]^p=\[a^{p+it-t}\]^p$

We choose i=p+1,we get $ \[a^{(1+t)p}\]^p $ $=a^{(1+t)p^{2}}$

we see that the power $(1+t)p^{2}$ has 4 dividers thus doesn't belong to the Language L where the power of a is $p^2$ with 3 dividers.

Is my answer correct?

# Answer
> 3 votes
Instead of looking at primes I would prove this:

The language { a^k: k is an element of S } where S is an infinite set of non-negative integers with arbitrary large gaps between elements is not regular.

It's not more difficult than the statement you have, and it proves immediately that languages like $a^{n^2}$, $a^{n!}$ etc. are all non-regular.

---
Tags: regular-languages, automata, finite-automata
---


# Question
Title: Coin exchange, find different triples of values
Suppose i have 3 coins: **A, B, C**. Each one of them have different value: **a, b, c**. And if want to exchange coins A for coins B, i need to be able to give exactly a units of currency A and get exactly b units of currency B in return. The problem is to find how many different triples of coins i can have? For example, if i got 1 coins of A, 0 coins of B, 3 coins of C, and its currencies is a=1 b=1 c=1, i can have 10 different triples of values:

* 0 0 3
* 0 3 0
* 3 0 0
* 1 0 2
* 1 2 0
* 2 1 0
* 0 1 2
* 0 2 1
* 2 0 1
* 1 1 1

Is there any mathematical formula that allows me to do this calculation without looping through all possible triples? (1 ≤ A, B, C ≤ 10^9), (0 ≤ a, b, c ≤ 10^9)

# Answer
1. Introduce integer variables $x,y,z$. Let $x$ count the number of times that you've exchanged a units of currency A for b units of currency B, $y$ count the number of times that you've exchanged a units of currency A for c units of currency C, and $z$ count the number of times that you've exchanged b units of currency B for c units of currency C.
2. Write down linear inequalities on $x,y,z$ that determine which values lead to an admissible triple. (This is your programming contest / exercise problem, so you get to do this part.)
3. Implement an algorithm to count the number of solutions to this integer linear program, or equivalently, count the number of integer lattice points in this convex polytope. See, e.g., Finding all solutions to an integer linear programming (ILP) problem, https://math.stackexchange.com/questions/3001715/find-the-number-of-non-negative-integer-solutions-to-linear-systems, Counting the number of satisfied models - given mathematical constraints.
4. Submit to your programming contest and win the contest. Make sure to credit all sources that you used in doing so.
> 0 votes

---
Tags: algorithms, coin-change
---


# Question
Title: Is the reason for a stack to decrease the size of a program (by adding the use of subroutines)?
The stack allows subroutines to be used. It can store return address for "return from subroutine" instruction (RTN) and also arguments for the function.

It is not possible to store return address in the program instruction list itself, because the subroutine might be called from many different places in the program, and the return address will differ.

The same with arguments, the argument passed to the subroutine differs.

Without stack, the subroutine as a whole would have to be printed out multiple times in the program instruction sequence (i.e., there would not be subroutines. )

So is the reason a stack architecture was developed/designed originally (and still to this day) to reduce the size of the program mainly?

There might be more reasons than arguments and return addresses for stack, but those are as much as I understand so far.

# Answer
> 5 votes
The reason for having a stack is recursion. You don’t need a stack if you don’t have recursion. CDC super computers in the 70s worked just fine without a stack - until they implemented Pascal.

On these machines the "Subroutine call" instruction stored a "Jump" instruction just before the start of the called subroutine. Which means only one call to any subroutine could be running at any time (recursion means one function is called again from a different location while it is running. A call from the same location would actually work, but the *first* recursively called function must have two calls from different locations, so the first Jump instruction would be overwritten with a different one). No limit on the number of subroutines being called. And no recursion means all variables can be stored at fixed addresses.

# Answer
> 1 votes
No, a compelling reason is that you can't predict the call pattern of the functions. In particular, you cannot predict the recursion depth so it is impossible to preallocate.

# Answer
> 1 votes
Alan Turing defined a stack in 1946 (article) and that it provided a way to save the return address of all active subroutines, thereby allowing code to be simplified into reusable subroutines. The stack was expanded on with the work of Klaus Samelson and Friedrich Bauer in 1955 (Wikipedia), that focused on locally declared data within scopes. This latter service is what stack is most indispensable for, reentrant functions need to have local variables for each iteration of the function being called. The storage of return addresses can be handled without a stack (although Turing himself did conceptualize a stack for this reason, and it is a logical architecture to manage that), so to be a bit pedantic, the stack is mostly indispensable for recursive functions, *but*, one reason for it is to allow subroutines, and thereby shrink and simplify the code.

# Answer
> 1 votes
> Without stack, the subroutine as a whole would have to be printed out multiple times in the program instruction sequence (i.e., there would not be subroutines. )

No. One can easily write the equivalent of a non-reentrant subroutine by storing the return address and the arguments in the "subroutine" itself:

```
          STORE_IMMEDIATE FAKE_SUB      .+4
          STORE           FAKE_SUB+1    ARG_1
          STORE           FAKE_SUB+2    ARG_2
          GOTO            FAKE_SUB+3
          …

FAKE_SUB  DATA            0
          DATA            0
          DATA            0
          …
          GOTO            *FAKE_SUB

```

Alternatively, the args could be stored in the caller's space, and the "subroutine" could access them relative to the return address.

> So is the reason a stack architecture was developed/designed originally (and still to this day) to reduce the size of the program mainly?

I don't know about *mainly*, but having a stack definitely makes that easier.

Consider having several subroutines, each of which needs to use a large array in which to manipulate data. With subroutines, those arrays can be allocated on the stack ("auto" in C), and so will make use of the same overlapping temporary memory rather than permanently allocating space for each subroutine.

---
Tags: computer-architecture, information-theory, cpu, history, stacks
---


# Question
Title: Multiplying 2 positive integers using FFT and convolutions
I was trying to figure out how I can perform multiplication of 2 big integers using FFT and convolutions, I ran into the following article: http://numbers.computation.free.fr/Constants/Algorithms/fft.html
I understand the main points behind the algorithm but I can't understand this part:

> **2.3 More on the complexity of multiplication with FFT**
>
> In fact, the time complexity of multiplication with FFT is a little bigger than n log(n).
>
> Let us be more precise.
>
> To multiply two numbers of N digits, we write them in a base B which contains k digits (say B = $10^k$), thus giving a number of coefficients equal to n $\approx$ N/k.
>
> The discussion above tells us that to multiply those two numbers, FFT permits to perform $O(n log(n))$ operations on basic numbers (basic numbers express coefficients in the base B, they are usually basic numerical data types like double in C of Fortran)
>
> Because of the numerical error bound (1), these basic numbers should be precise enough to represent integers up to 6n2B2log(n) (for example, working in double precision, the base B should be choosen small enough so that the error bound is not too large... and this is not even possible if n is too large).
>
> Thus the number of digits of these basic numbers should be of the order of log(B)+log(n). As a consequence, the basic operations on these numbers has cost O((log(B)+log(n))2) and the final cost is O( n log(n) (log(B) + log(n))2). The base B is choosen so that $k = log\_{10}(B)$ is of the same order than log(n), and finally, multiplying those two numbers of $N \approx kn$ digits have cost $O( n log(n)^3 ) = O( N log(N)^2)$.

I need some clarification on how to write the numbers in a certain base B and why when $B = 10^k$ the base contains k digits in their example, it shouldn't contain $10^k$ digits? Such implementation should be recursive? I'll be grateful if someone can provide an example with numbers on how to execute this algorithm (without performing the FFT of course). thanks!

# Answer
> 1 votes
Kind of covered this in a class of mine so taking excerpts from lecture slides/online resources here is my attempt at answering it.

In the context of using FFT for multiplication of two large integers, writing the numbers in a certain base $B$ refers to expressing the coefficients of the numbers in that base. This is done in order to reduce the number of coefficients that need to be multiplied, which in turn reduces the complexity of the multiplication. For example, if you have two large integers $X$ and $Y$ that you want to multiply, you can express each of these numbers in base $B$ as:

$\begin{align} X &= x\_0 + x\_1 \cdot B + x\_2 \cdot B^2 + \cdots + x\_n \cdot B^n\\ Y &= y\_0 + y\_1 \cdot B + y\_2 \cdot B^2 + \cdots + y\_n \cdot B^n \end{align}$

where $x\_0, x\_1, ..., x\_n$ and $y\_0, y\_1, ..., y\_n$ are the coefficients of the numbers in base $B$. The idea is to choose the base $B$ so that the number of coefficients $n$ is significantly smaller than the number of digits in the original numbers ($N$), allowing you to perform the multiplication more efficiently.

For example, if you choose $B = 10^k$, where $k$ is the number of digits in a single coefficient, then the base $B$ will contain $k$ digits. For instance, if you have two numbers $X$ and $Y$ with a total of 1000 digits, and you choose $k = 3$, then you can express $X$ and $Y$ in base $B = 1000$, which will contain 3 digits in each coefficient. This will result in a total of $n = 1000/3 = 333$ coefficients for each number, which is significantly smaller than the original number of digits ($N = 1000$).

The reason why the base $B$ is chosen so that $k = \log\_{10}B$ is of the same order as $\log n$ is because this allows the number of coefficients $n$ to be significantly smaller than the number of digits in the original numbers ($N$), which in turn reduces the complexity of the multiplication. For example, if you have two numbers $X$ and $Y$ with 1000 digits each, and you choose $k = 3$, then you will have a total of $n = 1000/3 = 333$ coefficients for each number. This is significantly smaller than the original number of digits ($N = 1000$), which allows you to perform the multiplication more efficiently.

I also don't think this approach is recursive, as the FFT algorithm itself is recursive. The idea is to express the numbers in a certain base $B$ in order to reduce the number of coefficients that need to be multiplied, which in turn reduces the complexity of the multiplication.

# Answer
> 1 votes
The Algorithm Archive has an article on Multiplication as a convolution where they give enough details to understand how to implement it, and they also have example code on both convolutions and FFT you can use to implement a full multiplication algorithm.

I implemented a version for my student to illustrate, perhaps it becomes clearer when you see actual code, and when you can experiment with it yourself:

```
from sys import argv

def convolve(F, G):
    NF = len(F)
    NG = len(G)
    N = NF + NG - 1
    C = [0 for _ in range(N)]
    s = 0
    for i in range(N):
        for j in range(max(0, i - NG), i + 1):
            if j < NF and (i - j) < NG:
                s += F[j] * G[i - j]
        C[i] = s
        s = 0
    return C

def carry(data):
    """Perform carrying, meaning that
    the "number" [2, 17, 5] becomes [3, 7, 5].
    """
    change = 1
    while change:
        change = 0
        cp = [0 for _ in data]
        for idx, e in enumerate(data):
            if e >= 10:
                change = 1
                car = e // 10
                cp[idx - 1] += car
                cp[idx] = e - (car * 10)
            else:
                cp[idx] = e
        data = cp
    return cp

if __name__ == "__main__":
    if len(argv) < 2:
        exit("Usage: convolution A B (integers)")
    x, y = [int(e) for e in argv[1]], [int(e) for e in argv[2]]
    print(f"{x=}\n{y=}")
    C = convolve(x, y)
    print(f"{C=}")
    M = carry(C)
    strM = "".join([str(e) for e in M])
    print(f"{argv[1]} * {argv[2]} = {strM}")

```

When run from the terminal: (the `C` array is the carrying that needs to be done)

```
[~]$ python convolution.py 1234 5678
x=[1, 2, 3, 4]
y=[5, 6, 7, 8]
C=[5, 16, 34, 60, 61, 52, 32]
1234 * 5678 = 7006652

```

# Answer
> 1 votes
Multiplication using FFT and convolution requires that your arithmetic is performed with some precision. There's always an argument "I use floating point arithmetic with rounding errors, but since I know that the correct result must be an integer, as long as I can prove that the rounding error is less than 0.5, I can determine the correct integer result." For example, if a result is known to be an integer for obvious mathematical reasons, and I tell you "I found the result 119.46, and the rounding error is less than 0.5", then it is obvious that the correct result is 119 and not 120 or any other number.

If your FFT uses many numbers, rounding errors become bigger. At some point using double precision floating point doesn't allow you to give a guarantee that the error is less than 0.5. So you use extended precision, or quad precision. So you can handle much much larger numbers with an error less than 0.5. And at some point that isn't enough, so you need to implement higher precision.

All in all, the number of operations grows with n log n, but the cost of each operation also grows very very slowly with n. Usually we will just implement say quad precision and note that "this implementation will not give the correct result if n \> (some huge number)". And that will be acceptable if (some huge number) is so big that no computer in the world would be able to calculate an FFT of that size anyway. Except in theory, it is not acceptable.

Now about recursion: Your double precision, quad precision, six time precision floating point arithmetic would be hand coded. However, n could become so incredibly huge that the basic operations are big enough to make implementing them with FFT becomes worthwhile. You could have an astronomically huge n so that your basic arithmetic needs to be performed with 10,000 bit precision, and then you would implement your basic arithmetic with FFT. And then we could make n even more astronomically huge, so that the FFT we use for implementing its basic arithmetic is so huge that we need higher precision for implementing that.

So to do things in a CS correct way, you figure out what number of bits you need to do FFTs of n numbers correctly, and what time you would need for the basic operations implementing your FFTs, and take that into account in your big-O.

There is also a psychological effect. Multiplication of two n bit numbers in a straightforward way takes O(n^2) operations. But a typical computer today implements this for n ≤ 64 using O(n^2) hardware and constant time. So in practice this O(n^2) factor doesn't matter to us and we ignore it. 3 x 3 bit or 64 x 64 bit are the same on a modern computer. (On an ancient 8 bit computer, the first would take one and the second would take 64 multiplications if implemented natively, so 40 years ago I wouldn't have said 64 x 64 bit takes constant time).

---
Tags: integers, multiplication, fast-fourier-transform
---


# Question
Title: what language does S->aaSbb|SS|epslion make?
I've been thinking about this for a day now,can someone help me ?

what language does S-\>aaSbb|SS|epslion make?

# Answer
> 0 votes
Let $L(G)$ as the language of grammar $G$ so

$$L=\\{w\in\\{aa,bb\\}^\* \mid n\_a(w)=n\_b(w)\text{ such that any prefix } u \text{ of } w:\ n\_{a}(u)\ge n\_{b}(u)\\}.$$ (Note that $n\_x$ count number of occurrence of $x$ in string $w$.)

Also you can prove that $L=L(G)$ by strong induction or try to show that $L(G)\subseteq L$ and visa verse.

---
Tags: automata
---


# Question
Title: In the declarative semantics of definite programs, $T_P \downarrow \omega$ is not equal to the greatest fixpoint of $T_P$
I am studying theoretical computer science using the book "Foundations of Logic Programming" by J. W. Loyd. I am in the part about declarative semantics of definite programs.

In the book, if $P$ is a definite program, we denote by $B\_P$ the Herbrand base of $P$ and we define $T\_P$ as:

> **Definition.** Let $P$ be a definite program. The mapping $T\_P: 2^{B\_P} \rightarrow 2^{B\_P}$ is defined as follows. Let $I$ be a Herbrand interpretation. Then $$T\_P(I) = \\{A \in B\_P \ | \ A \leftarrow A\_1, \ldots, A\_n \text{ is a ground instance of a clause in } P \text{ and } \\{A\_1, \ldots, A\_n \\} \subseteq I \\} $$

We denote by $gfp(T\_P)$ the greatest fixpoint of $T\_P$. I am currently trying to understand an example that shows that $T\_P \downarrow \omega \neq gfp(T\_P)$. The example is below:

> **Example** Consider the program $P$
>
> \begin{align\*} p(f(x)) &\leftarrow p(x) \\ q(a) &\leftarrow p(x) \\ \end{align\*} Then, $T\_P \downarrow \omega = \\{q(a)\\}$, but $gfp(T\_P) = \emptyset$. In fact $gfp(T\_P) = T\_P \downarrow (\omega + 1)$.

My doubt: why is $T\_P \downarrow \omega = \\{q(a)\\}$?

I tried looking at the definition of $T \downarrow \omega$ (written below), but I think I am failing to make the connection between this definition in terms of complete lattices and the mapping $T\_P$.

> **Definition** Let $L$ be a complete lattice and $T: L \rightarrow L$ be monotonic. Then we define:
>
> $T \downarrow 0 = \top$
>
> $T \downarrow \alpha = T(T\downarrow (\alpha - 1))$, if $\alpha$ is a successor ordinal
>
> $T \downarrow \alpha = glb\\{ T \downarrow \beta \ : \beta \< \alpha \\}$, if $\alpha$ is a limit ordinal. Here $glb$ denotes the greatest lower bound.

Can anyone tell me how do we obtain $T\_P \downarrow \omega = \\{q(a)\\}$? Thanks in advance.

# Answer
Our lattice is $L = 2^{B\_P}$ with the partial order being set inclusion. In this case, $\top = B\_P$ and $\bot = \emptyset$. Notice that the Herbrand universe is $U\_P = \\{f^n(a) \ | \ n \geq 0 \\}$ and hence $B\_P = \\{ p(t)\ | \ t \in U\_P \\} \cup \\{ q(t)\ | \ t \in U\_P \\} $.

If we apply the definitions we get:

> $T\_P \downarrow 0 = \top = B\_P$.
>
> $T\_P \downarrow 1 = T\_P(T\_P \downarrow 0) = T\_P(B\_P) = \\{ q(a) \\} \cup \\{ p(f(t)) \ | \ t \in U\_P \\}$, where we used the definition of $T\_P$ in the last equality.
>
> $T\_P \downarrow 2 = T\_P(T\_P \downarrow 1) = \\{q(a)\\} \cup \\{p(f^2(t)) \ | \ t \in U\_P \\}$
>
> $\vdots$
>
> $T\_P \downarrow n = \\{q(a)\\} \cup \\{p(f^n(t)) \ | \ t \in U\_P \\}$

Hence, we have $T\_P \downarrow \omega = glb \\{ T\_P \downarrow n \ | \ n \< \omega \\} $ and $T\_P \downarrow n = \\{q(a)\\} \cup \\{p(f^n(t)) \ | \ t \in U\_P \\} $, which let us conclude that $T\_P \downarrow \omega = \\{q(a)\\}$ by the definition of greatest lower bound.
> 0 votes

---
Tags: prolog, lattices
---


# Question
Title: Curry–Howard correspondence and functional programming "reliability"
The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".

I recently learnt about the Curry-Howard (CH) correspondence and I think this is what he was using as a basis for his assertion about functional languages.

However, I have trouble understanding how far this leads to "more reliable programs".

Especially, here is my understanding:

* In the CH view, a function type `A -> B` is the same as an implication $A \implies B$ in some constructive view of logic, and so on... (union type, product of type, etc.)
* So if we end up being able to build an instance `t` of a type `T` it means we used only the available function types / implications using the available variables / assumptions.

Still, there are many ways a program written this way could be incorrect :

* If I have several variables `a`, `b`, `c`, ... of the same type `A` available, I may use a transformation `A -> B` on the wrong one.
* I may have different functions with the same signature `A -> B` but different use cases, and the type system won't be able to detect if I use the wrong one.

My questions are:

* In practice, do functional programming languages enforce things like "there should be no more than one instance of a type" or some variant to avoid those kinds of errors ?
* Is there a theoretical background in which we enforce more restrictions on functional languages and give the "more reliable" a stronger meaning ?

# Answer
> 4 votes
The dependent types allow you to specify what properties your function should have, not just what its domain and codomain are. This way it becomes impossible to accidentally use the wrong function.

For example, suppose we want a function that sorts lists (of integers). In ordinary programming we would ask for a value of type `List → List`, and then we would write documentation in English that says "and it is supposed to sort lists".

With dependent types, we would write down a fancier type:

```
Σ (f : List → List) Π (lst : List) isSorted(f lst) × isPermutation(lst, f lst)

```

(See below how one defines `isSorted` and `isPermutation`.) An element of this type is a pair `(f, p)` such that `f : List → List` and `p` is a function which takes as input any list `lst` and outputs a pair `(q, r)`, such that: `q` is the proof that `isSorted f lst` and `r` is the proof that `lst` is a permutation of `f lst`. In other words, `p` proves that the output of `f lst` is precisely the sorted list `lst`.

If you think about it, it is impossible to accidentally use a non-sorting function. If you do, then you will not be able to also write down the proof that it really sorts lists.

In ordinary programming we are used to write down data and functions into the source code, but keep their *properties* in our heads. In dependent programming the properties are part of the source code, and so are the proof that those properties are satisfied.

P.S. We define `isSorted : List → Type` as

```
isSorted nil = True
isSorted (x :: lst) = (Π (y : int) . elementOf y lst → x ≤ y) × isSorted lst

```

It is a bit more annoying to define `isPermutation`, so I will not do it here.

# Answer
> 1 votes
The type system in FP languages helps you avoid a certain number of errors. The more you use various features of the type system, the more errors you can exclude.

For example, if you need the list of session IDs to be always non-empty, you can use a data type "non-empty list" and ensure at compile time that no place in the program will, by mistake, create an empty list as the list of session IDs.

If you are concerned that the function of type `a -> a -> b` should not confuse the two arguments, you can create two new types and use them instead of `a`. So, instead of a function of type `String -> String -> IO String` you write:

```
 newtype KafkaTopicForInput = KTFI String
 newtype KafkaTopicForOutput = KTFO String
 f :: KafkaTopicForInput -> KafkaTopicForOutput -> IO String

```

Then it is not possible to pass arguments to `f` in the wrong order.

There are other such tricks in the FP arsenal. If you use the `State` monad, you cannot accidentally forget to update the mutable state. If you use the `Either` monad, you cannot accidentally forget to handle an error situation.

The Curry-Howard correspondence ensures another type of correctness: that your program will not crash at runtime if it compiles without errors. In languages that do not fully follow the CH correspondence, one can write a program that will crash at runtime because the program appears to compute a value of some type but actually does not. (In the CH correspondence, the corresponding logical theorems are false but appear to be true because the logic is inconsistent and you can prove a false statement.)

At the same time, FP type systems typically will not help you write correct algorithms. If you need all session IDs to contain valid base-64 alphanumeric strings, the type system will not be able to help you, it's a very complicated condition. Other tools should be used to ensure that.

---
Tags: type-theory, functional-programming, correctness-proof, curry-howard
---