Hacker News Reader

Hacker News

Comment by mesarvagya | Hacker News Reader

Parent Full thread

mesarvagya

I was fascinated by Lambda calculus where you could think a number as the times of application of function. That is:

Symbol 0 = λs.λz.z

Symbol 1 = λs.λz.s(z)

Symbol 2 = λs.λz.s(s(z))

and so on.

Then we can find n+1 of a given number n as: Succ n = λn.λs.λz.s(ns(z))

To even think number as function, it's astonishing. Salute to Alonzo Church.

View on HN

Learning about Church and Scott encoding was much more interesting than I thought it would be. I was expecting it to be tedious and banal, but I came out of it feeling like I had some sort of revelation. Imagining naturals, lists, trees, etc. as function application was mind-bending at first, but it eventually clicks into place. Lambda calculus is so incredible in its combination of simple semantics, expressiveness, and abstraction/compositionality.

To go a step further, think about how you would implement a predecessor function on the Church encoding of the naturals. It is much more complicated than one might expect, and perfectly motivates the introduction of Scott encodings and the fixed-point function.

Scott encoding even has a weirder implications (if you're not used to it) if you think about it

    0 ≡ λf.λx.x
    1 ≡ λf.λx.x (λf.λx.x)
    2 ≡ λf.λx.x (λf.λx.x (λf.λx.x))

Or if you allow meta variables in your expression:

    0 ≡ λf.λx.x
    1 ≡ λf.λx.x 0
    2 ≡ λf.λx.x 1

This implies 2 contains 1, 1 contains 0. Bam. Scott encoding also encodes some parts of set theory.

Following from this, of course, all ADTs can be encoded following the Scott encoding scheme.

The Frege/Russell definition of numbers is pretty cool from that sort of perspective. The general style of their definitions is to temporarily sidestep the question of what X type of number is, and first ask to what sort of thing it applies to, and what is the relation of having the "same number" among such things. Then that sort of "number" is just defined as the equivalence classes of whatever the identified "same number" relation is.

There are two different definitions of the Naturals provided, that of finite Cardinal and Ordinal numbers. The first applies to sets, grouping them by "same cardinality" or same size. Thus, the cardinal number n is identified with the set of all sets with cardinality n. The second applies to well-ordered binary relations, and groups them by what we would call order-isomorphism. This might sound complicated, but the end result is that the ordinal number n becomes the set of all well-orders of length n (you can soft of think of this as the set of sequences of length n, at least for the finite case). Amusingly, both of these notions are too general to correspond to just the natural numbers, since they don't discriminate between finite and infinite numbers. Thus, the 'natural number' portion of each is actually defined as the smallest initial subset for which mathematical induction is valid.

Anyhow, the Principia Mathematica is pretty fun if you're into that sort of thing. It builds up a lot of neat and weird representation of all sorts of different numbers, up from the naturals, integers, ratios, and reals. It even provides its own weird definition of vectors, and gives a kind of analysis of "signed magnitudes" (like weight, height, temperature etc) and how their definition of real numbers as pure mathematical objects relate to them, providing a kind of abstract interpretation of what we mean when we measure something in the real world.

Iterestingly in the modern approach to set theory there still are both ordinal and cardinal numbers, but you can't say that the cardinal n is the set of all sets with cardinality n, because this is a proper class. Instead we choose a particular representative for this class, which also happens to be well ordered (this is in ZFC, you can still pick representatives for equipotence classes in ZF via Scott's trick but they are not necessarily well ordered or well orderable).

This is basically Peano numbers, hardly invented by Church. Not to discredit Church for lambda calc, of course.

The church encoding goes a lot further than that encoding conditionals and booleans and much more.

How does that system compare whether two numerical objects are the same?

3 = Succ 2

By evaluation? Evaluate Succ 2 such that the result is normal. then you may compare term equality

Do you have a text you recommend on this approach to natural arithmetic?

You mean lambda calculus? Or peano?

For the former, Barendregt. For the latter, Mandelson's Number System (first 5 or so chapters).

Reply on news.ycombinator.com