How do we define operations on naturals?

[kory33]

We first need to define addition and multiplication in order to define further number systems, like ℤ or ℚ.

The addition operation +: ℕ×ℕ -> ℕ is defined inductively in a following way:

n + 0 = n
n + S(m) = S(n + m)

Where S is a successor class function.

In a very similar way, we can define multiplication *: ℕ×ℕ -> ℕ as

n * 0 = 0
n * S(m) = n * m + n

Now what I want to do are:

• lift (+) operation to a Function from ℕ×ℕ to ℕ. Name this as PlusOpsFunction
• prove PlusOpsFunction is commutative, hence showing ℕ is a monoid under PlusOpsFunction

It is enough if we can prove that n + m =::= (m =::= S(k) forSome k ? S(n + k) : n), and I think this is a precise requirement. Is Scala able to express the conditional type as shown above? If so, can we use it to define +?

[kory33]

This seems pretty much achievable using the recursion theorem, which ensures the following:

For a set A, element a∈A and f: A => A, there exists a function r: ℕ => A such that r(0) = a r(S(n)) = f(r(n)) is satisfied.

This theorem allows construction of recursively defined function, for which the operations on naturals are good examples.

I will soon be working on this implementation.