계산 가능한 함수의 논리
Logic for Computable FunctionsLCF(Logic for Computable Functions)는 Dana Scott가 이전에 제안한 계산 가능 함수의 로직의 이론적 토대를 기반으로 1970년대 초 Robin Milner와 협력자들에 의해 스탠포드와 에든버러에서 개발된 인터랙티브 자동 정리 프로세서입니다.LCF 시스템에 대한 작업은 사용자가 정리 증명 전술, 대수 데이터 유형, 파라메트릭 다형성, 추상 데이터 유형 및 예외를 작성할 수 있도록 하기 위해 범용 프로그래밍 언어 ML을 도입했습니다.
기본 아이디어
시스템의 정리는 특별한 "테임" 추상 데이터 유형의 용어입니다.ML의 추상 데이터 유형의 일반적인 메커니즘은 정리 추상형의 연산에 의해 주어진 추론 규칙만을 사용하여 정리가 도출되도록 한다.사용자는 임의로 복잡한 ML 프로그램을 작성하여 정리할 수 있습니다.정리의 유효성은 이러한 프로그램의 복잡성에 좌우되지 않고 추상적인 데이터 타입의 구현의 건전성과 ML 컴파일러의 정확성에 따라 결정됩니다.
이점
LCF 접근법은 명시적 증명서를 생성하는 시스템과 유사한 신뢰성을 제공하지만 증명 객체를 메모리에 저장할 필요는 없습니다.시스템의 런타임 구성에 따라 증명 객체를 선택적으로 저장하도록 쉽게 구현할 수 있으므로 기본적인 증명 생성 접근 방식을 일반화할 수 있습니다.정리 개발을 위해 범용 프로그래밍 언어를 사용하는 설계 결정은 작성된 프로그램의 복잡성에 따라 동일한 언어를 사용하여 단계별 증명, 결정 절차 또는 정리 프로버를 작성할 수 있음을 의미합니다.
단점들
신뢰할 수 있는 컴퓨팅 기반
기반이 되는 ML 컴파일러의 실장은 신뢰할 수 있는 컴퓨팅 베이스에 추가됩니다.CakeML에서[1] 작업한 결과 공식적으로 검증된 ML 컴파일러가 생성되어 이러한 우려를 완화했습니다.
입증 절차의 효율성 및 복잡성
정리 증명은 종종 결정 절차와 그 정확성이 광범위하게 분석된 정리 증명 알고리즘으로부터 이익을 얻는다.LCF 접근방식에서 이러한 절차를 구현하는 간단한 방법은 결과를 직접 계산하는 것이 아니라 항상 시스템의 공리, 레마스 및 추론 규칙에서 결과를 도출하는 절차를 필요로 한다.잠재적으로 더 효율적인 접근법은 반사를 사용하여 공식에서 연산하는 함수가 항상 정확한 결과를 [2]제공함을 증명하는 것이다.
영향
그 후의 실장에는, Cambridge LCF가 있습니다.이후 시스템에서는 부분 함수 대신 토탈 함수를 사용하도록 로직을 단순화하여 HOL, HOL Light 및 다양한 로직을 지원하는 Isabelle 프루프 어시스턴트로 이어졌습니다.2019년 현재 이사벨 프루프 어시스턴트는 여전히 LCF 로직인 이사벨/LCF의 구현을 포함하고 있다.
메모들
- ^ "CakeML". Retrieved 2 November 2019.
- ^ Boyer, Robert S; Moore, J Strother. Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures (PDF) (Report). Technical Report CSL-108, SRI Projects 8527/4079. pp. 1–111. Archived (PDF) from the original on November 2, 2019. Retrieved 2 November 2019.
레퍼런스
- Gordon, Michael J.; Milner, Arthur J.; Wadsworth, Christopher P. (1979). Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science. Vol. 78. Berlin Heidelberg: Springer. doi:10.1007/3-540-09724-4. ISBN 978-3-540-09724-2.
- Gordon, Michael J. C. (2000). "From LCF to HOL: a short history". Proof, language, and interaction. Cambridge, MA: MIT Press. pp. 169–185. ISBN 0-262-16188-5. Retrieved 2007-10-11.
- Loeckx, Jacques; Sieber, Kurt (1987). The Foundations of Program Verification (2nd ed.). Vieweg+Teubner Verlag. doi:10.1007/978-3-322-96753-4. ISBN 978-3-322-96754-1.
- Milner, Robin (May 1972). Logic for Computable Functions: description of a machine implementation (PDF). Stanford University.
- Milner, Robin (1979). "Lcf: A way of doing proofs with a machine". In Bečvář, Jiří (ed.). Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science. Vol. 74. Berlin Heidelberg: Springer. pp. 146–159. doi:10.1007/3-540-09526-8_11. ISBN 978-3-540-09526-2.
