루프 변형

컴퓨터 과학에서 루프 변형은 컴퓨터 프로그램의 상태 공간에 정의된 수학적 함수로서, 어떤 불변 조건 하에서 잠깐의 루프를 반복함으로써 (엄격한) 근거 있는 관계에 대해 단조롭게 가치가 감소하여 종료를 보장한다.음이 아닌 정수로 범위가 제한되는 루프 변형은 바운드 함수로도 알려져 있는데, 이 경우 그것은 종료되기 전에 루프의 반복 횟수에 대해 사소한 상한을 제공하기 때문이다.그러나 루프 변형은 트랜스핀라이트일 수 있으므로 반드시 정수 값으로 제한되는 것은 아니다.

근거가 충분한 관계는 그 도메인의 모든 비빈 부분집합에 최소 요소가 존재하는 것이 특징이다.변종의 존재는 근거 있는 하강에 의해 컴퓨터 프로그램에서 잠시의 루프가 종료되었음을 증명한다.^[1]근거가 있는 관계의 기본 속성은 무한히 내려가는 체인이 없다는 것이다.따라서 변형을 가진 루프는 매번 신체가 종료되는 한 한정된 횟수의 반복 후에 종료된다.

A while loop, 즉 보다 일반적으로는 루프 중 포함할 수 있는 컴퓨터 프로그램이 부분적으로 정확하고 종료되면 완전히 맞는다고 한다.

전체 정확성에 대한 추론 규칙

우리가 위에서 입증한 잠시 루프의 종료에 대한 추론 규칙을 공식적으로 언급하기 위해, 플로이드에서 그것을 상기하라.Hoare 논리, 약간의 루프의 부분적 정확성을 표현하는 규칙은 다음과 같다.

$♪ 디스플레이 스타일(displaystyle) ♪\frac(*) ♪I\land C\}\;S\;\{I\}{{\}}{\\}I\}\;{\mathet{while}\;;;C\;{\mathet{do}\;S\;\{I\land \lnot C\}}}$

여기서 나는 불변이고, C는 조건이고, S는 루프의 몸이다.완전한 정확성을 표현하기 위해 우리는 대신 다음과 같이 쓴다.

${\displaystyle {\frac {{\text{{\text}},\;[I\land C\land V=z]\;S\;[I\land V<z]}{[I]\;{\mathtt{while}}\;;;C\;{\mathet{do}\;S\;[I\land \lnot C]}},}$

또한 V는 변종이며 관례에 의해 결합되지 않은 기호 z는 보편적으로 정량화된다.

종단되는 모든 루프에는 변종이 있다.

변종이 존재한다는 것은 간극이 종단됨을 암시한다.놀랍게 보일지 모르지만, 우리가 선택의 공리를 가정하는 한, 그 반대도 진실이다: (그 불변성을 고려해 볼 때) 종결되는 모든 루프는 변형을 가지고 있다.이를 증명하기 위해 루프가

${\displaystyle {\matht {swhile}\;C\;{\mathet{do}\;S}$

완전한 정확성 주장이 있는 불변 I에 주어진 종료.

$(\displaystyle [\displaystyle [I\land C]\;S\;[I]}$

불변성 I과 조건 C를 모두 만족하는 상태에서 문 S의 실행에 의해 유도된 상태 공간 Ⅱ에 대한 "처리기" 관계를 고려한다.즉, 우리는 국가 σ′은 만약의 경우에 한해서만 σ의 "successor"라고 말한다.

• 나나 C는 주 state에서 모두 진실이고,
• σ′는 주 σ에서 성문 S의 실행에서 비롯되는 상태를 말한다.

$그렇지$ 않으면 루프가 $종료$되지 않을 것이라는 점에 주목한다$.$

다음으로 "처리기" 관계의 반사적이고 전이적인 폐쇄를 고려한다.Call this iteration: we say that a state σ′ is an iterate of σ if either ${\displaystyle \sigma '=\sigma ,}$ or there is a finite chain ${\displaystyle \sigma _{0},\sigma _{1},\,\dots \,,\sigma _{n}}$ such that ${\displaystyle \sigma _{0}=\sigma ,}$ ${\displaystyle {\sigma }_n={\sigma }^{\prime }}$${\displaystyle \sigma _{n}=\sigma '}$과(와$)$ ${\displaystyle {\mathrm{\sigma }}_{}}$ i${\displaystyle {}_{}}$+ 1 {\$displaystyle$ \$sigma _$${$i$+$$1$}은(는) ${\displaystyle {모든}_{}}$ I${\displaystyle {}_{}}$ $$ i< $.$ {\$displaystystyle$ $\$$leq<$n의 "sucer"이다$.$$}$

우리는 and과 σ′이 두 개의 구별되는 상태이고, σ′이 σ의 반복인 경우, σ은 σ의 반복이 될 수 없다는 점에 주목한다. 다시 한 번, 그렇지 않으면 loop은 루프가 종료되지 않을 경우, loop은 ′의 반복이 될 수 없다.즉, 반복은 대칭성이므로 부분순서가 된다.

이제, 루프는 불변성 I을 주어진 한정된 수의 단계를 거쳐 종료되고, 내가 그 상태에서 진실하지 않는 한 어떤 국가도 후계자를 가지고 있지 않기 때문에, 우리는 모든 주가 미세하게 많은 반복만을 가지고 있고, 반복에 관한 모든 하강 사슬은 미세하게 많은 구별되는 값만 가지고 있으며, 따라서 무한 하강 사슬은 존재하지 않는다고 결론짓는다.즉, 루프 반복은 내림차인 조건을 만족시킨다.

따라서—선택의 공리를 가정해 보자—우리가 원래 루프에 대해 정의한 "처리기" 관계는 엄격한 (불가변성)이고 "반복적" 관계에 포함되어 있기 때문에, Ⅱ에 기초가 잘 되어 있다.따라서 이 상태 공간의 정체성 기능은 우리가 "수축기"와 "반복"으로서, 불변성 I과 조건 C를 주어진 신체 S가 실행될 때마다 엄격하게 감소해야 한다는 것을 보여주었듯이, 그 동안 루프에 대한 변형이다.

게다가, 우리는 어떤 변종의 존재는, 최초의 헤아릴 수 없는 서수, 즉, 에 변종의 존재를 내포하고 있다는 것을 카운팅 논거로 보여줄 수 있다.

$\displaystyle V:\Sigma \righarrow \omega _{1}.}$

유한한 입력으로부터 한정된 수의 스텝으로 유한한 컴퓨터 프로그램에 의해 도달할 수 있는 모든 상태의 수집은 카운트할 수 있을 정도로 무한하며, 카운트할 수 있는 집합의 모든 양호한 유형의 열거이기 때문이다.

현실적 고려

실제로 루프 변형은 음이 아닌 정수로 간주되거나 심지어 그렇게 되어야 하는 경우가 많지만,^[2] 모든 루프에는 정수 변형이 있다는 요건은 프로그래밍 언어에서 무한 반복의 표현력을 제거한다.그러한 (공식적으로 검증된) 언어가 재귀 함수 호출과 같은 다른 동등하게 강력한 구조에 대해 최종적인 종료 증명서를 허용하지 않는 한, 더 이상 완전한 μ-재귀는 할 수 없고 원시적인 재귀만 할 수 있다.Ackermann의 함수는 정수 변형이 있는 루프에서 계산할 수 없는 재귀함수의 표준적인 예다.

그러나 이들의 계산 복잡성 측면에서 원시적 재귀성이 아닌 기능은 보통 다루기 쉽다고 여겨지는 것의 영역을 훨씬 벗어나 있다.단순한 지수의 사례도 원시 재귀함수로, 원시 재귀함수의 구성이 원시 재귀함수라는 점을 고려하면 원시 재귀함수가 얼마나 빨리 성장할 수 있는지 알 수 있다.그리고 원시적 재귀 함수에 의해 경계가 되는 가동 시간에 튜링 기계에 의해 계산될 수 있는 기능은 그 자체로 원시적 재귀성이다.따라서 원초적 재귀가 하지 않는 완전한 μ-재귀에 대한 실용적 사용은 특히 후자에 의해 극히 긴 러닝타임까지 시뮬레이션될 수 있기 때문에 상상하기 어렵다.

그리고 어떤 경우든, 커트 괴델의 첫 번째 불완전성 정리와 중단 문제는 항상 종료되지만 증명될 수 없는 루프가 있다는 것을 암시한다. 따라서 종료의 공식적인 증명에 대한 어떤 요구사항도 프로그래밍 언어의 표현력을 줄여야 한다는 것은 피할 수 없다.우리가 종단하는 모든 루프는 변형을 가지고 있다는 것을 보여주었지만, 이것은 루프 반복의 충분한 근거가 증명될 수 있다는 것을 의미하지는 않는다.

예

여기 C형 유사 변종에서, 잠시 루프에 남아 있는 반복 횟수의 상한으로부터 계산된 정수 변종의 예가 있다.그러나 C는 표현의 평가에서 부작용을 허용하는데, 이는 컴퓨터 프로그램을 정식으로 검증한다는 관점에서는 받아들일 수 없다.

/*** 조건 변수, 절차 S() **/에서 변경됨 바가지 긁다 C; /** 함수로, 부작용 없이 루프 반복 바인딩을 계산한다 **/ 횡대로 서명이 없는 인트로 getBound();  /*** 루프 본체는 V **/를 변경해서는 안 된다.  횡대로 공허하게 하다 S();   인트로 본래의() {     서명이 없는 인트로 V = getBound(); /* 변종을 바운드 */로 설정     주장하다(I); /* 루프 불변성 */     하는 동안에 (C) {         주장하다(V > 0); /* 이 주장은 변종의 존재론(존재론) */         S(); /* 신체를 */라고 부른다.         V = 분(getBound(), V - 1); /* 변종은 */ 하나 이상 감소해야 함     };     주장하다(I && !C); /* 불변성은 여전히 참이고 조건은 거짓이다 */      돌아오다 0; }; 

왜 비정수 변종까지 고려했을까?

왜 정수가 아닌 변종이나 트랜스피니트 변종까지 고려했을까?이 문제는 프로그램이 종료된다는 것을 증명하고 싶은 모든 실제 사례에서, 우리는 또한 프로그램이 합리적인 시간 내에 종료된다는 것을 증명하고 싶기 때문이다.최소한 두 가지 가능성이 있다.

• 루프의 반복 횟수에 대한 상한은 애초에 종료를 증명하는 조건부일 수 있다.의 세 가지 속성을 별도로(또는 점진적으로) 증명하는 것이 바람직할 수 있다.
  • 부분적 정확성,
  • 종료, 그리고
  • 러닝 타임
• 일반성: 트랜스피니트 변형을 고려하는 것은 변종의 존재 측면에서 당분간 모든 가능한 종단 증거를 볼 수 있게 한다.

참고 항목

• while 루프
• 루프 불변성
• 트랜스핀라이트 유도
• 내림차인조건
• 큰 카운트 가능 서수
• 정확성(컴퓨터 과학)
• With 루프 중 가장 약한 조건

참조