Skip to main content

Questions tagged [equality]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer
68 views

Checking equality of self-referential lists

Define that an srlist ("self-referential list") over $X$ consists of a list of elements of $X \sqcup \mathrm{srlist}(X).$ So basically, the items can be primitive values, or further self-...
SocraticMathTutor's user avatar
3 votes
2 answers
150 views

Does this esoteric representation of integers have decidable equality?

Consider the following datatypes in Haskell: data Foo = Halt | Iter Foo newtype BigInt = BigInt {nthBit :: Foo -> Bool} Foo ...
Dannyu NDos's user avatar
0 votes
0 answers
127 views

How to find the intersection of two FAs and then check if two FAs are equal?

I am still quite confused on how to properly handle in answering the intersection and equality of two FAs in terms of table form and manipulating its transformation....
Ralph Henry's user avatar
1 vote
1 answer
84 views

Logical Consequence - Equivalent Assertions

I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
A. Boy's user avatar
  • 11
2 votes
3 answers
481 views

Complexity of string comparison vs whitespace-trimmed string comparison

I recently worked on an algorithm which, among other things, checks strings for equality using the classic builtin equality operator: str1 == str2 (I think it ...
Enlico's user avatar
  • 73
0 votes
1 answer
79 views

Is the equality of Bloom filters analogous to set equivalence?

I have two multisets $A$, $B$ where $A \subseteq B$. Using these two sets, we construct two Bloom filters $BF(A), BF(B)$; both using bitsets of size $n$ with the same $k$ hash functions. What's the ...
zetaprime's user avatar
  • 123
0 votes
2 answers
88 views

Equivalence relation between two CFG's

In our course: Automata and Computation there is a definition about Context-Free Grammars which states: "Two CFG's $CFG_{1}$ and $CFG_{2}$ are equivalent if $L_{CFG_{1}} = L_{CFG_{2}}$ where $L_{...
Matthias K.'s user avatar
0 votes
1 answer
198 views

Algorithm best compare similarities between two data sets in percentage

I'm trying to create an algorithm that finds the percentage of similarity between two subjects with sets of survey questions. Example: Q1: Do you prefer physically demanding tasks? A1: Nope Maybe Yes -...
syahiruddin's user avatar
1 vote
0 answers
40 views

n-bit ALU usually do comparison operation on maximum n/2-bit or n-bit?

For n-bit ALU is equal-to operation and similar comparisons generally limited to n/2-bit words, or n-bit?
Fiesta's user avatar
  • 11
1 vote
1 answer
52 views

Calculate transfers to equalize balances?

I'm playing a MMORPG where we party hunt, the problem is that at the end of the hunt each person may have different balances depending on what items they wasted and the stuff each one looted. The game ...
OiciTrap's user avatar
  • 171
3 votes
1 answer
78 views

Equality of lambda terms which do not have normal form

In the context of lambda calculus, how should one prove $\beta$-equality of terms that do not have normal form? In particular, how to prove that these are different combinators: $$ Y = λf.(λx.f(xx))(...
prog's user avatar
  • 105
0 votes
1 answer
941 views

Proving equivalence of two Turing machines

I have the following Turing machine: A 2R-3L-TM is similar to a standard TM with the change in which the head can only move either 3 cells to the left or 2 cells to the right (those are the only ...
Rika's user avatar
  • 3
0 votes
1 answer
34 views

Show that the inequality holds for all positive integers

$a_1=2,a_2=9,a_n=2a_{n-1}+3a_{n-2}$ for $n>=3$ Show $a_n<3^n$ for all positive integers n Base case: $a_3 = 2*9+3*2 = 24<=3^3$ is true Hypothesis: $a_k<=3^k$ for $k\epsilon\mathbb{N}$, ...
Rijad Hadzic's user avatar
2 votes
0 answers
162 views

Is Observational Equality better than intensional equality?

The Observational Equality from Epigram 2 seems to be intensional equality (like Coq and Agda have), but it also supports function extensionality. In that sense it seems that Observational Equality is ...
Labbekak's user avatar
  • 565
4 votes
1 answer
149 views

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

Let's have expressions that are composed of elements of $\mathbb N$ and a limited set of binary operations {$+,\times,-,/$} and functions {$\exp, \ln$}. The expressions are always well-formed and form ...
GolDDranks's user avatar
1 vote
0 answers
49 views

Decidability of equality of expressions involving exponentiation

Let's have expressions that are finite-sized trees, with elements of $\mathbb N$ as leaf nodes and the operations {$+,\times,-,/$, ^} with their usual semantics as the internal nodes, with the special ...
GolDDranks's user avatar
4 votes
1 answer
122 views

Is unification over regular expression equations doable?

By way of example, suppose I know that $X + a = b + Y$ where $X$ and $Y$ are variables standing for regular expressions, then $(X, Y) = (b, a)$ is a solution to this set of equations. Generalizing ...
Jonas Kölker's user avatar
1 vote
1 answer
487 views

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

$\Sigma^* - \{\epsilon\} = \Sigma^+$ $L^* - \{\epsilon\} = L^+$ Which of the above is always true? I was following a discussion on a site and I came across this question. Some fellow ...
Turing101's user avatar
  • 1,200
1 vote
1 answer
55 views

Equivalence of different automata

I have a question about the equivalence of different automata. I looked up the similiar questions but sadly none of them are exactly, what I need or am looking for. I know some of these are ...
Seran's user avatar
  • 13
3 votes
1 answer
144 views

Difference between computation in proposition proof and definitional computation?

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
al pal's user avatar
  • 621
4 votes
2 answers
180 views

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

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that: Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
al pal's user avatar
  • 621
4 votes
1 answer
241 views

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

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that: A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional ...
al pal's user avatar
  • 621
5 votes
1 answer
411 views

Definitional equality of two propositions about propositional equality

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that: It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is ...
al pal's user avatar
  • 621
5 votes
2 answers
270 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 ...
Christopher King's user avatar
3 votes
0 answers
110 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 ...
Vincent's user avatar
  • 221
2 votes
1 answer
291 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 ...
Vitaly Isaev's user avatar
4 votes
1 answer
329 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] = [...
Paul's user avatar
  • 149
1 vote
0 answers
39 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 ...
Bjerg466's user avatar
1 vote
1 answer
52 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 ...
Belgi's user avatar
  • 267
1 vote
1 answer
778 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 :)
Edan Ben Ivri's user avatar
3 votes
2 answers
812 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 ...
Janno's user avatar
  • 31
7 votes
0 answers
148 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, ...
fsestini's user avatar
0 votes
0 answers
127 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$...
choeger's user avatar
  • 610
8 votes
2 answers
325 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, ...
Mees de Vries's user avatar
12 votes
0 answers
282 views

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

Given a coinductive datatype, one can usually (always?) define a bisimulation as the largest equivalence relation over it. I would like to add an axiom stating that if two members of the type are ...
Jannis Limperg's user avatar
3 votes
0 answers
162 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 ...
Jake's user avatar
  • 3,800
1 vote
0 answers
41 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 ...
Saad Farooq's user avatar
8 votes
1 answer
235 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 ...
Filip Haglund's user avatar
8 votes
1 answer
876 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 ...
盛安安's user avatar
  • 944
0 votes
0 answers
264 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|\}$...
CorneliusCroitorus's user avatar
2 votes
2 answers
2k 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 ...
Daniel Lovasko's user avatar
3 votes
1 answer
1k 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?
MathCracky's user avatar
3 votes
1 answer
347 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 ...
Nathaniel M. Beaver's user avatar
7 votes
2 answers
208 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 ...
miniBill's user avatar
  • 419
3 votes
2 answers
1k 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 ...
egwspiti's user avatar
  • 133
3 votes
5 answers
299 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, ...
foobarbazquxx's user avatar
4 votes
2 answers
347 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 ...
zpavlinovic's user avatar
  • 1,654
5 votes
1 answer
121 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 ...
Steffen Schuler's user avatar
2 votes
2 answers
372 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 ...
Xabi's user avatar
  • 75