viewimage.php?id=2ab4c42ef0d0&no=24b0d769e1d32ca73cec81fa11d02831ce3cef1b9542c00ceb084720f8a2823a6294fa557084db136a0caea1e15a88881303c80c952f6eb9a90f29d72472fdfc3b


코드는 여기서 볼 수 있음.

https://github.com/damhiya/AgdaHeap/blob/master/WBLT.agda


일단 weight biased leftist tree는 뭐냐면

https://en.wikipedia.org/wiki/Leftist_tree
걍 priority queue로 쓸 수 있는 heap임.
내가 알기로는 성능이 별로 훌륭한 편은 아닌데 구현이 진짜 간단해서 이걸로 함. 증명도 어려운데 자료구조 구현까지 힘들면 못해먹으니까.
왜 구현이 간단하냐면 leftist tree는 merge만 구현하면 나머지 연산들은 전부 merge로 구현함.


그래서 이걸 예전에 깃갤 문제 열릴때 만들어볼라고 했던건데 그때는 멍청해서 못맨듬

https://gall.dcinside.com/mgallery/board/view/?id=github&no=4911&search_pos=-9111&s_type=search_subject_memo&s_keyword=idris&page=1


뭐 결과적으로 말하자면 저때 하던 접근법이 별로 좋지 않았음.

tree의 성질에 대한 증명을 tree자체에 저장하는건 멍청한 짓임. 타입을 별도로 정의하는게 훨씬 좋음.


위에 올린 구현을 좀 해설하자면

먼저 merge를 구현함. merge는 힙 두개를 병합하는 연산임.

근데 이게 그냥 하면 termination checking이 잘 안되서 accessibility를 사용해서 종료 검사를 도와줌.

(accessibility는 걍 재귀가 유한한 횟수 안에 끝나는걸 알려주는거임)

문제는 accessibility 때문에 불필요한 연산이 좀 생기는데, 이건 erasure (run-time irrelevance) 를 사용하면 문제가 안됨.

erasure는 간단히 말해서 컴파일 타임에 타입 검사에만 활용되고 런타임에 지워지는 정보임.

https://agda.readthedocs.io/en/v2.6.1.3/language/runtime-irrelevance.html

그리고 Leftist랑 Heap이라는 데이터 타입을 정의하는데, 이건 각각 어떤 트리가 Leftist property하고 Heap property를 만족함을 표현하는 타입임.

merge가 Leftist property하고 Heap property를 보존함을 증명할 수 있음.


마지막으로 WBLT (Weight Biased Leftist Tree)를 정의하는데, 이건 그냥 위에서 정의한 Tree, Leftist, Heap 타입의 래퍼임.

WBLT 로 래핑된 트리는 항상 Leftist와 Heap property를 만족함.

마찬가지로 Leftist, Heap도 erasure로 지정해서 런타임 코스트를 안들게 할 수 있음.


erasure가 제대로 되면 증명 때문에 생기는 런타임 오버헤드는 이론상 사라짐.