Lecture 7.5: Data in the Lambda Calculus

Data in the Lambda Calculus

So far we have worked with a lambda calculus that only has integers as constants, but no operations on these constants. In fact, we only need one constant in order to use the lambda calculus for all kinds of computation. The constant is only needed to provide an easy way to observe the result of computation.

Natural numbers (or "non-negative integers") can be represented using what is called the church encoding. The idea is to represent any number N as functions that take two arguments, and then return the result of applying the first argument N times to the second argument. The following functions provide a convenient way to encode numbers using this strategy:

let rec build n =
  if n = 0 then Vr(0) else
    Ap(Vr(1), build(n-1))

let writer n =
  Lm(Lm(build n))

To decode numbers, it is tempting to write a function that takes apart a lambda term. This strategy, however, would be two fragile, because it would require the result to have a very specific syntactic form. A better strategy is implemented by the following function:

let rec reader_step env e =
  let v = ev6 ((V_Cn 0)::env) e in
    match v with
        V_Lm(env', e') -> 1 + (reader_step env' e')
      | _ -> 0

let reader e =
  let v = ev6 [] (Ap(Ap(e,Lm(Lm(Vr 1))),(Cn 0))) in
    match v with
        V_Lm(env', e') -> 1 + reader_step env' e'
      | _ -> 0