22

次の例を知っている人はいますか？

  1. 証明アシスタント ( Coqなど) における正規表現(後方参照で拡張される可能性があります)に関する証明の開発。
  2. 正規表現に関する従属型言語 ( Agdaなど) のプログラム。
4

5 に答える 5

13

Certified Programming with Dependent Typesには、検証済みの正規表現マッチャーの作成に関するセクションがあります。Coq Contribsには、役に立つかもしれないオートマトンの貢献があります。Jan-Oliver Kaiser は、正規表現、有限オートマトン、および Coq の Myhill-Nerode キャラクタリゼーションの間の同等性を学士論文のために形式化しました。

于 2009-08-14T14:48:05.840 に答える
10

Moreira、Pereira & de Sousaの共著『 On the Mechanization of Kleene Algebra in Coq 』は、Coqの正規表現のアンチミロフ導関数の優れた検証済みの構築を提供します。この構造から CFA を読み取り、正規表現の交点を計算するのは非常に簡単です。

Coq を従属型付けプログラミングから分離する理由がよくわかりません。Coq は基本的に、帰納型 (つまり、CIC、帰納的構造の計算) を使用した、多相依存型付けラムダ計算でプログラミングしています。

依存型付けされた言語での正規表現の形式化については聞いたことがありませんし、バックトラッキングを使用した正規表現のアンチミロフのような派生物についても聞いたことがありませんが、Becchi & Crowley、Extending Finite Automata to Efficiently Match Perl-Compatible Regular Expressions Perl のような正規表現言語に一致する有限状態オートマトンの概念を提供します。それは、近い将来、フォーマライザーにとって魅力的なものになるかもしれません。

于 2009-12-24T22:26:35.307 に答える
6

正規表現を単独で扱う開発については知りません。

ただし、有限オートマトンは、NFAがこれらの正規表現に一致する標準的な方法であるため、NuPRLで研究されています。ロバート・L・コンスタブル、ポール・B・ジャクソン、パーヴェル・ナウモフ、フアン・ウリーベをご覧ください 。オートマトン理論を建設的に形式化する。

代数、特に、これらの形式言語にアプローチすることに興味がある場合。有限半群理論を開発する場合、さまざまな定理証明器で開発された代数ライブラリがいくつかあり、それらを使用することを考えることができます。そのうちの1つは有限設定で特に効率的です。

于 2009-06-26T11:34:29.153 に答える
5

証明アシスタントの Isabelle/HOL は、正規表現に関する多くの形式化された証明を提供しています (後方参照なし): http://afp.sourceforge.net/browser_info/devel/HOL/Regular-Sets/

（これは、著者が正確に何をしたかに関する論文です）。

もう 1 つのアプローチは、Myhill-Nerode の定理によって正規表現を特徴付けることです: http://www.dcs.kcl.ac.uk/staff/urbanc/Publications/itp-11.pdf

于 2012-07-26T18:34:28.453 に答える