September 29, 2017 Friday
Bedtime Story
What Makes Lambda-Calculus so Formidable?
Kleene-Rosser Paradox showed that certain
systems of formal logic are inconsistent.
This specially referred to the system of
combinatory logic invented by Haskell Curry in 1930s which we will go through
in some future night.
In fact Kleene and Rosser found some
inconsistency even in the original lambda calculus of Church.
This forced Church to isolate a portion of
his original work and publish just a portion that is relevant to computation.
He did so in 1936 and this is now called untyped
lambda calculus.
You should know that if there is an untyped
something then there also got to be its counterpart types something.
So in this case, there is also something
known as typed lambda calculus.
Typed lambda calculus was the original
version and they are characterized by the fact that the function can be applied
only if the given input “type” is compatible with the functionality of the
lambda calculus.
We need go into the details of types,
untyped and simply typed lambda calculus as that is too technical for a bedtime
story and may even bring you to sleep much faster that I would want to.
The point that I wanted to raise was is
what makes lambda calculus so important for computing in spite of the fact that
at its heart, its premises or its syntax are almost childishly simple.
There can be made three arguments for it:
[a] For one, there is a kind of
universality to it.
It was later discovered (meaning it was not
intended so in the initial publication) that lambda calculus can encode any
computation.
Any program in any programming language
that has ever been invented or will be invented can be coded in lambda calculus
no matter how tedious or convoluted it may be.
Now as it is known to all computer
scientists and programmers that Turing machine too can program or encode any
computation that is possible by any machine.
I will take up the concept of Turing
machine and its origins in more detail later.
It is a fascinating story that has its
origins once again in the foundations of mathematics crisis of late nineteenth
century.
The universality of Turing machine is far
better known but what is less well known is that both lambda calculus and
Turing machine are exactly compatible.
What can be programmed in Turing machine
can be programmed into equivalent lambda calculus program and vice versa.
Hence these two systems are formally
equivalent.
We shall take up the other two arguments in
the nights to come.
I like to keep my bedtime stories short,
sweet and engaging so that I don’t get burnt out in writing it and my reader doesn’t
get fed up reading it.
Stay tuned to the voice of an average story storytelling
chimpanzee or login at http://panarrans.blogspot.com
Good night mon ami and my fellow cousin ape.
Advertisements
Another great educator and a teacher that I am aware of is
Professor Subhashish Chattopadhyay in Bangalore, India.
While I narrate stories, Professor Subhashish an electronic
engineer and a former professor at BARC, does and teaches real mathematics and
physics.
He started the participation of Indian students at the
International Physics Olympiad.
Do visit him here:
All his books can be downloaded for free through this link:
For edutainment and English education of your children, I
recommend this large collection of Halloween Songs for Kids:
No comments:
Post a Comment