Num instances for 2-dimensional types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
44 messages Options
123
Reply | Threaded
Open this post in threaded view
|

Re: Re: Num instances for 2-dimensional types

Jason McCarty-2
Daniel Fischer wrote:
> Am Mittwoch 07 Oktober 2009 23:51:54 schrieb Joe Fredette:
> > I generally find semirings defined as a ring
> > structure without additive inverse and with 0-annihilation (which one
> > has to assume in the case of SRs, I included it in my previous
> > definition because I wasn't sure if I could prove it via the axioms, I
> > think it's possible, but I don't recall the proof).
>
> 0*x = (0+0)*x = 0*x + 0*x ==> 0*x = 0

This proof only works if your additive monoid is cancellative, which
need not be true in a semiring. The natural numbers extended with
infinity is one example (if you don't take 0*x = 0 as an axiom, I think
there are two possibilities for 0*∞).

--
Jason McCarty <[hidden email]>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Num instances for 2-dimensional types

Felipe Lessa
On Wed, Oct 07, 2009 at 08:44:27PM -0400, Jason McCarty wrote:

> Daniel Fischer wrote:
> > Am Mittwoch 07 Oktober 2009 23:51:54 schrieb Joe Fredette:
> > > I generally find semirings defined as a ring
> > > structure without additive inverse and with 0-annihilation (which one
> > > has to assume in the case of SRs, I included it in my previous
> > > definition because I wasn't sure if I could prove it via the axioms, I
> > > think it's possible, but I don't recall the proof).
> >
> > 0*x = (0+0)*x = 0*x + 0*x ==> 0*x = 0
>
> This proof only works if your additive monoid is cancellative, which
> need not be true in a semiring. The natural numbers extended with
> infinity is one example (if you don't take 0*x = 0 as an axiom, I think
> there are two possibilities for 0*∞).

Given that

x = 1*x = (0+1)*x = 0*x + 1*x = 0*x + x

we can show that

x = x + 0*x  (right)
x = 0*x + x  (left)

so, by definition of 'zero', we have that 0*x is a zero.  But we
can easily prove that there can be only one zero: suppose we have
two zeros z1 and z2; it follows that

z1 = z1 + z2 = z2

So 0*x = 0.  Any flaws?

--
Felipe.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Num instances for 2-dimensional types

Daniel Fischer-4
Am Donnerstag 08 Oktober 2009 03:05:13 schrieb Felipe Lessa:

> On Wed, Oct 07, 2009 at 08:44:27PM -0400, Jason McCarty wrote:
> > Daniel Fischer wrote:
> > > Am Mittwoch 07 Oktober 2009 23:51:54 schrieb Joe Fredette:
> > > > I generally find semirings defined as a ring
> > > > structure without additive inverse and with 0-annihilation (which one
> > > > has to assume in the case of SRs, I included it in my previous
> > > > definition because I wasn't sure if I could prove it via the axioms,
> > > > I think it's possible, but I don't recall the proof).
> > >
> > > 0*x = (0+0)*x = 0*x + 0*x ==> 0*x = 0
> >
> > This proof only works if your additive monoid is cancellative, which
> > need not be true in a semiring. The natural numbers extended with
> > infinity is one example (if you don't take 0*x = 0 as an axiom, I think
> > there are two possibilities for 0*∞).

It was a proof for a ring (with or without unit), which Joe stated above he didn't recall.
There your additive monoid is cancellative since it's a group :D

>
> Given that
>
> x = 1*x = (0+1)*x = 0*x + 1*x = 0*x + x
>
> we can show that
>
> x = x + 0*x  (right)
> x = 0*x + x  (left)
>
> so, by definition of 'zero', we have that 0*x is a zero.

Not necessarily, we don't know 0*x + y = y for arbitrary y yet.
If the additive monoid isn't cancellative, that needn't be the case.
In Jason's example, you can indeed set 0*∞ = ∞.

> But we can easily prove that there can be only one zero: suppose we have
> two zeros z1 and z2; it follows that
>
> z1 = z1 + z2 = z2
>
> So 0*x = 0.  Any flaws?
>
> --
> Felipe.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Num instances for 2-dimensional types

Ben Franksen
In reply to this post by jfredett
Joe Fredette wrote:
> A ring is an abelian group in addition, with the added operation (*)
> being distributive over addition, and 0 annihilating under
> multiplication. (*) is also associative. Rings don't necessarily need
> _multiplicative_ id, only _additive_ id.

Yes, this is how I learned it in my Algebra course(*). Though I can imagine
that this is not universally agreed upon; indeed most of the more
interesting results need a multiplicative unit, IIRC, so there's a
justification for authors to include it in the basic definition (so they
don't have to say let-R-be-a-ring-with-multiplicative-unit all the time ;-)

Cheers
Ben

(*) As an aside, this was given by one Gernot Stroth, back then still at the
FU Berlin, of whom I later learned that he took part in the grand effort to
classify the simple finite groups. The course was extremely tight but it
was fun and I never again learned so much in one semester.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
123