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

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

 
right adjointN : Type

term introduction rules

 

    Γright adjointn:N
Γright adjoint0:N   Γright adjoints(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:Nright adjointP(x):Type   right adjointp0:P(0)   x:N,p:P(x)right adjointps(x,p):P(sx)   right adjointn:N
right adjointrecpn(p0.ps):P(n)
computation rules
x:Nright adjointP(x):Type   right adjointp0:P(0)   x:N,p:P(x)right adjointps(x,p):P(sx)
right adjointrecp0(p0.ps):P(0)
x:Nright adjointP(x):Type   right adjointp0:P(0)   x:N,p:P(x)right adjointps(x,p):P(sx)   right adjointn:N
right adjointrecpsn(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:

  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

 

Natural Number Type

formation rule

N exists

 
right adjointN : Type

term introduction rules

 

    Γright adjointn:N
Γright adjoint0:N   Γright adjoints(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:Nright adjointP(x):Type   right adjointp0:P(0)   x:N,p:P(x)right adjointps(x,p):P(sx)   right adjointn:N
right adjointrecpn(p0.ps):P(n)
computation rules
x:Nright adjointP(x):Type   right adjointp0:P(0)   x:N,p:P(x)right adjointps(x,p):P(sx)
right adjointrecp0(p0.ps):P(0)
x:Nright adjointP(x):Type   right adjointp0:P(0)   x:N,p:P(x)right adjointps(x,p):P(sx)   right adjointn:N
right adjointrecpsn(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:

 


metadata block
see also:

http://www.mathreference.com/

Correspondence about this page

Book Shop - Further reading.

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.

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

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.