標準MLは等価性を検証する(CBV)か?

$ eta $関数の等価性はカテゴリ理論的意味論において基本的なものですが、実際には “機能的”な言語でさえそれに違反する
“不純な”機能を含んでいます。 CBN vs CBVの問題ではないことに注意してください。CBNηの等式$ M = lambda
xです。 M x $は任意の項M $:A 〜B $に対して保持されるが、CBVでは$ V = λxに制限される。 V×$。 CBV
$ eta $は完全に優れたカテゴリ理論的説明を持っています.LevyのPush-by-Valueを参照してください。

  1. Haskell includes seq, which can distinguish
    between (x -> error "") and error
    ""
  2. OCaml includes operations like “physical equality” (==), and
    which will distinguish fun x => x from fun y
    => (fun x => x) y
    because == corresponds to pointer
    equality.

だから私は、「実在の」言語が観測上の等価性のためにetaを満たすのだろうか?
コンパイラの実装がタイプに基づいてηの削減を実行することがわかっている場合は、すべてがより優れています。

私が知っている唯一の例は、最近のバージョンの定義上の平等としてそれを含むCoqです。たぶん同様の言語(Agda、Idris)でも同様です。これらは等価型を含んでおり、$
eta $やより強力な(?)拡張性の原則なしに関数の等価性を証明するのは非常にイライラです。

私の主な質問は、具体的には、私は関数のポインタの平等を持っていないと思う標準的なMLについてです。それはCBV $ eta
$法を満たしていますか?さらに、MLtonなどのSMLのコンパイラは、プログラムを最適化するときに$ eta
$を使用しますか?

ベストアンサー

@xuq01’s guess is (extremely surprisingly!) wrong. The CBV eta
rule described in the question is sound in Standard ML: the value
v is contextually equivalent to fn x => v
x
.

これには2つの注意点があります。

  1. First, in specific implementations this equivalence
    might not be sound: in SML/NJ, you could use
    Unsafe.cast to detect physical equality of function
    values. However, unsafe features are not part of the standard.

  2. Second, eta with functions and sums interacts in a slightly
    subtle way, due to clausal definitions and incomplete pattern
    matching. In particular, the definitions:

    fun f (SOME x) (SOME y) = x + y
    

    and

    val g = fn (SOME x) => (fn (SOME y) => x + y)
    

    are not contextually equivalent. This is because the call
    f NONE will return a function, and g NONE
    will raise an error.

    - f NONE;
    val it = fn : int option -> int
    
    - g NONE;
    uncaught exception Match [nonexhaustive match failure]
    raised at: stdIn:2.32
    

    The reason this happens is operationally obvious, and of course
    a call-by-push-value/polarization setup makes this choice
    explicable. But if you really want to seriously understand clausal
    definitions, you are led to the idea that clausal definitions
    should be primary, and the usual term formers should be derived
    notions. See Abel, Pientka, Thibodeau and Setzer’s Copatterns: programming infinite structures by
    observations
    for an example of a polarized calculus in
    this style. (See also Paul Levy’s Jumbo Lambda-Calculus, for another
    calculus based on this observation.)

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です