Shadow cities

The essay collection Letters of Transit: Reflections on Exile, Identity, Language, and Loss, published after a lecture series at the New York Public Library, includes “Shadow Cities” by André Aciman. An excerpt follows.

¶ And, indeed, there was something physically central about Straus Park. This, after all, was where Broadway and West End Avenue intersected, and the park seemed almost like a raised hub on West 106th Street, leading to Riverside Park on one side and to Central Park on the other. Straus Park was not on one street but at the intersection of four. Suddenly, before I knew why, I felt quite at home. I was in one place that had at least four addresses.

¶ Here you could come, sit, and let your mind drift in four different directions: Broadway, which at this height had an unspecified Northern European cast;

West End, decidedly Londonish;

107th, very quiet, very narrow, tucked away around the corner, reminded me of those deceptively humble alleys where one finds stately homes along the canals of Amsterdam.

And 106th, as it descended toward Central Park, looked like the main alley of a small town on the Italian Riviera,

where, after much trundling in the blinding light at noon as you take in the stagnant odor of fuel from the train station where you just got off, you finally approach a sort of cove, which you can’t make out yet but which you know is there, hidden behind a thick row of Mediterranean pines,

over which, if you really strain your eyes, you’ll catch sight of the tops of striped beach umbrellas jutting beyond the trees, and beyond these, if you could just take a few steps closer, the sudden, spectacular blue of the sea.

¶ To the west of Straus Park, however, the slice of Riverside and 106th had acquired a character that was strikingly Parisian,

and with the fresh breeze which seems to swell and subside all afternoon long, you sensed that behind the trees of Riverside Park,

serene and silent flowed an elusive Seine,

and beyond it, past the bridges that were to take you across, though you couldn’t see any of it yet, was not the Hudson, not New Jersey, but the Left Bank—

not the end of Manhattan, but the beginning of a whole bustling city waiting beyond the trees—as it waited so many decades ago when, as a boy, dreaming of Paris, I would go to the window, look out to the sea at night, and think that this was not North Africa at all, but the Ile de la Cité. Perhaps what lay beyond the trees was not the end of Manhattan, or even Paris, but the beginnings of another, unknown city, the real city, the one that always beckons, the one we invent each time and may never see and fear we’ve begun to forget.

¶ There were moments when, despite the buses and the trucks and the noise of people with boom boxes, the traffic light would change and everything came to a standstill and people weren’t speaking, and the unrelenting sun beat strong on the pavement, and I would almost swear this was an early summer afternoon in Italy, and that what lay behind Riverside Park was not just my imaginery Seine, but the Tiber as well. What made me think of Rome was that everything here reminded me of the kind of place all tourists know well: that tiny, empty piazza with a little fountain, where, thirsty and tired with too much walking all day, you douse your face, then unbuckle your sandals, sit on the scalding marble edge of a Baroque fountain, and simply let your feet rest a while in what is always exquisitely clear, non-drinkable water.

¶ Depending on where I sat, or on which corner I moved to within the park, I could be in any of four or five countries and never for a second be in the one I couldn’t avoid hearing, seeing, and smelling. This, I think, is when I started to love, if love is the word for it, New York. I would return to Straus Park every day, because returning was itself now part of the ritual of remembering the shadow cities hidden there—so that I, who had put myself there, the way squatters put themselves somewhere and start to build on nothing, with nothing, would return for no reason other than perhaps to run into my own footprints. This became my habit, and ultimately my habitat. Sometimes finding that you are lost where you were lost last year can be oddly reassuring, almost familiar. You may never find yourself; but you do remember looking for yourself. That too can be reassuring, comforting.

…

¶ How uncannily appropriate, therefore, to find out fifteen years later that the statue that helped me step back in time was not that of a nymph, but of Memory herself.

In Greek, her name is Mnemosyne, Zeus’s mistress, mother of the Muses. I had, without knowing it, been coming to the right place after all. This is why I was so disturbed by the imminent demolition of the park: my house of memories would become a ghost park. If part of the city goes, part of us dies as well.

免窗升級想板基本輸入輸出系統法門

為了讓我的 ThinkPad 風扇安靜一點，最近想要把它的 BIOS 升級到最新的版本。因為我的電腦上沒有裝 Windows，只有裝 Linux，所以除非麻煩地重灌 Windows，否則不能使用 IBM 或聯想發佈的 Windows 版 BIOS 升級程式。

以往在 ThinkPad X20 系列的年代，IBM 除了 Windows 版的升級程式以外，還會發佈一張軟碟開機片。也就是我可以下載一個 1.44MB 的檔案，寫到一張軟碟上用來開機。這張軟碟的內容其實是 IBM 用 DOS 拼湊而成的，開機以後 AUTOEXEC.BAT 會自動執行升級程式。就算沒有 ThinkPad 擴充的軟碟機，或手邊沒有空著不用的軟碟（我最近一次看到軟碟好像是馬蓋先的「醜小鴨」那集吧），也可以用 SYSLINUX 的 MEMDISK，直接從下載檔案裡的虛擬軟碟開機。例如我用 GRUB，在 /boot/grub/menu.lst 裡加上一段

title  MEMDISK
kernel (hd0,5)/lib/syslinux/memdisk
initrd (hd0,7)/ccshan/tmp/floppy.img

即可用 /usr/lib/syslinux/memdisk 從 /home/ccshan/tmp/floppy.img 裡的虛擬軟碟開機，因為 (hd0,5) 是我的 /usr 分割區，而 (hd0,7) 是我的 /home 分割區。就算既不用 GRUB 也不用 Linux，也可以用 PXELINUX 從網路上別台電腦上的虛擬軟碟開機進行升級。

現在時代不同了，ThinkPad X60 系列的 BIOS 已經大得軟碟裝不下了，於是 IBM 發佈的開機片不再是軟碟而是光碟。我沒有光碟機，也不想重灌 Windows，所以希望從虛擬光碟開機進行升級，但是事情沒那麼簡單，因為 MEMDISK 只會模擬磁碟，不會模擬光碟。這是因為從光碟開機的過程比從磁碟複雜，要遵從 El Torito 標準進行。IBM 的這張光碟開機片，除了把新的 BIOS 及其更新程式放在一般的 ISO 9660 檔案系統以外，另含一張虛擬的軟碟開機片。當一位有錢擴充 ThinkPad 的用戶，用燒好的實體光碟開機時，ThinkPad 會從實體光碟上載入虛擬軟碟，執行虛擬軟碟上的 DOS。這份 DOS 的 CONFIG.SYS 與 AUTOEXEC.BAT 得先載入實體光碟機的驅動程式，才能讀到前述的 ISO 9660 檔案系統，以執行實體光碟上的 BIOS 更新程式。

我徹夜試驗，發現可以用實體硬碟代替實體光碟，成功升級了我的 BIOS。基本的想法是，在一個實體硬碟的新分割區裡，結合軟碟上的 DOS 開機程式以及光碟上的 BIOS 升級程式。詳情如下。

首先得在實體硬碟裡造一個分割區，如下例 /dev/sda2。這個分割區不用很大，比 IBM 發佈的光碟檔稍大一點就夠了（約 5MB），不過必須位於實體硬碟的前 1024 個磁柱以內（這是 DOS 的限制，迫使我用 gparted 把原本在硬碟最前面的分割區稍微縮小了一點，幸好那只是我的 /usr/local 分割區而已，不很麻煩），而且必須是初選而非邏輯分割區（迫使我用 sfdisk -d 把一個不常用的初選分割區備份然後暫時刪除，升級完再用 sfdisk -uS -N… -O… 小心放回分割表內）。

在分割表裡，這個分割區的型別應設為 6 號（也就是 FAT16 的意思），並且可開機旗標應設為真，因為我們就是要用它開機。但是要把它作成 DOS 的開機分割區，除了新造檔案系統

$ sudo mkdosfs /dev/sda2

以外，還需一番移花接木。我從 IBM 下載的光碟檔名為 7buj25uc.iso，其中內含的虛擬軟碟開機片是從位元組位址 0xA800 (= 43008) 開始的 1.44M (= 1474560) 個位元組。為了方便，我把這部份資料擷取成為另一個檔案 7buj25uc.img。

$ dd if=7buj25uc.iso of=7buj25uc.img skip=43008 count=1474560 bs=1

這兩個數字是我邊用 tweak 查看光碟檔、邊參考 El Torito 標準文件找到的。我早知道的話，也可以用 Joachim Selke 寫好的程式直接擷取。

要能從 /dev/sda2 這個分割區開機，必須把 7buj25uc.img 這張軟碟的內容複製進去，但是有兩點需要注意的地方。第一，不只要複製檔案，還要複製檔案系統最開頭的開機磁區，但是不能蓋掉裡面所謂的 BIOS 參數區塊，因為那裡存有分割區大小等資訊。第二，根目錄裡表列的第一個檔案必須是 IBMBIO.COM，第二個必須是 IBMDOS.COM，不然開機磁區裡的程式會找不到。

開機磁區是檔案系統開頭的 512 個位元組，其中 BIOS 參數區塊佔用的是位址 3 到 62 之間的 59 個位元組，所以我把區塊前的 3 個位元組與區塊後的 450 個位元組分別從軟碟複製到分割區裡。

$ sudo dd bs=1 count=3 if=7buj25uc.img of=/dev/sda2
$ sudo dd bs=1 seek=62 skip=62 count=450 if=7buj25uc.img of=/dev/sda2

然後我把軟碟裡的所有檔案都複製到分割區裡，但是先複製 IBMBIO.COM 與 IBMDOS.COM。（以下指令假設已存兩個空目錄 /mnt/pool 以及 /mnt/loop。）

$ sudo mount -t msdos /dev/sda2 /mnt/pool
$ sudo mount -t msdos -o loop 7buj25uc.img /mnt/loop
$ sudo cp /mnt/loop/ibmbio.com /mnt/pool
$ sudo cp /mnt/loop/ibmdos.com /mnt/pool
$ sudo cp -u /mnt/loop/* /mnt/pool
$ sudo umount /mnt/loop

此時查看 /mnt/pool/config.sys 與 /mnt/pool/autoexec.bat 可以了解，這張虛擬開機片在掛上光碟以後會執行光碟上的另一個 COMMAND.COM。所以我在把光碟內容複製到分割區裡的同時，乾脆用光碟上的 COMMAND.COM 取代軟碟上 DOS 的 COMMAND.COM。

$ sudo mount -o loop 7buj25uc.iso /mnt/loop
$ sudo cp -i /mnt/loop/* /mnt/pool
cp: overwrite `/mnt/pool/COMMAND.COM'? y
$ sudo umount /mnt/loop

最後，我用文字編輯器修改 /mnt/pool/config.sys，把其中的 A: 統統換成 C:（因為要從硬碟而非軟碟開機），並且拿掉呼叫 COMMAND.COM 那一行後面給的參數。

$ vi /mnt/pool/config.sys
$ sudo umount /mnt/pool

大功告成。重新開機以後，請 GRUB 啟動這個新的分割區

root (hd0,1)
makeactive
chainloader +1

即可進入 IBM 的 BIOS 更新程式。

Differentiating regions

(An alternative title for this post is, what is the type of differentiation? Hint: it’s not quite (ℝ→ℝ)→(ℝ→ℝ), because how would you make sure the input function is differentiable?)

You can download this post as a literate Haskell program.

{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE OverlappingInstances   #-}

module Differentiation where

Automatic differentiation

The overloading approach to automatic differentiation has become more popular recently among typed functional programmers. The basic idea is to overload arithmetic operators such as +, ×, and sin so that they work on not just floating-point numbers but pairs (or more generally, sequences) of them, which track quantities along with their rates of change. The overloaded operators are easy to define because, unlike with integration, the rules of differentiation are compositional: you know, d(x + y) = dx + dy, d(x × y) = dx × y + x × dy, d(sin x) = cos x × dx, and so on. Here they are in Haskell.

data D a = D a a
  deriving Show

lift :: Num a => a -> D a
lift x = D x 0

infinitesimal :: Num a => D a
infinitesimal = D 0 1

instance Eq a => Eq (D a) where
  D x _ == D y _ = x == y

instance Ord a => Ord (D a) where
  compare (D x _) (D y _) = compare x y

instance Num a => Num (D a) where
  D x x' + D y y' = D (x + y) (x' + y')
  D x x' * D y y' = D (x * y) (x' * y + x * y')
  negate (D x x') = D (negate x) (negate x')
  abs    (D x x') = D (abs x) (signum x * x')
  signum (D x _)  = lift (signum x)
  fromInteger x   = lift (fromInteger x)

instance Fractional a => Fractional (D a) where
  recip (D x x') = D (recip x) (-x'/x/x)
  fromRational x = lift (fromRational x)

The two components of a D value are a quantity and its derivative, so the lift function ‘lifts’ a number to a constant quantity, and infinitesimal is a quantity with value 0 and derivative 1. Were abs defined by abs x = signum x * x by default, we wouldn’t have to define abs for D above.

Let us use these definitions to model how a parabola reflects light.

Suppose that a light ray (red above) enters a parabolic mirror y = x²/4 from above. Where does the reflected ray cross the y axis? In the diagram above, if the point where the ray hits the parabola is (x,y), then the derivative of y with respect to x is tan θ, and the y coordinate where the reflected ray crosses the y axis is y + x/tan 2θ, which is equal to y + x (1/tan θ − tan θ)/2. We can compute this coordinate by automatically differentiating y with respect to x:

curve x = x^2/4

reflect x = let D y y' = curve (lift x + infinitesimal)
            in y + x * (recip y' - y') / 2

As expected, the parabola reflects all incoming rays from above to the focal point (0,1).

*Differentiation> map reflect [1..5]
[1.0,1.0,1.0,1.0,1.0]

To be sure, this code does not work by symbolically differentiating y = x²/4 to yield y′ = x/2. Rather, it computes y alongside y′ for one particular x at a time, so the curve could just as well be defined by a more complex program that uses if and recursion. For example, a ray tracer usually deals with scenes much more complex than a single parabola. This code also does not work by numerically comparing the values of y at nearby values of x. Instead of approximating dy/dx by Δy/Δx where Δx is a very small real number, we compute with an actually infinitesimal dx.

Differentiation is a higher-order function

Before we continue, let us abstract the pattern for differentiation in reflect above into a new higher-order function d, which differentiates any given function at the input 0. For convenience, d also returns the value of the given function at 0.

d :: Num a => (D a -> D b) -> (b, b)
d f = let D y y' = f infinitesimal
      in (y,y')

reflect :: Fractional a => a -> a
reflect x = let (y,y') = d (\h -> curve (lift x + h))
            in y + x * (recip y' - y') / 2

Even though the reflect function uses differentiation internally, we can still differentiate it. Such differentiate is said to be nested. For the parabola, we can confirm that the reflected ray hits the focal point not just at but also around x = 3, because the derivative computed below is zero.

*Differentiation> d (\k -> reflect (3 + k))
(1.0,0.0)

For other curves and surfaces, the derivative is typically not zero and tells us the density of light energy that falls around each point on the y axis. Hence, as Dan Piponi noted, this kind of calculation is performed by ray tracers and other programs that sample from probability distributions.

Another application of automatic differentiation is to find roots of a function using Newton’s method. Therefore, we can use nested automatic differentiation to find local extrema and saddle points of a function using Newton’s method.

The danger of confusing infinitesimals

Jeff Siskind and Barak Pearlmutter pointed out a kind of programmer mistake that makes nested differentiation give the wrong result. As they show, this kind of mistake is easy to make in the framework defined above, because all it takes is putting a call to the lift function in the wrong place. The definition of reflectBug below is only slightly different from reflect, but the result is very different and very wrong.

reflectBug x = let (y,y') = d (\h -> lift (curve (x + h)))
               in y + x * (recip y' - y') / 2

*Differentiation> d (\k -> reflectBug (3 + k))
(Infinity,NaN)

They demonstrate this problem using running code in Haskell and Scheme that computes

to be 2 rather than the correct answer 1.

The essence of this problem is that the two nested invocations of differentiation use two different infinitesimals, which a mathematician would denote by dh and dk. These two infinitesimals should not be confused, just as years and feet and persons should not be confused.

Using types to check units

Björn Buckwalter showed that we can use a generic type system to prevent such confusion statically, just as Haskell uses state threads to distinguish pointers into different memory regions. Recall that the type ST s a in Haskell represents a monadic computation that yields a result of type a using mutable cells in the state thread represented by the phantom type s. To construct such a computation, we can use primitive operations such as

newSTRef :: a -> ST s (STRef s a)

and the fact that ST s is a monad. To run such a computation, we must use the primitive function

runST :: (forall s. ST s a) -> a

in which forall s forces different state threads, created by different calls to runST, to be represented by different phantom types s. One way to understand this rank-2 type is that it makes the type checker generate a new phantom type s for each argument to runST. Analogously, Buckwalter redefines the type constructor D to take a phantom-type argument s, which represents an infinitesimal unit.

data D s a = D a a
  deriving Show

Accordingly, the other definitions above change in their types, but not in their terms or behavior. The most important change is the new rank-2 type of d, which forces different infinitesimals, created by different invocations of differentiation, to be represented by different phantom types s.

d :: Num a => (forall s. D s a -> D s a) -> (a, a)
d f = let D y y' = f infinitesimal
      in (y,y')

lift :: Num a => a -> D s a
lift x = D x 0

infinitesimal :: Num a => D s a
infinitesimal = D 0 1

instance Eq a => Eq (D s a) where
  D x _ == D y _ = x == y

instance Ord a => Ord (D s a) where
  compare (D x _) (D y _) = compare x y

instance Num a => Num (D s a) where
  D x x' + D y y' = D (x + y) (x' + y')
  D x x' * D y y' = D (x * y) (x' * y + x * y')
  negate (D x x') = D (negate x) (negate x')
  abs    (D x x') = D (abs x) (signum x * x')
  signum (D x _)  = lift (signum x)
  fromInteger x   = lift (fromInteger x)

instance Fractional a => Fractional (D s a) where
  recip (D x x') = D (recip x) (-x'/x/x)
  fromRational x = lift (fromRational x)

Because the phantom type s is part of the type of a number, and because arithmetic operations such as + require the arguments and the return value to have the same type, it is a type error to add numbers denominated in different infinitesimals. In particular, the erroneous definition reflectBug above is now a type error, as desired.

Occurs check: cannot construct the infinite type: t = D s t
  Expected type: t
  Inferred type: D s t
In the first argument of `lift', namely `(curve (x + h))'
In the expression: lift (curve (x + h))

For this checking of infinitesimal units to be sound, this library for automatic differentiation should not export the values D and infinitesimal to its users, though of course the type constructor D and its type-class instances need to be exported, along with the functions d and lift.

(In the discussion that ensued, David Roundy noted that the same kind of static safety can be achieved by exporting just a function

d :: Num a => (forall b.
      Num b => (a -> b) -> b -> b) -> (a, a)

for differentiation. The type b makes it unnecessary and useless to export the type constructor D, even though d is still implemented using D. Also, the new argument of type a -> b makes it unnecessary and useless to export the lift function. Finally, the type-class context Num b makes it unnecessary and useless to export the Eq, Show, and Num instances for D. However, as Chris Smith lamented, we need additional differentiation functions of the types

Fractional a => (forall b.
 Fractional b => (a -> b) -> b -> b) -> (a, a)

Floating a => (forall b.
 Floating b => (a -> b) -> b -> b) -> (a, a)

in order to differentiate functions that use Fractional or Floating operations. Oleg Kiselyov used similar types to express symbolic differentiation.)

Automatic lifting

Although the type system now prevents us from putting calls to lift in the wrong place, it is still annoying to have to invoke lift manually—especially for nested differentiation, a useful case as discussed above. Depending on ‘how constant’ a quantity is, we need to feed it through a composition of exactly the right number of lifts. This manual coding is frustrating because the unique right number of lifts to apply is obvious from the input and output types desired: to convert a type a to the type D s a, apply lift once; to convert a to D s (D s' a), apply lift twice; and so on. We want the compiler to manage these subtyping coercions automatically.

An analogous situation arises with state threads, which can be organized into a hierarchy of memory regions. As part of a monadic computation that uses mutable cells in a parent region, we can create a child region and perform a subcomputation that allocates and accesses mutable cells in both regions. After the subcomputation completes, the child region is destroyed en bloc, but we can still use the parent region and observe any effect on it brought about by the subcomputation. To allow the subcomputation to use the parent region, we want every region to be a subtype of its descendents. Matthew Fluet and Greg Morrisett’s implementation of nested regions in Haskell uses explicit subtyping coercions just like our lift: depending on ‘how senior’ a region is, we need to compose exactly the right number of region coercions.

In a pending submission to the Haskell symposium, Oleg and I show how to automate region subtyping coercions using type classes. One might hope to apply that approach to lifting in automatic differentiation. Indeed we can, but I only know how to automate counting lifts, not how to automate placing them. That is, instead of feeding each use of an input quantity to the lift function exactly the right number of times, we can feed it to a new function once. The new function, called lifts, belongs to a new type class Lifts, which takes two type parameters. The constraint Lifts a b holds if and only if the type b is the result of applying zero or more type constructors D s to the type a.

class Lifts a b where
  lifts :: a -> b

More concretely, the following instances incompletely approximate the intended meaning of Lifts.

instance Lifts a a where
  lifts = id

instance Num a => Lifts a (D s a) where
  lifts = lift

instance Num a => Lifts a (D s (D s' a)) where
  lifts = lift . lift

instance Num a => Lifts a (D s (D s' (D s'' a))) where
  lifts = lift . lift . lift

The definition above of reflect in terms of d applies lift once to one occurrence of x but not to other occurrences of x and h. The same function can be expressed using Lifts, by applying lifts once to each occurrences of the input variables x and h.

reflectAuto :: Fractional a => a -> a
reflectAuto x
  = let (y,y') = d (\h -> curve (lifts x + lifts h))
    in y + lifts x * (recip y' - y') / 2

Expressing reflect in this new way frees us from counting how many times to lift the inputs x and h each time they are used.

How to implement Lifts? On one hand, as an implementation of Lifts, the approximate instances above are incomplete and unsatisfactory in theory, in that they restrict how many lift each lifts can stand for. They are perfectly useful in practice, however, and rely on no extension to Haskell other than rank-2 types and multiparameter type classes with flexible instances. On the other hand, a complete implementation is possible using the TypeCast class for type improvement (originally used by Kiselyov, Lämmel, and Schupke to implement heterogeneous collections), but it requires more Haskell extensions: functional dependencies, overlapping instances, and undecidable instances. Without further ado, below is the complete implementation.

instance Lifts a a where
  lifts a = a

instance (TypeCast (D s b') b, Num b', Lifts a b')
  => Lifts a b where
  lifts = typeCast . lift . lifts

class TypeCast a b | a -> b, b -> a where
  typeCast :: a -> b
class TypeCast' t a b | t a -> b, t b -> a where
  typeCast' :: t -> a -> b
class TypeCast'' t a b | t a -> b, t b -> a where
  typeCast'' :: t -> a -> b
instance TypeCast' () a b => TypeCast a b where
  typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where
  typeCast' = typeCast''
instance TypeCast'' () a a where
  typeCast'' _ x  = x

Although Lifts makes it easier to use automatic differentiation, this implementation is heavy lifting. I wonder if it is easier to express this combination of subtyping and rank-2 polymorphism in a language like Scala?

美國二卡 金綠雙輝 Two American membership cards

美國航空頒發的金卡、以及美國政府頒發的綠卡，張張都攸關大家在美國的生活。它們就如同深藏不露的礦泉水，讓不肖之徒伺機正中我們飛安的要害，又如同免費提供的行李牌，幫地勤人員千里尋回我們失散的骨肉。在這鳳凰花開、四面驪歌的時節，您是否也在金綠之間猶豫不決呢？與其腳踏兩條船，不如把雞蛋集中以便管理。為方便您睿智的抉擇，記者謹將兩卡的十二優劣點整理如下。

The gold card issued by American Airlines and the green card issued by the American government are each an integral part of our American lives. They are as powerful as the hidden water bottles that strip us of flight safety; they are as handy as the free luggage tags that unite us with abducted children. In this season of blooming Delonix regia and booming Auld Lang Syne, are you also hesitating to choose between gold and green? Decide wisely which basket to put your eggs in, with the help of this 12-point summary of the two cards’ pros and cons.

美國航空金卡 American Airlines gold card		美國政府綠卡 American government green card
✗	其實是塑膠的 Actually plastic	✗	其實是白色的 Actually white
✓	使用 Helvetica 字體印製，中性無襯線 Typeset using Helvetica, a neutral sans-serif typeface	✗	使用 Arial 字體印製，仿製沒水準 Typeset using Arial, a cheap knock-off typeface
✗	附送精美彩色印刷《新會員指南》一本，十二頁無索引 Comes with a guide for new members printed in 12 pages of fine color but without index	✓	附送精美彩色印刷《新移民指南》一本，一百頁附索引 Comes with a guide for new immigrants printed in 100 pages of fine color and with index
✓	有搭機、住宿、購物等多種參加方式 Qualify in a variety of ways: flights, accommodations, shopping, etc.	✓	有就業、依親、投資等多種參加方式 Qualify in a variety of ways: employment, family, investment, etc.
✓	接受會員挑戰，三個月衝刺後拿到身份 Get it in 3 months when you enter a Membership Challenge	✗	要求補送證據，三個月期限後失去身份 Lose it in 3 months when you receive a Request for Evidence
✓	快速通過出境安全檢查 Avoid long security lines at departure	✓	快速通過入境邊防檢查 Avoid long immigration lines at arrival
✓	選位、客服優先 Priority for seats and customer service	▵	謀職、徵兵優先 Priority for jobs and military service
✓	每飛行萬哩，可在網上免費獲取升級證 Earn complimentary upgrades online every 10,000 miles	✓	每居留兩年，可在網上付費申請回美證 Apply for reentry permits online every 2 years
✓	旅館、租車公司等合作夥伴提供優待 Special offers on hotels and cars from partner companies	✓	國家、過境機場等合作夥伴提供優待 Special offers on transit and visas from partner countries
✓	票選傑出空服人員 Vote for great flight attendants	✓	票選傑出校務委員 Vote for great school board members
✓	一年換一張新卡 Renew every year	✓	十年換一張新卡 Renew every decade
✓	在貴賓室裡靜待登機 Lounge while waiting for your flight	✓	在移民監裡靜待入籍 Lounge while waiting for your naturalization

Louder and louder

In response to the daytime jackhammering across the street, I put up the sign below at the entrance to our apartment building.

Sangre de mi sangre

Title: Sangre de Mi Sangre (Blood of My Blood), or Padre Nuestro

Overall rating: A (strong accept; will champion film)

Reviewer’s confidence: Y (I am knowledgeable in the area, though not an expert.)

General review:

By weaving together four deep instances of detachment, this well-organized film demonstrates how to derive immigrants from persons mechanically and vice versa. These derivations are intuitively obvious and should not bear any tedious demonstration. Yet, perhaps because they are so painfully obvious, they are often neglected—I often neglect them—when interacting with an immigrant. This neglect injures life, liberty, and the pursuit of happiness as we eat immigrant food, wear immigrant clothes, inhabit immigrant tenements, take immigrant transport, learn immigrant business, have immigrant fun. For example, just the other day I had the urge to run down some jaywalking immigrants as they crossed Canal Street in front of my bike. Or was it in Times Square?

This cinematic pearl thus serves as a rational reconstruction of motion, a timely and entertaining reminder that immigrants are people and people are immigrants. It points the way to a wide variety of practical applications, such as snapshotting the dialects of the Spanish diaspora, establishing my love for New York, and advocating open immigration alongside free trade. I recommend that y’all go see it (in New York this week and Los Angeles next week). Especially if you know how many passports Jason Bourne has. Less if you feel cheated at the end of “The Perfect Human”.

Comments for other reviewers:

Several reviews criticize this movie, on two fronts. On one hand, the story is too clear. The plot is too plotted, the morals too moralistic, and the characters too characteristic: “As a character Pedro never develops beyond a credulous, good-hearted cipher.” On the other hand, the story is too obscure: “As you watch the movie, questions accumulate… Little about the connection between Pedro and Magda makes sense.”

These fronts answer each other. (Pondering the questions develops the characters.) This movie is not simplistic and complicated but simple yet complex. Drawing “characters directly out of Hispanic-cliche central casting” reduces distraction, like studying continuation-passing style (named the canonical program transformation by Olivier Danvy). If “Sangre de Mi Sangre”, taking advantage of a conventional narrative structure as this review tries to, manages to pull tropes out of the ashes of an I-94 form in Williamsburg, then so much the better for a mechanical derivation and its inverse: as those viewers fixated on “impoverished Mexican illegal immigrants” show, it is all too easy to forget that we are all in the image of immigration. A moving target, so to speak.

Questions for the authors:

Why does this trailer credit neither the actress Paola Mendoza nor the actor Eugenio Derbez?

Do you have a shoe fetish?

Tidbits 1

Have you noticed that the tact filter applies to not just verbal behavior but also physical behavior? They’re installed in opposite directions in New York and Tokyo—except at Tsukijishijo (築地市場) perhaps? The most obvious example of a physical tact filter is the mouth mask that sick Japanese people wear in public, ostensibly to avoid infecting others.

The Suica is addictive. It’s like Cosmo’s access card in Sneakers, except of course the Suica charges you, and I bet Cosmo’s card doesn’t open his locker at the gym.

The leftover container problem is to partition a partial order into as few total orders as possible.

Pat Hanrahan wrote that “The BRDF is, in general, anisotropic” (on page 29 of “Rendering concepts”, chapter 2 of Radiosity and Realistic Image Synthesis by Cohen and Wallace, 1993). This sentence is the negation of “The BRDF is, in general, isotropic”! If “in general” in both sentences means “without exception” (which it does not in the true reading of “Primes are odd in general”), then the fact that these two sentences are the negation of each other is reminiscent of sentences such as “Hanna sucht kein Buch”, “Ze mogen geen eenhoorn zoeken”, and “You don’t need to bring any dessert” (Jacobs 1980, Theoretical Linguistics 7:121–136; de Swart 2000, in Reference and anaphoric relations, 118–142; inter alia). However, the sentences “The BRDF is always anisotropic” and “The BRDF is always isotropic” are not the negation of each other.

One of Olivier Danvy’s great examples of program transformation and continuation passing is to test in linear time whether a Calder mobile is balanced. For a mobile to be balanced is for each submobile to locate its center of mass right at its root. Real mobiles are of course never exactly balanced, yet the rods stay roughly horizontal—because even the rigid rods are not straight! Below is a program that rotates the submobiles of a two-dimensional mobile so that each submobile locates its center of mass right below its root. (Exercises left to the reader include handling higher-dimensional mobiles and using continuations to avoid repeatedly constructing and taking apart pairs.)

module Calder where
import Complex

data Mobile a = Point a | Rigid [(Complex a, Mobile a)]

balance :: RealFloat a => Mobile a -> (a, Mobile a)
balance (Point a) = (a, Point a)
balance (Rigid zms) = (sum as, Rigid zms') where
  (as, azs, zm's) = unzip3 [ (a, (a :+ 0) * z, (z, m'))
                           | (z, m) <- zms
                           , let (a, m') = balance m ]
  center = sum azs
  zms' | center == 0 = zm's
       | otherwise = [ (z / signum center, m') | (z, m') <- zm's ]

“Hendrik Lenstra claims that he can no more suggest to his students what problems they should work on than who they should marry.” (Update 2008-06-10: Vladimir Arnol’d said in 1995: “I never assign a thesis topic to my students. This is like assigning them a spouse.”)

Has anyone started designing the all-important logo for a joint Hillary-Obama/Obama-Hillary campaign?

What symbol(s) for disjoint union do you use—one of “+|∐⊔⊍⊎⊕” or something else? Do you use a different symbol for the presupposed disjoint union (which is undefined when applied to {{}} and {{}}) than for the tagged disjoint union (which yields a two-element set when applied to {{}} and {{}})? Those who work with sets up to isomorphism, such as topologists, are exempt from answering the latter question.

It is interesting to read “Nationalität: Jude” on the cover of the August 2007 AMS Notices. Inside the issue is more information about the cover and about Lipman Bers’s immigration.

Strengthening in Logical Frameworks (Twelf) oleg at pobox.com

Many logic systems admit a weakening principle: a derived conclusion continues to hold when more assumptions are added. Strengthening is the opposite: proving that the established conclusion holds given fewer assumptions. Strengthening certainly is not generally valid and has to be proven case-by-case. It seems strengthening is often needed when proving meta-theoretical properties such as totality of non-surjective endomorphisms of higher-order terms.

The article on Twelf Wiki <http://twelf.plparty.org/wiki/Strengthening> shows an example of the need for strengthening and describes one solution, which relies on defining term equality. In this article we demonstrate simpler examples requiring strengthening, and two surprisingly trivial solutions. Quite literally, one solution deals with the problem head-on, whereas the second one avoids the problem in a round-about way. The examples are inspired by staging calculi. At the end we describe the real development, which gives perhaps the first formal proof of type preservation of primitive reductions in an expressive staged calculus with escapes, run and cross-staged persistence. The type-preservation proof used both of our solutions and required two strengthening lemmas. Throughout we use Twelf – properly: we use the higher-order abstract syntax (HOAS) for higher-order terms, without ever resorting to concrete syntax for “variables”. The complete code is available at <http://okmij.org/ftp/Computation/staging/> .

The simplest example requiring strengthening

Perhaps the simplest example to illustrate the need of strengthening is based on lambda-calculus with terms marked by either 1 or 0. The challenge is to implement a function that converts terms marked by 1 into those marked by 0 – and show its totality.

Our calculus is elementary: we define two marks, 0 and 1

mark: type.
0: mark.
1: mark.

and marked terms, built of applications and abstractions:

exp: mark -> type.              %name exp E.
a: exp M -> exp M -> exp M.
l: (exp M -> exp M) -> exp M.

Here is a sample term, marked with 1:

t1 : exp 1 = a (l [x] (l [y] (a x y))) (l [x] x).

(in Haskell notation, it is (\x -> \y -> x y) (\x -> x) ). The definition of exp makes it clear that all subterms of a marked term have the same mark.

Our goal is to write a transformation taking a term marked by 1 and producing a term marked by 0:

cp1: exp 1 -> exp 0 -> type.
%mode cp1 +E1 -E2.

It is almost like copying terms and hence straightforward:

cp1-a: cp1 (a E1 E2) (a E1' E2')
         <- cp1 E2 E2'
         <- cp1 E1 E1'.
cp1-l: cp1 (l E1) (l E1')
         <- ({x}{x'} cp1 x x' -> cp1 (E1 x) (E1' x')).
%block cp1-l-bl : block {x:exp 1} {x':exp 0} {D:cp1 x x'}.
%worlds (cp1-l-bl) (cp1 _ _).
%total {E1} (cp1 E1 _).  %% Does not pass!

The clause cp1-a inductively handles applications. To transform an abstraction, we assume a term x marked with 1, a term x' marked with 0, and assume that x' is the result of transforming x, see cp1 x x'. Under those assumptions, we transform the body of the abstraction, cp1 (E1 x) (E1' x'). The notation (E1' x') means that E1' is a higher-order term applied to x'. That is, E1' is of the type exp 0 -> exp 0. The block declaration cp1-l-bl lists our set of assumptions; the regular worlds declaration asserts that cp1 is performed given no assumptions, or one set assumption cp1-l-bl, or two sets of such assumptions (with the different x and x' across the sets), etc.

Our transformation procedure is obviously total: we can take any 1-marked term, and, in finite time, always deliver the corresponding 0-marked term. We wish to state this formally, hence the %total assertion. Twelf verifies it first by checking that the transformation is terminating. It then checks that all pattern-matching is exhaustive: we have not missed a case. Alas, the totality check fails and Twelf reports an error:

Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{E1:exp 1 -> exp 1} {E2:exp 1 -> exp 0 -> exp 0}
   |- {x:exp 1} {x':exp 0} cp1 x x' -> cp1 (E1 x) (E2 x x').

In the clause cp1-l, we have introduced three assumptions: x, x' and cp1 x x'. By writing (E1' x') we asked the Twelf system to “factor out” the dependence on x'. Implicitly we stated that the result of transforming (E1 x) depends only on x' but not on x or cp1 x x' (more formally, the independence is seen from the fact E1' is used outside of the scope of x introduced via the universal quantification {x} in cp1-l). Twelf can see that the assumption cp1 x x' cannot possibly enter the set of terms because the definition of the type family exp (with constructors a and l) shows that no term can contain anything of the type cp1. But terms may occur in terms, and so the result of transforming the body of the abstraction generally depends on both x and x'. We have not handled that general case, and so our transformation is not total.

Twelf’s complaint is quite insightful: (E1 x) is the body of the abstraction that includes some term x (“the variable”). We transform the body replacing all those occurrences of x with x' – and so the result should include only x' but no x. Thus Twelf demands the proof that we indeed replaced all those x with x'.

Upon consideration, we can see that the result of transforming (E1 x) cannot really depend on, or contain, x. After all, x is an expression marked by 1 and the result of transforming (E1 x) is an expression marked by 0. Any sub-expression of a marked expression is marked with the same mark. Alas, Twelf cannot see this proof by itself and we have to write it down explicitly. The reason Twelf cannot see that proof by itself is because Twelf tracks the dependencies (so-called subordination) using only the names of the type families (e.g., exp) but not their parameters (e.g., exp 0 or exp 1).

Astonishingly, the most trivial way of writing this independence proof works. We state that whenever a term marked by 0 appears to depend on a term marked by 1, it actually doesn’t. Or, constructively, we assert the following proposition

strength : (exp 1 -> exp 0) -> exp 0 -> type.
%mode strength +H -E.

For any implication exp 1 -> exp 0, we can always constructively produce exp 0. Here is the proof, the detailed procedure of producing that exp 0 term:

-: strength ([x] E) E.
-: strength ([x] (a (E1 x) (E2 x))) (a E1' E2')
   <- strength E1 E1'
   <- strength E2 E2'.
-: strength ([x] (l [x'] (E x' x))) (l E')
   <- {x':exp 0} strength (E x') (E' x').

The first clause handles the case when E patently does not contain anything of the type exp 1. The rest of the clauses do straightforward induction on terms; the last clause requires hypothetical reasoning to examine the body of the abstraction, and for that we introduce the assumption x' of the type exp 0. Perhaps it is because of that hypothetical reasoning that Twelf cannot see the strengthening property on its own. We assert that so defined procedure is total, i.e., it is a constructive proof of the strength proposition:

%block strength-bl : block {x':exp 0}.
%worlds (strength-bl | cp2-l-bl) (strength _ _).
%covers strength +H -E.
%total {E} (strength E _).

The label cp2-l-bl describes the set of assumptions of the improved cp2 procedure below (in the actual code, it is defined in a forward declaration). Twelf has verified the totality of strength, and so we can use it to write the improved transformation procedure, cp2:

cp2: exp 1 -> exp 0 -> type.
%mode cp2 +E1 -E2.
cp2-a: cp2 (a E1 E2) (a E1' E2')
         <- cp2 E2 E2'
         <- cp2 E1 E1'.
cp2-l: cp2 (l E1) E1''
         <- ({x}{x'} cp2 x x' -> cp2 (E1 x) (E1' x x'))
         <- strength ([x] (l (E1' x))) E1''.
%block cp2-l-bl : block {x:exp 1} {x':exp 0} {d:cp2 x x'}.
%worlds (cp2-l-bl) (cp2 _ _).
%total {E1} (cp2 E1 _).

The only difference from cp1 is in the clause cp2-l: by writing (E1' x x') we state that the result of transforming the body of the abstraction may depend not only on x' but also on x. We build the transformed abstraction under that additional assumption: ([x:exp 1] (l (E1' x))). Using strengthening, we then prove that (l (E1' x)) does not actually depend on x. Now the totality assertion succeeds: cp2 is the total transformation of 1-marked terms.

The complete code is available at <http://okmij.org/ftp/Computation/staging/strengthen.elf>

A more realistic example: type preservation

We have encountered the problem of strengthening in staged calculi, e.g., when proving type preservation. We outline the problem and the solution; please see the complete code <http://okmij.org/ftp/Computation/staging/translation-problem.elf> for the full details.

We introduce a simple staged language, where each expression is annotated with the numeric stage label A. The language has three forms of expressions: natural literals, addition, and fix (i.e., recursive functions).

exp : nat -> type.              %name exp E.
n : nat -> exp A.               %prefix 110 n.
+ : exp A -> exp A -> exp A.    %infix left 154 +.
fix : (exp A -> exp A) -> exp A.

We introduce a trivial type system with only one type, int, and the equally simple type-checking relation of E T:

of : exp A -> tp -> type.       %name of Q.
%mode of +E *T.

Please see the code for details. As in the previous section we write the procedure to downgrade the level of an expression

downgrade : exp (1 N) -> exp N -> type.
%mode downgrade +E1 -E2.

We are not that interested in proving downgrade is total. Rather, we wish to prove a meta-theorem that downgrade is type preserving: if the original expression was typed, the downgraded expression shall be typed too. We state that property as a constructive proposition:

dn-pres : downgrade E1 E2 -> of E1 T -> of E2 T -> type.
%mode dn-pres +PD +PTI -PTO.

That is, given any downgradeable expression E1 and its type derivation of E1 T (the evidence that E1 is typed), we produce the typing derivation for the corresponding downgraded expression E2. The most interesting case is the following:

- : dn-pres (dn-f PEH) (of-f PTH) PTH''
        <- ({e:exp (1 A)} 
            {pt:of e int}
            {e':exp A}
            {dn:downgrade e e'}
            {pt':of e' int}
            dn-pres dn pt pt' ->
            dn-pres (PEH e e' dn) (PTH e pt) (PTH' e pt e' pt'))
        <- strength-of ([e] [pt] (of-f  (PTH' e pt))) PTH''.

Here, dn-f PEH of the type downgrade (fix E1) (fix E2) is the derivation of downgrading (fix E1) into (fix E2). We assume a term e of the type exp (1 A), and further assume it is typed (the assumption pt:of e int). Likewise we assume a typed term e' that is the result of downgrading e. Finally, we assume that the downgrading from e to e' was type preserving. Under those assumptions, we obtain the type derivation of the body of the downgraded fix, by inductively invoking dn-pres. The resulting type derivation (PTH' e pt e' pt') generally depends not only on the assumption e' and its typeability pt' – but also on e and pt, which are in scope and could in principle occur in type derivations. We must thus prove that we can remove the latter dependency. Again, the formal statement of that proposition is surprisingly simple:

strength-of : ({e:exp (1 N)} of e T -> of (E:exp N) T) -> 
              of (E:exp N) T -> type.
%mode strength-of +H -P.

We assert that the typing derivation of E T for an expression E at the level N cannot depend on any N+1-level expression e and the typing derivation of the latter. Our proof is again constructive: from the corresponding implication we produce its conclusion without assuming the hypotheses. The complete code has all details.

Other examples

The need for strengthening does occur (although not frequently) in other circumstances. Here are the example from Twelf distribution. One is “Representation of Mini-ML expressions in Mini-ML*” by David Swasey, file exercises/opt-eval/opt-rep1.elf. It defines a transformation from one higher-order language to another. Proving meta-theoretical properties of that translation (totality, type preservation, etc) requires strengthening.

The second, indirect solution

The second solution to strengthening is, too, trivial, albeit round-about. We use the same problem as in Section 1: in lambda-calculus whose terms are marked with 0 or 1, implement a function that converts terms marked by 1 into those marked by 0 – and show its totality.

Rather than transforming exp 1 to exp 0 directly, we introduce terms expi M isomorphic to exp M, turn exp 1 to expi 1 and then transform expi 1 to exp 0. The advantage is that terms exp M cannot appear in expi M and vice versa, so exp M cannot depend on assumptions of the type {x:expi M} and vice versa. We avoid strengthening altogether.

Here are a few details: we define intermediary, also marked, terms

expi: mark -> type.             %name expi _Ei.
a2: expi M -> expi M -> expi M.
l2: (expi M -> expi M) -> expi M.

that are clearly isomorphic to the terms exp M of the original calculus. We can state the isomorphism formally; however, we only need one direction of it: given any term exp M, we can always obtain the corresponding expi M:

exp-expi: exp M -> expi M -> type.
%mode exp-expi +E1 -E2.

We show only the more complex case of transforming abstractions:

-: exp-expi (l E1) (l2 E1')
   <- {e:exp M} {e2:expi M}
      exp-expi e e2 ->
      exp-expi (E1 e) (E1' e2).
%block bl-exp-expi : 
       some {M:mark} 
       block {e:exp M} {e2:expi M} {t:exp-expi e e2}.
%worlds (bl-exp-expi) (exp-expi _ _).
%total {E} (exp-expi E _).

Now Twelf verifies the totality assertion without any complaints that E1' could depend (that is, include) the assumption e, which is also present in the LF context. Twelf now sees that E1' cannot include e. Compared to Section 1, converting an expression of the type exp M gives us the term of the type expi M. The latter terms can only be constructed by l2 and a2; neither constructor can take any argument of the type exp M or contain exp M elsewhere. Strengthening is no longer needed.

The label-changing transformation now takes expi 1 rather than exp 1 as the source a term:

cpaux: expi 1 -> exp 0 -> type.
%mode cpaux +E1 -E2.

Here is the interesting case

cpa-l: cpaux (l2 E1) (l E1')
       <- ({x:expi 1}{x':exp 0} cpaux x x' -> cpaux (E1 x) (E1' x')).
%block bl-cpaux : block {x:expi 1} {x':exp 0} {t:cpaux x x'}.
%worlds (bl-cpaux) (cpaux _ _).
%total {E1} (cpaux E1 _).

Again, Twelf accepts the totality assertion without complaint because clearly no term of the type expi M may appear in the term exp M – in fact, expi was not even defined when exp was introduced. Thus (E1' x') cannot depend on x.

What remains is a mere composition of the two above transformations

cpi: exp 1 -> exp 0 -> type.
%mode cpi +E1 -E2.
-: cpi E1 E2 <- exp-expi E1 E1' <- cpaux E1' E2.
%worlds () (cpi _ _).
%total {} (cpi _ _).

The desired transformation now includes two steps: transforming the source expression into the isomorphic form, and changing the mark of the latter. Albeit indirect, the solution avoids strengthening altogether.

A real example: type-preservation in an expressive staged calculus

The file <http://okmij.org/ftp/Computation/staging/lambda-am1.elf> is the formalization of the two-level call-by-value calculus lambda-a1v based on lambda-a of Taha and Nielsen’s “Environment Classifiers” (POPL03). The calculus supports manipulation and splicing in of the open code, running of the closed code, and cross-staged persistence. The lambda-a1v calculus has been introduced in the paper Closing the Stage: From Staged Code to Typed Closures written with Yukiyoshi Kameyama and Chung-chieh Shan (PEPM08).

The file includes (maybe the first) formal proof that any non-value term can be decomposed into a pre-value and the context. This is quite challenging given that the calculus supports the evaluation under lambda and so the context can cross the arbitrary number of dependent binders: variable binders include classifiers that must be bound, too, at that point.

In our staged calculus, all terms are marked by their stage, present and future. This is quite like the examples in the earlier Sections. There is also an operation to demote a term, which takes a future-stage-marked term and changes its mark so the term can be evaluated at the present stage. Demotion is how a future-stage computation can be run. Demotion rebuilds a term as it traverses it, changing the marks along the way. The only special case is handling a cross-staged persistent (CSP) value. The latter is a present-stage expression that was “lifted” to the future stage, i.e., was encapsulated unevaluated. The demotion operation merely removes the encapsulation, splicing CSP into the demoted code.

The type-preservation proof is at the end of the development. The most complex part is proving that demotion is type preserving, in particular, that demoting an abstraction (l [x:exp (1q AL)] Body) from the future stage (marked by (1q AL)) to the present, marked as qt, stage yielding (l [x':exp qt] Body') is type preserving. As in the simpler examples earlier, the proof proceeds by introducing assumptions {x:exp (1q AL)}, {x':exp qt} and that x' is the result of demoting x. The challenge is to prove that Body' does not actually depend on x. That is no longer as simple as before: a future-stage expression exp (1q AL) could actually occur in the demoted expression – because of CSP. For example, consider the following future-stage term

(l [x:exp (1q AL)] (csp (AL > x)))

where AL > x is future-stage-x marked by classifier AL (in the PEPM08 paper, we write (l [x^AL] %(<x>^AL)). An attempt to run such future-stage computations does not type in MetaOCaml; accordingly, the lambda-a1v calculus rejects such expressions as mis-typed, due to a special typing rule of CSP. Our preservation proof must take into account that the demoted expression is typed and so possible CSPs are restricted in form. Only then strengthening can be proven.

In our proof, we had to use both approaches to proving strengthening described in this article. We had to prove a direct strengthening lemma

strength-tp-dem : csp-ok1 E ->
                  ({x:exp (1q AL)} of x TV -> of E T) -> 
                  of E T -> type.
%mode strength-tp-dem +CS +H -P.

asserting that the typing of a present-stage expression (of (E:exp qt) T) cannot depend on a future-stage expression exp (1q AL) and the latter’s typing derivation (of (_:exp (1q AL)) T) – provided that E is the result of a demotion. We also use the indirect approach and introduce a CSP restriction predicate csp-ok1 isomorphic to the predicate csp-ok. The latter may occur in typing derivations but the former may not. Finally, we had to prove the strengthening lemma for csp-ok1.

Continuation fest

Please consider submitting a paper to this year’s International Conference on Functional Programming (ICFP) and Conference on Generative Programming and Component Engineering (GPCE). The respective deadlines are April 2 and May 12–19. Both conferences solicit experience reports in addition to regular papers. As you might expect, ICFP also solicits functional pearls—“elegant, instructive, and fun essays on functional programming”.

Less formal is a Continuation Fest that a bunch of us are organizing. If you can be in Tokyo on April 13, please consider participating! Talk proposals are due on March 31. This event is scheduled on the day before the Symposium on Functional and Logic Programming (FLOPS); you can travel from Tokyo to Ise on the morning of April 14.

Continuations are used, and constantly re-discovered, in web programming, logic, event-based concurrency, linguistics, transactional systems, optimization, program generation and verification. Programming language systems … are (re-)implementing continuations, generators, iterators and related control structures. Continuations are also being studied for their own sake.

We call for an informal gathering of people working in all these areas—language designers, users, and researchers who study or use continuations in academic or practical work or as a hobby. The goal is to exchange ideas, terminology, new results, experience reports, works in progress, open problems, and friendly feedback—as well as meet each other and strengthen the community.

We plan a combination of 7–8 broadly accessible talks and 1–2 invited talks, with plenty of breaks for socializing and informal conversations. An evening event is planned. Participants are invited to submit working notes, source files, and abstracts for distribution to the attendees, but as the workshop has no formal proceedings, contributions may still be submitted for publication elsewhere.

We solicit talk proposals, about 2 paragraphs long … The topics of interest include, but are not at all limited to:

• descriptions of uses of continuations in program generation, linguistics, proof theory, model checking,
• system demonstrations
• libraries using continuations, such as generators
• verifying programs that use continuations explicitly or implicitly (exceptions, concurrency, backtracking)
• type systems of continuations and their formalizations
• open problems

It seems appropriate to translate “Continuation Fest” into Japanese as “継続祭”. As for Mandarin Chinese, how about “續繼節” (“续继节”)? It was 穆信成 Shin-Cheng Mu who taught me to noun a bisyllabic Chinese verb, such as “繼續” (“继续”, “continue”), by exchanging the two syllables.

Your point of view

Snappy quotes of the day

“Perhaps, as many neuroscientists believe, the brain escapes the limitations and requirements that computer scientists believe are imposed by mathematics, logic, and physics.”

“Such an architecture is prodigally wasteful of material resources. It is nakedly exposed to combinatorial explosions that lurk behind every tree in the computational forest.”

—Gallistel, C. R. 2008. Learning and representation. In Learning and memory: A comprehensive reference, behavioral approaches, ed. Randolf Menzel and John Byrne. Amsterdam: Elsevier Science.

Are associative theories of learning the Viet Nam of cognitive science?

Administrivia

The notion of administrative reductions comes up all over the place, even though the term is usually used when discussing continuation-passing style. Briefly, an administrative reduction is a trivial rewriting step that simplifies an expression that is easy to crank out into an equivalent expression that is natural to take in.

Here is an example from modal logic. Kripke figured out that we can translate modal logic formulas systematically into predicate logic by adding an extra “world” argument x to every proposition. For instance, whereas the formula S∧T (“snow is white and trains are late”) translates to the formula S(x)∧T(x) (“snow is white at world x and trains are late at world x”), the formula S∧◻T (“snow is white and it is necessary that trains are late”) translates to the formula

S(x) ∧ ∀y. R(x,y) → T(y).

I follow the convention that all operators associate to the right, so the above is short for S(x) ∧ (∀y. (R(x,y) → T(y))) (“snow is white at world x and, for every world y accessible from x, trains are late at y”). More formally, we can define a function f that maps a modal formula and a world variable to a predicate formula, by induction on the modal formula:

1. f(A,w) = A(w), if A is an atomic proposition.
2. f(φ∧ψ,w) = f(φ,w) ∧ f(ψ,w).
3. f(◻φ,w) = ∀wʹ. R(w,wʹ) → f(φ,wʹ), if w and wʹ are distinct world variables.

Because f takes a world variable for a second argument (so the metavariables w and wʹ stand for world variables), this definition can be a bit tricky to write and understand. For one thing, because the last case above does not pin down the choice of wʹ, the function f is only defined up to α-equivalence among predicate formulas.

We can avoid the second argument to f if we define the translation a bit differently. Let us translate S∧◻T to

S(x) ∧ ∀y. R(x,y) → ∃x. (x=y) ∧ T(x)

or

S(x) ∧ ∀y. R(x,y) → ∀x. (x=y) → T(x)

instead (it doesn’t matter which). This alternative translation is more verbose and requires equality in the target language, but it is more straightforward to define inductively:

1. g(A) = A(x), if A is an atomic proposition.
2. g(φ∧ψ) = g(φ) ∧ g(ψ).
3. g(◻φ) = ∀y. R(x,y) → ∃x. (x=y) ∧ g(φ).

To turn the output of g, which is easier to crank out, into the output of f, which is more natural to take in, we can define a second pass of processing that rewrites the use of equality away. Such a rewriting step is called an administrative reduction because it simplifies an expression into an equivalent expression in a trivial, bureaucratic way.

In general, when we build an expression generator (especially a translator), we can often choose whether to express the same meaning using facilities in the metalanguage or in the object language. Often, the generated expression is easier to understand if we use the metalanguage’s facilities, but the generation process is easier to understand if we use the object language’s facilities. Hence, the latter strategy calls for a subsequent pass of administrative reductions. The two passes of this pipeline can be merged to form a so-called one-pass translation by anticipating where administrative reductions take place.

Another example of an administrative reduction lies in flow chart connectors. We can draw a big flow chart either using a large piece of paper (the metalanguage) or using connector symbols (the object language). Having drawn a big flow chart using connector symbols, we can use scissors and glue (administrative reductions) to simplify it into a connector-free flow chart on a large piece of paper.

Yet another example: When you choose “Save as … MacWrite” in Microsoft Word, Word pipes your document in Rich Text Format to an export converter module, which in turn produces a MacWrite file. As I recall faintly (I probably have the details wrong—is it MacWrite or some other format?), the beginning of a MacWrite file must contain some kind of a count, which unfortunately the converter cannot determine until it reaches the end of its RTF input. Yet, the MacWrite converter manages to process its input and produce its output sequentially without buffering up anything, using the following hack. The MacWrite format has a “fast save” feature, which allows a document to be expressed as an old version followed by a series of patches (differences) to bring it up to date. The converter writes out a dummy count at the beginning, then appends a patch to fix the count at the end.

As far as I know, the term “administrative” was first used by Gordon Plotkin in his seminal study of continuation-passing-style translations. For example, one translation Plotkin defines (the call-by-value one) maps the term λx.xx to the term

λκ. κ λx. λκ. (λκ.κx) λα. (λκ.κx) λβ. αβκ

instead of the simpler (β-reduced) and equivalent term

λκ. κ λx. λκ. xxκ.

Plotkin introduced the term inside quotation marks, suggesting that he coined it.

Speaking of modal logic, how about this for a disappointing subtitle: “The neuroscience of belief: effects of placebo treatments on brain & body”? Reading the part before the colon, I expected to find the modal box for knowledge or belief expressed in the brain as a homunculus of a mind, tragically sandboxed from accessing variables in outer scopes.

Teaching models

In the coming semester, I get to teach “Computational Modeling” again. This new course is part of our interdisciplinary graduate training program in perceptual science. The aim of “Computational Modeling” and its quasi-prerequisite “Computational Thinking” is to get first-year graduate students in fields such as psychology, linguistics, anthropology, biomedical engineering, and philosophy and their peers in computer science to collaborate using computational tools, concepts, and ways of thinking.

The main point of the course is well put by Abelson and Sussman in their preface to SICP:

a computer language is not just a way of getting a computer to perform operations but rather that it is a novel formal medium for expressing ideas about methodology. Thus, programs must be written for people to read, and only incidentally for machines to execute.

Call me a computer scientist, but I think to really understand something is to be able to write a program to simulate it. My notion of programs is pretty broad, so this claim is not as outlandish as it might first seem, and maybe I’m just a funny mathematician. Nevertheless, the claim emphasizes the practical value of executable specifications: explanations that are formal enough to run yet grounded enough to share, concrete enough to see yet abstract enough to generalize, controlled enough to replicate yet flexible enough to change. You can’t be right if you can’t be wrong.

The goal of this class is for scientists to talk across disciplines. The premise is that computational models can help us talk. The theme of perception and cognition makes the models recursive.

Leaving the slogans aside, what am I actually going to teach? The relevant skills come down simply to reading, writing, and arithmetic, if in a generalized sense: they are to identify essences, separate components, deduce consequences, and communicate arguments. But how to teach these skills for executable specifications? For instance, how well do design recipes for algebraic data types apply to models of perception? I don’t know of a computer-science textbook that is tailored for cognitive science; please tell me if I should.

Here are some questions whose variants I hope will be asked.

• What to explain? What do people say that irks you, and why?
• What doesn’t make sense? What can I ask about?
• How does a game illustrate, with interaction and inspection?
• What are the types of the props, the behaviors, the right or wrong explanations?
• Where are the parts? Which should we refine? Which can we hide?
• How to not repeat ourselves?

Here are some examples whose like I hope will come up; I don’t have enough.

• SimCity, Monopoly, Settlers of Catan, Dungeons and Dragons.
• Optical perspective and graphics to model vision.
• Constraint search to model interpreting sentences and line drawings.
• Probabilities and utilities to model beliefs and desires.
• Processing rule languages for computational chemistry and systems biology.

In the end, of course, the students themselves must originate the questions and the examples, the writings (for sure) and the readings (I hope). Each domain is a great opportunity for the collaborators themselves to develop a toolbox and a vocabulary, be it a set of of MATLAB scripts or program transformations. My job is to coordinate the activities and the space. To this community of learning, I bring executability and polymorphism. And apprehension.

Restaurant recommendations

I’ve been buffering up these restaurant recommendations for a while.

Sampurna (Indonesian)

• Singel 498, 1017 AX Amsterdam, +31 20 625 32 64

Piquant (Indian fusion)

• 349A George St, New Brunswick NJ 08901, +1 732 246 2468

Spices: Szechuan Trenz 辣妹子 (Taiwanese Szechuan)

1. 294 8th Ave, San Francisco CA 94118, +1 415 752 8884
2. 291 6th Ave, San Francisco CA 94118, +1 415 752 8885
3. 369 12th St, Oakland CA 94620, +1 510 625 8889

Lahore Karahi (Pakistani)

• 612 OFarrell St, San Francisco CA 94109, +1 415 567 8603

Cha-ya 茶屋 (Japanese vegetarian)

• 762 Valencia St, San Francisco CA 94110, +1 415 252 7825
• 1686 Shattuck Ave, Berkeley CA 94709, +1 510 981 1213

Maxfield’s House of Caffeine (coffee shop and wifi)

• 398 Dolores St, San Francisco CA 94110

At this coffee shop, Oleg and I enjoyed a drawing of All Over Coffee by Paul Madonna:

Takahashi method for Beamer の高橋メソッド：高橋流簡報法

Surprisingly, I couldn’t find support on the Web for the Takahashi method of slide presentations in the Beamer class. So, I wrote it. This LaTeX package provides a single command \takahashi, documented at the beginning of the file. Some usage examples appear at the end of the file.

Update: To demonstrate, this source file produces this PDF output. For further testing, that source file produces that PDF output.

網上竟然找不到用 Beamer 格式製作高橋流簡報的方法，所以我就自己寫了。本 LaTeX 套件只提供一個命令 \takahashi。用法請見檔頭；用例請見檔尾。

追加：為示範起見，這個原始檔造成這樣的 PDF 輸出。更進一步測試，那個原始檔造成那樣的 PDF 輸出。

Hamming’s problem

To demonstrate his “discipline of programming”, Dijkstra discusses “an exercise attributed to R. W. Hamming”:

To generate in increasing order the sequence 1, 2, 3, 4, 5, 6, 8, 9, 10, 12, … of all numbers divisible by no primes other than 2, 3, or 5.

Here’s Dijkstra’s solution in Haskell:

hamming = 1 : foldl1 merge [ map (n*) hamming | n <- [2,3,5] ]

merge (x:xs) (y:ys) = case compare x y of
    LT -> x : merge xs (y:ys)
    GT -> y : merge (x:xs) ys
    EQ -> x : merge xs ys

Even in Haskell, I recommend Dijkstra’s two exercises.

This problem was later used to illustrate “perpetual processes” (i.e., the lazy evaluation of infinite terms) in logic programming:

• Keith L. Clark and Steve Gregory. 1981. A relational language for parallel programming. In FPCA ‘81: Proceedings of the 1981 conference on functional programming languages and computer architecture, 171–178. ACM Press.

• Åke Hansson, Seif Haridi, and Sten-Åke Tärnlund. 1982. Properties of a logic programming language. In Logic programming, ed. Keith L. Clark and Sten-Åke Tärnlund, 267–280. Academic Press.

• John Wylie Lloyd. 1987. Foundations of logic programming. Second, extended edition. Springer. (page 189)

Beyond amsmath

The \intertext command in the amsmath package for LaTeX is useful for interjecting text between two aligned rows of displayed math. However, it puts too much space around the text: compared to the usual vertical spacing around displayed math, it leaves \jot too much, both above and below. (\jot is 3 pt or more.) To fix this problem, load my amsmath1 package with the intertext option.

While investigating this problem, Dylan and I discovered the mathtools and nccmath packages, which add many useful macros to amsmath. Unfortunately, even though both packages extend \intertext, neither package really removes the extra \jot space.

The the

To search for duplicate words in a manuscript (such as “the the”) in Vim, look for this pattern.

\m\c\<\\\@<!\([a-z]\%(['a-z]\+[a-z]\)\?\)\_W\+\\\@<!\1\>

用 Vim 搜尋上列樣式，可以抓到文稿裡諸如 “the the” 一類的重複詞。

There’s no type class like Show type class

(Sing to the tune of “There’s no business like show business”)

There’s no type class like Show type class
Like no type class I know
Everything about it is deriving
Everything the standard talks about
No where could you start evaluating
When you aren’t writing to standard-out

There’s no instance like Show instance
They scale when programs grow
Yesterday they hired you at the software firm
That night you opened and closed the term
Nothing ever can go wrong, the types confirm
Let’s go on with the show

The spaces, the brackets, the infix with ease
The monad that lifts you when you’re down
The state threads, the functions, the infinite trees
The boilerplate that makes Ralf Lämmel frown
To simulate a quantified constraint
To wish that superclass of Num it ain’t

There’s no type class like Show type class
If you tell me it’s so
Polymorphic recursion’s so thrilling
Overloading gives you such a blast
Smiling as you watch the console filling
And see your functions composing fast

There’s no instance like Show instance
They scale when programs grow
Even with some data that you know will fold
The type checker may find that you’re too bold
Still you wouldn’t wait till run-time to be told
Let’s go on with the show
Let’s go on with the show

(Thanks to Dylan Thurston, the original lyrics online, and RhymeZone.)

Form-ing web continuations, or asking several questions at once oleg at pobox.com

In the ICFP 2000 paper The influence of browsers on evaluators or, continuations to program web servers Christian Queinnec offered a compelling view of web interactions as browsers’ operating on continuations of server computations. He exhorted web application programmers to use first-class continuations to write interactive (web) programs in direct style. “Instead of thinking in terms of state and transitions from page to page, we propose an alternative view where a program is suspended and resumed, continuations automatically reifying the state of the computation.”

The popular introductory example of a dynamic web page asking for two numbers and showing their difference can be programmed essentially as get_int "n1" - get_int "n2". The library function get_int should make a web form and embed into it some representation of the current continuation. The continuation is resumed when the form is submitted. The above web program appears conventional (with inputs seemingly coming from a “file”) relieving the programmer from worrying about page transitions and state maintenance. This style also makes dynamic pages do the right thing when the user pushes the “Back” or “Forward” buttons one or more times, or bookmarks a form and comes back to it later.

Queinnec’s paper proved influential and has inspired the development of many continuation-based servers: Yahoo’s query: continuation-based web servers

The original approach was restricted in that the answers were solicited one-by-one. When running our example get_int "n1" - get_int "n2", the server sends a web form asking the user for the first number. After that form is submitted, the server sends the next form asking for the second number. Upon submission of the latter, the web page with the answer is generated. We observe that the two questions are independent and could have been asked together. The notable benefit of bundling the questions is reducing the traffic between the server and the browser and resources for storing continuations. Most of the forms on the web typically contain more than one question.

This message presents a uniform mechanism for flexible and automatic bundling of questions into forms. We still write our server code essentially as get_int "n1" - get_int "n2". Our library automatically groups the questions into one web form. The library takes care of parsing multiple responses, matching them with the questions and validating the replies. Should some inputs turn invalid, the library automatically generates an error form with the questions, the given answers and the corresponding error messages, asking the user to edit the answers and re-submit the form. The error handling is automatic and transparent for the servlet.

Our mechanism relies on call-by-need: the library delays asking questions until their answers are demanded. When a question really needs to be answered, the library collects all outstanding questions, makes a web form and sends it to the client as the response of the server computation so far. When the form is submitted and the computation resumes, the library parses all the replies and stores them for future answer demands. Since our particular implementation language (OCaml) is strict, call-by-need is not automatic: The programmer does have to write Lazy.force explicitly. The type system ensures that the programmer does not forget the forcing, thus making the data dependencies apparent. OCaml type checker will tell the programmer the points where a value is demanded. The programmer should insert Lazy.force there – or at some earlier point, if the programmer so chooses. If the programmer forces the answer after asking each question, we get back the sequential behavior of asking questions one-by-one.

Our framework may be regarded as a different mode of composing questions: not serially (one-after-another) but in parallel. A follow-up message will draw the correspondence with monads (which embody sequential composition) and arrows.

Note on examples

To fully demonstrate our approach we need a web browser and a continuation web server. Although many such servers exist, they are not fully compatible, may require special privileges to install and may conflict with the web server already installed on readers’ computers. That makes it impractical to demonstrate any real servlets. Therefore, we emulate web interactions by those at the OCaml top level prompt. To invoke a server computation, rather than entering a URL into a web browser, we type the corresponding expression at the prompt. When the computation finishes, the top level prints its result (in the “natural” rather than HTML format). The result, which may be a “web form”, can be “bookmarked” (that is, bound to a top-level variable) and then reinvoked none or many times. Our emulation thus captures all attributes of web interactions: taking turns, interactivity, back-and-forth navigation, bookmarking.

The complete OCaml code for this article is available at http://okmij.org/ftp/ML/ask-by-need.ml

Warm-up: asking questions one-by-one

As a warm-up and the illustration of our “web interactions” and for contrast with the next section, we reproduce here the standard example of using continuations for web programming: we ask the user for two integers n1 and n2 and send the “page” showing their difference. Each question comes on its own “form”. This is essentially the example from the Queinnec paper (only he used currency conversion).

First we define the type of “web pages” shown to the user

type 'a req = 
  | Done of 'a
  | Req of string * (string -> 'a req)

One should read the value Done x as if it were a web page showing the result x. If the “server” computation gave the result Req str k, imagine it were a web form containing the string str, with the continuation k embedded as a hidden form parameter. We should use the procedure answer req reply_str to “submit” such a form.

The servlet library is so simple that we can show the whole code.

let topp = new_prompt ()
let run th = push_prompt topp th    (* how to run the servlet *)

The servlet calls exit v to send the “final web page” with the computed answer:

let exit v = abort topp (Done v);;

The following is a procedure to ask a question. The second argument is the conversion function, from string to the desired reply type. The function may raise an exception Scanf.Scan_failure if the conversion fails. The library then repeats the question.

let question (str:string) cnv =
  let rec loop errstr = 
    let ans = shift topp (fun k -> Req ((errstr ^ str),k)) in
    try cnv ans with Scanf.Scan_failure e -> loop e
  in loop ""

A sample conversion function, to convert user’s answer to an int:

let read_int (str: string) : int = Scanf.sscanf str "%i" (fun x -> x)

If req is a “web form” sent by a “server computation”, we should use answer req reply_str to “submit” the form with our reply.

let answer (Req (_,k)) reply_str = k reply_str;;

Here is the servlet itself, asking for two numbers and computing their difference:

let test1 () =
  let n1 = question "Enter 1st number" read_int in
  let n2 = question "Enter 2nd number" read_int in
  exit (n1 - n2);;

Let us show a sample interaction (the replies from the server are indented)

We type the test1 “URL” and get the form in reply

let it =  run test1
  val it : int req = Req ("Enter 1st number", <fun>)

let bookmark1 = it;;

let it = answer it "456";;  (* Submit the web form, get another one *)
  val it : int req = Req ("Enter 2nd number", <fun>)

let it = answer it "123";;  (* Submit it too, get the answer *)
  val it : int req = Done 333

let it = answer bookmark1 "111";; (* Go back to bookmarked form 1 *)
  val it : int req = Req ("Enter 2nd number", <fun>)

let it = answer it "xyz";;   (* If the answer is unacceptable, we are *)
                             (* asked to repeat it *)
  val it : int req =
    Req ("scanf: bad input at char number 1: xEnter 2nd number", <fun>)

let it = answer it "10";;
  val it : int req = Done 101

Asking several questions at once: ask-by-need

Let us now show the code that uses the extended servlet library, which asks questions lazily. First we reproduce the old sequential behavior: we force the answer right after asking a question:

let test21 () =
  let n1 = Lazy.force (question "Enter 1st number" read_int) in
  let n2 = Lazy.force (question "Enter 2nd number" read_int) in
  exit (n1 - n2);;

Not surprisingly, the servlet test21 behaves exactly as test1 above.

We now demonstrate the asking several questions at once. We insert Lazy.force only where the typechecker tells us to, but not earlier. We emulate call-by-need.

let test2 () =
  let n1 = question "Enter 1st number" read_int in
  let n2 = question "Enter 2nd number" read_int in
  exit (Lazy.force n1 - Lazy.force n2);;

If we “enter the URL”, we see the form with two questions

let bm2 = run (fun () -> topqq test2);;
  val bm2 : int req =
    Req
     ("Enter 2nd number: ; Enter 1st number: ; 
       Needed 2 answers. Separate with & character",
   <fun>)

let it = answer bm2 "xxx";;
  val it : int req =
    Req
     ("incorrect number of ansEnter 2nd number: ; Enter 1st number: ;
       Needed 2 answers. Separate with & character",
   <fun>)

Below, both numbers failed validation, and so two error messages are given:

let it = answer it "xxx&aaa";;
  val it : int req =
    Req
     ("Enter 2nd number: scanf: bad input at char number 1: x in xxx; 
       Enter 1st number: scanf: bad input at char number 1: a in aaa; 
       Needed 2 answers. Separate with & character",
   <fun>)

If one number was acceptable, we still include it into the error form:

let it = answer it "xxx&123";;
  val it : int req =
    Req
     ("Enter 2nd number: scanf: bad input at char number 1: x in xxx; 
       Enter 1st number: 123; 
       Needed 2 answers. Separate with & character",
   <fun>)

Finally we give an acceptable answer, and the servlet may proceed:

let it = answer it "456&123";;
  val it : int req = Done (-333)

The new servlet library is the extension of the above code. To keep track of outstanding questions and not-yet consumed replies, we maintain the queue of qq values, identified by qid.

type qid = int;;
type qq = {qq_str    : string;         (* question string *)
           qq_answer : string option;  (* received answer, if any *)
           qq_id     : qid;
           qq_validate : string -> string option}

The following data type defines the protocol within the library, between the lower-level and the QnA supervisor. The lower-level may submit a question, receiving qid. The lower-level may ask the supervisor to provide the answer to the question identified by qid.

type qreq = 
  | QReq of string * (string -> string option) * (qid -> qreq)
  | QRes of qid    * (string -> qreq)

We re-define the question function, keeping its interface. This function no longer sends any form to the user. Rather, we submit the question to the QnA supervisor and make the promise to resolve the received qid into the real answer.

let question (str:string) cnv =
  let qq_validate = 
    fun str -> try cnv str; None with Scanf.Scan_failure e -> Some e in
  let qid = shift qp (fun k -> QReq (str, qq_validate, k)) in
  lazy (cnv (shift qp (fun k -> QRes (qid,k))))

The URL given earlier contains the complete code.