10

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

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

4

1 に答える 1

12

問題は、call/ccでは結果が評価の順序に依存することです。次の Haskell の例を考えてみましょう。call/cc演算子があると仮定します。

callcc :: ((a -> b) -> a) -> a
callcc = undefined

定義しましょう

example :: Int
example =
    callcc (\s ->
        callcc (\t ->
            s 3 + t 4
        )
    )

どちらの関数も純粋であるため、 の値はexample一意に決定される必要があります。ただし、評価順によります。が最初に評価される場合s 3、結果は3; が最初に評価される場合t 4、結果は4です。

これは、継続モナド (順序を強制する) の 2 つの異なる例に対応します。

-- the result is 3
example1 :: (MonadCont m) => m Int
example1 =
    callCC (\s ->
        callCC (\t -> do
            x <- s 3
            y <- t 4
            return (x + y)
        )
    )

-- the result is 4
example2 :: (MonadCont m) => m Int
example2 =
    callCC (\s ->
        callCC (\t -> do
            y <- t 4 -- switched order
            x <- s 3
            return (x + y)
        )
    )

用語がまったく評価されるかどうかにも依存します。

example' :: Int
example' = callcc (\s -> const 1 (s 2))

が評価される場合s 2、結果は2、そうでない場合は1です。

これは、 call/ccが存在する場合、 Church-Rosser の定理が成り立たないことを意味します。特に、用語には固有の正規形がなくなりました。

おそらく 1 つの可能性として、 call/ccを、さまざまなサブタームをさまざまな順序で評価する (評価しない) ことによって得られるすべての可能な結果を​​結合する非決定論的 (非構成的) 演算子と見なすことが考えられます。プログラムの結果は、そのようなすべての可能な正規形のセットになります。ただし、標準のcall/cc実装では、(特定の評価順序に応じて) 常にそのうちの 1 つだけが選択されます。

于 2014-07-12T09:39:08.220 に答える