Most tutorials on Lambda Calculus provide example where Positive Integers and Booleans can be represented by Functions. What about -1 and i?


2 Answers 2


First encode natural numbers and pairs, as described by jmad.

Represent an integer $k$ as a pair of natural numbers $(a,b)$ such that $k = a - b$. Then you can define the usual operations on integers as (using Haskell notation for $\lambda$-calculus):

neg = \k -> (snd k, fst k)
add = \k m -> (fst k + fst m, snd k + snd m)
sub = \k m -> add k (neg m)
mul = \k m -> (fst k * fst m + snd k * snd m, fst k * snd m + snd k * fst m)

The case of complex numbers is similar in the sense that a complex number is encoded as a pair of reals. But a more complicated question is how to encode reals. Here you have to do more work:

  1. Encode a rational number $q$ as a pair $(k,a)$ where $k$ is an integer, $a$ is natural, and $q = k / (1 + a)$.
  2. Encode a real number $x$ by a function $f$ such that for every natural $k \in \mathbb{N}$, $f k$ encodes a rational number $q$ such that $|x - q| < 2^{-k}$. In other words, a real is encoded as a sequence of rationals converging to it at the rate $k \mapsto 2^{-k}$.

Encoding reals is a lot of work and you do not want to actually do it in the $\lambda$-calculus. But see for example the etc/haskell subdirectory of Marshall for a simple implementation of reals in pure Haskell. This could in principle be translated to the pure $\lambda$-calculus.

  • 1
    $\begingroup$ Wow =) I'm wondering intuitively what that means... for example, using the church numbers encoding... ie. a church number of integer value n is represented by a function that applies a function to a value n times. Do pairs and negative lambda values have that similar intuitive feel about them? $\endgroup$
    – zcaudate
    Jun 8, 2012 at 18:47
  • 1
    $\begingroup$ Church encoding encodes natural numbers $0$, $1$, $2$, ... It does not encode negative numbers. In the answer above I assumed you already know about an encoding of natural numbers, so I explained how to get integers. The integers as I encoded them are a more formal construction, unlike the Church numerals, which are more intricately connected with the $\lambda$-calculus. I don't think "negative lambda values" is a meaningful phrase. $\endgroup$ Jun 8, 2012 at 21:56
  • $\begingroup$ @zcaudate [Type annotations: i:ℤ,x:a,f,u,s:a→a,p:(a→a,a→a)] If you encode ℤ as (Sign,ℕ) then, given a pair of functions (s,f) as p, the term λi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x) will produce either f(…f(x)…) or s(f(…f(x)…)) (if the result is negative). If you encode ℤ as (ℕ,ℕ), you need a function that has an inverse – given a pair (f,u) and x, the function λi.λp.λx.(snd i)(snd p)((fst i)(fst p) x) will produce u(…u(f(…f(x)…))…) which will leave f applied i times to x. Both work in different contexts (result can be "flipped" || f is invertible). $\endgroup$
    – nobody
    Sep 12, 2014 at 0:08
  • $\begingroup$ @zcaudate The extra functions are necessary as Church-encoded numbers "recurse on their own", but pairs will only hand you their components. The helper functions just glue the components together in the "right" order (which is happening automatically for nats.) See also: en.wikipedia.org/wiki/… – Church encoding is basically fold . ctor for any constructor and that type's fold(r). (Which is why, for recursive types, the data will "recurse on its own". For non-recursive types it's more like a case / pattern match.) $\endgroup$
    – nobody
    Sep 12, 2014 at 0:22

Lambda-calculus can encode most data structures and basic types. For example, you can encode a pair of existing terms in the lambda calculus, using the same Church encoding that you usually see to encode nonnegative integers and boolean:

$$\mbox{pair}= λxyz.zxy$$ $$\mbox{fst} = λp.p(λxy.x)$$ $$\mbox{snd} = λp.p(λxy.y)$$

Then the pair $(a,b)$ is $p=(\mbox{pair }ab)$ and if you want to get back $a$ and $b$ you can do $(\mbox{fst }p)$ and $(\mbox{snd }p)$.

That means that you can easily represent positive and negative integers with a pair: the sign on the left and the absolute value on the right. The sign is be a boolean that specified whether the number is positive. The right is a natural number using Church encoding.


And now that you have relative integers. The multiplication is easy to define, you just have to apply the $\mbox{xor}$ function on the sign and the multiplication on natural numbers on the absolute value:

$$\mbox{mult}_ℤ=λab.\mbox{pair} ~~(\mbox{xor}(\mbox{fst }a)(\mbox{fst }b)) ~~(\mbox{mult}_ℕ(\mbox{snd }a)(\mbox{snd }b))$$

To define the addition, you have to compare two natural numbers and use subtraction when the signs are different, so this is not a λ-term but you can adapt it if you really want to:

$$\mbox{add}_ℤ=λab.\left\{\begin{array}{ll} (\mbox{true},\mbox{add}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a≥0∧b≥0 \\ (\mbox{false},\mbox{add}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a<0∧b<0 \\ (\mbox{true},\mbox{sub}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a≥0∧b<0∧|a|≥|b| \\ (\mbox{false},\mbox{sub}_ℕ(\mbox{snd }b)(\mbox{snd }a)) & \mbox{if } a≥0∧b<0∧|a|<|b| \\ (\mbox{true},\mbox{sub}_ℕ(\mbox{snd }b)(\mbox{snd }a)) & \mbox{if } a<0∧b≥0∧|a|<|b| \\ (\mbox{false},\mbox{sub}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a<0∧b≥0∧|a|≥|b| \\ \end{array}\right.$$

but then subtraction is really easy to define:

$$\mbox{minus}_ℤ=λa.\mbox{pair}(\mbox{not}(\mbox{fst } a))(\mbox{snd } a)$$ $$\mbox{sub}_ℤ=λab.\mbox{add}_ℤ(a)(\mbox{minus}_ℤb)$$

Once you have positive and negative integers you can define complex integers very easily: it is just a pair of two integers $(a,b)$ which represents $a+b\mbox{i}$. Then addition is point-wise and multiplication is as usual, but I won't write it, it should be easy:

$$\mbox{add}_{ℤ[\mbox{i}]}=λz_1z_2.\mbox{pair} (\mbox{add}_ℤ(\mbox{fst }z_1)(\mbox{fst }z_2)) (\mbox{add}_ℤ(\mbox{snd }z_1)(\mbox{snd }z_2))$$

  • 7
    $\begingroup$ You can avoid the case distinctions if instead you represent the integer $k$ as a pair of natural numbers $(a,b)$ such that $k = a - b$. $\endgroup$ Jun 8, 2012 at 10:34
  • $\begingroup$ Complex integers alright, but he was asking for complex numbers. Then again, they of course can never be represented since there are uncountable. $\endgroup$
    – HdM
    Jun 8, 2012 at 11:19
  • $\begingroup$ @AndrejBauer: very nice trick (maybe not that simpler) HdM: sure they can, even in not all of them. But I figured that the method for building stuff in the λ-calculus with Church encoding was more important/appropriate here. $\endgroup$
    – jmad
    Jun 8, 2012 at 11:30
  • $\begingroup$ I wish I could give two correct answers =) I wasn't even thinking that reals could be represented when I asked about complex numbers but there you go!. $\endgroup$
    – zcaudate
    Jun 8, 2012 at 18:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.