지연 모달을 사용하여 루트 경로에서 무한 트리를 계산하십시오.

Question

이것은 "Compute an (infinite) tree from fixpoint operator using delay modality"의 변형입니다.

설정입니다.

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

경로가 어떤 루트의 맥락에서 정의되며,이 식별 : 우리는 루트에서 경로 트리의 임의의 다른 노드를 참조 할 수있는 능력 증강 이진 트리의 언어를 공부 경로에서 거짓/참을 볼 때 왼쪽/오른쪽 자식을 따라 연속적으로 발견 된 하위 트리. 예를 들어 경로 [False, True]은 SNode (SNode (SLeaf 1) (SLeaf 2)) (SLeaf 3) 트리의 SLeaf 2을 식별합니다.

이러한 나무는 임의의 흐름 그래프를 식별하는데 이용 될 수있다 (돌이킬 수없는 그래프, fixpoint 연산자를 사용 할 수 없습니다 것을 포함합니다.)

우리는이 설명에 의해 유도 된 무한 트리를 고려할 수 있습니다. 여기

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 [])에 있습니다.

문제가 있습니다. 이제 우리는 지연 모달리티 ("Compute an (infinite) tree from fixpoint operator using delay modality"에서 설명 됨)와 함께 Loop 생성자를 사용하여 자체 참조 루프를 나타 내기 위해이 구조의 변형을 고려합니다.

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

비 구조적으로 재귀 함수 호출을 사용하지 않고 (그래서, 당신은 구조적으로 같이 Recurse STree 및 Path에 수), 무한 트리를 전개하는 기능 STree -> Tree (또는 유사)를 작성합니다.

추록. 많은 경우, 우리는 무한 전개를 계산하기를 원하지 않습니다. 존재하는 경우 유한 전개를 원하고, 그렇지 않으면 오류를 원합니다. 특히, 원래 데이터 형식 주어진 : 비 구조적으로 재귀 사용하지 않고

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

을, 우리는 그것이 존재하는 경우 유한 트리로 구문을 전개하고, 그렇지 않으면 실패하는 기능 STree -> Maybe Tree (또는 유사)을 작성 할 수 있습니다. 이 구조에서 지연 양식이 없기 때문에이 구조가 유한 함을 보증합니다.

이 구조에는 지연 양식이 없기 때문에 fixD을 사용하면 불가능합니다. 우리는 결코 사용할 수없는 지연된 결과를 얻게됩니다. 우리는 트리를 그래프로 변환하고 토폴로지별로 정렬 한 다음 fixD을 사용하지 않고 알고리즘을 직접 구현하는 것으로 보입니다.

언 폴딩을 원래의 (잘못된) 코드처럼 우아하게 구현할 수있는 다른 타이핑 규율이 있습니까? 그렇다면 그래프에서주기를 찾는 또 다른 알고리즘을 (재) 발견했을 수 있습니다.

Answer 1

글쎄, 여기에 문제에 대한 부분적인 관찰이 있습니다.

필자가 적어 놓은 문제의 구체적인 공식화는 아마도 약간 어려울 수 있습니다. 의도 한 것보다 어렵다. 여기에서 특히 성가신 예이다

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

이 잘 형성 그래프 아니지만 사이클 만 SVar [] 발생을 전개 한 후에 명백해진다. False을 True으로 바꾸면 제대로 형성됩니다.

의도는 기약 그래프를 표현할 수있는 것이고, 실제로는이 목표를 달성 할 수있는 letrec을 기반으로 한 더 간단한 구문이 있습니다.

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

SMu가 letrec 스타일 바인딩 작업입니다 : 우리는 직접 (일관성을 위해 이름을 바꾼 PHOAS없이, 그리고 생성자) 무한 이진 트리 (https://www.cs.utexas.edu/~wcook/Drafts/2012/graphs.pdf) 종이 올리베이라 - 쿡의 "구조적 그래프와 기능 프로그래밍"에서 표현을 채택 : SMu ["x", "y"] [t1, t2]은 본질적으로 letrec x = t1; y = t2 in x입니다. 원하는 노드의 경로를 적는 대신 이름을 지정하기 만하면됩니다. 또한이 문제는 이전 StackOverflow 질문과 훨씬 더 비슷합니다. (Compute an (infinite) tree from fixpoint operator using delay modality) 그래서 우리는 같은 방식으로 해결할 수 있습니까?

대답은 "예,하지만 ..."입니다.주의 사항은 SMu ["x", "y"] [SVar "y", SLeaf 0]입니다. 이 "재귀 적"바인딩은 재귀 적이 아니지만 지연된 컨텍스트 스타일 알고리즘에 의해 거부 될 것입니다. 왜냐하면 변수 y을 사용할 때 사용할 수 없기 때문입니다 (실제로는 보호되지 않습니다). 사실이 "빈 싸이클 금지"에서 제안 된 제한 사항과 정확히 일치합니다. 삽입 된 어커런스 f은주기가 발생할 수 없도록 보장하기위한 보호 기능 검사의 역할을합니다.

분명히, SMu에있는 모든 바인딩이 강하게 연결된다는 것을 의미합니다. 따라서 우리의 알고리즘은 바인딩의 강력한 연결 요소를 먼저 계산하여 진정한 재귀 바인딩으로 전처리하는 경우에만 적합합니다. 따라서 비 재귀 바인딩을 fixD없이 순서대로 처리 할 수 ​​있습니다. 사실 이것은 Haskell과 같은 바인딩이 실제로 어떻게 처리되는지를 일치시킵니다. 먼저 바인딩을 강하게 연결된 구성 요소로 분리 한 다음 SCC를 한 번에 하나씩 처리하고 이러한 경우 매듭을 묶습니다 (비어있는 것을 감지하면 오류가 발생합니다 SCC의 사이클).

하지만 그게 전부는 아닙니다. SMu ["x" "y"] [SVar "y", SNode (SVar "x") (SVar "x")]을 고려하십시오. 모든 구성 요소가 강하게 연결되어 있으며, y은 보호받지 못했지만 무방비 루프가 없습니다. 따라서 topsort만으로는 충분하지 않습니다. 베어 변수도 삭제해야합니다. 다행히도이 작업은 매우 간단합니다 (이 경우 모든 "x"를 "y"로 바꿉니다).

원래 문제는 무엇을 의미합니까? 나는 그것이 완전히 해결되었다고 생각지 않는다 : 뿌리를 내린 경로는 나무의 "토폴로지 적으로 분류 된"버전이 처음에 있어야한다고 말하는 것을 어렵게 만든다!