2022 Developer Survey is open! Take survey.
11 votes
Accepted

Why is `map insertionsort` not to equal to`map mergesort`?

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 = ...
user avatar
  • 3,419
8 votes
Accepted

Elimination rule for the equality type aka J axiom

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 ...
user avatar
7 votes
Accepted

Logical equivalence and equality

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 ...
user avatar
5 votes
Accepted

On $L^* - \{\epsilon\} = L^+$

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 ...
user avatar
5 votes

Why values can not be replaced with their extensionally equal values in an intensional system?

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 ...
user avatar
  • 28.1k
5 votes
Accepted

Definitional equality of two propositions about propositional equality

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 ...
user avatar
5 votes

Equivalence relation between two CFG's

$G_1$ and $G_2$ are equivalent if and only if $L_{G_1} = L_{G_2}$. Since the relation $=$ is an equivalence relation over languages, so is the equivalence between grammars.
user avatar
  • 7,154
4 votes
Accepted

Computability of equality to zero for a simple language

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 =...
user avatar
  • 140k
4 votes

Computability of equality to zero for a simple language

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, ...
user avatar
  • 7,744
4 votes
Accepted

Unification --- most specific unifier

I found out that such a thing is called anti-unification. This problem was addressed by Plotkin and Reynolds. Here is a brief overview.
user avatar
  • 1,604
4 votes
Accepted

Why values can not be replaced with their extensionally equal values in an intensional system?

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. ...
user avatar
3 votes
Accepted

Definition of extensional and propositional equality in Martin-Lof extensional type theory

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 \...
user avatar
  • 29.1k
3 votes

Decidability of Equality of Radical Expressions

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 ...
user avatar
3 votes
Accepted

Decidability of equality, and soundness of expressions involving elementary arithmetic and exponentials

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 ...
user avatar
  • 140k
3 votes

Unification --- most specific unifier

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 ...
user avatar
  • 7,744
2 votes
Accepted

Branchless function equivalent

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 (...
user avatar
  • 18.8k
2 votes

Uniqueness of byte arrays

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 ...
user avatar
  • 24.9k
2 votes

Difference between computation in proposition proof and definitional computation?

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. ...
user avatar
  • 28.1k
2 votes
Accepted

Complexity of string comparison vs whitespace-trimmed string comparison

From the viewpoint of complexity theory, comparing two strings, with or without surrounding whitespace, takes time linear in the lengths of the strings, because there is no computational model, ...
user avatar
  • 11k
1 vote

Algorithm best compare similarities between two data sets in percentage

You'll need two algorithms (definitions, actually) here: one to define a distance between answers with in questions one to define a distance between complete questionnaires It makes working with 2 ...
user avatar
  • 121
1 vote

Is unification over regular expression equations doable?

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 ...
user avatar
  • 29.1k
1 vote
Accepted

A $log(k)$ algorithm for the matroid secretary problem

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^...
user avatar
1 vote
Accepted

Does a graph diameter equal to DFS tree depth?

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, ...
user avatar
1 vote

Canonical representation of finite maps on non-overlapping finite rational intervals

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 ...
user avatar
  • 140k
1 vote

Canonical representation of finite maps on non-overlapping finite rational intervals

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 ...
user avatar
  • 140k
1 vote
Accepted

Properties of Reverse Polish Notation expressions that are algebraically invariant

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 ...
user avatar
  • 2,059
1 vote
Accepted

match an array with a given set of arrays

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 \...
user avatar
  • 19.1k
1 vote

match an array with a given set of arrays

You could calculate something like crc32 of the arrays and compare them with the crc32 of the new array. If the crc32's of the arrays match then you can do further check if the elements actually match ...
user avatar
  • 141

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