Racketの継続オペレータの意味論

[Racket](https://racket-lang.org/)にはRnRSで定義されている`call/cc`や`dynamic-wind`、例外処理、動的束縛に加えて、`shift`/`reset`、`control`/`prompt`等々といった種々の限定継続オペレータが定義されている。

これらの機能がどのように相互作用するのか理解していなかったので、[Adding Delimited and Composable Control to a Production Programming Environment](https://www.cs.utah.edu/plt/publications/icfp07-fyff.pdf)に書かれている意味論を読みながらメモをしていく。

# 構文と評価文脈

```
e ::= m
    | (wcm w m)

m ::= x
    | v
    | (e e ...)
    | (begin e e)
    | (% e e e)
    | (dw x e e)

v ::= (list v ...)
    | (λ (x ...) e)
    | (cont v E)
    | (comp E)
    | dynamic-wind
    | abort
    | current-marks
    | cons
    | u

u ::= call/cc
    | call/comp
    | call/cm

w ::= ((v v) ...)

E ::= W
    | W[(dw x e E e)]

W ::= M
    | (wcm w M)

M ::= []
    | (v ... W e ...)
    | (begin W e)
    | (% v W v)

D ::= []
    | E[(dw x e [] e)]
```

# 意味論
## プロンプト

`%` は `call-with-continuation-prompt` に相当する。 prompt-tag, proc, abort 時の handler を引数に取る。

### prompt-v

```
(% v1 v2 v3)
↝ v2
```

プロンプトの本体部分 `v2` が値になったら、それがプロンプト式全体の値になる。

## begin

RnRS の `begin`と同じ。

### begin-v

```
(begin v e1)
↝ e1
```

`begin` は左から右に評価し、最初の式が値になったら、その値を破棄し、次の式を評価する。

## dynamic-wind

RnRS の `dynamic-wind` とおおむね同じ。

### dw

```
(dynamic-wind (λ () e1) (λ () e2) (λ () e3))
↝ (begin e1 (dw x1 e1 e2 e3))
where x1 is fresh
```

`dynamic-wind` は `dw` という内部表現に変換する。

このとき、各 `dw` を識別するために、評価時に新しい識別子 `x1` を生成する。

また、 R[567]RSでは `dynamic-wind` の before/after thunk に継続を使って出入りした場合の挙動は未規定だが、この意味論では、 `begin` + `dw` に変換することで挙動を定めている。

### dw-v

```
(dw x e1 v1 e3)
↝ (begin e3 v1)
```

`dw` の本体部分が値 `v1` になったら、 `e3` を評価した上で、 `v1` を結果として返す。

## abort

`abort` は `abort-current-continuation` に相当する。 prompt-tag と v を受け取る（多値には未対応）。

### abort

```
(% v1 W2[(abort v1 v2)] v3)
↝ (v3 v2)
where W2 ≠ E[(% v1 E v)]
```

`abort` で指定したタグ `v1` を持つ直近のプロンプトまで脱出する。 `abort` に渡した値 `v2` は、プロンプトのハンドラ `v3` に渡る。外側のプロンプトは残らない。

where で指定した条件で、プロンプトが直近のものになることを保証している。

### abort-post

```
(dw x1 e1 W2[(abort v1 v2)] e2)
↝ (begin e2 (abort v1 v2))
```

`dynamic-wind` の本体部分で `abort` した場合は、after thunk を実行した上で `abort` 処理を再開する。

## composable continuation

### call/comp

`call/comp` は `call-with-composale-continuation` に相当する。 prompt-tag と proc を取る。

```
(% v2 E2[(wcm w1 (call/comp v1 v2))] v3)
↝ (% v2 E2[(wcm w1 (v1 (comp E2)))] v3)
where E2 ≠ E[(% v2 E v)]
```

`call/comp` を呼び出すと、指定したタグ `v1` を持つ直近のプロンプトまでの継続をcomposable continuationとして切り出す。プロンプトは継続に含まない。また、 `call/comp` の呼び出しに付加されたcontinuation markも切り出された継続には含まない。

### comp-pre

composable continuationの起動（`dw` 付き）。

```
((comp W1[(dw x e1 E2 e2)]) v1)
~> ⟦W1[(begin e1 (dw x1 e1 ((comp E2) v1) e2)]⟧_{wcm}
```

composable continuationのトップレベルが（`wcm`で包まれた）`dw`の場合、まずbefore thunkを実行し、 `dw` を外側に移したうえで、composable continuationを適用する。このとき、もとの継続に付加されていたcontinuation markは意味関数 `⟦・⟧_{wcm}` で外側の文脈に付加しなおす（後述）。

### comp

composable continuationの起動（`dw` なし）。

```
((comp W1) v1)
~> ⟦W1[v1]⟧_{wcm}
```

`dw` がない場合は、単純に `call/comp` で切り出した文脈に引数の値を挿入する。ただし、もとの継続に付加されていたcontinuation markは意味関数 `⟦・⟧_{wcm}` で外側の文脈に付加しなおす。

意味関数 `⟦・⟧_{wcm}` の定義は以下の通り。

```
⟦e1⟧_{wcm} = e1
where e1 ≠ (wcm w e)

⟦(wcm () e1)⟧_{wcm} = e1

⟦(wcm ((v1 v2) (v3 v4) ...) e1)⟧_{wcm} =
= (call/cm v1 v2 (λ () ⟦(wcm ((v3 v4) ...) e1)⟧_{wcm}))
```

意味関数 `⟦・⟧_{wcm}` は `wcm` を `call/cm` に置き換える。こうすることで、継続を起動した場所のcontinuation frameに破壊的にcontinuation markを追加する（[wcm-set](#wcm-set) や [wcm-add](#wcm-add) 規則を参照）。

このようにせず、継続の起動ごとにcontinuation frameを作成して、そこにcontinuation markを付加するようにすると、継続を末尾位置で起動した場合でもリソースを消費するようになってしまう。

## non-composable continuation

Racketの `call/cc` は full-continuation ではなく、指定されたプロンプトまでの継続を切り取る。 `call/comp` で切り出した継続とは起動時の意味論が異なる。 delimited/full continuation という関係ではなく、 composable/non-composable continuation の違いと見るのがよいと思う。

### call/cc

`call-with-current-continuation` 相当。 RnRS と異なり、 prompt-tag を取る。

```
(% v2 E2[(wcm w1 (call/cc v1 v2))] v3)
↝ (% v2 E2[(wcm w1 (v1 (cont v2 E2)))] v3)
where E2 ≠ E[(% v2 E v)]
```

`call/comp` とほぼ同じ。non-composable continuationは起動時にもタグを見るので、 `cont` の下にタグ `v2` を持っておく。

### cont-post
non-composable continuation の起動で `dynamic-wind` のafter thunkが起動するケース。

```
(% v2 D2[E3[(dw x1 e1 W5[((cont v2 D6[E4]) v1)] e2)]] v3)
↝ (% v2 D2[E3[(begin e2 ((cont v2 D6[E4]) v1))]] v3)
where
  D2[E3] ≠ E[(% v2 E v)], -- (1)
  sameDWs(D2, D6), -- (2)
  W5 ≠ E[(% v2 E v)], -- (3)
  noShared(E3[(dw x1 e1 W5 E2)], E4)
```

contは `v2` として捕捉時のタグを覚えているので、そのタグに対応する直近のプロンプトを探す。

条件 1, 3 でプロンプトが直近のものであることを保証する（1は `dw` の外側に他の対応するプロンプトがないこと、3は `dw` の内側に他に対応するプロンプトがないことを保証する）。

条件 2, 4 は必要なafter thunkだけが実行されることを保証する。

`sameDWs` と `noShared` の定義は以下の通り。

```
sameDWs(W1, W2)
= true

sameDWs(W1[(dw x1 e1 E1 e2)], W2[(dw x1 e1 E2 e2)])
= sameDWs(E1, E2)

otherwise = false
```

```
noShared(W1[(dw x1 e1 E1 e2)], W2[(dw x1 e1 E2 e2)])
= false

otherwise = true
```

`sameDWs` は文脈内の `dw` 列が同一であることをチェックする。

`noShared` は文脈内の最初の `dw` が同一でないことをチェックする。

`cont` 実行前の文脈は `D2[E3[(dw x1 ...)]]` で、実行後の文脈は `D6[E4]` になる。このとき、 continuation frame は以下のようになる。

```
実行前
      D2      E3    x1
    <-----> <-----> <->
..-%--...--o--...--o---o

実行後
   D6      E4
    <-----> <----->
..-%--...--o--...--o
```

この場合、 `D2` と `D6` は同一の `dw` 列を持つので before/after thunk を実行する必要がない。 `E3` + `x1` と `E4` は同一の `dw` を共有しないため、この評価規則では、まず最内の `x1` のafter thunkを実行する。

### cont-pre

non-composable continuation の起動で `dynamic-wind` の before thunk が起動するケース。

```
(% v1 D2[W3[((cont v1 k1) v2)]] v3)
↝ (% v1 D6[W4[(begin e1 (dw x1 e1 ((cont v1 k1) v2) e2))]] v3)
where
  k1 = D6[W4[(dw x1 e1 E5 e2)]], -- (1)
  D2[W3] ≠ E[(% v1 E v)], -- (2)
  sameDWs(D2, D6), -- (3)
  noShared(W3, W4[(dw x1 e1 E5 e2)]) -- (4)
```

1の条件は読みやすさのため、2は直近のプロンプトを選択するため、3, 4 は必要なbefore thunk を実行するための条件である。

実行前後で continuation frame は以下のようになる。

```
実行前
      D2      W3
    <-----> <----->
..-%--...--o--...--o

実行後
      D6      W4      x1
    <-----> <------> <->
..-%--...--o--....--o---o
```

`D2` と `D6` は同一の `dw` 列を持つのでbefore/after thunkを実行する必要はない。 `W` 自体は `dw` を含まない文脈である。 `cont` の中にさらに `dw` が含まれる場合は、上図の `x1` までが次の `D2` の範囲になり、内側のbefore thunkが実行される。

### cont

non-composable continuation の起動で `dynamic-wind` のbefore/after thunk が実行されないケース。

```
(% v1 D2[W3[((cont v1 D6[W4]) v2)]] v3)
↝ (% v1 D6[W4[v2]] v3)
where
  D2[W3] ≠ E[(% v1 E v)],
  sameDWs(D2, D6),
  noShared(W3, W4)
```

`D2` と `D6` は同一の `dw` 列を持ち、`W3` と `W4` は `dw` を持たないので実行すべきbefore/after thunk はない。

## continuation mark

### marks

```
(% v2 E2(current-marks v1 v2) v3)
↝ (% v2 ⟦E2, v1, (list)⟧_{marks} v3)
where
  E2 ≠ E[(% v1 E v)]
```

`⟦・, ・, ・⟧_{marks}` の定義は以下の通り。

```
⟦[], v, e2⟧_{marks}
= e2

⟦(wcm w1 E1), v1, e2⟧_{marks}
= ⟦E1, v1, (cons v3 e2)⟧_{marks}
where w1 = ((v v) ... (v1 v3) (v v) ...)

⟦(wcm w1 E1), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
where v1 ∉ Dom(w1)

⟦(v ... E1 e ...), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}

⟦(begin E1 e), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}

⟦(% v E1 v), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}

⟦(dw x e E1 e), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
```

直近の対応するプロンプトまで切り出したものを渡し、 `wcm` をたぐっていってキー `v1` に対応する値を集めてくる。


## wcm

`call/cm` が `with-continuation-mark` に相当する。 `wcm` 相当のものは実コード上には陽に現れない。

### wcm-v

```
(wcm w v1)
↝ v1
```

`wcm` の本体部分が値になったら、それが `wcm` 式全体の値になる。

### wcm-set

```
(wcm ((v1 v2) ... (v3 v4) (v5 v6) ...)
  (call/cm v3 v7 (λ () e1))
↝ (wcm ((v1 v2) ... (v3 v7) (v5 v6) ...) e1)
```

`call/cm` を使うとキーを指定して外側の `wcm` の continuation mark を書き換えることができる。

### wcm-add

```
(wcm ((v1 v2) ...)
  (call/cm v3 v4 (λ () e1))
↝ (wcm ((v1 v2) ... (v3 v4)) e1)
where v3 ∉ (v1 ...)
```

外側の `wcm` に対応するキーがない場合は新たにエントリを追加する。

### wcm-intro

```
E1[(u1 v1 ...)]
↝ E1[(wcm () (u1 v1 ...))]
where E1 ≠ E[(wcm w [])]
```

意味論上 `wcm` が必要な場合にそれを補う規則。 where の条件で `wcm`が入れ子にならないようにしている。

# TODO

`shift`/`reset`, `control`/`prompt`、動的束縛、例外処理の実現方法の概要を説明する。

概要:

* `shift`/`reset`, `control`/`prompt` 等のプロンプトの設定は `call-with-continuation-prompt` で実現し、継続の切り出しは `call-with-composable-continuation` で実現されている。これらのオペレータでは、切り出した継続は `shift` や `control` の継続からは取り除かれる。一見、 `abort-current-continuation` で継続を破棄すればよいように見えるが、それでは `reset` や `prompt` で設定したプロンプトまで破棄されてしまう（[abort](#abort-1) 規則を参照）。これらの限定継続オペレータは外側のプロンプトは残したいので、 `call-with-current-continuation` をつかってプロンプトを残したまま継続をすげかえる（例えば [cont](#cont) 規則を参照）。ちなみに、 `shift0`/`reset0` や `control0`/`prompt0` のような外側のプロンプトを残さない限定継続オペレータは `abort-current-continuation` を使って実現できる。
* 動的束縛はcontinuation markで実現されている。
* 例外処理は、 `with-exception-handler` の呼び出しごとに continuation mark に例外ハンドラを設定することで実現している（例外ハンドラが起動したときに `continuation-marks` で例外ハンドラ列を取り出す。ハンドラ実行中の例外ハンドラはいい感じに設定する）。ところで、 RnRS の `guard` 式では、 clause で例外を処理した場合は、その処理結果が `guard` 式の値になる。これは、 `guard` の外側にプロンプトを設定し、 clause の処理結果でそのプロンプトまで `abort-current-continuation` することで実現している。このとき、ハンドラに値を返すためのプロンプトとそれ以外の継続操作を区別するためにプロンプトタグを使っている。

# 付: `shift`/`reset`, `call/cc` の関係

下記の意味論は [Final Shift for Call/cc: Direct Implementation of Shift and Reset](https://www.deinprogramm.de/sperber/papers/shift-reset-direct.pdf) による。

```
⟦_⟧_ : Expr → Env → Cont -> Val
Env = Expr → Val
Cont = Val → Val

⟦x⟧ρ         = λk. k (ρ x)
⟦λx. M⟧ρ     = λk. k (λv.λkʹ. ⟦M⟧(ρ[x↦v]) kʹ)
⟦E1 E2⟧ρ     = λk. ⟦E1⟧ρ (λf. ⟦E2⟧ρ (λa. f a k))
⟦call/cc E⟧ρ = λk. ⟦E⟧ρ (λf. f (λv.λkʹ. k v) k)
⟦reset E⟧ρ   = λk. k (⟦E⟧ρ (λv. v))
⟦shift c M⟧ρ = λk. ⟦M⟧(ρ[c↦λv.λkʹ. kʹ (k v)]) (λv. v)
```

`shift`/`reset` と `call/cc` ありのλ計算の意味を、それらのないλ計算への変換で表現すると上記のようになる（continuation semantics）。

ところで、この意味論では、 `reset` の変換後の項に末尾呼び出しでない適用があるので、右辺にさらにCPS変換をかける。

```
⟦_⟧_ : Expr → Env → Cont → MCont -> Val
Env = Expr → Val
Cont = Val → MCont → Val
MCont = Val → Val

⟦x⟧ρ         = λk.λm. k (ρ x) m
⟦λx. M⟧ρ     = λk.λm. k (λv.λkʹ.λmʹ. ⟦M⟧(ρ[x↦v]) kʹ mʹ) m
⟦E1 E2⟧ρ     = λk.λm. ⟦E1⟧ρ (λf.λmʹ. ⟦E2⟧ρ (λa.λmʺ. f a k mʺ) mʹ) m
⟦call/cc E⟧ρ = λk.λm. ⟦E⟧ρ (λf.λmʹ. f (λv.λkʹ.λmʺ. k v mʺ) k mʹ) m
⟦reset E⟧ρ   = λk.λm. ⟦E⟧ρ (λx.λmʹ. mʹ x) (λr. k r m)
⟦shift c M⟧ρ = λk.λm. ⟦M⟧(ρ[c↦λv.λkʹ.λmʺ. k v (λw. kʹ w mʺ)])
                (λw.λmʹ. mʹ w)
                m
```

さらに継続っぽい引数が増えるので、 `MCont` の方をメタ継続と呼ぶことにする。この意味論をmeta-continuation semanticsと呼ぶ（[Abstracting Control](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.6.960&rep=rep1&type=pdf) も参照。ちなみに、さらにCPS変換をくり返して、メタ継続、メタメタ継続……を操作するような `shift`/`reset` の変種を考えることもできる）。

`reset` 以外はメタ継続を操作しないので、地道にメタ継続引数を渡していく。

`reset` は継続を空の継続 `λv.λm. m v` にし、もとの継続をメタ継続に移したうえで本体部分 `E` を評価する。

この方向で進むと、 `call/cc` は `reset` でメタ継続に移された継続は触れないので、 Racket の `call/cc` がプロンプトを見るのは素直な流れのように見える。