不滅の言葉をフィーチャーしたTシャツが販売されていたことを誓います。
のどの部分
分かりませんか？
私の場合、答えは...すべてです！
特に、Haskellの論文ではこのような表記がよく見られますが、それが何を意味するのかわかりません。数学のどの分野になっているのかわかりません。
もちろん、ギリシャ文字の文字と「∉」（通常、何かが集合の要素ではないことを意味します）などの記号を認識します。
一方、私はこれまで「⊢」を見たことがありません（ウィキペディアはそれが「パーティション」を意味するかもしれないと主張しています）。ここでの括線の使用にも慣れていません。（通常、それは分数を示しますが、ここではそうではないようです。）
誰かが少なくとも、このシンボルの海が何を意味するのかを理解するためにどこから始めればよいかを教えてくれるなら、それは役に立ちます。
誰かが少なくともこのシンボルの海が何を意味するのかを理解するためにどこから始めればよいか教えてくれたら
判断と導出による論理のスタイルについては、「プログラミング言語の実用的な基礎」の第2章と第3章を参照してください。本全体がAmazonで利用できるようになりました。
帰納的定義は、プログラミング言語の研究に不可欠なツールです。この章では、帰納的定義の基本的なフレームワークを開発し、それらの使用例をいくつか示します。帰納的定義は、さまざまな形式の判断またはアサーションを導出するための一連のルールで構成されます。判断は、指定された種類の1つ以上の構文オブジェクトに関するステートメントです。規則は、判断の有効性のための必要十分条件を指定し、したがってその意味を完全に決定します。
まず、構文オブジェクトに関する判断またはアサーションの概念から始めます。以下のような例を含め、さまざまな形の判断を利用します。
判断では、1つ以上の構文オブジェクトがプロパティを持っているか、相互に何らかの関係にあると述べています。プロパティまたは関係自体は判断フォームと呼ばれ、1つまたは複数のオブジェクトがそのプロパティを持っている、またはその関係にあるという判断は、その判断フォームのインスタンスと呼ばれます。判断フォームは述語とも呼ばれ、インスタンスを構成するオブジェクトはそのサブジェクトです。Jがaを保持していると主張する判断のためにJ を書きます。判断の対象を強調することが重要でない場合（ここではテキストが途切れます）
表記は自然演繹に由来します。
⊢シンボルは回転式改札口と呼ばれます。
6つのルールはとても簡単です。
Varルールはかなり些細なルールです-識別子のタイプがタイプ環境にすでに存在する場合、タイプを推測するには、環境からそのまま取得するということです。
Appルールによると、2つの識別子がe0ありe1、それらのタイプを推測できる場合は、アプリケーションのタイプを推測できますe0 e1。e0 :: t0 -> t1そして（同じt0！）を知っている場合、ルールは次のようe1 :: t0になります。アプリケーションは適切に型指定され、型は。ですt1。
AbsとLetは、ラムダ抽象化とレットインの型を推測するためのルールです。
Instルールは、タイプをより一般的でないタイプに置き換えることができると言っています。
There are two ways to think of e : σ. One is "the expression e has type σ", another is "the ordered pair of the expression e and the type σ".
View Γ as the knowledge about the types of expressions, implemented as a set of pairs of expression and type, e : σ.
The turnstile ⊢ means that from the knowledge on the left, we can deduce what's on the right.
The first rule [Var] can thus be read:
If our knowledge Γ contains the pair e : σ, then we can deduce from Γ that e has type σ.
The second rule [App] can be read:
If we from Γ can deduce that e_0 has the type τ → τ', and we from Γ can deduce that e_1 has the type τ, then we from Γ can deduce that e_0 e_1 has the type τ'.
It's common to write Γ, e : σ instead of Γ ∪ {e : σ}.
The third rule [Abs] can thus be read:
If we from Γ extended with x : τ can deduce that e has type τ', then we from Γ can deduce that λx.e has the type τ → τ'.
The fourth rule [Let] is left as an exercise. :-)
The fifth rule [Inst] can be read:
If we from Γ can deduce that e has type σ', and σ' is a subtype of σ, then we from Γ can deduce that e has type σ.
The sixth and last rule [Gen] can be read:
If we from Γ can deduce that e has type σ, and α is not a free type variable in any of the types in Γ, then we from Γ can deduce that e has type ∀α σ.