Powered by AppSignal & Oban Pro
Would you like to see your link here? Contact us

Exercises

2.1_exercises.livemd

Exercises

Exercise 2.6

> In case representing pairs as procedures wasn’t mind-boggling enough, consider that, in a language that can manipulate procedures, we can get by without numbers (at least insofar as nonnegative integers are concerned) by implementing 0 and the operation of adding 1 as > > > (define zero (lambda (f) (lambda (x) x))) > > (define (add-1 n) > (lambda (f) (lambda (x) (f ((n f) x))))) > > > This representation is known as Church numeral’s, after its inventor, Alonzo Church, the logician who invented the λ-calculus. > > Define one and two directly (not in terms of zero and add-1). (Hint: Use substitution to evaluate (add-1 zero)). Give a direct definition of the addition procedure + (not in terms of repeated application of add-1).

defmodule ChurchNumerals do
  def zero do
    fn _f ->
      fn x -> x end
    end
  end

  def add_1(n) do
    fn f ->
      fn x ->
        f.(n.(f).(x))
      end
    end
  end
end

zero = ChurchNumerals.zero()
one = ChurchNumerals.add_1(zero)
two = ChurchNumerals.add_1(one)
# one   = fn f -> fn x -> f.(x) end end
# two   = fn f -> fn x -> f.(one.(f).(x)) end end
# three = fn f -> fn x -> f.(two.(f).(x)) end end
# three = fn f -> fn x -> f.((fn f -> fn x -> f.(f.(x)) end end).(f).(x)) end end
# four  = fn f -> fn x -> f.(three.(f).(x)) end end

church_to_int = fn n ->
  n.(fn x -> x + 1 end).(0)
end

IO.puts(church_to_int.(zero))
IO.puts(church_to_int.(one))
IO.puts(church_to_int.(two))