エンコーディングのニュアンスと、存在型をユニバーサルに変換した後の使用のニュアンスをよりよく理解しようとしています。要するに、存在型を使用することは、エンコードするよりもはるかに簡単であるように思われます。それが私にとって何を意味するのかを以下で説明します。これをよりよく説明するために、ロジックからの 2 つのルールから始めましょう。

1. ∀xP(x) ⇒ ¬(∃x.¬P(x))
2. ∃xP(x) ⇒ ¬(∀x.¬P(x))

これから、私たちはそれを持っています

1. ∀x.(P(x) ⇒ Q)
2. ∀x.(¬P(x) ⩖ Q)
3. (∀x.¬P(x)) ⩖ Q
4. (¬¬(∀x.¬P(x))) ⩖ Q
5. (¬(¬(∀x.¬P(x)))) ⩖ Q
6. (¬(∃xP(x))) ⩖ Q
7. (∃xP(x)) ⇒ Q

したがって、

(∃xP(x)) ⇒ Q = ∀x.(P(x) ⇒ Q)。

つまり、関数の最初の引数が存在型である場合、その存在型を左側に引き出して、それをユニバーサルとして表すことができます。これを私は実存的ルールの使用と呼んでいます。通常、人々が普遍型と実存型の同等性について話すとき、

∃xP(x) = ∀y.(∀xP(x) ⇒ y) ⇒ y.

これは、私が存在規則のエンコーディングと呼んでいるものです。この等価性を確認するために、

1. ∀y.(∀xP(x) ⇒ y) ⇒ y
2. ∀y.((∃xP(x)) ⇒ y) ⇒ y
3. ∀y.¬((∃xP(x)) ⇒ y) ⩖ y
4. ∀y.¬(¬(∃xP(x))⩖y)⩖y
5. ∀y.((∃xP(x)) ⩕ ¬y) ⩖ y
6. ∀y.((∃xP(x)) ⩖ y) ⩕ (yv ¬y)
7. ∀y.(∃xP(x))⩖y
8. (∃xP(x)) ⩖ ∀yy
9. ∃xP(x)

さて、このルールが私に言っているのは、存在型は、P(x) を y に変換してから y を出力するプログラムを受け入れる関数であるということです。

ここで、実存的なものを使用することと実存的なものを構築することの違いについて、私が言いたいことは次のとおりです。OCaml のような言語で貧乏人のモジュールを構築したいとします。このようなプログラムでそれを行うことができます。

これは、上記の存在規則の使用を使用します。タイプに関しては、

基本的に、 simpleProg : (∃x.mypackage(x)) ⇒ string という関数を設計したいと考えています。そのために、代わりに ∀x.mypackage(x) ⇒ string 型の関数を作成し、パッケージをユニバーサルでエンコードします。これは、ほとんどの関数型言語で簡単に実行できます。代わりに、実際に int_package と str_package をユニバーサル パッケージではなく実存パッケージとしてエンコードしたい場合は、実存ルールのエンコードを使用し、代わりに次のようなコードになります。

ここに、それがあります

これは基本的に私たちが望むものです。int 型と string 型はパッケージの中に隠されています。次に、

これもまた、ほとんどが私たちが望むものです。本当に、私たちはちょっと欲しかった

しかし、型変数がこれを整理してくれます (または、私はひどい間違いを犯しました。2 つのうちの 1 つです)。

いずれにせよ、2 番目のプログラムが示すように、ユニバーサルから実存を実際に作成するための構造は非常に重く見えますが、最初のプログラムが示すように、実存を使用するための構造は非常に単純に見えます。基本的に、それは私が意味することであり、存在を使用することは、作成するよりもはるかに簡単です.

だから、本当に、私の2つの質問は次のとおりです。

1. 関数内で存在パッケージを使用することのみを気にする場合、ユニバーサル型へのエンコードは、独立して存在するパッケージを作成するよりもはるかに簡単ですか? これが正しいと仮定すると、これは、既存のパッケージをユニバーサル パッケージ (上記のタイプ mypackage) でエンコードできるためと思われます。
2. 存在規則の使用とこれらの普遍的なパッケージの使用だけに制限すると、最終的に何を失うのでしょうか? 繰り返しになりますが、ユニバーサル パッケージとは、上記のタイプ mypackage のトリックを意味します。

編集 1

camlspotter と Leo White は、私のタイプが公開され、パッケージが台無しになったことは正しかったです。これは、同じコードの書き直された非常に冗長なバージョンです。

このプロセスで私が学んだ最大のことは、本質的に、この再エンコードのトリックは、物事がどのように構築されるかの順序を逆転させるということです. 基本的に、これらのパッケージは、プログラムを受け入れ、このプログラムを内部表現に適用するプロセスを構築します。このトリックを実行すると、パッケージの内部タイプが隠されます。これは理論的には実存型と同等ですが、個人的には、Pierce の本「Types and Programming Languages」などで説明されているように、実存型の直接実装とはプロセスが異なると思います。

上記の私の質問に対する直接の回答として

1. パッケージを関数に直接渡すことのみに関心がある場合は、ユニバーサル パッケージのトリックが機能し、実装がはるかに簡単になります。これは絶対に実在するパッケージではありませんが、その使用法は、この同じコンテキストで使用される真の実在するパッケージと非常に似ていますが、解凍は必要ありません。同様に、異なる型に基づくパッケージの異なる表現を関数に渡し、これらの表現で一般的に計算する機能を保持することを意味します。
2. これらのユニバーサル パッケージで失われるのは、これらのパッケージを真のファースト クラス メンバーのように扱う能力です。最も単純な例は、それらのタイプが公開されているため、これらのユニバーサル パッケージの束をリストに入れることができないということです。真の存在パッケージは型を隠しているため、より大きなプログラムに渡すのがはるかに簡単です。

また、ユニバーサルパッケージはひどい言葉です。int_package と str_package は特殊化されているため、実際には普遍的ではありません。ほとんどの場合、私はより良い名前を持っていません。

この質問は #haskell の議論で出てきました。

深くネストされた forall の発生が正の場合、その forall を一番上に持ち上げることは常に正しいですか?

例えば：

(ここで、P、S、T はメタ変数として理解されるべきです)

(通常は次のように記述します。(P(a) -> S) -> T

ラストの右側など、いくつかのポジティブな位置からフォーラルを収集することが確かに許可されていることを私は知っています->。

これは古典論理では有効なので、ばかげた考えではありませんが、一般的に直観主義論理では無効です。ただし、各型変数が「呼び出し元によって選択された」または「呼び出し先によって選択された」という量指定子の非公式のゲーム理論の直感は、実際には2つの選択肢しかなく、すべての「呼び出し元によって選択された」オプションを持ち上げることができることを示唆していますトップ。ゲーム内の動きのインターリーブが重要でない限り?

最初に、この質問は、グループを取得する方法や、私がよく知っている正規表現の 2 つの機能である量指定子の使用方法に関するものではないことを説明させてください。エキゾチックなエンジンの珍しい構文に精通している可能性のある正規表現愛好家にとっては、より高度な質問です。

数量詞のキャプチャ

正規表現フレーバーで量指定子をキャプチャできるかどうか知っている人はいますか? これにより、+ や * などの量指定子によって一致する文字の数がカウントされ、この数が別の量指定子で再び使用できるようになるということです。

たとえば、次のような文字列で L と R の数が同じであることを確認したいとします: LLLRRRRR

次のような構文を想像できます

ここで、L の + 量指定子がキャプチャされ、キャプチャされた数値が R の量指定子で {\q1} として参照されます。

@@@@ "Star Wars" ==== "1977" ---- "Science Fiction" //// "ジョージ・ルーカス」

再帰との関係

場合によっては、量指定子のキャプチャが再帰をエレガントに置き換えます。たとえば、同じ数の L と R で囲まれたテキストの一部、

このアイデアは、次のページで詳細に説明されています:キャプチャされた量指定子

また、キャプチャされた量指定子の自然な拡張についても説明します。前に一致した文字数 (3*x + 1) に一致させたい場合の量指定子算術です。

このようなものが存在するかどうかを調べようとしています。

あなたの洞察を事前にありがとう!!!

アップデート

Casimir は、パターンのさまざまな部分が同じ長さであることを検証する 2 つの方法を示す素晴らしい回答を出しました。しかし、日常業務ではどちらにも頼りたくありません。これらは本当に素晴らしいショーマンシップを示すトリックです。私の考えでは、これらの美しいが複雑な方法は、質問の前提を確認します: 数量詞 (+ や * など) が一致できる文字数を取得する正規表現機能は、そのようなバランスパターンを非常に単純にし、構文を拡張します心地よい表現方法。

更新 2 (かなり後で)

.NET には、私が求めていたものに近い機能があることがわかりました。機能を実証するための回答を追加しました。

次の例でタイムアウトが発生しています。 http://rise4fun.com/Z3/zbOcW

これを機能させるためのトリックはありますか (たとえば、問題を再構成するか、トリガーを使用することによって)?

I can't seem to figure out regular expression quantifiers. Something as simple as look for "..." does not work for me.

This is my pattern:

Am I understanding something wrong? The expression "X{n}" means, take X exactly n times?

But Strings like "...." work just fine, even though it isn't exactly 3 times.