Maths - Natural Number Types

Natural Number Type

ref

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)

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-2021 Martin John Baker - All rights reserved - privacy policy.