gusl: (Default)
Computer gamers solve problem in AIDS research that puzzled scientists for years

Yay for gamification! This is very exciting!

Where else could we outsource intellectual labor to computer gamers? What other bits of science can be formalized and modularized away so as to not require the context that only comes with years of experience? Is this the same set of problems where you might use AI search algorithms?

For anyone interested in the logical structure of scientific theories and inter-theory relations, I recommend Theo Kuipers's "Structures in Science".


Tangentially, I've been working on a homework problem: if X and Y are independent geometric random variables, show that min(X,Y) is geometric. It is easy to write a semantic proof of this statement: just interpret X as "first time period in which a man arrives" and Y as "first time period in which a woman arrives", then min(X,Y) is "the first time period in which a person arrives". X and Y can be thought of as arising from memoryless arrival processes; and since they are independent, min(X,Y) arises from the combination of the two processes, which is clearly also memoryless.

Despite what some might say, this argument is 100% rigorous; though it is probably a distraction from the intent of the exercise, which is to play with equations... which is understandable, since that object-level axiomatic system is more well-known by mathematical bureaucrats who can rubber-stamp proofs as "valid".

To use a term from diagrammatic reasoning, semantic proofs give us a "free ride".
gusl: (Default)
I am all about working with multiple representations, combining induction with deduction, merging probability with logic, etc.

When we write software, we desire it to be correct, and demonstrably so ("demonstrably" in the sense of being able to convince someone: perhaps "demoably" is a better term). There are many ways of doing this:
* empirical testing: we see that it does the right thing.
* agreement: testing, not against the world or our belief of what it should do, but against an "independent" implementation. We could unify these two by defining the concept of "agent", which could encompass a human test-judger, another program, etc.
* formal proving: more definite than the above two, but we have to rely on the system in which the proof is built.

Software development routinely involves all of the above, except for the "proving", which is informal. But, (as would be typical of me to say) we do make real deductions when writing or judging a piece of code.

The mainstream of software development follows an engineering / instrumentalist epistemology: they know that the program has bugs, but they don't mind them as long as the program is still useful. As a consequence, they "abrem mão" of formal proofs and are satisfied if the program passes a particular class of empirical test cases.

The purpose of test cases is often to convince one that the program would work on a broader class of test cases (otherwise all you would be proving is that the program will work on a non-interactive demo). This is induction. Perhaps the most important epistemological question for software is: how far and how confidently can one generalize from a set of test cases?

Another question has to do with the dynamic development process: when and how should we test? Common-sense testing methodology tells us to write simple test cases first. This is Occam's razor.

Btw, this is similar to mathematical epistemology: how do we combine experimental mathematics with normal deductive math? How do we combine different pieces of intuitive knowledge in a consistent, logical framework?


If you ask a doctor (or any specialist) to write down probabilities about a particular domain that he/she knows about, these numbers will almost certainly be susceptible to Dutch book. Bayesians consider this to be a bad thing.

I believe that, by playing Dutch book with him/herself, our doctor would achieve better estimates. I would like to see experiments in which this is done. Actually, I should probably write some of this software myself. The input is a set of initial beliefs (probabilities), and the output is a Dutch-book strategy. This Dutch-book strategy corresponds to an argument against the set of beliefs. This forces our specialist to reevaluate his beliefs, and choose which one(s) to revise. This is like a probabilistic version of Socratic dialogue.


Do you see the connection between the above two? Please engage me in dialog!
gusl: (Default)
It has been said that being formal forces one to be honest. But I think it does more than that: by leaving nothing implicit, formal expositions also force the author to really understand what he/she is saying, to iron out one's contradictions and "semi-contradictions" (e.g. the Nixon diamond).

Gerald Sussman and Jack Wisdom, about their computational exploration of classical mechanics:
When we started, we expected that using this approach to formulate mechanics would be easy. We quickly learned that many things we thought we understood we did not in fact understand (1). Our requirement that our mathematical notations be explicit and precise enough that they can be interpreted automatically, as by a computer, is very effective in uncovering puns and flaws in reasoning (2). The resulting struggle to make the mathematics precise, yet clear and computationally effective, lasted far longer than we anticipated.
We learned a great deal about both mechanics and computation by this process. We hope others, especially our competitors, will adopt these methods, which enhance understanding while slowing research.

A few comments:

(1) It's probably safe to say that most physics professors don't understand those things either, unless they have undergone similar formalization efforts. Scientists' expertise is usually correct with regard to the particular exemplars that they study and similar systems, but, unless their understanding is really thorough, there will be examples in which their expertise will not generalize correctly.
There are many cases in which physicists' intuitions get tangled up (see, e.g. Feynman's inverted underwater sprinkler, or even the infamous Monty Hall problem), but these are the lucky cases, since a problem got detected, which subsequently led to the debate: but, in general, if we're going to just rely on intuitions, this could lead to plain oversights: we might never even suspect that we're wrong.
The solution to such shameful persistent disagreements is to have a formal framework for reasoning about such problems: the solutions to these problems are logical consequences of widely agreed-upon laws, but disagreement persists because there is no standard formal framework in use, and learning a new framework would be too steep a learning curve for most scientists. My guess is that we could settle many interesting questions just by checking whether they are in the deductive closure of different combinations of theories.

(2) I like the expression "puns in reasoning", because it's a very good analogy: in fact, I suspect that many errors in scientific reasoning come from a certain sloppiness in using words to denote concepts, which is like using the same name for different variables in one's mind. The cognitive practices of being careful not to confuse concepts are very similar to good programming practice.

On the costs of being formal: Formality might be an unnecessary burden for those who have a good intuitive understanding, but I think it is generally worth the trouble. It is certainly a much greater burden on those who don't understand.

... and how this relates to me:

Anyway, I think this tendency towards thoroughness makes me a rather slow researcher. Being eternally skeptical, interested in foundational questions, and unwilling to proceed without a solid understanding, I have always tended towards the "enhance understanding" side of the trade-off. It's hard to make fast progress in one's research when you're questioning your teachers' assumptions or trying to reformulate it in different terms or seeking analogies with other ideas (which are other ways of making one's understanding more solid).

I'm reminded of my high school physics teacher saying in my college recommendation letter that I was good at deriving things from first principles... I also think it's unusual for professors to recommend a student to "just memorize the formula", "just learn the cookbook". My grades have certainly suffered from ignoring such advice.



~ "In general, I feel if you can't say it clearly you don't understand it yourself." - John Searle

... I'm looking for another relevant quote about programming being "universal". Possibly a Dijkstra quote. Anyone?


gusl: (Default)

December 2016

18 192021222324


RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags