Natural numbers
From The Twelf Project
The natural numbers are the numbers 0, 1, 2, etc. The term is generally used to indicate a specific technique of representing natural numbers as either zero or the successor of some other natural number - 0, s(0), s(s(0)), etc - as in Peano arithmetic, a technique also sometimes referred to as unary numbers.
Contents |
[edit] Natural numbers in Twelf
Natural numbers in Twelf are usually defined in a similar way. Mathematically, natural numbers can be defined as zero or the successor of some other natural number:
This representation translates easily into Twelf:
nat: type. z: nat. s: nat -> nat.
The first line declares that nat is a type. The second line declares z (zero) to be an object of type nat, and the third line declars s (successor) to be a type constructor that takes an object N of type nat and produces another object (s N) of type nat.
[edit] Addition of natural numbers in Twelf
The addition of these natural numbers is defined by the judgment 
, where N1, N2, and N3 are natural numbers. In the definition below, capital letters stand for metavariables that can range over all natural numbers.
These judgments also translate cleanly into Twelf:
plus: nat -> nat -> nat -> type. p-z: plus z N N. p-s: plus (s N1) N2 (s N3) <- plus N1 N2 N3.
The first line defines the judgment, declaring plus to be a type family indexed by three terms of type nat.
The second line declares that for any natural number N, p-z is an object of type plus z N N, which corresponds to the axiom p-z above. The N is an implicit parameter - it is treated as a bound variable by Twelf, which you can see by looking at Twelf's output after checking the above code.
The third line says that p-s is a type constructor that, given an object D of type plus N1 N2 N3 (where N1, N2, and N3 are all implicit parameters that can
be treated as metavariables), produces an object, p-s D, with type plus (s N1) N2 (s N3). This corresponds to the rule p-s, which given a derivation of allows us to conclude 
.
Consider this derivation which encodes the fact that 2 + 1 = 3:
This can be represented in Twelf by applying the type constructor p-s to the object p-z twice:
2+1=3 : plus (s (s z)) (s z) (s (s (s z))) = p-s (p-s p-z).Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)2+1=3 : plus (s (s z)) (s z) (s (s (s z))) = p-s (p-s p-z).
%% OK %%
[edit] See also
- Natural numbers with inequality
- Division over the natural numbers
- Proving metatheorems with Twelf, which uses natural numbers as an example, and also discusses the adequacy of the encoding.
