Maths - Natural Number Types

Natural Number Type

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).

Notation

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 z₀ z_s O = z₀
rec nat z₀ z_s( S n) = z_s (n ,(rec nat z₀ z_s, n))

where

z₀ is the value returned for zero.
z_s is the value returned for succesor.

x:NP(x):Type		p₀:P(0)		x:N,p:P(x)p_s(x,p):P(sx)		n:N
rec_pⁿ(p₀.p_s):P(n)

computation rules

x:NP(x):Type		p₀:P(0)		x:N,p:P(x)p_s(x,p):P(sx)
rec_p⁰(p₀.p_s):P(0)

x:NP(x):Type		p₀:P(0)		x:N,p:P(x)p_s(x,p):P(sx)		n:N
rec_p^sn(p₀.p_s):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
advantages	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.

defined inductively

predicates in higher order logic

define them axiomatically

advantages

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

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 z₀ z_s O = z₀
rec nat z₀ z_s( S n) = z_s (n ,(rec nat z₀ z_s, n))

where

z₀ is the value returned for zero.
z_s is the value returned for succesor.

x:NP(x):Type		p₀:P(0)		x:N,p:P(x)p_s(x,p):P(sx)		n:N
rec_pⁿ(p₀.p_s):P(n)

computation rules

x:NP(x):Type		p₀:P(0)		x:N,p:P(x)p_s(x,p):P(sx)
rec_p⁰(p₀.p_s):P(0)

x:NP(x):Type		p₀:P(0)		x:N,p:P(x)p_s(x,p):P(sx)		n:N
rec_p^sn(p₀.p_s):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:

Maths - Natural Number Types

Natural Number Type

Notation

Rules

Idris Code

Computer Implementation

Idris

Coq

Enumeration Type

Inductive Types

Natural Number Type

W-Types

Next Steps

EuclideanSpace

Overview