LFPL: 재검토 및 기계화

Hofmann (1999)은 아핀 타입 시스템 (affine type system)을 사용하여 다항 시간 (polynomial time) 내에 계산 가능한 함수들을 특징짓기 위해 함수형 프로그래밍 언어인 LFPL을 도입했습니다. LFPL은 중첩 재귀 (nested recursion)를 포함한 자연스러운 프로그래밍 스타일을 가능하게 하며, 자동 비용 분석 (automatic cost analysis), 선형 의존 타입 이론 (linear dependent type theories), 그리고 함수형 프로그래밍 언어에서의 효율적인 메모리 관리 (memory management)를 위한 타입 시스템 개발에 영감을 주었습니다. 이러한 중요성에도 불구하고, LFPL과 그 핵심 메타 이론 (metatheory)에 대한 완전한 기계화 (mechanization)는커녕, 그 자체로 완결된 설명조차 존재하지 않습니다. 본 논문은 가장 강력하다고 알려진 건전성 (soundness) 및 완전성 (completeness) 결과를 간소화하는 동시에, 완결성을 갖추고 접근 가능하도록 하는 것을 목표로 LFPL과 그 메타 이론에 대한 현대적인 설명과 기계화를 제시합니다. 건전성 증명은 LFPL에 추가적인 언어 기능을 확장한 언어인 LFPL+를 대상으로 합니다. 이 증명은 Aehlig와 Schwichtenberg (2002)의 기법을 응용하여, 빅스텝 비용 의미론 (big-step cost semantics)에 대해 LFPL+ 표현식의 비용을 제한하는 명시적 다항식 (explicit polynomials)을 구축하는 새로운 방식입니다. 완전성 증명은 LFPL 프로그램이 제한된 형태의 선형 함수 (linear functions)와 리스트 (lists)에만 의존하면서도 다항 시간 튜링 머신 (polynomial-time Turing machines)을 시뮬레이션할 수 있음을 보여줍니다. 이는 Hofmann (2002)의 원본 증명과 동일한 구조를 가지지만, 퍼스트 클래스 함수 (first-class functions)와 리스트로 구현된 새로운 스택 형태의 데이터 구조를 사용하여 핵심 논증을 크게 단순화했습니다. 기계화에는 완전한 건전성 및 완전성 증명이 포함되며, 이는 최근 개발된 증명 보조기 (proof assistant)인 Istari에서 기계화된 메타 이론의 첫 번째 사례 연구 중 하나로 기능합니다.