Skew Heaps 및 Leftist Heaps의 자동화된 분할 상환 분석 (확장 버전)

우리는 skew heaps와 같이 순수 함수형 데이터 구조(purely functional data structures)뿐만 아니라, 가중치 및 랭크 편향 leftist heaps에 대한 완전 자동화된 분할 상환 분석 (amortised analysis)을 연구합니다. 이를 위해 범용 타입 시스템 (generic type system)을 갖춘 타입 추론 (type inference) 기반 접근 방식을 개발함으로써, 자동화된 분할 상환 자원 분석에 관한 이전 연구들을 일반화합니다. 이를 통해 모듈식 추론 (modular reasoning)과 정밀하고 최적화된 비용 경계 (cost bounds)의 추론이 가능해집니다. 구체적으로, 우리는 splay trees 및 이와 밀접하게 관련된 일부 데이터 구조의 분석을 다루기 위해 개발된 Leutgeb 등의 ATLAS 시스템에 관한 연구를 확장합니다. 그러나 skew heaps의 분석과 더욱 도전적인 leftist heaps의 (분할 상환) 분석을 가능하게 하기 위해, 우리는 타입 기반 자동 분석을 위한 일련의 새로운 기술들을 개발했습니다. 범용 타입 시스템을 도입함으로써, ATLAS에서 사용되었던 하드코딩된 포텐셜 함수 (potential functions)의 사용과 비교하여 임의의 (클래스 형태의) 포텐셜 함수를 사용할 수 있도록 하였으며, 이를 Haskell로 완전히 모듈식인 방식으로 구현했습니다. 또한 우리는 경로 민감 추론 (path-sensitive reasoning), 데이터 구조 불변량 (data structure invariants), 그리고 구간별로 정의된 포텐셜 함수를 위한 템플릿 매개변수 (template parameters)를 포함하여 여러 방향으로 확장함으로써 기존의 타입 추론 알고리즘을 크게 개선했습니다. 우리는 새로 개발된 시스템이 skew heaps 및 leftist heaps 분석을 위해 알려진 모든 포텐셜 함수의 사용을 어떻게 지원하는지 보여주며, 기존에 알려진 경계값들을 확인합니다.