11

It has to do with the axiom of extensionality, i.e. whether you accept it for functions or not. The statement of this axiom with regard to functions is $$\forall f,g:A \to B,\ ((\forall x:A ,\ f\ x = g\ x) \Leftrightarrow f = g).$$ Informally it means that if two functions are equal point-wise, then we consider them equal. Syntactically merge-sort and ...


8

This problem is known as rigid E-unification. This problem is NP-complete. The first proof was given by Gallier, Narendran, Plaisted and Snyder [1]. However a related problem, the Simultaneous rigid E-unification that is to find a substitution that simultaneously satisfies several instances of rigid E-unification is undecidable. This result was proved by ...


7

A complete understanding of what J was actually saying and why has only come fairly recently. This blog post discusses it. While thinking in terms of homotopy and continuous functions provides a lot of intuition and connects to a very rich area of mathematics, I'm going to try to keep the discussion below at the logical level. Let's say you axiomatized ...


6

Equality is a syntactic notion, equivalence is a semantic notion. Two expressions are equal if they are the same expression — in other words, an expression is only equal to itself. Two logical expressions are equivalent if they have the same truth value in every interpretation. Two equal expressions are always equivalent, but the converse doesn't hold....


5

Recall that (a few paragraphs above) two objects are definitionally equal if after certain computation steps they evaluate to identical results. Assume throughout this post that $M$ and $N$ are definitionally equal. This means that there is a series of computation steps $M_0 \leftrightarrow M_1 \leftrightarrow \ldots \leftrightarrow M_n$ where I use $\...


5

You got the definition of $L^+$ wrong. It is not $L^* \setminus \{\epsilon\}$. Rather, it is $$ L^+ = \bigcup_{n=1}^* L^n. $$ You can check that $\epsilon \in L^+$ iff $\epsilon \in L$. Therefore: If $\epsilon \notin L$ then $L^+ = L^*\setminus\{\epsilon\}$. If $\epsilon \in L$ then $L^+ = L^*$.


5

Supposing we have $a$ and $b$ of type $A$ and $p : \mathrm{Id}_A(a,b)$, there simply is not any rule of type theory that would allow you to replace $b$ with $a$ arbitrarily. So one answer is "because type theory does not let you do that", and if you think that it can be done, please show me how. But I suppose that is a non-answer, what you really are asking ...


4

We don't always want extentionality In mathematics, a function is a relation between its inputs and its output. Two functions are equal if and only if they map the same outputs to the same inputs. But in computer science, we're often interested in descriptions of computations which we also call “functions”, where it matters how the outputs are calculated ...


4

If you use the operators $\{+,-,\times,/\}$ (i.e., you don't included the power operator), then all of your problems are likely decidable. Testing equality with zero For instance, let's consider $L = \mathbb{Z} \cup \{\pi\}$. Then you can treat $\pi$ as a formal symbol, so that each leaf is a polynomial in $\mathbb{Z}[\pi]$ (e.g., the integer $5$ is the ...


4

This is a rather tricky question! As you seem to understand, the real issue is the presence of $\hat{}$. It is intimately related to a well known conjecture: Schanuel's conjecture, which states that, essentially, there are no non-trivial algebraic relationships between $\pi$ and $e$. The (expected) positive answer to this conjecture would give you a ...


4

I found out that such a thing is called anti-unification. This problem was addressed by Plotkin and Reynolds. Here is a brief overview.


3

In rewrite theory, you often want confluence of your system: if $$ u_1\leftarrow t\rightarrow u_2$$ Then there is some term $v$ such that $$ u_1\rightarrow v\leftarrow u_2$$ It is possible to tell whether a set of rewrite rules is confluent by examining the critical pairs: pairs of rules $t_1\rightarrow u_1,t_2\rightarrow u_2$ and an instance $\theta$ such ...


3

The idea of "stack" and "heap" is incoherent in my view. It is best not to think in those terms. The real difference is between locations that are named by (variable) symbols in the program (call them named locations) and locations (or groups of locations) whose references are stored in other locations (call them referenced locations). If you want, you ...


3

Algebraic numbers are solutions of polynomials with rational coefficients. $+,\times,-,/$ of algebraic numbers result in algebraic numbers because algebraic numbers form a field (1). This means nested radicals are algebraic numbers too (2). Nested radicals can be denested by algorithm (3,4). Each algebraic number of degree $n$ can be uniquely represented as ...


3

I don't know, but I suspect it's an open question. If the theory of the reals with exponential function is decidable, then your problem is decidable, too. It is known that if Shanuel's Conjecture holds, then the former is decidable, so your problem is too. If I understand correctly, the following paper tackles your problem: The identity problem for ...


2

The general answer to your question is no. Consider a function which measures the length of a linked list. How would you implement that without a branch? But if you just stick with functions which (say) take a machine word and return a machine word (which your example does) then the answer is "yes, sort of". In fact, when analysing algorithms in the word-...


2

What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $a$ and $b$, it normalizes both of them (based on judgemental ...


2

what does it mean by becoming extensional in the first place? The axiom of extensionality relates to what it means for two functions to be equal. Specifically, extensionality says: $f = g \iff \forall x \ldotp f(x) = g(x)$ That is, functions are equal if they map equal inputs to equal outputs. By this definition, quicksort and mergesort are equal, even if ...


2

You need to read all items in the worst case. Assume you have written some algorithm which reads items in any order and processes them with any amount of cleverness. And I'm your opponent and try to make you read as many items as possible. Here's what I do: Whenever your algorithm reads an item I store an "X" just before you read it. I do that except when ...


1

I'm fairly sure this is possible. This seems to me as a special case of set constraints over tree languages: we can view regular expressions as a restriction of regular tree languages where each node has 0 or 1 children. These can handle union, concatenation, and recursion (star), and you can solve for variables like you describe. They're decidable, even ...


1

It seems that there is a typo – $v_{i+1} - v_i$ should be $v_i - v_{i+1}$. Suppose first that all elements are distinct. Then (using the convention $v_0 = 0$) $$ \sum_{i=1}^{q-1} (v_i-v_{i+1}) n_i(B^*) + v_q n_q(B^*) = \\ \sum_{i=1}^{q-1} i (v_i-v_{i+1}) + q v_q = \\ \sum_{i=1}^q i v_i - \sum_{i=2}^q (i-1) v_i = \sum_{i=1}^q v_i. $$ Consider now the ...


1

Regarding DFS the answer is no. Here there is a counter example. The red arcs represent the DFS tree starting from the topmost node. This tree depth is 5 while the diameter is 3. On the other hand, the maximum BFS tree depth coincides with the diameter of the graph (of course, this is valid if the graph is connected). If you run BFS from a source node S, ...


1

Here is another solution. You can use the SeqHash data structure in the following paper: VerSum: Verifiable Computations Over Large Public Logs. Jelle van den Hooff, M. Frans Kaashoek, and Nickolai Zeldovich. CCS 2014. The SeqHash data structure is a tree-based data structure that lets you store a sequence of numbers. You can do each of the following ...


1

It's possible to build a data structure that in practice has $O(\lg n)$ lookup, $O(\lg n)$ insertion, and $O(1)$ equality-tests. I'll describe how below. (If you care about theoretical worst-case complexity, there are some caveats, but those caveats can probably be ignored for practical implementation.) You can handle the lookup, insertion, and creation ...


1

You ask for a computable property that can be used as a fingerprint for equivalence (algebraic equivalence in your case). There are two general approaches to this kind of question: Take a canonical element of the equivalence class (a normal form) as the fingerprint. Take the equivalence class itself as the fingerprint. Of course this requires classes to be ...


1

Assuming $N$ is not too large, consider using a bitvector. For example, you can use a single integer type as a data structure, or an array of bits. Insertion can be done in constant time, and equality checking is very fast as well.


1

If you are not allowed to add the same value more than once, then the insert operation can add the hash value of $i$ to some accumulator associated with $s$, and the equality testing can compare the accumulators. If you are allowed to add the same value twice, you can use Bloom filters.


1

Let $s$ be the size of an array (36 in your example), $v$ the number of possible values (here 13) of each element, $n$ the numbers of reference arrays (here 24), i.e., the size of the set $S=\{A_i \mid i\in[1..n]\}$ of arrays. I am assuming that the cost for preprocessing the arrays does not matter. Else, you can alsways simplify the procedure below, as ...


Only top voted, non community-wiki answers of a minimum length are eligible