fixedpoint.jp - call/cc in R6RS




call/cc in R6RS

先月に引き続き R6RS の詳細を調べています。ただ英文を眺めているだけでは理解が進まないので、具体的なコード1つ1つがどのように振る舞うのか確認中です。

興味深い題材に call-with-current-continuation があります。過去に R5RS の call/cc の振る舞いで一見奇妙に思われることを William Clinger 氏が述べました: http://www.ccs.neu.edu/home/will/Personal/Nerdliness/callcc.txt

(call-with-current-continuation (lambda (c) (0 (c 1))))

上を評価すると「1を返す、もしくは、メモリを消費しつくす」という結果になるといい、その証明を載せています。これは R5RS の7章にある表示的意味論に基づくものです。

では、R6RS ではどうなるのでしょうか?

R6RS の補遺で与えられている形式的な意味論は操作的意味論ですので、それに従って検証してみました: callcc.txt

結論としては「1を返す」ということになります。その証明もぐっと分かりやすくなっており(項書換えのステップごとに前提条件が成立していることを確認するのは煩雑ですが)、操作的意味論を採用したメリットがうかがえます。

また、こういった検証の際に参考になるのが PLT Redex による意味論の参照実装です。公式ページで公開されており、例えば mzscheme で動作します。この実装のテストケースを編集することで、上の例もテストすることができます:

--- r6rs-plt-redex-model/r6rs-tests.scm.orig 2007-01-22 13:19:05.000000000 +0900
+++ r6rs-plt-redex-model/r6rs-tests.scm 2007-10-06 02:02:43.000000000 +0900
@@ -888,6 +888,8 @@
   (define dw-tests
     (list 
      
+     (make-r6test/v '(call/cc (lambda (c) (0 (c 1)))) 1)
+     
      ;; an infinite loop that produces a finite (circular) reduction graph
      (make-r6test
       '(store ()

© 2006,2007 Takeshi Abe