Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [equality]

The tag has no usage guidance.

0
votes
1answer
30 views

Elegant algorithm to semi-decide if two lambda calculus terms are equivalent

Given two lambda terms $t_1$ and $t_2$, it is semi-decidable if they are equivalent (i.e. can be rewritten as each other using alpha, beta, and eta conversions). An algorithm to do this is to try ...
0
votes
0answers
15 views

How do Clojure's persistent data structure determine equality?

I'm trying to understand the time complexity of determining equality between persistent data structures in Clojure (Vectors, Maps, Sets, etc.). These are based on data structures pioneered by Phil ...
1
vote
0answers
21 views

Summary of types of equivalence and equality in type theory, with notations and examples

Coming from non-computer science background, I am trying to understand the different types of equivalence and equality usually used in type theory. Ideally, I am looking for clear definitions and ...
2
votes
1answer
38 views

Uniqueness of byte arrays

Consider the situation, when you're given M byte arrays of size N, and you need to check if all of them have unique content (so ...
5
votes
1answer
188 views

Check if two items are equal after replacing

Let's say that an item is either a natural number or a list of items. Examples of items are: 1 [2] [4, [3, 1], 3, 4] A rule states that two items are equal. For example: 1 = 2 3 = [3, 1] [4, 3] = [...
1
vote
0answers
29 views

Checking Multiple Equal Graphs

first post on this amazing community, always been a lurker, so I'm sry if my formatting sucks. I'm having a really hard time trying to solve this problem: Given m graphs each composed of the same n ...
1
vote
1answer
30 views

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

I'm reading the following article that presents a $log(k)$ algorithm for your secretary problem. I'm in the analysis section at the left part of page 5 there is the following claim: $B^*$ is a ...
1
vote
1answer
220 views

Does a graph diameter equal to DFS tree depth?

given an unweighted graph, does the graph diameter equal to the maximum DFS tree depth? and the same about BFS? regarding both directed and undirected graphs. thanks :)
2
votes
2answers
109 views

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

I would like to have a canonical representation of a map from rational intervals (f, t] with f, t ∈ ℚ to some irrelevant value type. These intervals are non-overlapping and there exist only finitely ...
8
votes
0answers
115 views

Extensional constructs in minimal extensional type theory without eta equality

The extensional version of Intuitionistic Type Theory is usually formulated in a way that makes extensional concepts like functional extensionality derivable. In particular, equality reflection, ...
0
votes
0answers
71 views

Reasonable definition of beta-equivalence in big-step semantics

Assume, an extension of the lambda calculus with terms $t$ and values $v$ is defined in big-step operational semantics with evaluation relation $t \Downarrow v$. It is intuitive to assume that $\beta$...
8
votes
2answers
197 views

Decidability of Equality of Radical Expressions

Consider terms built from elements of $\mathbb Q$ and the operations $+,\times,-,/$, and $\sqrt[n]{\,\cdot\,}$ for each natural number $n$. Given the promise that two terms are well-formed -- that is, ...
8
votes
0answers
122 views

Is extensionality for coinductive datatypes consistent with Coq's logic?

Given a coinductive datatype, one can usually (always?) define a bisimulation as the smallest equivalence relation over it. I would like to add an axiom stating that if two members of the type are ...
3
votes
0answers
92 views

Solving systems of boolean equations

So I have a system of equations where varibles range over $\{0,1\}$ and the only operation is logical or ($\lor$). Each equation is of the one of two forms 1) $a = b \lor c$ 2) $1 = a \lor b$ where ...
1
vote
0answers
28 views

Similarity of Objects based on multiple variables

I am working on a Simple hypothetical Allocation Problem. I have some Virtual Machines(VM) placed on a Physical Machine (PM). The VMs and PMs have 3 common variables, CPU, Memory, Network. The VMs ...
8
votes
1answer
121 views

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

In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as ...
5
votes
1answer
259 views

Elimination rule for the equality type aka J axiom

I'm implementing a interpreter for lambda calculus, and now I want to add the equality type. The introduction rule for it is easy, but the elimination rule is rather obscure for me. I found this ...
0
votes
0answers
77 views

Vertex-independent paths [duplicate]

Let $s$ and $t$ be 2 vertices (not adjacent) in graph $G$. Let $p_l(s,t;G)$ be the $maximum$ number of vertex-independent paths from $s$ to $t$ in graph $G$, of length $\le$ $l$ ($l \in \{1,...,|G|\}$...
2
votes
2answers
295 views

Branchless function equivalent

Does every pure function have a branchless equivalent? By pure function I understand a function that uses only its input values and no global state to produce the output. By branchless function I ...
1
vote
1answer
152 views

Logical equivalence and equality

Let be $F=(A\land B)$ and $G=\neg(\neg A \lor \neg B)$. Which of the following statements are correct $F=G, F\equiv G, \neg F=\neg G, \neg F\equiv\neg G$? Is there a difference?
3
votes
1answer
176 views

Properties of Reverse Polish Notation expressions that are algebraically invariant

The RPN expressions a b + c * and f d e + * are algebraically equivalent, though the names of the variables are different ...
7
votes
2answers
130 views

Computability of equality to zero for a simple language

Suppose we have a tree in which leaves are labeled with a set of numbers $L$, and internal nodes with a set of operations $O$. In particular $L$ can be $\mathbb{N}, \mathbb{Z}$ or $\mathbb{Q}$, and ...
3
votes
2answers
606 views

match an array with a given set of arrays

We have a set of 24 distinct arrays, each array has 36 elements and each element can have one of 13 possible values. Then we're given an array X (this array is certainly part of our set) and we have ...
3
votes
5answers
228 views

Efficient set data structure supporting insert and set equal

What's the best way to represent sets that support the following two operations: Insert(s, i) - adds nonnegative integer i to set s Equal(s1, s2) - Tests if s1 and s2 are the same set. In addition, ...
4
votes
2answers
287 views

Unification — most specific unifier

In unification, given a set of equations, a standard problem is to compute a most general unifier (mgu). I am interested in a somewhat reversed problem. Imagine having a set of equations that do not ...
5
votes
1answer
113 views

Is the validity of some instance of an equational problem decidable?

Is the following FOL-problem (equality is a logical symbol) effectively decidable? Given. A finite equation system $E$ and an equation $s = t$. Question. Is there a substitution $\sigma$, such ...
2
votes
2answers
329 views

Equality testing of arrays and integers in a procedural language

In terms of references and their implementation on the heap and the stack, how is equality testing for arrays different from that for integers? This is to do with Java programming, if you have a ...