かつて、不滅の言葉をプリントしたT シャツが売られていたと断言できます。
どの部分
分かりませんか？
私の場合、答えは...すべてです！
特に、Haskell の論文ではこのような表記をよく見かけますが、それが何を意味するのか全くわかりません。数学のどの分野を指すのか全くわかりません。
もちろん、ギリシャ語のアルファベットの文字や「∉」（通常は何かが集合の要素ではないことを意味する）などの記号も認識できます。
一方、「⊢」は今まで見たことがありません（Wikipediaによれば「パーティション」を意味する可能性があるという。）。また、ここでの vinculum の使用法もよくわかりません。(通常は分数を表しますが、ここではそうではないようです。 )
この記号の海が何を意味するのかを理解するために、どこから調べ始めればよいか、少なくとも誰かが教えてくれると助かります。
ベストアンサー1
- 水平バーは「[上]は[下]を意味する」という意味です。
- [上記] に複数の式がある場合は、それらをAND で結合して考えます。[下記] を保証するには、[上記] がすべて真である必要があります。
:タイプがあることを意味します∈は「含まれる」という意味です。（同様に∉「含まれない」という意味です。）Γは通常、環境またはコンテキストを参照するために使用されます。この場合、識別子とその型を組み合わせた型注釈のセットと考えることができます。したがって、は、x : σ ∈ Γ環境に型 を持つΓという事実が含まれていることを意味します。xσ⊢は、証明する、または決定する、と読むことができます。Γ ⊢ x : σは、環境がの型Γを決定することを意味します。xσ,は、特定の追加の仮定を環境 に含める方法ですΓ。
したがって、は、 がタイプ であるという追加の優先仮定を伴うΓ, x : τ ⊢ e : τ'環境 がΓ、がタイプ であることを証明していることを意味します。xτeτ'
要求に応じて、演算子の優先順位は最高から最低の順です。
- 言語固有の挿入辞および混合挿入辞演算子 (
λ x . e、、、、および関数適用用の空白など)∀ α . σ。τ → τ'let x = e0 in e1 :∈そして∉,(左結合)⊢- 複数の命題を区切る空白（結合的）
- 水平バー