<div dir="auto">A simpler example of groups with no computable equality: the Sum group on computable reals. x + negate x === 0 for all x, but we can never fully prove it, only demonstrate it for each number of digits. And yet this is a perfectly well behaved abelian group.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Dec 12, 2020, 23:41 Viktor Dukhovni <<a href="mailto:ietf-dane@dukhovni.org">ietf-dane@dukhovni.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Sun, Dec 13, 2020 at 12:19:18AM -0500, Carter Schonwald wrote:<br>
<br>
> Having a decidable equality seems important for reasoning about groups.  Or<br>
> computing on representations thereof.<br>
<br>
This is of course not always possible.  If a group is presented as a<br>
quotient of a free group on a set of generators via some set of<br>
relators, then deciding whether two words are equal is IIRC known to be<br>
generally intractable.  One can still perform the group operation, but<br>
there is no known terminating algorithm for constructing a canonical<br>
form for an element, performing equality tests, ...<br>
<br>
Of course one might take the view that groups where equality is not<br>
computable are not "useful", but that might rule out some applications.<br>
<br>
-- <br>
    Viktor.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>