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 ...
Jannis Limperg's user avatar
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
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
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 ...
Vincent's user avatar
  • 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 ...
Jake's user avatar
  • 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 ...
Labbekak's user avatar
  • 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 ...
A. Boy's user avatar
  • 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?
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
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
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
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
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....
Ralph Henry'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