Skip to main content

# Questions tagged [equality]

The tag has no usage guidance.

14 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 ...
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, ...
• 71
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 ...
3 votes
0 answers
111 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 ...
• 221
3 votes
0 answers
164 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 ...
• 3,800
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 ...
• 565
1 vote
1 answer
85 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 ...
• 11
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?
• 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 ...
• 171
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 ...
• 161
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 ...
• 11
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 ...
• 111
0 votes
0 answers
129 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....
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$...
• 610