In Bove and Dybjer’s Agda tutorial “Dependent Types at Work”, section 2.5 briefly introduces Gödel’s System T, which is based on the simply typed lambda calculus with booleans and natural numbers. They give Agda definitions of the primitives of System T, as well as the multiplication and addition operator, using those primitives. As an exercise to the reader, they ask for for further definitions like cut-off subtraction and a few Boolean operations.

Building abstractions by using this rather limited set of primitives turned out to be a pleasant diversion, so I went on and implemented further operations. But to start, here are the primitives of System T in Agda, as they were given by the authors. The six primitives of System T are true, false, zero, succ, if_then_else_, and natrec, i.e. recursion on natural numbers.

module SystemT where

data Bool : Set where
  true  : Bool
  false : Bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

if_then_else_ : {C : Set} → Bool → C → C → C
if true  then x else y = x
if false then x else y = y

natrec : {C : Set} → C → (ℕ → C → C) → ℕ → C
natrec p h  zero    = p
natrec p h (succ n) = h n (natrec p h n)

Further, Bove and Dybjer give definitions for addition and multiplication:

_+_ : ℕ → ℕ → ℕ
_+_ n m = natrec m (λ x y → succ y) n

_*_ : ℕ → ℕ → ℕ
_*_ n m = natrec zero (λ x y → y + m) n

The subtraction operation requires the predecessor function. Note that the predecessor of zero is zero. Further note that since we are restricting ourselves to natural numbers, subtraction is defined as so-called cut-off subtraction. This means that computations that yield negative numbers when performed on integers yield zero instead. Concretely, 1 – 2 = 0 instead of -1 because we restrict ourselves to nonnegative integers.

pred : ℕ → ℕ
pred n = natrec n (λ x y → x) n

_-_ : ℕ → ℕ → ℕ
_-_ n m = natrec n (λ x y → (pred y)) m

This might look a bit hairy, so it’s probably helpful to walk through this function. First, subtract one from zero:

zero - (succ zero)
= natrec zero (λ x y → pred y) (succ zero)
= (λ x y → pred y) zero (natrec zero (λ x y → pred y) zero)
= (λ x y → pred y) zero  zero
= pred zero
= zero

Second, two minus one:

(succ (succ zero)) - (succ zero)
= natrec (succ (succ zero)) (λ x y → pred y) (succ zero)
= (λ x y → pred y) zero (natrec (succ (succ zero)) (λ x y → pred y) zero)
= (λ x y → pred y) zero (succ (succ zero))
= pred (succ (succ zero))
= succ zero

To do a bit more in System T, Boolean operators would be nice to have. Using “if_then_else_” the operators for not, and, or, and xor are straightforward to define:

¬ : Bool → Bool
¬ b = if b then false else true

_∧_ : Bool → Bool → Bool
a ∧ b = if a then b else false

_∨_ : Bool → Bool → Bool
a ∨ b = if a then true else b

_⊕_ : Bool → Bool → Bool
a ⊕ b = if a then (¬ b) else b

An equality check for boolean values follows naturally:

equalityBool : Bool → Bool → Bool
equalityBool a b = if a then (a ∧ b) else (¬ (a ∧ b))

On the other hand, I found the definition of equality for natural numbers tricky. The function ‘zero?’ is therefore not defined using the perviously mentioned primitives of System T. I’ll have to look further into lambda calculus. As it is, ‘zero?’ is a small blemish of this implementation of System T.

zero? : ℕ → Bool
zero? zero = true
zero? _    = false

positive? : ℕ → Bool
positive? n = ¬ (zero? n)  -- there are no negative numbers

equalityNat : ℕ → ℕ → Bool
equalityNat a b = (zero? (a - b)) ∧ (zero? (b - a))

Lastly, here are comparison operators for natural numbers:

_>_ : ℕ → ℕ → Bool
a > b = positive? (a - b)

_<_ : ℕ → ℕ → Bool
a < b = positive? (b - a)

_≥_ : ℕ → ℕ → Bool
a ≥ b = (a > b) ∨ (equalityNat a b)

_≤_ : ℕ → ℕ → Bool
a ≤ b = (a < b) ∨ (equalityNat a b)

All of this looks pretty clean. I let Agda evaluate a few expressions, which all worked fine.