問題タブ [callcc]

構造的である直観的論理は、関数型プログラミングにおける型システムの基礎です。古典的な論理は建設的ではありません。特に、除外された中央の A ∨ ¬Aの法則 (または、二重否定消去やピアスの法則などの同等のもの)は建設的ではありません。

ただし、たとえばSchemeのように、 call-with-current-continuation演算子 (別名call/cc )を実装 (構築) できます。では、なぜcall/ccは建設的ではないのでしょうか?

以下が無限ループを設定しない方法がわかりません。

を呼び出すと(return 22)、継続に戻りますが、call/ccフォームの新しい評価結果として渡された値 22 が使用されます。それ(return 22)は次のステートメントとして評価され、無限ループを設定することになりませんか?

無限ループではないことはわかっていますが、そうでない理由がわかりません。

Racket でこれを試していると、答えは 5 になります。

以下のように展開しました。

展開が正しいと仮定すると、k 継続が k1 継続に適用されたときに何が起こるか、および 5 を生成するために外側のラムダの実行にどのように影響するかはまだわかりません。

Racket の継続のタイプは何ですか? そして、call/cc 呼び出しを見て現在の継続を判断する方法は? (例: 現在の継続が call/cc 閉じ括弧の直後に続くものであると仮定するのは正しい戦略ですか?)

次の定義を検討してください。ラケットを使用しています。

次のように呼び出した場合

(5 1)

それは何も与えません。それを行った後、5 を直接呼び出すと 120 になります。

$5

120

しかし、再試行すると (5 1)、120 は手順ではないと言って失敗します。

(zero? n) ベース ケースでキャプチャされた継続に対する最初の 5 つのポイントを理解しています。しかし、上記の動作をどのように説明できるかわかりません。

別のパラメーターで別の実行

$ (5 4)

5ドル

480

私はSchemeでの呼び出しの継続に完全に迷っています。誰かがこの例で私を助けることができますか?

最初の結果(3)はわかりますが、2017年の結果はわかりません。

前文

私は実際にどのように使用するか、ContTそしてcallCC何か役に立つものについて頭を悩ませようとしています。コードに関する情報と制御の流れをたどるのに問題があります。（でも、そこが続きのポイントじゃない？）

このモナドといくつかのあまり単純ではないコンビネータを使用してピースを移動するには、さまざまな方法があります。ContT がどのように機能するかについての理解にまだ満足していないことを告白しますが、これまでに読んだことを指摘します。

• Haskell/継続渡しスタイル
• Haskell Cont モナドはどのように、なぜ機能するのですか?
• Haskell callCC の例を理解する
• Haskell での Goto: 継続モナドの使用によるこの一見非常識な効果を説明できる人はいますか?
• HaskellでcallCCを解釈するには?
• Parsec General (私がこの道を歩むきっかけとなった記事)

私がやりたいのは、疑似コードの例を投稿して、それについていくつか質問することです。これは、ContT を使用したコードの典型的な外観を表しています。

疑似コード

質問

1. の値と型を決定するものは何outputですか?
2. とはbどういう意味kですか?
3. 与えられた価値はどこへk行くのか?
4. いつinner_block実行されますか？どのバージョンの状態が表示されますか?
5. どこにrval行き、そのタイプは何ですか？
6. kとの関係は何rvalですか?
7. ka) in inner_block、b) in after_callcc、c) outside ofを適用するとどうなりblockますか?
8. 上記のそれぞれの状態のバージョンは何ですか?
9. kから抜け出すにはどうすればいいblockですか？
10. 州に入れkますか？

読みやすいように色分けされています

私はラケットで紙の行に沿って勉強しcall/ccています 。

call/ccこの論文では、最も有利な API はプロシージャを提供することによって得られると述べていますlambda (cc) (cc cc)。この特定のcall/cc呼び出しは、現在の継続ファーストクラス オブジェクトをメイン プログラムに返すことを理解しています。

次の例では、ペーパーはこれらすべてを と呼んでいます(right-now)。

私が見ているのは、その同じ例の中で、上記の呼び出しccによって返されたオブジェクトは、それ自体に適用することによって常に後で実行されるということです。call/ccそれは私が理解していないものです。

cc値として何が特別なの(cc ())かわかりません。喜びはまったくありません。明らかに、継続は、実行を開始するために、そのアプリケーションだけを必要としています。(cc (lambda () ()))(cc "whatever")(cc)

何故ですか？を行うことで cc を実行することの独自性を明確に示す例は何(cc cc)ですか?

ラケットの継続について説明しているこの面白いページを読んでいました。

それらは、計算の現在の継続を保存するコードを提示します (そして、後でこのトリックを使用してバックトラッキングを実装します)。コードは次のようになります。

今、私は標準 ML で同じトリックを実行したいと考えています。ニュージャージーの SML が継続を実装している唯一のインタープリターであるように思われるので、そこで実行しています。

そこにある継続署名は次のようになります。

直訳は次のようになります。

しかし、ML の型システムはこれを禁止しています (これは循環であるため)。

だから私は次のようなものを試しました：

および参照を使用した他のさまざまなトリックですが、現在の継続を実際に保存する方法が見つかりません(この例では、後で !glcc を使用して必要な継続を変更するため)。

savecc演算子を実装する方法を知っている人はいますか?backjumpそれにより、プログラムの現在の継続を保存し、後で標準 ML でその時点に戻ることができますか?

よろしくお願いします！

ヤニック