# Maths - Natural Number Types

### Natural Number Type

ncatlab ref

Natural numbers can be defined in terms of Peano algebra. This is not very practical for everyday use but has nice properties for proving things about natural numbers.

Elimination is usually a way to prove properties of inductivly defined types like this.

 For example, for natural numbers: Idris2 ```nat_induction : (prop : Nat -> Type) -> -- Property to show (prop Z) -> -- Base case ((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step (x : Nat) -> -- Show for all x prop x nat_induction prop p_Z p_S Z = p_Z nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)```

That is, for all properties on natural numbers, if it holds for zero and P n implies P (S n) then the property holds for all numbers. (proof by induction).

### Rules

Types are defined by their formation, term introduction, term eliminator and computation rules.

In order to avoid having a infinite number of constructors we can define Nat in terms of functions Z and S.

Nat Type

formation rule

N exists N : Type

term introduction rules

 Γ n:N Γ 0:N Γ s(n)

term eliminator

Proof by induction

To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx)

rec is recursor (see recursor section above) where:

rec nat z0 zs O = z0
rec nat z0 zs( S n) = zs (n ,(rec nat z0 zs, n))

where

• z0 is the value returned for zero.
• zs is the value returned for succesor.
 x:N P(x):Type p0:P(0) x:N,p:P(x) ps(x,p):P(sx) n:N recpn(p0.ps):P(n)
computation rules
 x:N P(x):Type p0:P(0) x:N,p:P(x) ps(x,p):P(sx) recp0(p0.ps):P(0)
 x:N P(x):Type p0:P(0) x:N,p:P(x) ps(x,p):P(sx) n:N recpsn(p0.ps):P(sn)

#### Idris Code

Idris Code for Nat is here.

 The formation and term introduction rules can be represented in Idris like this: `data Nat = Z | S Nat` The term eliminator can be implemented by the 'case' construct. computation and local completeness rules `ie `

## Computer Implementation

How do we implement natural numbers in computer algebra and proof assistant programs? Some alternatives are:

• Define inductively from Zero and Successor as in Coq (Calculus of Inductive Constructions) .
• Define them as predicates in higher order logic.
• Define them axiomatically.
defined inductively predicates in higher order logic define them axiomatically

Can automatically generate induction proof principle.

Can define functions by well-founded recursion.

Keeps program simple

Don't need to show each recursive definition represents a terminating algorithm, unique for each input.

disadvantages   each function requires a proof.

### Idris

 github Elimination (pattern matching) is built in to Idris. ```data Nat = ||| Zero Z | ||| Successor S Nat Eq Nat where Z == Z = True (S l) == (S r) = l == r _ == _ = False ```

### Coq

 github ``` Inductive nat : Set := | 0 : nat | S : nat -> nat.```

### Enumeration Type

ref

An enumerated type is any type given by a finite disjoint sum of unit types.

Can be thought of as a sum (1+1...) or as a degenerate form of an inductive type.

## Inductive Types

### Natural Number Type

Natural Number Type

formation rule

N exists N : Type

term introduction rules

 Γ n:N Γ 0:N Γ s(n)

term eliminator

Proof by induction

To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx)

rec is recursor (see recursor section above) where:

rec nat z0 zs O = z0
rec nat z0 zs( S n) = zs (n ,(rec nat z0 zs, n))

where

• z0 is the value returned for zero.
• zs is the value returned for succesor.
 x:N P(x):Type p0:P(0) x:N,p:P(x) ps(x,p):P(sx) n:N recpn(p0.ps):P(n)
computation rules
 x:N P(x):Type p0:P(0) x:N,p:P(x) ps(x,p):P(sx) recp0(p0.ps):P(0)
 x:N P(x):Type p0:P(0) x:N,p:P(x) ps(x,p):P(sx) n:N recpsn(p0.ps):P(sn)

### W-Types

This is ageneralisation of the way natural numbers can be inductivly defined, see page here.

### Next Steps

Other types are discussed on the following pages:

http://www.mathreference.com/

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.      Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.