Hard decisions on K2

Crazy story.  The death zone of a mountain is the part so high that it cannot sustain human life.  Your body loses oxygen faster than it can replace it by breathing.  Some time in 2008, after 8pm, 10 climbers were stuck in the death zone of K2 when their ropes were all lost during a serac slide.  Some bivouacked, and some descended without ropes in the darkness. 

 

Real Mathematicians Don't Prove

Essay from Dijkstra.

LaTeX bar charts

A nIce tool for making bar charts in LaTeX.

Caffeine works

I'm very surprised by this.  Caffeine definitively makes people perform better, even if they are habituated to its use.

LaTeX: pdfsync and tabular p-width

If you include pdfsync, a nice package that adds hyperlinks to a pdf generated from LaTeX, be warned that it will break the p-widths of tables.  For instance

\begin{tabular}{p{1in}}
abc def
\end{tabular}

will make the column nearly the width of the entire page rather than 1 inch.  I don't have a workaround for this yet.  If you have one, please let me know.  The bug is noted elsewhere, but I haven't seen a correction.

algorithmic-fix

If you try to use line numbers with the LaTeX algorithmic package and also hyperref, you are in trouble.  You get lots of annoying warnings about symbols being defined twice.  The solution is found here.
You need to include a little latex package called algorithmic-fix.sty, provided by the author of hyperref.  The content is:

\NeedsTeXFormat{LaTeX2e}[1994/12/01]
\ProvidesPackage{algorithmic-fix}%
  [2008/02/27 v0.1 Fixes algorithmic for hyperref (capt...@sommerfee.de)]
% 1. Replace the two wrong \refstepcounter's with \stepcounter's
\begingroup
  \long\def\x#1\refstepcounter#2\@nil{%
    \endgroup
    \def\ALC@item[##1]{#1\stepcounter#2}}%
\expandafter\x\ALC@item[{#1}]\@nil
\newcommand\ALC@list{%
  \begingroup
    \long\def\x\refstepcounter##1\@nil{%
      \endgroup
      \def\ALC@it{\stepcounter##1}}%
  \expandafter\x\ALC@it\@nil
  \let\list\ORI@list\list}%
\renewcommand\ALC@setref{}%
% 2. Define a unique \theHALC@line
\newcounter{algorithmic}
\let\ORI@algorithmic\algorithmic
\def\algorithmic{%
  \stepcounter{algorithmic}%
  \let\ORI@list\list\let\list\ALC@list\ORI@algorithmic}
\def\theHALC@line{\thealgorithmic-\theALC@line}
% That's all
\endinput

Writing about a program

I'm working on my thesis proposal.  I'm wondering what details of my theorem provers to include in a text writeup.  There are hundreds of small choices you make implementing a piece of software.  Which are important enough to explain and record, and which are just artifacts of, say a particular choice of data structure?  After reading a bunch of related papers, I think the best answer is that you should include enough information so that if you totally lost the memory of implementing the system, you could produce an "equivalent" program, i.e., one that has "roughly" the same operational behavor.  This should include the high-level optimizations.  An optimization is high-level if it operates at the level of abstraction.  For instance, if your theorem prover does term indexing, the kind of term indexing, and any non-standard tweaks, it performs should be recorded.   The actual structure should be elided.  Perhaps the best way to describe this in SML would be as "maximally abstract" signatures and functors.  Well, I obviously need to think about this more...

Fitting in

Moving article about Michael Jordan's son.

Vietnam Visa

You need a visa to visit Vietnam.  The fee is not marked on their website.  I called the embassy.

1 month, single entry: $65
1 month, multiple entry: $110
3 months, single entry: $90
3 months, multiple entry: $150

Training

Nice essay about training for a first marathon.

Votes by economic status

Stories from Narita Airport in Tokyo

Robert Acker, teaching the globalization course Geography 20 at Berkeley, has the following stories about Japan that I thought were fascinating.

1) He was sitting in the airport, and walked by a store in the airport mall.  There was a sign next to the register, in English and Japanese, that said "I'm out sick for the day.  If you need anything, take it and pay the cashier across the way." 

2) Global clothing companies budget %4 of the annual expenses for shoplifting.  In Japan it's %0.4. 

In his humorous words, "If something's not done in a society, you don't do it.  It's as simple as that."

Lots of drafts

Apple's Mail program is telling me I'm not good at finishing my email correspondence.

Best American Short Stories, 1998

I just finished a really good collection of short stories that I bought at a thrift store while helping Roland get furniture.  It's from the Best American Short Stories series that I just learned has been produced since 1978.  My favorites:

Kathryn Chetkovich, Appetites
Chris Adrian, Every Night for a Thousand Years
Matthew Crain, Penance
Padgett Powell, Wayne in Love

Best dialogue:

"Does your mamas ever talk to y'all about, you know, God?"

"My mama says 'God' when she's cussing Melvin"

"That's not what I mean.  Do they read Bible stories to y'all at bedtime?"

Freddie's face brightened.  "She rented Conan the Barbarian for us once.  That movie kicked ass."

AbeBooks

I recently used google and ebay to try to find the cheapest copy of Dacher Keltner's Social Psychology textbook.  The cheapest I found was $54 from England.  I just found out about AbeBooks.   (Perhaps I'm the last to know.) This is a great resource.  It is the Orbitz (or Kayak) of book buying.  They had dozens of copies from $34.00.  So my ignorance cost me $20 this time.

In Memoriam: Jack Schwartz

I was very sorry to read the following email today.  Jack Schwartz was an inspiring teacher and scientist.  I recall his computational logic course as one of my favorite, and had many interesting conversations with him about his SETL formalization of the Cauchy integral theorem in his own theorem prover.  I was learning HOL-Light at the time, and the contrasts were striking.  I recall being at a lunch with Schwartz, Tom Hales and John Harrison at a Burmese restaurant in Greenwich Village where the topic of conversation turned to formalizing mathematics.  What struck me about him was his youthful eagerness and enthusiasm about the project.  And it was only one of many such projects he was interested in when I knew him.  I hope to be so thoughtful and vibrant at half his age.


    Dear members of the CIMS community,

    It is with sadness that I write to let you
    know that Jack Schwartz passed away in his
    sleep early this morning. He was 79 years old.
    As many of you know, Jack was the founding
    chair of the computer science department and
    the central player in setting the computer
    science research agenda here in the decades
    before and after the department's founding;
    this included seminal work in compilers,
    programming languages, parallel computing,
    robotics, bioinformatics, and multimedia.
    Most of the large-scale research efforts of
    the last forty years in the computer science
    department owe their initial impulse to his
    vision, his tireless energy, and his
    omnivorous scientific curiosity.

    Jack came to Computer Science after a
    distinguished career as a mathematician, the
    junior author of the three-volume "Linear
    Operators" and of numerous books on pure and
    applied mathematics, ranging from C* algebras
    to mathematical economics.  He was an
    inspiring teacher (who at one time or another
    taught pretty much every course in the
    computer science curriculum) and was the
    advisor for more than 50 Ph.D. theses.

    He was a generous friend and an inspiration to
    many of us.

    The Courant Institute will be holding a
    memorial in the next few weeks, to honor his
    life and achievements. We will send a more
    detailed announcement when we have more
    information.


    Richard

    ---

    Richard Cole Deputy Director Courant
    Institute, NYU

Free logic programming book.

A good (free) intro to the theory of logic programming.  It looks like a textbook that went out of print.  Gives a model theoretic account.  Consider also my adviser's notes for a type theoretic approach.

Not so disappointed I'm not graduating this year

Brad DeLong is reading applications at Berkeley.

I was just looking through the lecturer applications. OMG. So many people who would be so good in the classroom, and who know so much, and would be such general assets to the Berkeley intellectual community. This has to be the worst year to apply for an academic job in America since... the Great Depression

And I think we are going to be offering them half-time jobs...