4

私はコンパイラ/プルーフチェッカーに取り組んでいますが、次のような構文ツリーがあるかどうか疑問に思っていました。たとえば、次のようになります。

data Expr
    = Lambdas (Set String) Expr
    | Var String
    | ...

sのアルファ等価性（等価モジュロ名前変更）をチェックする方法があった場合Expr。ただし、これExprはラムダ計算とは異なり、ラムダ内の変数のセットは可換です。つまり、パラメーターの順序はチェックに考慮されません。

（ただし、簡単にするために、とLambda ["x","y"] ...は異なりLambda ["x"] (Lambda ["y"] ...)ます。その場合、順序は重要です）。

言い換えると、2つが与えられたExprs場合、1つが一方から他方への名前変更を効率的に見つけるにはどうすればよいでしょうか。この種の組み合わせ問題は、NP完全のにおいがします。

4

2 に答える 2

6

パラメータの可換性は、指数関数的な比較を示唆しています。

しかし、パラメータリストを正規化できるので、それらを1つの順序で比較するだけでよいと思います。その場合、名前の変更と比較したツリーは、ツリーのサイズが本質的に線形になります。

私が提案するのは、パラメーターリストごとに、のサブツリーにアクセスし（順序が一致している限り、順序は関係ありません）、訪問が最初に発生した順序のインデックスでパラメーターを並べ替えることです。パラメータの使用。だからあなたが持っているなら

  lambda(a,b):  .... b .....  a  ... b ....

パラメータリストを次のように並べ替えます。

  lambda(b,a)

最初にbに遭遇し、次に2番目に遭遇し、bの追加の遭遇は重要ではないためです。ツリーを正規化されたパラメータリストと比較します。

ラムダ句の演算子が可換である可能性があると主張すると、人生はより厄介になります。私の推測では、まだ正規化できると思います。

于 2012-02-27T11:19:24.967 に答える
4

DaanLeijenのHMFにいくつかのアイデアをアピールできます。（彼は「foralls」のバインダーを扱っていますが、これも可換として出くわします。

特に、本文の出現順に変数を再バインドします。

次に、用語の比較には、同じ方法でスコーレミングし、結果を比較することが含まれます。

そのスコーレム化パスをローカルで名前のない表現に置き換えることで、それよりもうまくいくことができます。

data Bound t a = Bound {-# UNPACK #-} !Int t | Unbound a

instance Functor (Bound t) where ...
instance Bifunctor Bound where ...

data Expr a
  = Lambdas {-# UNPACK #-} !Int (Expr (Bound () a))
  | Var a

したがって、ラムダの下でのBoundのオカレンスは、ラムダによって直接バウンドされる変数であり、オカレンスに入れたいタイプ情報とともに、ここでは（）を使用しました。

これで、閉じた用語は「a」で多形になり、ラムダの要素を使用サイトで並べ替えると（未使用の用語を削除することでラムダを常に正規化できるようになります）、アルファに相当する用語は単純に（==）と比較されます。オープンタームが必要な場合は、ExprStringまたはその他の表現を使用できます。

ExprとBoundのシグネチャのより肛門性格のバージョンは、存在型と自然な型レベルを使用して、バインドされている変数の数を識別し、Boundコンストラクターで「Fin」を使用しますが、すでに不変条件を維持する必要があるためです。ラムダで発生する＃よりも多くの変数をバインドしないこと、および型情報がすべてVar (Bound n _)同じで一致すること、別の変数nを維持するための負担はそれほど大きくないこと。

更新：私のboundパッケージを使用して、完全に自己完結型の方法でこれの改善されたバージョンを実行できます！

于 2012-02-27T15:31:12.713 に答える