On 10/13/05, Dave Whipp <[EMAIL PROTECTED]> wrote:
> (ref: http://svn.openfoundry.org/pugs/docs/notes/theory.pod)
>  >    theory Ring{::R} {
>  >        multi infix:<+>   (R, R --> R) {...}
>  >        multi prefix:<->  (R --> R)    {...}
>  >        multi infix:<->   (R $x, R $y --> R) { $x + (-$y) }
>  >        multi infix:<*>   (R, R --> R) {...}
>  >        # only technically required to handle 0 and 1
>  >        multi coerce:<as> (Int --> R)  {...}
>  >    }
>  >
>  > This says that in order for a type R to be a ring, it must
>  > supply these operations.  The operations are necessary but
>  > not sufficient to be a ring; you also have to obey some
>  > algebraic laws (which are, in general, unverifiable
>  > programmatically), for instance, associativity over
>  > addition: C<(a + b) + c == a + (b + c)>.
> I started thinking about the "in general, unverifiable programmatically"
> bit. While obviously true, perhaps we can get closer than just leaving
> them as comments. It should be possible to associate a
> unit-test-generator with the theory, so I can say:

I've been thinking about this. If we have a type inferencer, we know
that any function we define to be N,N->N will be that way. The only
items we have to show is for all a in N, there is a unique succesor
which is also in N and that for all b in N, b != 1, there is a unique
predecessor. If we have that, then we get the laws of arithmetic. Is
it possible to put that into the type inferencer if the types are
defined as iterators? Kind of like Church numbers, but in P6 notation.
I think that by defining our types as iterators, we can satisfy the
succ/pred requirements of Peano's, meaning we have the arithmetic


Reply via email to