2

これは、「遅延モダリティを使用して固定点演算子から (無限) ツリーを計算する」のバリエーションです。

設定。ルートからのパスによってツリー内の任意の他のノードを参照する機能が追加されたバイナリ ツリーの言語を研究します。

type Path = [Bool]
data STree = SNode STree STree
           | SPath Path
           | SLeaf Int
    deriving (Show)

パスは何らかのルートのコンテキストで定義され、パスに False/True が表示されると、左/右の子を連続してたどって見つかったサブツリーを識別します。たとえば、パスはツリーで[False, True]識別されます。SLeaf 2SNode (SNode (SLeaf 1) (SLeaf 2)) (SLeaf 3)

このようなツリーは、たとえば、任意のフロー グラフを識別するために使用できます (既約グラフを含み、固定小数点演算子を使用することはできません)。

この記述によって導かれる無限木を考えることができます。

data Tree = Node Tree Tree
          | Leaf Int
    deriving (Show)

follow以下は、ツリーのあるパスでサブツリーを見つける補助関数を利用した、一方から他方への変換関数です。

follow :: Path -> Tree -> Tree
follow [] s = s
follow (False : p) (Node s _) = follow p s
follow (True  : p) (Node _ s) = follow p s
follow _ (Leaf _) = error "bad path"

flatten' :: Tree -> STree -> Tree
flatten' root (SPath p) = follow p root
flatten' root (SNode s1 s2) =
    Node (flatten' root s1) (flatten' root s2)
flatten' _ (SLeaf i) = Leaf i

flatten :: STree -> Tree
flatten s = fix (\root -> flatten' root s)

残念ながら、この関数は生産的ではありません: で無限ループしflatten (SPath [])ます。

問題。ここで、遅延モダリティ ( 「遅延モダリティを使用して固定点演算子から (無限) ツリーを計算する」で説明されているように) で拡張されたこの構造の変形と、Loop自己参照ループを示すコンストラクターを検討します。

data Tree = Node (D Tree) (D Tree)
          | Leaf Int
          | Loop
    deriving (Show)

非構造的に再帰的な関数呼び出しを使用せずに (構造的にSTreeand を再帰することができます)、無限ツリーを展開Pathする関数STree -> Tree(または同様のもの) を記述します。

追記。多くの場合、無限の展開を計算したくありません。存在する場合は有限の展開が必要であり、そうでない場合はエラーが必要です。具体的には、元のデータ型が与えられた場合:

data Tree = Node Tree Tree
          | Leaf Int
    deriving (Show)

非構造的再帰を使用せずにSTree -> Maybe Tree、構文を有限ツリーに展開する関数 (または同様の関数) を記述したいと思うかもしれません。この構造に遅延モダリティがないため、有限であることが保証されます。

この構造には遅延モダリティのインスタンスがないため、 でこれを行うことは不可能に思われfixDます。決して使用できない遅延結果が得られます。ツリーをグラフに変換し、それをトポロジカルにソートしてから、 を使用せずにガウス消去法のアルゴリズムを直接実装する必要があるように思われますfixD。

元の (間違った) コードと同じくらいエレガントに展開を実装できる別の型付け規則はありますか? もしそうなら、グラフのサイクルを見つけるための別のアルゴリズムを (再) 発見しただけかもしれません。

4

1 に答える 1

1

さて、ここに問題に関する少なくともいくつかの部分的な観察があります。

私が書き留めた問題の特定の定式化は、おそらく少し難しすぎるでしょう。意図したより難しい。以下は、特に厄介な例の 1 つです。

SNode (SVar [True, False]) (SVar [])

これは整形式のグラフではありませんが、SVar []発生を展開した後にのみサイクルが明らかになります。を に置き換えるFalseとTrue整形式になります。

letrecその目的は、既約グラフを表現できるようにすることでした。実際、この目標を達成できる、より単純な構文が存在します。Oliveira-Cook の「Functional Programming with Structured Graphs」( https://www.cs.utexas.edu/~wcook/Drafts/2012/graphs.pdf ) の論文 (PHOAS なし)から無限二分木表現を直接採用し、一貫性のために名前が変更されたコンストラクター):

data STree
  = SVar Var
  | SMu [Var] [STree] -- first tree gets "returned"
  | SLeaf Int
  | SNode STree STree

SMuは letrec スタイルのバインド操作です:SMu ["x", "y"] [t1, t2]は本質的にletrec x = t1; y = t2 in xです。必要なノードへのパスを書き留める代わりに、名前を付けるだけです。さらに、これにより、この問題は以前の StackOverflow の質問により似たものになります。(遅延モダリティを使用して固定点演算子から (無限) ツリーを計算します) では、同じ方法で解決できますか?

答えは「はい、しかし...」ですSMu ["x", "y"] [SVar "y", SLeaf 0]。この「再帰的」バインディングはまったく再帰的ではありyませんが、使用したいときに変数を使用できないため (保護されていないため)、遅延コンテキスト スタイルのアルゴリズムによって拒否されます。実際、これは正確には、 「空のサイクルの禁止」で提案されている制限に対応します。挿入された の出現はf、サイクルが発生しないようにするための保護チェックとして機能します。

明らかに、その意図はすべてのバインディングをSMu強く結び付けることです。したがって、私たちのアルゴリズムは、バインディングの強く連結されたコンポーネントを最初に計算し、真に再帰的なバインディングに前処理する場合にのみ適切です (したがって、非再帰的なバインディングを誤って拒否しません) fixD。実際、これは Haskell などのバインディングが実際に処理される方法と一致します。最初にバインディングを強く接続されたコンポーネントに分離し、次に SCC を一度に 1 つずつ処理して、これらの場合に結び目を結びます (そして、空のSCC でサイクルします。)

しかし、それだけではありません。を検討してくださいSMu ["x" "y"] [SVar "y", SNode (SVar "x") (SVar "x")]。すべてのコンポーネントは強く接続されており、保護されyていませんが、保護されていないループはありません。したがって、トップソートだけでは十分ではありません。裸の変数も削除する必要があります。幸いなことに、これはかなり簡単です (この場合、"x" をすべて "y" に置き換えます)。

では、これは元の問題について何を意味するのでしょうか? 私はそれが完全に解決されたとは思いません: ルート化されたパスは、ツリーの「トポロジー的にソートされた」バージョンがそもそも何であるべきかを言うのを難しくします!

于 2016-06-17T03:20:20.487 に答える