Isomorphism/More Syntax

Main page: Isomorphism

foldn(c, h, n) function

We defined the number likes these:

one = succ zero
two = succ (succ zero)
three = succ (succ (succ zero))
......

In mathematics, we uses n` but not succ n to express the successor of n.

So, we can say two plus three like this:

  two + three
= zero`` + zero```
= zero``` + zero``
= zero```` + zero`
= zero````` + zero
= zero`````
= five

The result is ((((zero's successor)'s successor)'s successor)'s successor)'s successor, five.

But, how did we express 1747156280461389750146873209578461807205641950? Did we express it with zero```````````````````````````````...(1747156280461389750146873209578461807205641950 `'s)? It's too much trouble! So, a new thing is appears!

Tada!

def func foldn(z, f(, n))
{
    foldn(z, f, 0) = z
    foldn(z, f, n`) = f(foldn(z, f, n))
}

If z is zero, f is succ, n is any natural number, then foldn defines the WHOLE natural number.

foldn(zero, succ, 0) = zero
foldn(zero, succ, 1) = one
foldn(zero, succ, n) = a_natural_number

If z isn't zero, f isn't succ, then foldn describes something isomorphic to natural numbers.

(+m) => foldn(m, succ)
(*m) => foldn(0, (+m))
m^() => foldn(1, (*m))

List type

List can also define with isomorphic to natural numbers.

According to Peano's axiom 1, an empty list (nil) is equivalent to zero; According to Peano's axiom 2, for all lists, we can use cons, to link a new element of type A on the left. Thus cons is equivalent to succ in natural numbers.

Isomorphic to the addition of natural numbers, we can define the linking operation of a list as follows:

nil ‡ a = a
cons(a, x) ‡ y = cons(a, x ‡ y)

But, 1 ‡ (2 ‡ (3 ‡ nil)) is too complex, so we can simplify it with [1, 2, 3]. And, ['H', 'e', 'l', 'l', 'o', ',', ' ', 'w', 'o', 'r', 'l', 'd', '!'] can simplify with "Hello, world!".

However, unlike natural numbers, lists do not satisfy the commutative law. (That's why I'm using a double dagger sign here instead of a plus sign for the list connection. But many programming languages use the plus sign, which creates a potential problem.(That's why I like Haskell. too.))