8/2/2010

Doing research is really needed you to be disinterested. Proving things step by step
and showing your imaginations are true needed great patient. Oh my, I am still too
impacted and naive to be a genuine researcher.

Interpretation

It should be noticed that interpretation of types is very different from
the interpretation of terms. The connection between the two is the soundness
theorem: the interpretation of term is in the interpretation of types.

New thoughts on 7/15

I just realize that the applicative structure is just not expressive enough to
describe the axioms. I need a more expressive signature.

Learning note 7/15

1. Term algebra provides us an algebraic formalization on the term signature, so that
we can use tool from algebra to study term. So in a sense, Herbrand is a smart guy.

2. The only identities or equational classes in term algebra are those syntatical identities.

3. It is(is it?) possible to have a sigma-algebras which has it's own equational classes that can not be formalized by the identities in sigma-signature.

4. A spec=<\sigma,E> is only a form of algebraic specification, we can replace E by
a bunch of axioms.

Research

Maybe I am still used to letting another person remind me, hey! you have to finish the $#$%^ by the end of #@!@##$. But that's not the case when you are a phD student. Some may like this kind of being pushed feeling, but I don't. In my opinion, there's two kind of research, one is giving by others like your advisor, the other is your own research, which you are pretty much on your own. Sometimes, your advisor is just too busy to give you more instructions. For me, I am kind of feeling frustrated when I find out the fact that I am alone in this research. Yes, my advisor can give me advice, but I realize that he is any possibly closed to the answer than me. He may point out a problem or field that he think it's worthwhile to do, but he will pretty much let you explore this area by yourself. So don't expect too much from your advisor, he also has his own research to do, just like you except maybe ten times busier than you. But what if I am too frustrated by the research I've done so far and don't even have a clue where it will lead me to? Well, hang on there, you will figure it out eventually, always remember, nobody force you to do anything, you are on your own, you struggling in these years of PhD, but after all these years of struggling, you may form your own style of handling things and your own foundations for your future research.

Understand

People use different perspective to understand how things work! I find it out because today I was reading another student's code. And I find that I am the kind of person who tend to understand the complex aspect of it, is it good or bad? I realize the complexity of my code is way much than his.

Learn from the Prof. Stump

1. People need encouragement,especially for new researcher like me,a little positive comments on my new idea will really help me to overcome the difficulties in this endless research.

2. Maybe most people ask you for help, they're actually ask you for encouragement, you may not actually help them sometimes, but your encouragement is the best help for them.

3. Maybe I am the kind of picky person, or I never try to think for other people, maybe I will never be a good teacher, although I do have the passion to share my understanding of something to someone. But maybe it's because the communication skills problems.

Correctness of Programming

When we try to write everything as function, or in another word, for imperative programming language, we write everything composably from the basic function. The basic function is something correctness is definitely guaranteed. And we use Dikjstra 's great method-"structure programming", try to compose program from 'atom' to bigger one, increasingly--but I want to push it to extreme, everything in the big program is composed by a strictly smaller one, then the final function is the outer layer, and the basic element is from the 'atom'. In this style(which I will call it well-founded structure programming), I intuitionisticly feel that this kind of program, we can always check whether is correct or not. I have this intuition feeling because, I write program ill form most of the time, or in fact, I write the whole program as an 'atom', then it's really hard to guarantee the correctness. But once I figure out each part of the program actually can be written as a smaller function, then the checking of whether my whole program is well behaved can be done much easily.

Evaluation Function

Why is so hard to find a perfect evaluation function? Maybe because the standard is so blur that based on our blur standard, our evaluation function is also not perfect. Evaluation function map a situation to a partial order set, but we can see that not every situation can be "mapped" to an element of the partial order set, or this is impossible. So why not discard the mapping idea completely, so that our optimistic technique based on other theory like probability or some comparable theory other than partial order set.

Reserch opinions

When we try to accept any kind of 'facts' or 'theories' or 'opinions' in our research field, it's really dangerous if we accept them blindly, I mean, really really dangerous. Because it's research, not something casual in our daily life. So when it comes to research, it's business, it's not personal. No matter who tells you somethings that they believe it's 'facts' for them, you always has the responsibility to double check it yourself if you want to accept it. Even if you don't care or these 'facts' does not directly related to your research, it's always better to believe it's
'Not True' at all, because a false believe may eventually give you some wrong opinions about that thing, which can be really harmful and restrict your future extension.

Fear

I am always fear this situation: What I think I have understood, but actually is not the case. Because we have no way(or hard to ) check the correctness and preciseness of what we think we have understood. To approach checking, we really need to share our opinions with others, with at least a hope or a chance to let other point out my misunderstanding or errors.

Thoughts on How human Understanding the world

How we as human understand the world? I am here giving my own answer. We understand it through interpretation. When we encounter a new object, we tend to find a way to translate it to another object(s) that we have already understood(or at least we think we understand). This style of understanding correspondent to model theory in the sense of logic.

But we can also understand this new object in this way, we observe it's behaviors and get familiar with it's behavior, and we learn its behaviors so well that we may predict it or simulate it in another different context, then in this way, we also can say now we understand this object. This pattern of understanding is what we call proof theory in the sense of logic.

And off course, most of the time, we mix these ways together to understand, then that blur the essence of human understanding a little bit. At last, I also want to ask, are the two styles I mentioned above are the most basic ways to understand a new object? Or There may exist another way that I cannot even describe?

New observation about Proof by Induction

Here is a special case of how we use proof by induction:
We want to prove P->Q by induction on n.
base case: n=0, P always false. Then P->Q is a tautology.
step case: show that (P->Q)(n-1) => (P->Q)(n)

Then is it still a constructive proof?
If we consider to prove (P->Q)(0) => (P->Q)(1), which we actually need to prove
(P->Q)(1) without any helps because (P->Q)(0)tell us nothing. Then it may has two situation, one is P(0) is also false, that makes (P->Q)(1) a tautology. So Now let's consider n=j, where P(j) is true, and P(j-1) is false. Then if we want to prove
(P->Q)(j),without any help from (P->Q)(j-1). Once we successfully prove (P->Q)(j), we can prove (P->Q)(n), where n>j, with the help of induction hypothesis,that is if P(n-1) is true, we can get Q(n-1), with the help of Q(n-1), we try to prove (P->Q)(n).

The thing is,if the j above doesn't exist(and we know that), then of course it's easy to explain. If j does exist, we still need to show (P->Q)(j) is true, then we can go on to use induction hypothesis. But Am I right?

Basic Proof techniques

So far, all the techniques I used in my proof are induction proof and modus ponens, and other propositional judgements. I really think that I can do my proof on the theorem prover, that will definitely eliminate my doubts of correctness of my proof.

Theory and Applications

Sometimes I couldn't help to wonder: Am I a theorist or a practitionist? Or should we distinct these two as two different objects,or even think these two are on the each side of a polar. And I sense that there is a trend that one does not respect the other. I realize at least I have this kind of prone. And I also notice that most theorists pay no attention to the application, and the practitionists do the same things. I think for any subjects, there are three kinds of people, one is pure theorist, one is trying to put the theory he understands to the practice, one focus only on practice, he assume the existence of a theory foundation for his work, all he need to do is improved the practical impact of it. If this kind of situation is true, I feel that my favor is somewhere between the first two, or I want to be both the first two kind of people at the same time. yes, I want to invent my own theory, and see how it work out in practice. And the sadness is some theorist cannot see the flourish of his theory in their lifetime. But, I want to be an optimist, and with the hope and passion, to delve into the pure theory,figure out the essential relations of the objects.

The world

To see a world in a grain of sand
Or a heaven in a wild flower,
Hold infinity in the palm of your hand
And eternity in an hour.
WILLIAM BLAKE (1757-1827)

Thinking

CLAUDE SHANNON once told me that as a kid, he remembered being stuck on a jigsaw puzzle.
His brother, who was passing by, said to him:
"You know: I could tell you something."
That's all his brother said.
Yet that was enough hint to help Claude solve the puzzle.
The great thing about this hint... is that you can always give it to yourself !!!
I advise you, when you're stuck on a hard problem,
to imagine a little birdie or an older version of yourself whispering
"... I could tell you something..."

Cited from http://www-2.cs.cmu.edu/~mblum/research/pdf/grad.html

Stand in the Truth of Mountain And see the Chaos Under

After A month's Studying and learning and Researching, I finally see through what's the structure behind the lambda D system. That's fantastic! Amazingly, the structure is so simple that I feel lambda D actually only have a little tiny improvement compare to simple typed lambda system. Anyway, Nail it!

Thoughts about Proof by Induction.

When we use the method of Proof by Induction,
First, we need to figure out we do induction on what.
Second, when we figure out the thing that we're going to do induction on, we also
need to show the well-foundness of that thing.
Finally, we can safely use the Induction Method.

Different Opinions

People use different point of view to see their research, some use practical point of view, some just don't. Can we say one is better than the other? I don't think they are comparable. But sadly sometimes there are people try to compare them and try to convince me one is better than the other, what should I say.