Python の抽象代数ライブラリに取り組んでいたとき、多くの汚れた作業が量指定子を使用した論理式に対応するループを構築しているだけであることに気付きました。その後、Python で論理量化の関数を実装するのは難しいかもしれませんが、Haskell や他の言語では簡単に実装できることに気付きました。
現在、プロパティが量化されている1つの変数のみを含む限り機能する量指定子があり、量化する関係に3つの変数がある場合にのみ、これらの障壁を乗り越えるのは難しい部分のようです.
たとえば、ステートメント∀x ∃y (x < y)
は問題を引き起こしますが、問題ありません∀x (x = 2) ∃y (y < 3)
。
このような値レベルの論理量指定子を実装する既存の Haskell ライブラリはありますか? 「論理量指定子Haskell」の行に沿って何かを検索するたびに、型量指定子について多くのことを取得するため、検索が困難です。これは私が望んでいるものではありません。
私が見つけた唯一のものはforAll
Test.QuickCheckであり、これには「存在」はありません。