3

有限ドメインを使用した有限マップ モデル置換。無限ドメインでの置換操作をエミュレートするか、無限ドメインでの置換を表す適切な方法を見つける必要があります。たとえば、置換に対する制限操作を考えてみましょう。

  • σ| e (x n ) = if x n ∈ FV(e) then σ(x n ) else x n

制限操作は無限セットの可能性があるすべての変数に適用されるため、有限マップのようなデータ型は、新しいバインディングが追加されたときに制限を予測するために「先を見越す」ことができません。もちろん、無限のドメインを持つ有限マップを使用すると、非終了が発生します。有限マップを使用した制限などの操作をシミュレートする方法や、制限などの操作を簡単に記述できる置換の別の表現はありますか? 明らかな解決策を見落としているように感じます-たとえば、遅延評価や関数置換を利用しています。

編集：

参考までに、有限マップを使用した単純なソリューションを次に示します。代入 σ と式 e に制限操作を適用するたびに、e の自由変数の集合 FV( e ) を求めます。σ のドメイン内の各変数 x nに対して、x n ∈ FV( e ) の場合、σ'(x n ) = x nを設定します。σ' を返します。x n ∉ dom(σ') の場合、σ'(x n ) = x nとします。

編集：これは私が見落とした明らかな解決策です。

4

1 に答える 1

4

まあ、置換の最も直接的なモデルは関数そのものです。

newtype Subst = Subst { apply :: Var -> Expr }

singleton :: Var -> Expr -> Subst
singleton v e = Subst (\v' -> if v == v' then e else Var v')
-- etc.

言語を実装する最初のパスとして、これはおそらく、有限マップが壊れたらすぐに使用するものです。高速ではありません (n がドメインのサイズの場合、O(n) 時間かかります) が、単純です。後で交換できるように、カプセル化したままにしておきます。

O(n) 時間までにヒットし始めたら、トライに切り替えることができます。 data-inttrieは、整数に対する関数のように動作するように特別に記述されていますが、単一のポイントで効率的な変更を行うことができます (置換関数で必要な場合)。変数が整数によって一意に識別される場合は、それを直接使用できます。そうでない場合は、文字列または使用しているもののスタイルをエミュレートできます。

しかし、「楽しみにする」必要があるのも奇妙に思えます。私の言語実装では、これが必要になったことはありません。制限された置換に新しいバインディングを追加すると、その制限は新しいバインディングに適用されません(適用された場合、セマンティクスは正しくありません)。有限マップは、私がばかげて奇妙なことをしていない場合 (通常はうまくいきません)、すべてのケースでうまくいきます。

于 2011-10-11T03:25:33.497 に答える