1

It’s easy to surpass a predecessor

 2 years ago
source link: https://janmaru.medium.com/its-easy-to-surpass-a-predecessor-2b3f64d1c390
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

Responses

There are currently no responses for this story.

Be the first to respond.

You have 2 free member-only stories left this month.

“Men first felt necessity, then look for utility, next attend to comfort, still later amuse themselves with pleasure, thence grow dissolute in luxury, and finally go mad and waste their substance. (G.V.)”

Giambattista Vico’s birth home in Naples.

Giambattista Vico probably was the first to suggests that people had a fundamentally different schema of thought in different historical eras. Hence, he started imagining a different course of history, a History that depends on the way the ordinary mind functions and changes over time.

Having present all this, we could say that it’s easy to surpass a predecessor, all that you need is to survive him.

In the “Arithmetices principia, nova methodo expositaPeano published a simplified version of a previous axiomatization of the natural number arithmetic. The idea was very simple: define a first element and a single-valued “successorOf” function S under witch all natural numbers are assumed to be “closed”.

  • The first axiom states that the 0 is a natural number.
  • For every natural number n, S(n) is a natural number.
  • For all natural numbers m and n, m = n if and only if S(m) = S(n).
  • For every natural number n, S(n) = 0 is false.

So, let’s see if we can with F# enforce these axioms and think of a simple arithmetic.

Natural numbers

F# uses a sum type called a “discriminated union” type. Each component type (called a union case) must be tagged with a label so that they can be told apart (“discriminated”).

For istance:

type IntOrBool = 
| I of int
| B of bool

According to Peano we can define a type Natural in this way:

type Natural = Zero | SuccessorOf of Natural

Also we can introduce a recursive function Compare, in order to define a simple relation. A relation r over a collection of sets

D1, D2, . . . , Dn

is a subset of the Cartesian Product.

D1 × D2 × . . . × Dn

A relation thus is a set of n-tuples (d1, d2, . . . , dn). In particular, an order relation is a relation, or a criterion of comparison between objects, which satisfies the properties of reflexivity, antisymmetry and transitivity.

Also, we can easily introduce a simple concept of “sum”, in the natural sense, where the sum of a natural with zero is the number, while the sum of two arbitrary numbers is the sum of the predecessor of the first and the successor of the second. We know, of course, that this binary operation is closed in the set N.

Let’s say we want to sum 1+1, we have:

let value = (+) One Oneprintfn "%A" valueSuccessorOf (SuccessorOf Zero)

Can we imagine to represent an infinite set of values, like all the natural numbers?

The great thing about Sequence in F# is that the elements in a sequence or sequence expression are computed when required. We can, even, define infinite sequences by using the Seq.initInfinite function. For istance the alternating series of reciprocals of squares of successive integers.

Hence:

and if we print N we have:

seq
[SuccessorOf Zero; SuccessorOf (SuccessorOf Zero);
SuccessorOf (SuccessorOf (SuccessorOf Zero));
SuccessorOf (SuccessorOf (SuccessorOf (SuccessorOf Zero))); ...]

I can see the narrow line between this implementation and the specific construction due to John von Neumann, in the area of mathematics called Set Theory.

So how we deal with the fact that we re-write history and every discover anticipates its past finds and make roots for the next anticipation?

Jorge Luis Borges, once stated a nice paradox:

Every writer creates his own precursors.

and we have to live with that.


About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK