종료분석

공허하게 하다 f(인트로 n) {    하는 동안에 (n > 1)       만일 (n % 2 == 0)           n = n / 2;       다른           n = 3 * n + 1; } 

컴퓨터 과학에서 종료 분석은 주어진 프로그램의 평가가 각 입력에 대해 중단되는지 여부를 결정하는 프로그램 분석이다.이것은 입력 프로그램이 총 함수를 계산하는지 여부를 결정하는 것을 의미한다.

그것은 주어진 입력에 대해 주어진 프로그램이 중지되는지, 그리고 어떤 프로그램이 해석할 수 없는지를 결정하는 Halting 문제와 밀접한 관련이 있다.종료 분석은 Halting 문제보다 훨씬 더 어렵다: 계산 가능한 기능을 구현하는 프로그램 모델로서의 Turing 기계 모델에서의 종료 분석은 주어진 Turing 기계가 총 Turing 기계인지 여부를 결정하는 목표를 가질 것이다. 그리고 이 문제는 수준 $Ⅱ{\displaystyle {\mathrm{}}_{}^{}}$ ${\displaystyle {2\mathrm{}}_{}^{}}$ ${\displaystyle {\mathrm{}}_{}^{}}$ ${\$에 있다.$}}^{0}$ 산술적 계층 구조로$$ 해서 할팅 문제보다 엄밀히 말하면 더 어렵다.

이제 그 질문은 계산할 수 있는 기능은 총 있지 않semi-decidable,[1]각 사운드 종결 분석기(i.e.는 긍정적인 대답은non-terminating 프로그램에 대해서도 알려 주지 않다)은 완전하지 않i.e.야 한다 실패하게 결정할 종료에 대한 무한히 많은 종단 프로그램도에 재가동되 영원히 또는 중단을 가진 부정 answ.음.정말

해지 증명서

종료 증명서는 알고리즘의 전체 정확성이 종료에 따라 달라지기 때문에 형식 검증에서 중요한 역할을 하는 수학적 증명의 한 유형이다.

종료 증명을 구성하는 간단하고 일반적인 방법에는 알고리즘의 각 단계와 측정값을 연관시키는 것이 포함된다.이 측정은 서수적 숫자와 같이 근거가 있는 관계의 영역에서 취해진다.측정치가 알고리즘의 가능한 모든 단계를 따라 관계에 따라 "감소"되는 경우, 근거가 충분한 관계에 대한 무한 내림차인이 없기 때문에 종료해야 한다.

일부 유형의 종료 분석은 종료 증명서의 존재를 자동으로 생성하거나 암시할 수 있다.

예

종료될 수도 있고 종료되지 않을 수도 있는 프로그래밍 언어 구성의 예는 반복적으로 실행될 수 있기 때문에 루프다.일반적으로 데이터 처리 알고리즘에서 발견되는 카운터 변수를 사용하여 구현되는 루프는 일반적으로 종료되며, 아래의 유사 코드 예에 의해 입증된다.

i := 0 루프 ~ i = SIZE_OF_DATA process_data(data[i]) // 위치 i := i + 1 // 처리할 다음 데이터 청크로 이동

SIZE_OF_DATA의 값이 음이 아닌, 고정된, 유한한 경우, 프로세스_데이터도 종료된다고 가정하여 루프가 결국 종료된다.

일부 루프는 인간 검사를 통해 항상 종료되거나 결코 종료되지 않는 것으로 보일 수 있다.예를 들어 다음과 같은 루프는 이론적으로 결코 멈추지 않을 것이다.그러나 산술 오버플로로 인해 물리적 기계에서 실행될 때 중단될 수 있다. 예외로 유도하거나 카운터가 음의 값으로 감겨 루프 조건을 충족할 수 있게 한다.

i :=1 루프 ~ i = 0 i := i + 1

종료 분석에서 일부 알 수 없는 입력에 따라 일부 프로그램의 종료 동작을 결정하려고 할 수도 있다.다음 예는 이 문제를 예시한다.

i :=1 루프 ~ i = 알 수 없음 i := i + 1

여기서 루프 조건은 알 수 없는 값을 사용하여 정의된다(예: 프로그램이 실행될 때 사용자의 입력에 의해 정의됨).여기서 종료 분석은 Unknown의 가능한 모든 값을 고려해야 하며, 가능한 UNUNNMING = 0(원래 예시처럼)의 경우 종료를 표시할 수 없음을 알아내야 한다.

그러나 인간에게 검사를 위임할 때 조차도 루핑 명령을 포함하는 표현이 중단될 것인지를 결정하는 일반적인 절차는 없다.그 이론적 이유는 Halting 문제의 불분명함 때문이다: 주어진 프로그램이 정확히 많은 계산 단계를 거쳐 중단되는지 여부를 결정하는 알고리즘은 존재할 수 없다.

모든 알고리즘은 주어진 프로그램에서 관련 정보를 추출할 수 있는 유한한 방법 집합으로 작동하기 때문에 실제로 종료(또는 종료되지 않음)를 보여주지 못한다.어떤 방법은 어떤 루프 조건(아마도 그 루프의 종료를 보여주는 것)과 관련하여 변수가 어떻게 변화하는지 볼 수 있으며, 다른 방법들은 프로그램의 계산을 어떤 수학 구조로 변환하여 그것에 대해 작용하려고 할 수 있으며, 아마도 이 수학 모델의 일부 특성에서 종단 동작에 대한 정보를 얻을 수 있다.그러나 각 방법은 (비)종료에 대한 일부 구체적인 이유만을 "알 수 있기 때문에, 그러한 방법의 조합을 통해서도 (비)종료에 대한 가능한 모든 이유를 다룰 수는 없다.^{[citation needed]}

반복함수와 루프는 표현에 있어서 동등하다. 루프를 포함하는 모든 표현은 재귀로 쓸 수 있고, 그 반대의 경우도 마찬가지다.따라서 재귀적 표현의 종료 역시 일반적으로 해석할 수 없는 것이다.일반적인 사용법(즉 병리학적 표현이 아님)에서 발견되는 대부분의 재귀적 표현은 일반적으로 표현 자체의 정의에 따라 다양한 수단을 통해 종료되는 것으로 보일 수 있다.예를 들어, 아래의 요인 함수에 대한 재귀 식에 있는 함수 인수는 항상 1씩 감소한다. 자연수의 순서가 잘 되어 있는 속성에 의해, 인수는 결국 1에 도달하고 재귀는 종료된다.

함수 요인(인수가 0이거나 인수가 1일 경우 자연수인 인수) * 요인(인수 - 1)

종속형

종료 점검은 Coq와 Agda와 같은 의존적으로 타이핑된 프로그래밍 언어와 정리 증명 시스템에서 매우 중요하다.이 시스템들은 프로그램과 증명 사이에 Curry-Howard 이형성을 사용한다.유도 원리를 사용하여 유도적으로 정의된 데이터 형식에 대한 증거를 전통적으로 설명하였다.그러나, 패턴 매칭으로 재귀적으로 정의된 기능을 통해 프로그램을 기술하는 것이 유도 원리를 직접 사용하는 것보다 더 자연스러운 증명 방법이라는 것이 나중에 밝혀졌다.불행히도 중단되지 않는 정의를 허용하면 형식 이론에^{[citation needed]} 논리적 불일치가 발생하는데, 이것이 아그다와 콕이 종료 체크인을 내장하고 있는 이유다.

크기 유형

의존적으로 입력된 프로그래밍 언어에서 종료 확인 접근방식 중 하나는 크기 유형이다.주요 아이디어는 크기 주석을 사용하여 반복할 수 있는 유형에 주석을 달 수 있고 더 작은 인수에서만 재귀적 호출을 허용하는 것이다.크기 유형은 구문 확장으로 아그다에서 구현된다.

현재 연구

종료를 보여줄 수 있는 새로운 방법을 연구하고 있는 여러 연구팀이 있다.많은 연구자들은 이러한 방법들을 자동적으로 (그러므로 인간의 상호작용 없이) 종료 행동을 분석하려는 프로그램에^[2] 포함시킨다.현재 진행 중인 연구 측면은 "실제" 프로그래밍 언어로 작성된 프로그램의 종료 동작을 분석하는 데 기존의 방법을 사용할 수 있도록 하는 것이다.하스켈, 수성, 프롤로그와 같은 선언적 언어의 경우 많은 결과가 존재한다^[3][4][5](주로 이러한 언어의 강한 수학적 배경 때문이다).연구계는 또한 C, 자바와 같은 필수 언어로 작성된 프로그램의 종료 행동을 분석하기 위한 새로운 방법을 연구하고 있다.

이 분야의 '해결 문제' 연구가 불분명하기 때문에 완전성에 도달할 수 없다.종료의 새로운 (불만) 이유를 찾아내는 새로운 방법을 항상 생각할 수 있다.

참고 항목

• 복잡성 분석 - 종료에 필요한 시간 추정 문제
• 루프 변형
• 총 기능 프로그래밍 - 프로그램 범위를 종료될 가능성이 있는 프로그램으로 제한하는 프로그래밍 패러다임
• 발터 재귀

참조

자동화된 프로그램 종료 분석에 대한 연구 논문은 다음과 같다.

• Christoph Walther (1988). "Argument-Bounded Algorithms as a Basis for Automated Termination Proofs". Proc. 9th Conference on Automated Deduction. LNAI. Vol. 310. Springer. pp. 602–621.
• Christoph Walther (1991). "On Proving the Termination of Algorithms by Machine" (PDF). Artificial Intelligence. 70 (1).
• Xi, Hongwei (1998). "Towards Automated Termination Proofs through Freezing" (PDF). In Tobias Nipkow (ed.). Rewriting Techniques and Applications, 9th Int. Conf., RTA-98. LNCS. Vol. 1379. Springer. pp. 271–285.
• Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Termination Analysis for Functional Programs". In W. Bibel; P. Schmitt (eds.). Automated Deduction - A Basis for Applications (postscript). Vol. 3. Dordrecht: Kluwer Academic Publishers. pp. 135–164.
• Christoph Walther (2000). "Criteria for Termination". In S. Hölldobler (ed.). Intellectics and Computational Logic (postscript). Dordrecht: Kluwer Academic Publishers. pp. 361–386.
• Christoph Walther; Stephan Schweitzer (2005). "Automated Termination Analysis for Incompletely Defined Programs" (PDF). In Franz Baader; Andrei Voronkov (eds.). Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). LNAI. Vol. 3452. Springer. pp. 332–346.
• Adam Koprowski; Johannes Waldmann (2008). "Arctic Termination ...Below Zero". In Andrei Voronkov (ed.). Rewriting Techniques and Applications, 19th Int. Conf., RTA-08 (PDF). Lecture Notes in Computer Science. Vol. 5117. Springer. pp. 202–216. ISBN 978-3-540-70588-8.

자동 종료 분석 도구의 시스템 설명에는 다음이 포함된다.

• Giesl, J. (1995). "Generating Polynomial Orderings for Termination Proofs (system description)". In Hsiang, Jieh (ed.). Rewriting Techniques and Applications, 6th Int. Conf., RTA-95 (postscript). LNCS. Vol. 914. Springer. pp. 426–431.
• Ohlebusch, E.; Claves, C.; Marché, C. (2000). "TALP: A Tool for the Termination Analysis of Logic Programs (system description)". In Bachmair, Leo (ed.). Rewriting Techniques and Applications, 11th Int. Conf., RTA-00 (compressed postscript). LNCS. Vol. 1833. Springer. pp. 270–273.
• Hirokawa, N.; Middeldorp, A. (2003). "Tsukuba Termination Tool (system description)". In Nieuwenhuis, R. (ed.). Rewriting Techniques and Applications, 14th Int. Conf., RTA-03 (PDF). LNCS. Vol. 2706. Springer. pp. 311–320.
• Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S. (2004). "Automated Termination Proofs with AProVE (system description)". In van Oostrom, V. (ed.). Rewriting Techniques and Applications, 15th Int. Conf., RTA-04 (PDF). LNCS. Vol. 3091. Springer. pp. 210–220. ISBN 3-540-22153-0.
• Hirokawa, N.; Middeldorp, A. (2005). "Tyrolean Termination Tool (system description)". In Giesl, J. (ed.). Term Rewriting and Applications, 16th Int. Conf., RTA-05. LNCS. Vol. 3467. Springer. pp. 175–184. ISBN 978-3-540-25596-3.
• Koprowski, A. (2006). "TPA: Termination Proved Automatically (system description)". In Pfenning, F. (ed.). Term Rewriting and Applications, 17th Int. Conf., RTA-06. LNCS. Vol. 4098. Springer. pp. 257–266.
• Marché, C.; Zantema, H. (2007). "The Termination Competition (system description)". In Baader, F. (ed.). Term Rewriting and Applications, 18th Int. Conf., RTA-07 (PDF). LNCS. Vol. 4533. Springer. pp. 303–313.

외부 링크

• 고차기능 프로그램의 종료해석
• 종료 도구 메일링 목록
• 종료 경기 — 설명은 Marché, Zantema(2007)를 참조하십시오.
• 종료 포털