Life in Death

The truth of life is in death,
is this why our dreams are never met.
We go on with our lives everyday,
while the moment of truth is far away.

Life comes in its many shades,
while the blow of death is always gray.
Hopes are born with beginning of life,
death crushes them with no respite.

But is this really even life ?
filled with pain, sorrow, grief and spite.
When death is the only salvation,
why are we condemned to life's damnation.

Can you really repent your sins,
when you are bound by karma.
Will death be your salvation,
when in life you had no dharma.

Do you live to seek and find,
or to just go on with life's grind.
The seek ends at sundown with death,
when life cannot make further progress.

Death tests our regression into abyss,
filled with guilt and regret of life.
Do we really rise on the other side,
or death takes us for a long ride.

To live one must fight,
there is solace in last rite.
Does our fight go on beyond,
or does it end with the last yawn.

All our lives we move in different boxes,
the move always ends in the same casket.
Is death really the end of a move ?
or, on the other side, our journey begins anew.

When you see my cold dead eyes,
will you still care for the warmth of life ?
When the spirit leaves the humble abode,
does it travel a lonely road ?

We live all our lives divided by life,
while in death we all ultimately unite.
Is death then the only true god ?
when religions are filled with fright and fraud.

And what say we to this humble god,
not today, we are not ready to go abroad.
How long can we keep saying no ?
Does it even matter to all those in the know ?

The cycle of life and death goes on and on,
we come, we go, we shuffle around.
Life in death and death in life,
is there any difference, or, are they alike?

List Example for Extracting OCaml from Coq

In this post I will show how to extract a simple list append function written in Coq as OCaml code.

First let us create an inductive type in Coq to define our lists as follows.

Inductive mylist : Type :=

| nil : mylist 

| cons : nat -> mylist -> mylist.

Next, we will define an append function over these lists using the "Function" keyword.

Function myappend (l1:mylist) (l2:mylist) {struct l1} : mylist :=

match l1 with

| nil => l2

| cons x xs => cons x (myappend xs l2)

end.

The append function has a special "struct" which tells Coq that the first argument l1 is the recursive parameter to the function. This is essential as without that Coq will not let you define a function. In this particular case the recursive call is always made on a smaller list thus termination can be proven as an instance of structural recursion. However if we write a function where we want to use more general recursion we have to define a "measure" and prove that it decreases with every recursive call. Once the myappend function is defined in Coq it is easy to state and prove properties about append. The following theorem shows that myappend function is associative. 

Theorem myappend_assoc : forall l1 l2 l3 : mylist , myappend (myappend l1 l2) l3 =

(myappend l1 (myappend l2 l3)).

Proof.

intros.

induction l1.

simpl.

trivial.

simpl.

rewrite IHl1.

trivial.

Qed.

Once we have stated the desired properties and proven their correctness we can also generate OCaml (or Haskell) code from Coq using extraction process. The extraction process will recursively remove the proof terms from the code and convert the program to a corresponding OCaml program. Extraction for the myappend function can be using the following statements in Coq.

Extraction Language Ocaml.

Extraction "mylist.ml" myappend.

The generated code in mylist.ml file looks as below.

type nat =

| O

| S of nat

type mylist =

| Nil

| Cons of nat * mylist

(** val myappend : mylist -> mylist -> mylist **)

let rec myappend l1 l2 =

match l1 with

| Nil -> l2

| Cons (x, xs) -> Cons (x, (myappend xs l2))

The OCaml code extracted from Coq includes all the corresponding data types - nat and mylist used in the program. Also the function myappend is extracted without the proof of termination. Other proof constructs like theorems are also dropped from the extracted code. The extracted code can now be used inside a larger OCaml program.

Using Ocsigen for Web Development with OCaml on Nitrous.IO

As I said in my last post, once you have configured OPAM on nitrous.io, it is quite easy to install additional OCaml libraries and framework. Ocsigen is a web development framework for OCaml. In this post we will see how to configure Ocsigen on nitrous.io to build a simple website with OCaml. To install Ocsigen, just use OPAM

opam install ocsigenserver

After installing Ocsigen we need to install Eliom to enable dynamic websites with Ocsigen. Again run the following command to install it from OPAM.

opam install eliom

If the installations were successful you will now have  a working Ocsigen setup on your machine. In order to test it out let's just create a simple website from the hello world example. Make a new folder in your box inside that copy the following example eliom source file.

 (* ************************************************************************** *)  
 (* Project: Ocsigen Quick Howto : Page                    *)  
 (* Description: Example of a simple page (The famous "Hello World"!)     *)  
 (* Author: db0 (db0company@gmail.com, http://db0.fr/)             *)  
 (* Latest Version is on GitHub: http://goo.gl/sfvvq              *)  
 (* ************************************************************************** *)  
 open Eliom_content  
 open Html5.D  
 open Eliom_parameter  
 (* ************************************************************************** *)  
 (* Application                                *)  
 (* ************************************************************************** *)  
 module Example =  
  Eliom_registration.App  
   (struct  
    let application_name = "example"  
    end)  
 (* ************************************************************************** *)  
 (* Service declaration                            *)  
 (* ************************************************************************** *)  
 let main =  
  Eliom_service.service  
   ~path:[]  
   ~get_params:unit  
   ()  
 (* ************************************************************************** *)  
 (* Service definition                             *)  
 (* ************************************************************************** *)  
 let _ =  
  Example.register  
   ~service:main  
   (fun () () ->  
    Lwt.return  
      (html  
        (head (title (pcdata "Hello World of Ocsigen")) [])  
        (body [h1 [pcdata "Hello World!"];  
            p [pcdata "Welcome to my first Ocsigen website."]])))  

In my box I saved this file as the example/example.eliom. Then I created example/static folder to host the static resources of the website. In order to build this file you can use the magic makefile provided by Ocsigen. Change the static dir to "./static" and  in server files put "example.eliom" , in addition I had to remove the "-noinfer" option from the file as the compiler was giving an error with it. Once you make these changes you can compile your eliom web application example.eliom by typing "make" on the console. It will create a directory structure as follows in the same directory.

The compiled web application is "example.cma". Now we need to launch the Ocsigen server with this web application. For that we take help of the following conf file. 

 <!-- ----------------------------------------------------------------------- -->  
 <!-- Project: Ocsigen Quick Howto                      -->  
 <!-- Description: Configuration file to launch the examples         -->  
 <!-- Author: db0 (db0company@gmail.com, http://db0.fr/)           -->  
 <!-- Latest Version is on GitHub: https://github.com/db0company/Gallery/   -->  
 <!-- ----------------------------------------------------------------------- -->  
 <ocsigen>  
  <server>  
   <port>3000</port>  
   <logdir>./tmp/</logdir>  
   <datadir>./tmp/</datadir>  
   <user></user>  
   <group></group>  
   <commandpipe>./tmp/ocsigen_command</commandpipe>  
   <mimefile>/home/action/.opam/4.01.0/etc/ocsigenserver/mime.types</mimefile>  
   <extension findlib-package="ocsigenserver.ext.ocsipersist-sqlite">  
    <database file="./tmp/ocsidb"/>  
   </extension>  
   <extension findlib-package="ocsigenserver.ext.staticmod"/>  
   <extension findlib-package="eliom.server"/>  
   <charset>utf-8</charset>  
   <debugmode/>  
   <host hostfilter="*">  
    <static dir="./static/" />  
    <eliom module="./example.cma">  
    </eliom>  
   </host>  
  </server>  
 </ocsigen>  

Save the above file as "example.conf" in the same directory and launch the server with the following command.

ocsigenserver -c example.conf 

 This is configure the server to run on the 3000 port as specified in "example.conf" and run the example application. You can test that the application is running using the Preview feature on nitrous.io.

Just use the 3000 port and then the web server should serve the following page in a new window.

This enables nitrous.io to be used as a web development environment for OCaml.  You can now use the Web IDE to develop web applications for OCaml in the same way as you can do for the default boxes supported by nitrous.io. 

Configuring OPAM for OCaml on Nitrous.IO

In the previous post I showed how to get a working OCaml compiler installed on a nitrous.io box.  We had to get the source code of OCaml from github and build it. It turns out there is a much easier way to get the compiler and all the necessary libraries. We can install the OPAM package manager inside our box and then use OPAM to download additional libraries. In order to configure OPAM on nitrous.io we follow the steps on the quick install page  for the binary installer of OPAM. Run the following commands in the terminal.

wget http://www.ocamlpro.com/pub/opam_installer.sh 

sh ./opam_installer.sh /home/action/.local/bin

The installer will guide you through the process of setting up and installing the OCaml compiler. Once the installation finishes you can use the OCaml system from console. You can also use OPAM to install additional libraries. Details on the usage of OPAM as a package manager are given here. By default it OPAM will install the libraries shown in the screenshot below.

OCaml on Nitrous.IO

Nitrous.IO provides free servers with console access to developers. The servers can be provisioned across different geographies and allows for a good way to code on the web. Each nitrous box comes with a web based IDE and console access. They provide boxes for web development in Ruby/Rails, Go, Python/Django and node.js. However since they allow console access it is possible to install many other systems on your nitrous box. It can be used as a good way to do we based tutorials or small projects inside the box as well. The web based IDE also has experimental support for collaboration so it can be a good tool to work on some project together with others. In this post I will show how to install OCaml on Nitrous so that you can code and test simple OCaml programs. It can be ideal for class assignments or small projects since the OCaml compiler is not the easiest thing to install on Windows and Mac platforms (based on my experience of teaching a class of undergrads). 

To begin, register on nitrous.io and create a new box, you can choose any of the default box but I chose python. Give it some name (dev-box) and chose the region closest to you (Southeast Asia).

Once you create a box you should be logged into the web based IDE on the box with console at bottom as shown below.

We will use the console to download and install the OCaml compiler. You can use the source code from the OCaml github repository. Just clone the source code using the https url to the repository. ("git clone https://github.com/ocaml/ocaml.git") 

It will create an ocaml directory with all the source code in your workspace. Change to that directory and then run "./configure -prefix /home/action/.local" This will tell the compiler to install in your local user directory under .local folder. 

Once the configuration finishes successfully, we can use "make world.opt" to build the compiler and "make install" to install it. (Look up INSTALL file in the ocaml directory for more detailed notes on installation. It is pretty standard way of  building the compiler on a linux machine.)  If you followed the steps without errors you will now have a working OCaml compiler on your nitrous box. You can run the OCaml toplevel by running "ocaml" from your workspace. Additional OCaml libraries like findlib can also be installed by using wget command to get the source code from their website and building them. 

You can use the web based IDE provided with your nitrous box to edit OCaml programs and run them using the console.

As you can see above I am using C for syntax highlighting as the web IDE doesn't support OCaml yet. The setup is not perfect but it allows anyone to try OCaml on the web without much fuss and hey its free !!! I actually managed to run all the lab assignments and tutorials for the module I am TAing this semester at NUS.

Air Pollution in New Delhi

After the furor created by the recent haze situation in Singapore, I wondered about the air quality back home in India. So I decided to check up the air pollution levels in New Delhi which is known to be one of the most polluted cities in India. What I found surprised me, the PSI level on average in New Delhi is 200+. The Delhi Pollution Control Committee provides real time data on air quality in different parts of Delhi on its website. A quick glance on the PM 10 concentration in Delhi suggests that the PSI level routinely goes above 400 (a level considered extremely hazardous by Singapore). I was really surprised that there is no one talking about it in India. The air quality in Delhi is one of the worst in the world. A recent article on Slate also found that air pollution in Delhi is far worse than Beijing (a city considered worst by many in terms of air pollution).

Residents in Delhi continuously breath air which is considered extremely dangerous by accepted standards in other parts of the world. Even though I have lived in Delhi for some time now and was aware of the pollution problem, I wasn't aware that it is possibly the worst in the world. News about air quality is rarely reported in the Indian media. As such many Indians are blissfully unaware about the gravity of the situation in Delhi. There is some evidence that the gains made by the CNG public transportation program in Delhi are already eroded. The high particulate content in Delhi is mostly due to road dust and industrial exhaust rather than vehicular pollution. This means than government intervention and systemic policy making can improve the air quality by shutting down industrial facilities near Delhi.

However it may be too much to expect the Delhi (State and Central) government to do anything concrete about this problem in the near future. In this respect India may be even worse than China where the local governing bodies have acknowledged the problem at least. The environmental bodies in Delhi are doing a good job providing real time air quality data but lack of awareness among the public, limited coverage by the local media and inaction by the appropriate agencies has left the residents high and dry. Can people themselves do something to make the air better ? May be the new Aam Admi Party can take up air pollution as an important issue for the next elections ? I am sure residents of Delhi could do with a bit of fresh air.

Time Travel - Wormholes

The theory of general relativity predicts that if traversable wormholes exist, they could allow time travel. This would be accomplished by accelerating one end of the wormhole to a high velocity relative to the other, and then sometime later bringing it back; relativistic time dilation would result in the accelerated wormhole mouth aging less than the stationary one as seen by an external observer, similar to what is seen in the twin paradox. However, time connects differently through the wormhole than outside it, so that synchronized clocks at each mouth will remain synchronized to someone traveling through the wormhole itself, no matter how the mouths move around. This means that anything which entered the accelerated wormhole mouth would exit the stationary one at a point in time prior to its entry.

For example, consider two clocks at both mouths both showing the date as 2000. After being taken on a trip at relativistic velocities, the accelerated mouth is brought back to the same region as the stationary mouth with the accelerated mouth's clock reading 2004 while the stationary mouth's clock read 2012. A traveler who entered the accelerated mouth at this moment would exit the stationary mouth when its clock also read 2004, in the same region but now eight years in the past. Such a configuration of wormholes would allow for a particle's world line to form a closed loop in spacetime, known as a closed timelike curve.

It is thought that it may not be possible to convert a wormhole into a time machine in this manner; the predictions are made in the context of general relativity, but general relativity does not include quantum effects. Analyses using the semiclassical approach to incorporating quantum effects into general relativity have sometimes indicated that a feedback loop of virtual particles would circulate through the wormhole with ever-increasing intensity, destroying it before any information could be passed through it, in keeping with the chronology protection conjecture. This has been called into question by the suggestion that radiation would disperse after traveling through the wormhole, therefore preventing infinite accumulation. The debate on this matter is described by Kip S. Thorne in the book Black Holes and Time Warps, and a more technical discussion can be found in The quantum physics of chronology protection by Matt Visser. There is also the Roman ring, which is a configuration of more than one wormhole. This ring seems to allow a closed time loop with stable wormholes when analyzed using semiclassical gravity, although without a full theory of quantum gravity it is uncertain whether the semiclassical approach is reliable in this case.

A possible resolution to the paradoxes resulting from wormhole-enabled time travel rests on the many-worlds interpretation of quantum mechanics. In 1991 David Deutsch showed that quantum theory is fully consistent (in the sense that the so-called density matrix can be made free of discontinuities) in spacetimes with closed timelike curves. However, later it was shown that such model of closed timelike curve can have internal inconsistencies as it will lead to strange phenomena like distinguishing non orthogonal quantum states and distinguishing proper and improper mixture. Accordingly, the destructive positive feedback loop of virtual particles circulating through a wormhole time machine, a result indicated by semi-classical calculations, is averted. A particle returning from the future does not return to its universe of origination but to a parallel universe. This suggests that a wormhole time machine with an exceedingly short time jump is a theoretical bridge between contemporaneous parallel universes. Because a wormhole time-machine introduces a type of nonlinearity into quantum theory, this sort of communication between parallel universes is consistent with Joseph Polchinski’s discovery of an “Everett phone” in Steven Weinberg’s formulation of nonlinear quantum mechanics.

Geet Nahi Gata Hun - Atal Bihari Vajpayee

गीत नहीं गाता हूँ, गीत नहीं गाता हूँ

बेनकाब चेहरे हैं दाग बड़े गहरे हैं

टूटता तिलिस्म आज सच से भय खाता हूँ 

गीत नहीं गाता हूँ, गीत नहीं गाता हूँ 

लगी कुछ ऐसी नज़र, बिखरा शीशे का शहर,

अपनों के मेले में, मीत नहीं पता हूँ ,

पीठ में छूरी सा चाँद, राहु गया रेखा फान्द,

मुक्ति के शानो में, बंध जाता हूँ, 

गीत नहीं गाता हूँ, गीत नहीं गाता हूँ (II)

गीत नया गाता हूँ, गीत नया गाता हूँ

टूटे हुए तारों से फूटे वासंती स्वर

पत्थर की छाती में उग आया नव अंकुर

झरे सब पीले पात, कोयल की कुहुक रात

प्राची में, अरुणिमा की रेत देख पाता हूँ

गीत नया गाता हूँ, गीत नया गाता हूँ

टूटे हुए सपने की सुने कौन, सिसकी 

अंतर को चीर व्यथा, पलकों पर ठिठकी

हार नहीं मानूंगा, रार नहीं ठानूंगा 

काल के कपाल पर, लिखता-मिटाता हूँ

गीत नया गाता हूँ, गीत नया गाता हूँ

Sometimes I wrestle with my demons Sometimes we just snuggle

Sometimes I wrestle with my demons

Sometimes we just snuggle

Sometimes I fight them

Sometimes we just play

Sometimes they hide in my closet

Sometimes I keep them away 

Sometimes they pull me under the bed

Sometimes we just push each other

Sometimes they make me suffer

Sometimes we just laugh together

Sometimes they get on to me

Sometimes we just stay away from each other

Sometimes they haunt me in my dreams

Sometimes I wish I could see them in the day

Sometimes they make me do things

Sometimes I want them to go away

Sometimes I see them in my eyes

Sometimes they disappear from my life

Sometimes they lurk in the shadows

Sometimes they brighten the day

Sometimes they help me overcome my fears

Sometimes they make me afraid

Sometimes they sin

Sometimes we pray

Main Tumhe Doondhne - Hindi Poem By Kumar Vishwas

मैं तुम्हे ढूंढने स्वर्ग के द्वार तक, 

रोज़ आता रहा रोज़ जाता रहा। 

तुम ग़ज़ल बन गई, गीत में ढल गई,

मंच से मैं तुम्हे गुनगुनाता रहा। 

ज़िन्दगी के सभी रस्ते एक थे, 

गहरा ठहरा हुआ जल बनी ज़िन्दगी,

तुम बिना जैसे महलों में बीता हुआ, 

उर्मिला का कोई पल बनी ज़िन्दगी, 

दृष्टि आकाश में आस का एक दिया, 

तुम बुझाती रही मई जलाता रहा। 

मैं तुम्हे ढूंढने स्वर्ग के द्वार तक, 

रोज़ आता रहा रोज़ जाता रहा।

Vikram Singh Rawat Poem

Read the full book of his poems - https://bookdown.org/content/0a3463d1-8940-4f82-b50a-7d6579c78297/

ज़िन्दगी में कुछ भी कभी हरपल नहीं रहता

जो आज साथ होता है तुम्हारे वो कल नहीं रहता

मैं फ़िज़ूल रोया करता था लम्हों पे दशको पे

समझ आया अब की वक़्त खुद भी सदा प्रबल नहीं रहता

मरते हैं इसके भी पल जो बहते हैं इसकी धाराओ में

सदा को ठहरा हुआ कोई भी इसका पल नहीं रहता

सिर्फ तू भंवर में है ये सोचना सरासर भूल है

ये झरना है, इस अहद में अब ये कल-कल नहीं बहता

इस दूध की धारा को मैंने पूजा भी दिए भी सिराये

पर जब से सागर में मिला फिर वो गंगाजल नहीं रहता

कितना लालची हूँ की जिसके सजदे किये नवाज़ा भी

वो जब से खारा हुआ ठोकरों के भी काबिल नहीं रहता

तू हाथों की लकीरों पे चला तो नदी जैसा भटकता रहा

तूने खुद को कभी नहीं खोजा तभी तू सफल नहीं रहता

और तू मुझे मसीहा मत समझ मैं खुद विफल हूँ हालातों से

हाँ मगर होंसला अब नहीं हरा वर्ना ये ग़ज़ल नहीं कहता

Einstein Quote

Politics it the art of possible, Science is the art of soluble - Albert Einstein

Dushyant Kumar's New Poem

आज सड़कों पर लिखे हैं सैंकड़ों नारे न देख

घर अँधेरा देख तू आकाश के तारे न देख 

एक दरिया है यहाँ पर दूर तक फैला हुआ

आज अपने बाजुओं को देख पतवारें न देख 

अब यक़ीनन ठोस है धरती हक़ीक़त की तरह

यह हक़ीक़त देख, लेकिन ख़ौफ़ के मारे न देख 

वे सहारे भी नहीं अब जंग लड़नी है तुझे

कट चुके जो हाथ ,उन हाथों में तलवारें न देख 

दिल को बहला ले इजाज़त है मगर इतना न उड़

रोज़ सपने देख, लेकिन इस क़दर प्यारे न देख 

ये धुँधलका है नज़र का,तू महज़ मायूस है

रोज़नों को देख,दीवारों में दीवारें न देख 

राख, कितनी राख है चारों तरफ़ बिखरी हुई

राख में चिंगारियाँ ही देख, अँगारे न देख.

40 Rules for a Better Life

1. Drink plenty of water. 

2. Eat breakfast like a king, lunch like a prince and dinner like a beggar. 

3. Eat more foods that grow on trees and plants, and eat less food that is manufactured in plants. 

4. Live with the 3 E’s — Energy, Enthusiasm, and Empathy. 

5. Make time for prayer and reflection 

6. Play more games. 

7. Read more books than you did in 2012. 

8. Sit in silence for at least 10 minutes each day. 

9. Sleep for at least 7 hours. 

Personality: 

10. Take a 10-30 minutes walk every day —- and while you walk, smile. 

11. Don’t compare your life to others’. You have no idea what their journey is all about. 

12. Don’t have negative thoughts or things you cannot control. Instead invest your energy in the positive present moment. 

13. Don’t over do; keep your limits. 

14. Don’t take yourself so seriously; no one else does. 

15. Don’t waste your precious energy on gossip. 

16. Dream more while you are awake. 

17. Envy is a waste of time. You already have all you need. 

18. Forget issues of the past. Don’t remind your partner with his/her mistakes of the past. That will ruin your present happiness. 

19. Life is too short to waste time hating anyone. Don’t hate others. 

20. Make peace with your past so it won’t spoil the present. 

21. No one is in charge of your happiness except you. 

22. Realize that life is a school and you are here to learn. Problems are simply part of the curriculum that appear and fade away like algebra class but the lessons you learn will last a lifetime. 

23. Smile and laugh more. 

24. You don’t have to win every argument. Agree to disagree. 

Community: 

25. Call your family often. 

26. Each day give something good to others. 

27. Forgive everyone for everything. 

28. Spend time with people over the age of 70 & under the age of 6. 

29. Try to make at least three people smile each day. 

30. What other people think of you is none of your business. 

31. Your job won’t take care of you when you are sick. Your family and friends will. Stay in touch. 

Life:

32. Do the right things. 

33. Get rid of anything that isn’t useful, beautiful or joyful. 

34. Forgiveness heals everything. 

35. However good or bad a situation is, it will change. 

36. No matter how you feel, get up, dress up and show up. 

37. The best is yet to come. 

38. When you awake alive in the morning, don’t take it for granted – embrace life. 

39. Your inner most is always happy. So, be happy and ENJOY LIFE! 

Last but not least: 

40. Grow your relationship with God